awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Finite (goal)
Goal:
R S : Type u_5
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Finset R
hs : Eq (α := Ideal R) (Ideal.span (↑s : Set R)) ⊤
this_1 : Algebra R S := f.toAlgebra
this_2 : (r : ↥s) →
  Algebra (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)) :=
  fun (r : ↥s) ↦ toAlgebra (Localization.awayMap f (↑r : R))
this_3 :
  ∀ (r : ↥s),
    IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) (Submonoid.powers (↑r : R)))
      (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
this :
  ∀ (r : ↥s), IsScalarTower R (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
H :
  ∀ (r : ↥s),
    Submodule.FG.{u_5, u_5} (R := Localization.Away (↑r : R)) (M :=
      Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)) ⊤
⊢ Submodule.FG.{u_5, u_5} (R := R) (M := S) ⊤
have fg_top : ∀ (s₁ : (r : ↥s) → Finset (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
  (s₂ :
    ∀ (r : ↥s),
      Eq (α := Submodule (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
        (Submodule.span (Localization.Away (↑r : R)) (↑(s₁ r) : Set (Localization.Away ((f : (a : R) → S) (↑r : R)))))
        ⊤),
  Submodule.FG.{u_5, u_5} (R := R) (M := S) ⊤
Tactic: choose s₁ s₂ using H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Finite (goal)
Goal:
R S : Type u_5
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Finset R
hs : Eq (α := Ideal R) (Ideal.span (↑s : Set R)) ⊤
this_1 : Algebra R S := f.toAlgebra
this_2 : (r : ↥s) →
  Algebra (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)) :=
  fun (r : ↥s) ↦ toAlgebra (Localization.awayMap f (↑r : R))
this_3 :
  ∀ (r : ↥s),
    IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) (Submonoid.powers (↑r : R)))
      (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
this :
  ∀ (r : ↥s), IsScalarTower R (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
s₁ : (r : ↥s) → Finset (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
s₂ :
  ∀ (r : ↥s),
    Eq (α := Submodule (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
      (Submodule.span (Localization.Away (↑r : R)) (↑(s₁ r) : Set (Localization.Away ((f : (a : R) → S) (↑r : R))))) ⊤
sf : (x : ↥s) → Finset S :=
  fun (x : ↥s) ↦ IsLocalization.finsetIntegerMultiple (Submonoid.powers ((f : (a : R) → S) (↑x : R))) (s₁ x)
⊢ Submodule.FG.{u_5, u_5} (R := R) (M := S) ⊤
have h : Eq (α := Submodule R S) (Submodule.span R (↑(s.attach.biUnion sf) : Set S)) ⊤
Tactic: use s.attach.biUnion sf
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Finite (goal)
Goal:
R S : Type u_5
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Finset R
hs : Eq (α := Ideal R) (Ideal.span (↑s : Set R)) ⊤
this_1 : Algebra R S := f.toAlgebra
this_2 : (r : ↥s) →
  Algebra (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)) :=
  fun (r : ↥s) ↦ toAlgebra (Localization.awayMap f (↑r : R))
this_3 :
  ∀ (r : ↥s),
    IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) (Submonoid.powers (↑r : R)))
      (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
this :
  ∀ (r : ↥s), IsScalarTower R (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
s₁ : (r : ↥s) → Finset (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
s₂ :
  ∀ (r : ↥s),
    Eq (α := Submodule (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
      (Submodule.span (Localization.Away (↑r : R)) (↑(s₁ r) : Set (Localization.Away ((f : (a : R) → S) (↑r : R))))) ⊤
sf : (x : ↥s) → Finset S :=
  fun (x : ↥s) ↦ IsLocalization.finsetIntegerMultiple (Submonoid.powers ((f : (a : R) → S) (↑x : R))) (s₁ x)
⊢ Eq (α := Submodule R S) (Submodule.span R (↑(s.attach.biUnion sf) : Set S)) ⊤
have h : LE.le.{u_5} (α := Submodule R S) ⊤ (⨆ (x : ↥s), Submodule.span R (↑(sf x) : Set S))
Tactic: rw [Submodule.span_attach_biUnion, eq_top_iff]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Finite (goal)
Goal:
R S : Type u_5
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Finset R
hs : Eq (α := Ideal R) (Ideal.span (↑s : Set R)) ⊤
this_1 : Algebra R S := f.toAlgebra
this_2 : (r : ↥s) →
  Algebra (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)) :=
  fun (r : ↥s) ↦ toAlgebra (Localization.awayMap f (↑r : R))
this_3 :
  ∀ (r : ↥s),
    IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) (Submonoid.powers (↑r : R)))
      (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
this :
  ∀ (r : ↥s), IsScalarTower R (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
s₁ : (r : ↥s) → Finset (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
s₂ :
  ∀ (r : ↥s),
    Eq (α := Submodule (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
      (Submodule.span (Localization.Away (↑r : R)) (↑(s₁ r) : Set (Localization.Away ((f : (a : R) → S) (↑r : R))))) ⊤
sf : (x : ↥s) → Finset S :=
  fun (x : ↥s) ↦ IsLocalization.finsetIntegerMultiple (Submonoid.powers ((f : (a : R) → S) (↑x : R))) (s₁ x)
x : S
⊢ Membership.mem (γ := Submodule R S) (⨆ (x : ↥s), Submodule.span R (↑(sf x) : Set S)) x
have apply : ∀ (r : (↑(↑s : Set R) : Type u_5)),
  ∃ (n : ℕ), Membership.mem (γ := Submodule R S) (⨆ (x : ↥s), Submodule.span R (↑(sf x) : Set S)) ((↑r : R) ^ n • x)
Tactic: apply Submodule.mem_of_span_eq_top_of_smul_pow_mem _ (s : Set R) hs _ _
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Finite (goal)
Goal:
R S : Type u_5
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Finset R
hs : Eq (α := Ideal R) (Ideal.span (↑s : Set R)) ⊤
this_1 : Algebra R S := f.toAlgebra
this_2 : (r : ↥s) →
  Algebra (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)) :=
  fun (r : ↥s) ↦ toAlgebra (Localization.awayMap f (↑r : R))
this_3 :
  ∀ (r : ↥s),
    IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) (Submonoid.powers (↑r : R)))
      (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
this :
  ∀ (r : ↥s), IsScalarTower R (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
s₁ : (r : ↥s) → Finset (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
s₂ :
  ∀ (r : ↥s),
    Eq (α := Submodule (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
      (Submodule.span (Localization.Away (↑r : R)) (↑(s₁ r) : Set (Localization.Away ((f : (a : R) → S) (↑r : R))))) ⊤
sf : (x : ↥s) → Finset S :=
  fun (x : ↥s) ↦ IsLocalization.finsetIntegerMultiple (Submonoid.powers ((f : (a : R) → S) (↑x : R))) (s₁ x)
x : S
r : (↑(↑s : Set R) : Type u_5)
⊢ Membership.mem (α := Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)) (γ :=
    Submodule (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
    (Submodule.span (Localization.Away (↑r : R)) (↑(s₁ r) : Set (Localization.Away ((f : (a : R) → S) (↑r : R)))))
    ((algebraMap S (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)) :
          (a : S) → Localization.Away ((f : (a : R) → S) (↑r : R)))
        x :
      Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
have rw : Membership.mem (α := Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)) (γ :=
  Submodule (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))) ⊤
  ((algebraMap S (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)) :
        (a : S) → Localization.Away ((f : (a : R) → S) (↑r : R)))
      x :
    Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
Tactic: rw [s₂ r]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Finite (goal)
Goal:
R S : Type u_5
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Finset R
hs : Eq (α := Ideal R) (Ideal.span (↑s : Set R)) ⊤
this_1 : Algebra R S := f.toAlgebra
this_2 : (r : ↥s) →
  Algebra (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)) :=
  fun (r : ↥s) ↦ toAlgebra (Localization.awayMap f (↑r : R))
this_3 :
  ∀ (r : ↥s),
    IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) (Submonoid.powers (↑r : R)))
      (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
this :
  ∀ (r : ↥s), IsScalarTower R (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
s₁ : (r : ↥s) → Finset (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
s₂ :
  ∀ (r : ↥s),
    Eq (α := Submodule (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
      (Submodule.span (Localization.Away (↑r : R)) (↑(s₁ r) : Set (Localization.Away ((f : (a : R) → S) (↑r : R))))) ⊤
sf : (x : ↥s) → Finset S :=
  fun (x : ↥s) ↦ IsLocalization.finsetIntegerMultiple (Submonoid.powers ((f : (a : R) → S) (↑x : R))) (s₁ x)
x : S
r : (↑(↑s : Set R) : Type u_5)
⊢ ∃ (n : ℕ), Membership.mem (γ := Submodule R S) (⨆ (x : ↥s), Submodule.span R (↑(sf x) : Set S)) ((↑r : R) ^ n • x)
have obtain : ∀ (n₁ : ℕ)
  (hn₁ :
    Membership.mem (γ := Submodule R (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
      (Submodule.span R (↑(s₁ r) : Set (Localization.Away ((f : (a : R) → S) (↑r : R)))))
      (HSMul.hSMul (β := Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
        (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers (↑r : R)) x)
          ((fun (x : ℕ) ↦ (↑r : R) ^ x) n₁) sorry)
        ((algebraMap S (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)) :
              (a : S) → Localization.Away ((f : (a : R) → S) (↑r : R)))
            x :
          Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))),
  ∃ (n : ℕ), Membership.mem (γ := Submodule R S) (⨆ (x : ↥s), Submodule.span R (↑(sf x) : Set S)) ((↑r : R) ^ n • x)
Tactic: obtain ⟨⟨_, n₁, rfl⟩, hn₁⟩ :=
    multiple_mem_span_of_mem_localization_span (Submonoid.powers (r : R))
      (Localization.Away (r : R)) (s₁ r : Set (Localization.Away (f r))) (algebraMap S _ x)
      (by rw [s₂ r]; trivial)
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Finite (hypothesis)
Goal:
R S : Type u_5
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Finset R
hs : Eq (α := Ideal R) (Ideal.span (↑s : Set R)) ⊤
this_1 : Algebra R S := f.toAlgebra
this_2 : (r : ↥s) →
  Algebra (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)) :=
  fun (r : ↥s) ↦ toAlgebra (Localization.awayMap f (↑r : R))
this_3 :
  ∀ (r : ↥s),
    IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) (Submonoid.powers (↑r : R)))
      (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
this :
  ∀ (r : ↥s), IsScalarTower R (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
s₁ : (r : ↥s) → Finset (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
s₂ :
  ∀ (r : ↥s),
    Eq (α := Submodule (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
      (Submodule.span (Localization.Away (↑r : R)) (↑(s₁ r) : Set (Localization.Away ((f : (a : R) → S) (↑r : R))))) ⊤
sf : (x : ↥s) → Finset S :=
  fun (x : ↥s) ↦ IsLocalization.finsetIntegerMultiple (Submonoid.powers ((f : (a : R) → S) (↑x : R))) (s₁ x)
x : S
r : (↑(↑s : Set R) : Type u_5)
n₁ : ℕ
hn₁ :
  Membership.mem (γ := Submodule R (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
    (Submodule.span R (↑(s₁ r) : Set (Localization.Away ((f : (a : R) → S) (↑r : R)))))
    (HSMul.hSMul (α := ↥(Submonoid.powers (↑r : R))) (β := Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
      (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers (↑r : R)) x) ((↑r : R) ^ n₁)
        ⋯)
      ((algebraMap S (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)) :
            (a : S) → Localization.Away ((f : (a : R) → S) (↑r : R)))
          x :
        Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
⊢ ∃ (n : ℕ), Membership.mem (γ := Submodule R S) (⨆ (x : ↥s), Submodule.span R (↑(sf x) : Set S)) ((↑r : R) ^ n • x)
have hn₂ : Membership.mem (α := Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)) (γ :=
  Submodule R (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
  (Submodule.span R (↑(s₁ r) : Set (Localization.Away ((f : (a : R) → S) (↑r : R)))))
  ((algebraMap S (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)) :
        (a : S) → Localization.Away ((f : (a : R) → S) (↑r : R)))
      (HMul.hMul (α := S)
        ((algebraMap R S : (a : R) → S)
            (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers (↑r : R)) x)
                  ((↑r : R) ^ n₁) sorry) :
              R) :
          S)
        x) :
    Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
Tactic: rw [Submonoid.smul_def, Algebra.smul_def, IsScalarTower.algebraMap_apply R S, ← map_mul] at hn₁
Cleared hypotheses: hn₁
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Finite (goal)
Goal:
R S : Type u_5
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Finset R
hs : Eq (α := Ideal R) (Ideal.span (↑s : Set R)) ⊤
this_1 : Algebra R S := f.toAlgebra
this_2 : (r : ↥s) →
  Algebra (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)) :=
  fun (r : ↥s) ↦ toAlgebra (Localization.awayMap f (↑r : R))
this_3 :
  ∀ (r : ↥s),
    IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) (Submonoid.powers (↑r : R)))
      (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
this :
  ∀ (r : ↥s), IsScalarTower R (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
s₁ : (r : ↥s) → Finset (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
s₂ :
  ∀ (r : ↥s),
    Eq (α := Submodule (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
      (Submodule.span (Localization.Away (↑r : R)) (↑(s₁ r) : Set (Localization.Away ((f : (a : R) → S) (↑r : R))))) ⊤
sf : (x : ↥s) → Finset S :=
  fun (x : ↥s) ↦ IsLocalization.finsetIntegerMultiple (Submonoid.powers ((f : (a : R) → S) (↑x : R))) (s₁ x)
x : S
r : (↑(↑s : Set R) : Type u_5)
n₁ : ℕ
hn₁ :
  Membership.mem (α := Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)) (γ :=
    Submodule R (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
    (Submodule.span R (↑(s₁ r) : Set (Localization.Away ((f : (a : R) → S) (↑r : R)))))
    ((algebraMap S (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)) :
          (a : S) → Localization.Away ((f : (a : R) → S) (↑r : R)))
        (HMul.hMul (α := S)
          ((algebraMap R S : (a : R) → S)
              (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers (↑r : R)) x)
                    ((↑r : R) ^ n₁) ⋯) :
                R) :
            S)
          x) :
      Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
⊢ ∃ (n : ℕ), Membership.mem (γ := Submodule R S) (⨆ (x : ↥s), Submodule.span R (↑(sf x) : Set S)) ((↑r : R) ^ n • x)
have obtain : ∀ (n₂ : ℕ)
  (hn₂ :
    Membership.mem (γ := Submodule R S)
      (Submodule.span R
        (↑(IsLocalization.finsetIntegerMultiple
              (Submonoid.map (F := R →+* S) (algebraMap R S) (Submonoid.powers (↑r : R))) (s₁ r)) :
          Set S))
      (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers (↑r : R)) x)
          ((fun (x : ℕ) ↦ (↑r : R) ^ x) n₂) sorry •
        HMul.hMul (α := S)
          ((algebraMap R S : (a : R) → S)
              (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers (↑r : R)) x)
                    ((↑r : R) ^ n₁) sorry) :
                R) :
            S)
          x)),
  ∃ (n : ℕ), Membership.mem (γ := Submodule R S) (⨆ (x : ↥s), Submodule.span R (↑(sf x) : Set S)) ((↑r : R) ^ n • x)
Tactic: obtain ⟨⟨_, n₂, rfl⟩, hn₂⟩ :=
    IsLocalization.smul_mem_finsetIntegerMultiple_span (Submonoid.powers (r : R))
      (Localization.Away (f r)) _ (s₁ r) hn₁
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Finite (hypothesis)
Goal:
R S : Type u_5
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Finset R
hs : Eq (α := Ideal R) (Ideal.span (↑s : Set R)) ⊤
this_1 : Algebra R S := f.toAlgebra
this_2 : (r : ↥s) →
  Algebra (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)) :=
  fun (r : ↥s) ↦ toAlgebra (Localization.awayMap f (↑r : R))
this_3 :
  ∀ (r : ↥s),
    IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) (Submonoid.powers (↑r : R)))
      (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
this :
  ∀ (r : ↥s), IsScalarTower R (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
s₁ : (r : ↥s) → Finset (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
s₂ :
  ∀ (r : ↥s),
    Eq (α := Submodule (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
      (Submodule.span (Localization.Away (↑r : R)) (↑(s₁ r) : Set (Localization.Away ((f : (a : R) → S) (↑r : R))))) ⊤
sf : (x : ↥s) → Finset S :=
  fun (x : ↥s) ↦ IsLocalization.finsetIntegerMultiple (Submonoid.powers ((f : (a : R) → S) (↑x : R))) (s₁ x)
x : S
r : (↑(↑s : Set R) : Type u_5)
n₁ : ℕ
hn₁ :
  Membership.mem (α := Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)) (γ :=
    Submodule R (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
    (Submodule.span R (↑(s₁ r) : Set (Localization.Away ((f : (a : R) → S) (↑r : R)))))
    ((algebraMap S (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)) :
          (a : S) → Localization.Away ((f : (a : R) → S) (↑r : R)))
        (HMul.hMul (α := S)
          ((algebraMap R S : (a : R) → S)
              (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers (↑r : R)) x)
                    ((↑r : R) ^ n₁) ⋯) :
                R) :
            S)
          x) :
      Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
n₂ : ℕ
hn₂ :
  Membership.mem (γ := Submodule R S)
    (Submodule.span R
      (↑(IsLocalization.finsetIntegerMultiple
            (Submonoid.map (F := R →+* S) (algebraMap R S) (Submonoid.powers (↑r : R))) (s₁ r)) :
        Set S))
    (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers (↑r : R)) x)
        ((fun (x : ℕ) ↦ (↑r : R) ^ x) n₂) ⋯ •
      HMul.hMul (α := S)
        ((algebraMap R S : (a : R) → S)
            (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers (↑r : R)) x)
                  ((↑r : R) ^ n₁) ⋯) :
              R) :
          S)
        x)
⊢ ∃ (n : ℕ), Membership.mem (γ := Submodule R S) (⨆ (x : ↥s), Submodule.span R (↑(sf x) : Set S)) ((↑r : R) ^ n • x)
have hn₃ : Membership.mem (γ := Submodule R S)
  (Submodule.span R
    (↑(IsLocalization.finsetIntegerMultiple (Submonoid.map (F := R →+* S) (algebraMap R S) (Submonoid.powers (↑r : R)))
          (s₁ r)) :
      Set S))
  ((↑r : R) ^ (n₂ + n₁) • x)
Tactic: rw [Submonoid.smul_def, ← Algebra.smul_def, smul_smul, ← pow_add] at hn₂
Cleared hypotheses: hn₂
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Finite (hypothesis)
Goal:
R S : Type u_5
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Finset R
hs : Eq (α := Ideal R) (Ideal.span (↑s : Set R)) ⊤
this_1 : Algebra R S := f.toAlgebra
this_2 : (r : ↥s) →
  Algebra (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)) :=
  fun (r : ↥s) ↦ toAlgebra (Localization.awayMap f (↑r : R))
this_3 :
  ∀ (r : ↥s),
    IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) (Submonoid.powers (↑r : R)))
      (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
this :
  ∀ (r : ↥s), IsScalarTower R (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
s₁ : (r : ↥s) → Finset (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
s₂ :
  ∀ (r : ↥s),
    Eq (α := Submodule (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
      (Submodule.span (Localization.Away (↑r : R)) (↑(s₁ r) : Set (Localization.Away ((f : (a : R) → S) (↑r : R))))) ⊤
sf : (x : ↥s) → Finset S :=
  fun (x : ↥s) ↦ IsLocalization.finsetIntegerMultiple (Submonoid.powers ((f : (a : R) → S) (↑x : R))) (s₁ x)
x : S
r : (↑(↑s : Set R) : Type u_5)
n₁ : ℕ
hn₁ :
  Membership.mem (α := Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)) (γ :=
    Submodule R (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
    (Submodule.span R (↑(s₁ r) : Set (Localization.Away ((f : (a : R) → S) (↑r : R)))))
    ((algebraMap S (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)) :
          (a : S) → Localization.Away ((f : (a : R) → S) (↑r : R)))
        (HMul.hMul (α := S)
          ((algebraMap R S : (a : R) → S)
              (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers (↑r : R)) x)
                    ((↑r : R) ^ n₁) ⋯) :
                R) :
            S)
          x) :
      Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
n₂ : ℕ
hn₂ :
  Membership.mem (γ := Submodule R S)
    (Submodule.span R
      (↑(IsLocalization.finsetIntegerMultiple
            (Submonoid.map (F := R →+* S) (algebraMap R S) (Submonoid.powers (↑r : R))) (s₁ r)) :
        Set S))
    ((↑r : R) ^ (n₂ + n₁) • x)
⊢ ∃ (n : ℕ), Membership.mem (γ := Submodule R S) (⨆ (x : ↥s), Submodule.span R (↑(sf x) : Set S)) ((↑r : R) ^ n • x)
have hn₃ : Membership.mem (γ := Submodule R S)
  (Submodule.span R
    (↑(IsLocalization.finsetIntegerMultiple (Submonoid.powers ((algebraMap R S : (a : R) → S) (↑r : R))) (s₁ r) :
          Finset S) :
      Set S))
  ((↑r : R) ^ (n₂ + n₁) • x)
Tactic: simp_rw [Submonoid.map_powers] at hn₂
Cleared hypotheses: hn₂