awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.RingHom.Finite
Goal:
R S : Type u_5
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
M : Submonoid R
R' S' : Type u_5
inst_2 : CommRing R'
inst_3 : CommRing S'
inst_4 : Algebra R R'
inst_5 : Algebra S S'
inst_6 : IsLocalization M R'
inst_7 : IsLocalization (Submonoid.map f M) S'
hf : f.Finite
this_1 : Algebra R S := f.toAlgebra
this_2 : Algebra R S' := toAlgebra (comp (algebraMap S S') f)
f' : R' →+* S' := IsLocalization.map S' f ⋯
this_3 : Algebra R' S' := f'.toAlgebra
this_4 : IsScalarTower R R' S'
this_5 : IsScalarTower R S S'
this_6 : IsLocalization (Algebra.algebraMapSubmonoid S M) S'
this : Module.Finite R S
⊢ Finite (A := R') (IsLocalization.map S' f ⋯)

Tactic:
.of_isLocalization R S M

Premises used: Module.Finite.of_isLocalization, RingHom.Finite
-- Module: Mathlib.RingTheory.RingHom.Finite
Goal:
R S : Type u_5
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
M : Submonoid R
R' S' : Type u_5
inst_2 : CommRing R'
inst_3 : CommRing S'
inst_4 : Algebra R R'
inst_5 : Algebra S S'
inst_6 : IsLocalization M R'
inst_7 : IsLocalization (Submonoid.map f M) S'
hf : f.Finite
this_1 : Algebra R S := f.toAlgebra
this_2 : Algebra R S' := toAlgebra (comp (algebraMap S S') f)
f' : R' →+* S' := IsLocalization.map S' f ⋯
this_3 : Algebra R' S' := f'.toAlgebra
this_4 : IsScalarTower R R' S'
this_5 : IsScalarTower R S S'
this_6 : IsLocalization (Algebra.algebraMapSubmonoid S M) S'
this : Module.Finite R S
⊢ Finite (A := R') (IsLocalization.map S' f ⋯)

Tactic:
exact .of_isLocalization R S M
-- Module: Mathlib.RingTheory.RingHom.Finite
Goal:
R S R' S' : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing R'
inst_3 : CommRing S'
inst_4 : Algebra R R'
f : R →+* S
inst_5 : Algebra S S'
r : R
inst_6 : IsLocalization.Away r R'
inst_7 : IsLocalization.Away (R := S) ((f : (a : R) → S) r : S) S'
hf : f.Finite
⊢ Finite (IsLocalization.Away.map R' S' f r)

Tactic:
finite_localizationPreserves.away f r _ _ hf

Premises used: RingHom.finite_localizationPreserves, RingHom.LocalizationPreserves.away
-- Module: Mathlib.RingTheory.RingHom.Finite
Goal:
rw : OfLocalizationFiniteSpan @Finite
⊢ OfLocalizationSpan @Finite

Tactic:
rw [RingHom.ofLocalizationSpan_iff_finite]

Premises used: RingHom.ofLocalizationSpan_iff_finite
-- Module: Mathlib.RingTheory.RingHom.Finite
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)) ⊤
H : ∀ (r : ↥s), Finite (A := Localization.Away (↑r : R)) (Localization.awayMap f (↑r : R))
this_1 : Algebra R S := f.toAlgebra
this : (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))
r : ↥s
rw :
  IsLocalization (R := S) (Submonoid.powers ((algebraMap R S : (a : R) → S) (↑r : R)) : Submonoid S)
    (Localization.Away (M := S) ((f : (a : R) → S) (↑r : 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))

Tactic:
rw [Submonoid.map_powers]

Premises used: Submonoid.map_powers
-- Module: Mathlib.RingTheory.RingHom.Finite
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)) ⊤
H : ∀ (r : ↥s), Finite (A := Localization.Away (↑r : R)) (Localization.awayMap f (↑r : R))
this_1 : Algebra R S := f.toAlgebra
this : (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))
r : ↥s
⊢ IsLocalization (R := S) (Submonoid.powers ((algebraMap R S : (a : R) → S) (↑r : R)) : Submonoid S)
    (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))

Tactic:
Localization.isLocalization

Premises used: Localization.isLocalization
-- Module: Mathlib.RingTheory.RingHom.Finite
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)) ⊤
H : ∀ (r : ↥s), Finite (A := Localization.Away (↑r : R)) (Localization.awayMap f (↑r : R))
this_1 : Algebra R S := f.toAlgebra
this : (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))
r : ↥s
⊢ IsLocalization (R := S) (Submonoid.powers ((algebraMap R S : (a : R) → S) (↑r : R)) : Submonoid S)
    (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))

