awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.FiniteTypeLocal (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
s_1 : Set S
hs_1 : Eq (α := Ideal S) (Ideal.span s_1) ⊤
s : Finset S
h₁ : (↑s : Set S) ⊆ s_1
hs : Eq (α := Ideal S) (Ideal.span (↑s : Set S)) ⊤
t : (r : ↥s) → Finset (Localization.Away (↑r : S))
ht :
  ∀ (r : ↥s),
    Eq (α := Subalgebra R (Localization.Away (↑r : S))) (adjoin R (↑(t r) : Set (Localization.Away (↑r : S)))) ⊤
l : (↑(↑s : Set S) : Type u_2) →₀ S
hl :
  Eq (α := S)
    ((Finsupp.linearCombination S (Subtype.val (p := fun (x : S) ↦ x ∈ (↑s : Set S))) :
          (a : (↑(↑s : Set S) : Type u_2) →₀ S) → S)
        l :
      S)
    (1 : S)
sf : (x : ↥s) → Finset S := fun (x : ↥s) ↦ IsLocalization.finsetIntegerMultiple (Submonoid.powers (↑x : S)) (t x)
x : S
r : (↑(↑s : Set S) : Type u_2)
refine_1 :
  (↑(IsLocalization.finsetIntegerMultiple (Submonoid.powers (↑r : S)) (t r)) : Set S) ⊆
    (↑(adjoin R
          ((⋃ x ∈ (↑s.attach : Set ↥s), (↑(sf x) : Set S)) ∪ (↑s : Set S) ∪
            (↑(Finset.image (⇑l : (a : (↑(↑s : Set S) : Type u_2)) → S) l.support) : Set S))) :
      Set S)
refine_2 :
  LE.le (α := Submonoid S) (Submonoid.powers (↑r : S))
    (Subsemiring.toSubmonoid
      (Subalgebra.toSubsemiring
        (adjoin R
          ((⋃ x ∈ (↑s.attach : Set ↥s), (↑(sf x) : Set S)) ∪ (↑s : Set S) ∪
            (↑(Finset.image (⇑l : (a : (↑(↑s : Set S) : Type u_2)) → S) l.support) : Set S)))))
⊢ ∃ (m : ↥(Submonoid.powers (↑r : S))),
    Membership.mem (γ := Subalgebra R S)
      (adjoin R
        ((⋃ x ∈ (↑s.attach : Set ↥s), (↑(sf x) : Set S)) ∪ (↑s : Set S) ∪
          (↑(Finset.image (⇑l : (a : (↑(↑s : Set S) : Type u_2)) → S) l.support) : Set S)))
      ((↑m : S) • x)
have refine_3 : Membership.mem (α := Localization.Away (↑r : S)) (γ := Subalgebra R (Localization.Away (↑r : S)))
  (adjoin R (↑(t r) : Set (Localization.Away (↑r : S))))
  ((algebraMap S (Localization.Away (↑r : S)) : (a : S) → Localization.Away (↑r : S)) x : Localization.Away (↑r : S))
Tactic: refine IsLocalization.exists_smul_mem_of_mem_adjoin
      (Submonoid.powers (r : S)) x (t r) (Algebra.adjoin R _) ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.FiniteTypeLocal (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
s_1 : Set S
hs_1 : Eq (α := Ideal S) (Ideal.span s_1) ⊤
s : Finset S
h₁ : (↑s : Set S) ⊆ s_1
hs : Eq (α := Ideal S) (Ideal.span (↑s : Set S)) ⊤
t : (r : ↥s) → Finset (Localization.Away (↑r : S))
ht :
  ∀ (r : ↥s),
    Eq (α := Subalgebra R (Localization.Away (↑r : S))) (adjoin R (↑(t r) : Set (Localization.Away (↑r : S)))) ⊤
l : (↑(↑s : Set S) : Type u_2) →₀ S
hl :
  Eq (α := S)
    ((Finsupp.linearCombination S (Subtype.val (p := fun (x : S) ↦ x ∈ (↑s : Set S))) :
          (a : (↑(↑s : Set S) : Type u_2) →₀ S) → S)
        l :
      S)
    (1 : S)
sf : (x : ↥s) → Finset S := fun (x : ↥s) ↦ IsLocalization.finsetIntegerMultiple (Submonoid.powers (↑x : S)) (t x)
x_1 : S
r : (↑(↑s : Set S) : Type u_2)
x : S
hx : x ∈ (↑(IsLocalization.finsetIntegerMultiple (Submonoid.powers (↑r : S)) (t r)) : Set S)
⊢ x ∈
    (↑(adjoin R
          ((⋃ x ∈ (↑s.attach : Set ↥s), (↑(sf x) : Set S)) ∪ (↑s : Set S) ∪
            (↑(Finset.image (⇑l : (a : (↑(↑s : Set S) : Type u_2)) → S) l.support) : Set S))) :
      Set S)
have refine_1 : x ∈
  (⋃ x ∈ (↑s.attach : Set ↥s), (↑(sf x) : Set S)) ∪ (↑s : Set S) ∪
    (↑(Finset.image (⇑l : (a : (↑(↑s : Set S) : Type u_2)) → S) l.support) : Set S)
Tactic: apply Algebra.subset_adjoin
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.FiniteTypeLocal (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
s_1 : Set S
hs_1 : Eq (α := Ideal S) (Ideal.span s_1) ⊤
s : Finset S
h₁ : (↑s : Set S) ⊆ s_1
hs : Eq (α := Ideal S) (Ideal.span (↑s : Set S)) ⊤
t : (r : ↥s) → Finset (Localization.Away (↑r : S))
ht :
  ∀ (r : ↥s),
    Eq (α := Subalgebra R (Localization.Away (↑r : S))) (adjoin R (↑(t r) : Set (Localization.Away (↑r : S)))) ⊤
l : (↑(↑s : Set S) : Type u_2) →₀ S
hl :
  Eq (α := S)
    ((Finsupp.linearCombination S (Subtype.val (p := fun (x : S) ↦ x ∈ (↑s : Set S))) :
          (a : (↑(↑s : Set S) : Type u_2) →₀ S) → S)
        l :
      S)
    (1 : S)
sf : (x : ↥s) → Finset S := fun (x : ↥s) ↦ IsLocalization.finsetIntegerMultiple (Submonoid.powers (↑x : S)) (t x)
x : S
r : (↑(↑s : Set S) : Type u_2)
⊢ LE.le (α := Submonoid S) (Submonoid.powers (↑r : S))
    (Subsemiring.toSubmonoid
      (Subalgebra.toSubsemiring
        (adjoin R
          ((⋃ x ∈ (↑s.attach : Set ↥s), (↑(sf x) : Set S)) ∪ (↑s : Set S) ∪
            (↑(Finset.image (⇑l : (a : (↑(↑s : Set S) : Type u_2)) → S) l.support) : Set S)))))
have refine_2 : (↑r : S) ∈
  (↑(Subsemiring.toSubmonoid
        (Subalgebra.toSubsemiring
          (adjoin R
            ((⋃ x ∈ (↑s.attach : Set ↥s), (↑(sf x) : Set S)) ∪ (↑s : Set S) ∪
              (↑(Finset.image (⇑l : (a : (↑(↑s : Set S) : Type u_2)) → S) l.support) : Set S))))) :
    Set S)
Tactic: rw [Submonoid.powers_eq_closure, Submonoid.closure_le, Set.singleton_subset_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.FiniteTypeLocal (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
s_1 : Set S
hs_1 : Eq (α := Ideal S) (Ideal.span s_1) ⊤
s : Finset S
h₁ : (↑s : Set S) ⊆ s_1
hs : Eq (α := Ideal S) (Ideal.span (↑s : Set S)) ⊤
t : (r : ↥s) → Finset (Localization.Away (↑r : S))
ht :
  ∀ (r : ↥s),
    Eq (α := Subalgebra R (Localization.Away (↑r : S))) (adjoin R (↑(t r) : Set (Localization.Away (↑r : S)))) ⊤
l : (↑(↑s : Set S) : Type u_2) →₀ S
hl :
  Eq (α := S)
    ((Finsupp.linearCombination S (Subtype.val (p := fun (x : S) ↦ x ∈ (↑s : Set S))) :
          (a : (↑(↑s : Set S) : Type u_2) →₀ S) → S)
        l :
      S)
    (1 : S)
sf : (x : ↥s) → Finset S := fun (x : ↥s) ↦ IsLocalization.finsetIntegerMultiple (Submonoid.powers (↑x : S)) (t x)
x : S
r : (↑(↑s : Set S) : Type u_2)
⊢ (↑r : S) ∈
    (↑(Subsemiring.toSubmonoid
          (Subalgebra.toSubsemiring
            (adjoin R
              ((⋃ x ∈ (↑s.attach : Set ↥s), (↑(sf x) : Set S)) ∪ (↑s : Set S) ∪
                (↑(Finset.image (⇑l : (a : (↑(↑s : Set S) : Type u_2)) → S) l.support) : Set S))))) :
      Set S)
have refine_2 : (↑r : S) ∈
  (⋃ x ∈ (↑s.attach : Set ↥s), (↑(sf x) : Set S)) ∪ (↑s : Set S) ∪
    (↑(Finset.image (⇑l : (a : (↑(↑s : Set S) : Type u_2)) → S) l.support) : Set S)
Tactic: apply Algebra.subset_adjoin
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.FiniteTypeLocal (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
s_1 : Set S
hs_1 : Eq (α := Ideal S) (Ideal.span s_1) ⊤
s : Finset S
h₁ : (↑s : Set S) ⊆ s_1
hs : Eq (α := Ideal S) (Ideal.span (↑s : Set S)) ⊤
t : (r : ↥s) → Finset (Localization.Away (↑r : S))
ht :
  ∀ (r : ↥s),
    Eq (α := Subalgebra R (Localization.Away (↑r : S))) (adjoin R (↑(t r) : Set (Localization.Away (↑r : S)))) ⊤
l : (↑(↑s : Set S) : Type u_2) →₀ S
hl :
  Eq (α := S)
    ((Finsupp.linearCombination S (Subtype.val (p := fun (x : S) ↦ x ∈ (↑s : Set S))) :
          (a : (↑(↑s : Set S) : Type u_2) →₀ S) → S)
        l :
      S)
    (1 : S)
sf : (x : ↥s) → Finset S := fun (x : ↥s) ↦ IsLocalization.finsetIntegerMultiple (Submonoid.powers (↑x : S)) (t x)
x : S
r : (↑(↑s : Set S) : Type u_2)
⊢ Membership.mem (α := Localization.Away (↑r : S)) (γ := Subalgebra R (Localization.Away (↑r : S)))
    (adjoin R (↑(t r) : Set (Localization.Away (↑r : S))))
    ((algebraMap S (Localization.Away (↑r : S)) : (a : S) → Localization.Away (↑r : S)) x : Localization.Away (↑r : S))
have refine_3 : Membership.mem (α := Localization.Away (↑r : S)) (γ := Subalgebra R (Localization.Away (↑r : S))) ⊤
  ((algebraMap S (Localization.Away (↑r : S)) : (a : S) → Localization.Away (↑r : S)) x : Localization.Away (↑r : S))
Tactic: rw [ht]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.FiniteTypeLocal (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
s_1 : Set S
hs_1 : Eq (α := Ideal S) (Ideal.span s_1) ⊤
s : Finset S
h₁ : (↑s : Set S) ⊆ s_1
hs : Eq (α := Ideal S) (Ideal.span (↑s : Set S)) ⊤
h : ∀ (i : ↥s), FiniteType.{u_1, u_2} R (Localization.Away (↑i : S))
⊢ FiniteType R S
have Suppose : ∀ (h : ∀ (r : ↥s), Subalgebra.FG.{u_1, u_2} (R := R) (A := Localization.Away (↑r : S)) ⊤), FiniteType R S
Tactic: classical
  -- Suppose `s : Finset S` spans `S`, and each `Sᵣ` is finitely generated as an `R`-algebra.
  -- Say `t r : Finset Sᵣ` generates `Sᵣ`. By assumption, we may find `lᵢ` such that
  -- `∑ lᵢ * sᵢ = 1`. I claim that all `s` and `l` and the numerators of `t` and generates `S`.
  replace h := fun r => (h r).1
  choose t ht using h
  obtain ⟨l, hl⟩ :=
    (Finsupp.mem_span_iff_linearCombination S (s : Set S) 1).mp
      (show (1 : S) ∈ Ideal.span (s : Set S) by rw [hs]; trivial)
  let sf := fun x : s => IsLocalization.finsetIntegerMultiple (Submonoid.powers (x : S)) (t x)
  use s.attach.biUnion sf ∪ s ∪ l.support.image l
  rw [_root_.eq_top_iff]
  -- We need to show that every `x` falls in the subalgebra generated by those elements.
  -- Since all `s` and `l` are in the subalgebra, it suffices to check that `sᵢ ^ nᵢ • x` falls in
  -- the algebra for each `sᵢ` and some `nᵢ`.
  rintro x -
  apply Subalgebra.mem_of_span_eq_top_of_smul_pow_mem _ (s : Set S) l hl _ _ x _
  · intro x hx
    apply Algebra.subset_adjoin
    rw [Finset.coe_union, Finset.coe_union]
    exact Or.inl (Or.inr hx)
  · intro i
    by_cases h : l i = 0; · rw [h]; exact zero_mem _
    apply Algebra.subset_adjoin
    rw [Finset.coe_union, Finset.coe_image]
    exact Or.inr (Set.mem_image_of_mem _ (Finsupp.mem_support_iff.mpr h))
  · intro r
    rw [Finset.coe_union, Finset.coe_union, Finset.coe_biUnion]
    -- Since all `sᵢ` and numerators of `t r` are in the algebra, it suffices to show that the
    -- image of `x` in `Sᵣ` falls in the `R`-adjoin of `t r`, which is of course true.
    -- Porting note: The following `obtain` fails because Lean wants to know right away what the
    -- placeholders are, so we need to provide a little more guidance
    -- obtain ⟨⟨_, n₂, rfl⟩, hn₂⟩ := IsLocalization.exists_smul_mem_of_mem_adjoin
    --   (Submonoid.powers (r : S)) x (t r) (Algebra.adjoin R _) _ _ _
    rw [show ∀ A : Set S, (∃ n, (r : S) ^ n • x ∈ Algebra.adjoin R A) ↔
      (∃ m : (Submonoid.powers (r : S)), (m : S) • x ∈ Algebra.adjoin R A) by
      { exact fun _ => by simp [Submonoid.mem_powers_iff] }]
    refine IsLocalization.exists_smul_mem_of_mem_adjoin
      (Submonoid.powers (r : S)) x (t r) (Algebra.adjoin R _) ?_ ?_ ?_
    · intro x hx
      apply Algebra.subset_adjoin
      exact Or.inl (Or.inl ⟨_, ⟨r, rfl⟩, _, ⟨s.mem_attach r, rfl⟩, hx⟩)
    · rw [Submonoid.powers_eq_closure, Submonoid.closure_le, Set.singleton_subset_iff]
      apply Algebra.subset_adjoin
      exact Or.inl (Or.inr r.2)
    · rw [ht]; trivial
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.FiniteTypeLocal (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
s : Set R
hs : Eq (α := Ideal R) (Ideal.span s) ⊤
h : ∀ i ∈ s, FiniteType (Localization.Away i) (Localization.Away i ⊗[R] S)
⊢ FiniteType R S
have obtain : ∀ (s_1 : Finset R) (h₁ : (↑s_1 : Set R) ⊆ s) (hs : Eq (α := Ideal R) (Ideal.span (↑s_1 : Set R)) ⊤), FiniteType R S
Tactic: obtain ⟨s, h₁, hs⟩ := (Ideal.span_eq_top_iff_finite s).mp hs
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.FiniteTypeLocal (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
s_1 : Set R
hs_1 : Eq (α := Ideal R) (Ideal.span s_1) ⊤
h : ∀ i ∈ s_1, FiniteType (Localization.Away i) (Localization.Away i ⊗[R] S)
s : Finset R
h₁ : (↑s : Set R) ⊆ s_1
hs : Eq (α := Ideal R) (Ideal.span (↑s : Set R)) ⊤
⊢ FiniteType R S
have h₂ : ∀ (i : ↥s), FiniteType (Localization.Away (↑i : R)) (Localization.Away (↑i : R) ⊗[R] S)
Tactic: replace h (i : s) := h i.val (h₁ i.property)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.FiniteTypeLocal (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
s_1 : Set R
hs_1 : Eq (α := Ideal R) (Ideal.span s_1) ⊤
s : Finset R
h₁ : (↑s : Set R) ⊆ s_1
hs : Eq (α := Ideal R) (Ideal.span (↑s : Set R)) ⊤
h : ∀ (i : ↥s), FiniteType (Localization.Away (↑i : R)) (Localization.Away (↑i : R) ⊗[R] S)
this : (r : ↥s) →
  Algebra.{u_1, u_2} (Localization.Away (↑r : R))
    (Localization.Away (M := S) ((algebraMap R S : (a : R) → S) (↑r : R) : S)) :=
  fun (r : ↥s) ↦ RingHom.toAlgebra (Localization.awayMap (algebraMap R S) (↑r : R))
⊢ FiniteType R S
have set : let f : R →+* S := algebraMap R S;
∀
  (this :
    (r : ↥s) →
      Algebra.{u_1, u_2} (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))),
  FiniteType R S
Tactic: set f := algebraMap R S
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.FiniteTypeLocal (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
s_1 : Set R
hs_1 : Eq (α := Ideal R) (Ideal.span s_1) ⊤
s : Finset R
h₁ : (↑s : Set R) ⊆ s_1
hs : Eq (α := Ideal R) (Ideal.span (↑s : Set R)) ⊤
h : ∀ (i : ↥s), FiniteType (Localization.Away (↑i : R)) (Localization.Away (↑i : R) ⊗[R] S)
f : R →+* S := algebraMap R S
this :
  (r : ↥s) →
    Algebra.{u_1, u_2} (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
⊢ FiniteType R S
have out : Subalgebra.FG.{u_1, u_2} (R := R) (A := S) ⊤
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.FiniteTypeLocal (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
s_1 : Set R
hs_1 : Eq (α := Ideal R) (Ideal.span s_1) ⊤
s : Finset R
h₁ : (↑s : Set R) ⊆ s_1
hs : Eq (α := Ideal R) (Ideal.span (↑s : Set R)) ⊤
h : ∀ (i : ↥s), FiniteType (Localization.Away (↑i : R)) (Localization.Away (↑i : R) ⊗[R] S)
f : R →+* S := algebraMap R S
this :
  (r : ↥s) →
    Algebra.{u_1, u_2} (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
⊢ Subalgebra.FG.{u_1, u_2} (R := R) (A := S) ⊤
have H : ∀ (r : ↥s), Subalgebra.FG (R := Localization.Away (↑r : R)) (A := Localization.Away (↑r : R) ⊗[R] S) ⊤
Tactic: replace H := fun r => (h r).1
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.FiniteTypeLocal (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
s_1 : Set R
hs_1 : Eq (α := Ideal R) (Ideal.span s_1) ⊤
s : Finset R
h₁ : (↑s : Set R) ⊆ s_1
hs : Eq (α := Ideal R) (Ideal.span (↑s : Set R)) ⊤
h : ∀ (i : ↥s), FiniteType (Localization.Away (↑i : R)) (Localization.Away (↑i : R) ⊗[R] S)
f : R →+* S := algebraMap R S
this :
  (r : ↥s) →
    Algebra.{u_1, u_2} (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
H : ∀ (r : ↥s), Subalgebra.FG (R := Localization.Away (↑r : R)) (A := Localization.Away (↑r : R) ⊗[R] S) ⊤
⊢ Subalgebra.FG.{u_1, u_2} (R := R) (A := S) ⊤
have out : ∀ (s₁ : (r : ↥s) → Finset (Localization.Away (↑r : R) ⊗[R] S))
  (s₂ :
    ∀ (r : ↥s),
      Eq (α := Subalgebra (Localization.Away (↑r : R)) (Localization.Away (↑r : R) ⊗[R] S))
        (adjoin (Localization.Away (↑r : R)) (↑(s₁ r) : Set (Localization.Away (↑r : R) ⊗[R] S))) ⊤),
  Subalgebra.FG.{u_1, u_2} (R := R) (A := S) ⊤
Tactic: choose s₁ s₂ using H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.FiniteTypeLocal (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
s_1 : Set R
hs_1 : Eq (α := Ideal R) (Ideal.span s_1) ⊤
s : Finset R
h₁ : (↑s : Set R) ⊆ s_1
hs : Eq (α := Ideal R) (Ideal.span (↑s : Set R)) ⊤
h : ∀ (i : ↥s), FiniteType (Localization.Away (↑i : R)) (Localization.Away (↑i : R) ⊗[R] S)
f : R →+* S := algebraMap R S
this :
  (r : ↥s) →
    Algebra.{u_1, u_2} (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
s₁ : (r : ↥s) → Finset (Localization.Away (↑r : R) ⊗[R] S)
s₂ :
  ∀ (r : ↥s),
    Eq (α := Subalgebra (Localization.Away (↑r : R)) (Localization.Away (↑r : R) ⊗[R] S))
      (adjoin (Localization.Away (↑r : R)) (↑(s₁ r) : Set (Localization.Away (↑r : R) ⊗[R] S))) ⊤
sf : (x : ↥s) → Finset S :=
  fun (x : ↥s) ↦ IsLocalization.finsetIntegerMultiple (Submonoid.powers ((f : (a : R) → S) (↑x : R))) (s₁ x)
⊢ Subalgebra.FG.{u_1, u_2} (R := R) (A := S) ⊤
have h₂ : Eq (α := Subalgebra R S) (adjoin R (↑(s.attach.biUnion sf) : Set S)) ⊤
Tactic: use s.attach.biUnion sf
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.FiniteTypeLocal (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
s_1 : Set R
hs_1 : Eq (α := Ideal R) (Ideal.span s_1) ⊤
s : Finset R
h₁ : (↑s : Set R) ⊆ s_1
hs : Eq (α := Ideal R) (Ideal.span (↑s : Set R)) ⊤
h : ∀ (i : ↥s), FiniteType (Localization.Away (↑i : R)) (Localization.Away (↑i : R) ⊗[R] S)
f : R →+* S := algebraMap R S
this :
  (r : ↥s) →
    Algebra.{u_1, u_2} (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
s₁ : (r : ↥s) → Finset (Localization.Away (↑r : R) ⊗[R] S)
s₂ :
  ∀ (r : ↥s),
    Eq (α := Subalgebra (Localization.Away (↑r : R)) (Localization.Away (↑r : R) ⊗[R] S))
      (adjoin (Localization.Away (↑r : R)) (↑(s₁ r) : Set (Localization.Away (↑r : R) ⊗[R] S))) ⊤
sf : (x : ↥s) → Finset S :=
  fun (x : ↥s) ↦ IsLocalization.finsetIntegerMultiple (Submonoid.powers ((f : (a : R) → S) (↑x : R))) (s₁ x)
⊢ Eq (α := Subalgebra R S) (adjoin R (↑(s.attach.biUnion sf) : Set S)) ⊤
have h₂ : Eq.{u_2 + 1} (α := Subalgebra R S) (⨆ (x : ↥s), adjoin R (↑(sf x) : Set S)) ⊤
Tactic: convert! (Algebra.adjoin_attach_biUnion (R := R) sf).trans _
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.FiniteTypeLocal (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
s_1 : Set R
hs_1 : Eq (α := Ideal R) (Ideal.span s_1) ⊤
s : Finset R
h₁ : (↑s : Set R) ⊆ s_1
hs : Eq (α := Ideal R) (Ideal.span (↑s : Set R)) ⊤
h : ∀ (i : ↥s), FiniteType (Localization.Away (↑i : R)) (Localization.Away (↑i : R) ⊗[R] S)
f : R →+* S := algebraMap R S
this :
  (r : ↥s) →
    Algebra.{u_1, u_2} (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
s₁ : (r : ↥s) → Finset (Localization.Away (↑r : R) ⊗[R] S)
s₂ :
  ∀ (r : ↥s),
    Eq (α := Subalgebra (Localization.Away (↑r : R)) (Localization.Away (↑r : R) ⊗[R] S))
      (adjoin (Localization.Away (↑r : R)) (↑(s₁ r) : Set (Localization.Away (↑r : R) ⊗[R] S))) ⊤
sf : (x : ↥s) → Finset S :=
  fun (x : ↥s) ↦ IsLocalization.finsetIntegerMultiple (Submonoid.powers ((f : (a : R) → S) (↑x : R))) (s₁ x)
⊢ Eq.{u_2 + 1} (α := Subalgebra R S) (⨆ (x : ↥s), adjoin R (↑(sf x) : Set S)) ⊤
have h₂ : ∀ (x : S), Membership.mem (γ := Subalgebra R S) (⨆ (x : ↥s), adjoin R (↑(sf x) : Set S)) x
Tactic: rw [eq_top_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.FiniteTypeLocal (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
s_1 : Set R
hs_1 : Eq (α := Ideal R) (Ideal.span s_1) ⊤
s : Finset R
h₁ : (↑s : Set R) ⊆ s_1
hs : Eq (α := Ideal R) (Ideal.span (↑s : Set R)) ⊤
h : ∀ (i : ↥s), FiniteType (Localization.Away (↑i : R)) (Localization.Away (↑i : R) ⊗[R] S)
f : R →+* S := algebraMap R S
this :
  (r : ↥s) →
    Algebra.{u_1, u_2} (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
s₁ : (r : ↥s) → Finset (Localization.Away (↑r : R) ⊗[R] S)
s₂ :
  ∀ (r : ↥s),
    Eq (α := Subalgebra (Localization.Away (↑r : R)) (Localization.Away (↑r : R) ⊗[R] S))
      (adjoin (Localization.Away (↑r : R)) (↑(s₁ r) : Set (Localization.Away (↑r : R) ⊗[R] S))) ⊤
sf : (x : ↥s) → Finset S :=
  fun (x : ↥s) ↦ IsLocalization.finsetIntegerMultiple (Submonoid.powers ((f : (a : R) → S) (↑x : R))) (s₁ x)
x : S
t : Set S
⊢ Membership.mem (γ := Set (Set S))
      (Set.range fun (t : Subsemiring S) ↦
        ⋂ (_ :
          Membership.mem (γ := Set (Subsemiring S))
            {S_1 : Subsemiring S |
              Set.range.{u_2, u_1 + 1} (ι := R) (⇑(algebraMap R S) : (a : R) → S) ∪
                  sSup
                    (Set.image (α := Subalgebra R S) SetLike.coe
                      (Set.range fun (x : ↥s) ↦ adjoin R (↑(sf x) : Set S))) ⊆
                (↑S_1 : Set S)}
            t),
          (↑t : Set S))
      t →
    x ∈ t
have apply : ∀ (r : (↑(↑s : Set R) : Type u_1)),
  ∃ (n : ℕ),
    Membership.mem (γ := Submodule R S)
      ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) (⨆ (x : ↥s), adjoin R (↑(sf x) : Set S)) :
        Submodule R S)
      ((↑r : R) ^ n • x)
Tactic: apply (⨆ x : s, Algebra.adjoin R (sf x : Set S)).toSubmodule.mem_of_span_eq_top_of_smul_pow_mem
    _ hs _ _
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.FiniteTypeLocal (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
s_1 : Set R
hs_1 : Eq (α := Ideal R) (Ideal.span s_1) ⊤
s : Finset R
h₁ : (↑s : Set R) ⊆ s_1
hs : Eq (α := Ideal R) (Ideal.span (↑s : Set R)) ⊤
h : ∀ (i : ↥s), FiniteType (Localization.Away (↑i : R)) (Localization.Away (↑i : R) ⊗[R] S)
f : R →+* S := algebraMap R S
this :
  (r : ↥s) →
    Algebra.{u_1, u_2} (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
s₁ : (r : ↥s) → Finset (Localization.Away (↑r : R) ⊗[R] S)
s₂ :
  ∀ (r : ↥s),
    Eq (α := Subalgebra (Localization.Away (↑r : R)) (Localization.Away (↑r : R) ⊗[R] S))
      (adjoin (Localization.Away (↑r : R)) (↑(s₁ r) : Set (Localization.Away (↑r : R) ⊗[R] S))) ⊤
sf : (x : ↥s) → Finset S :=
  fun (x : ↥s) ↦ IsLocalization.finsetIntegerMultiple (Submonoid.powers ((f : (a : R) → S) (↑x : R))) (s₁ x)
x : S
t : Set S
r : (↑(↑s : Set R) : Type u_1)
⊢ Membership.mem (α := Localization.Away (↑r : R) ⊗[R] S) (γ :=
    Subalgebra (Localization.Away (↑r : R)) (Localization.Away (↑r : R) ⊗[R] S))
    (adjoin (Localization.Away (↑r : R)) (↑(s₁ r) : Set (Localization.Away (↑r : R) ⊗[R] S)))
    ((algebraMap S (Localization.Away (↑r : R) ⊗[R] S) : (a : S) → Localization.Away (↑r : R) ⊗[R] S) x :
      Localization.Away (↑r : R) ⊗[R] S)
have rw : Membership.mem (α := Localization.Away (↑r : R) ⊗[R] S) (γ :=
  Subalgebra (Localization.Away (↑r : R)) (Localization.Away (↑r : R) ⊗[R] S)) ⊤
  ((algebraMap S (Localization.Away (↑r : R) ⊗[R] S) : (a : S) → Localization.Away (↑r : R) ⊗[R] S) x :
    Localization.Away (↑r : R) ⊗[R] S)
Tactic: rw [s₂ r]