Tactic:
exact Localization.isLocalization

Premises used: Localization.isLocalization
-- Module: Mathlib.RingTheory.RingHom.Finite
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)) ⊤
H : ∀ (r : ↥s), Finite (A := Localization.Away (↑r : R)) (Localization.awayMap f (↑r : R))
this_1 : Algebra R S := f.toAlgebra
this : (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))
⊢ ∀ (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))

Tactic:
have (r : s) : IsLocalization ((Submonoid.powers (r : R)).map (algebraMap R S))
      (Localization.Away (f r)) := by
    rw [Submonoid.map_powers]; exact Localization.isLocalization
-- Module: Mathlib.RingTheory.RingHom.Finite
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)) ⊤
H : ∀ (r : ↥s), Finite (A := Localization.Away (↑r : R)) (Localization.awayMap f (↑r : 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 :
  ∀ (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))
⊢ ∀ (r : ↥s), IsScalarTower R (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))

Tactic:
haveI : ∀ r : s, IsScalarTower R (Localization.Away (r : R)) (Localization.Away (f r)) :=
    fun r => IsScalarTower.of_algebraMap_eq'
      (IsLocalization.map_comp (Submonoid.powers (r : R)).le_comap_map).symm
-- Module: Mathlib.RingTheory.RingHom.Finite
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)) ⊤
H : ∀ (r : ↥s), Finite (A := Localization.Away (↑r : R)) (Localization.awayMap f (↑r : 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))
fg_top : Submodule.FG.{u_5, u_5} (R := R) (M := S) ⊤
⊢ f.Finite

Tactic:
constructor
-- Module: Mathlib.RingTheory.RingHom.Finite
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)) ⊤
H : ∀ (r : ↥s), Finite (A := Localization.Away (↑r : R)) (Localization.awayMap f (↑r : 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))
⊢ ∀ (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)) ⊤

Tactic:
replace H := fun r => (H r).1
-- Module: Mathlib.RingTheory.RingHom.Finite
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)) ⊤
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) ⊤
⊢ Submodule.FG.{u_5, u_5} (R := R) (M := S) ⊤

Tactic:
choose s₁ s₂ using H
-- Module: Mathlib.RingTheory.RingHom.Finite
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)
h : Eq (α := Submodule R S) (Submodule.span R (↑(s.attach.biUnion sf) : Set S)) ⊤
⊢ Submodule.FG.{u_5, u_5} (R := R) (M := S) ⊤

Tactic:
use s.attach.biUnion sf

Premises used: Finset.biUnion, Finset.attach
-- Module: Mathlib.RingTheory.RingHom.Finite
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)
h : LE.le.{u_5} (α := Submodule R S) ⊤ (⨆ (x : ↥s), Submodule.span R (↑(sf x) : Set S))
⊢ Eq (α := Submodule R S) (Submodule.span R (↑(s.attach.biUnion sf) : Set S)) ⊤

Tactic:
rw [Submodule.span_attach_biUnion, eq_top_iff]

Premises used: eq_top_iff, Submodule.span_attach_biUnion
-- Module: Mathlib.RingTheory.RingHom.Finite
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
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)
⊢ Membership.mem (γ := Submodule R S) (⨆ (x : ↥s), Submodule.span R (↑(sf x) : Set S)) x

Tactic:
apply Submodule.mem_of_span_eq_top_of_smul_pow_mem _ (s : Set R) hs _ _

Premises used: Submodule.mem_of_span_eq_top_of_smul_pow_mem, SetLike.coe
-- Module: Mathlib.RingTheory.RingHom.Finite
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)
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))
⊢ 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))

Tactic:
rw [s₂ r]
-- Module: Mathlib.RingTheory.RingHom.Finite
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))) ⊤
    ((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:
trivial
-- Module: Mathlib.RingTheory.RingHom.Finite
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)
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₁) ⋯)
          ((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)
⊢ ∃ (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)

Premises used: Algebra.algebraMap, Localization.Away, multiple_mem_span_of_mem_localization_span, SetLike.coe, Submonoid.powers, Subtype.val, DFunLike.coe, rfl
-- Module: Mathlib.RingTheory.RingHom.Finite
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)))
⊢ 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))

Tactic:
rw [Submonoid.smul_def, Algebra.smul_def, IsScalarTower.algebraMap_apply R S, ← map_mul] at hn₁

Premises used: Submonoid.smul_def, map_mul, Algebra.smul_def, IsScalarTower.algebraMap_apply