awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Finiteness.FiniteTypeLocal
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)
⊢ ∀ (A : Set S),
    (∃ (n : ℕ), Membership.mem (γ := Subalgebra R S) (adjoin R A) ((↑r : S) ^ n • x)) ↔
      ∃ (m : ↥(Submonoid.powers (↑r : S))), Membership.mem (γ := Subalgebra R S) (adjoin R A) ((↑m : S) • x)

Tactic:
exact fun _ => by simp [Submonoid.mem_powers_iff]
-- Module: Mathlib.RingTheory.Finiteness.FiniteTypeLocal
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)
⊢ ∀ (A : Set S),
    (∃ (n : ℕ), Membership.mem (γ := Subalgebra R S) (adjoin R A) ((↑r : S) ^ n • x)) ↔
      ∃ (m : ↥(Submonoid.powers (↑r : S))), Membership.mem (γ := Subalgebra R S) (adjoin R A) ((↑m : S) • x)

Tactic:
{ exact fun _ => by simp [Submonoid.mem_powers_iff] }
-- Module: Mathlib.RingTheory.Finiteness.FiniteTypeLocal
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)
rw :
  ∃ (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)
⊢ ∃ (n : ℕ),
    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)))
      ((↑r : S) ^ n • x)

Tactic:
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] }]
-- Module: Mathlib.RingTheory.Finiteness.FiniteTypeLocal
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)
⊢ ∃ (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)

Tactic:
IsLocalization.exists_smul_mem_of_mem_adjoin
      (Submonoid.powers (r : S)) x (t r) (Algebra.adjoin R _) ?_ ?_ ?_

Premises used: Set.Mem, Algebra.adjoin, IsLocalization.exists_smul_mem_of_mem_adjoin, Submonoid.powers, Subtype.val
-- Module: Mathlib.RingTheory.Finiteness.FiniteTypeLocal
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)))))
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))
⊢ ∃ (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)

Tactic:
refine IsLocalization.exists_smul_mem_of_mem_adjoin
      (Submonoid.powers (r : S)) x (t r) (Algebra.adjoin R _) ?_ ?_ ?_

Premises used: Algebra.adjoin, IsLocalization.exists_smul_mem_of_mem_adjoin, Submonoid.powers, Subtype.val
-- Module: Mathlib.RingTheory.Finiteness.FiniteTypeLocal
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)
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)
⊢ 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)

Tactic:
apply Algebra.subset_adjoin

Premises used: Algebra.subset_adjoin
-- Module: Mathlib.RingTheory.Finiteness.FiniteTypeLocal
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 ∈
    (⋃ 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:
Or.inl (Or.inl ⟨_, ⟨r, rfl⟩, _, ⟨s.mem_attach r, rfl⟩, hx⟩)

Premises used: Set.union, Set.Mem, setOf, Finset.mem_attach, And.intro, Exists.intro, Or.inl, rfl
-- Module: Mathlib.RingTheory.Finiteness.FiniteTypeLocal
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 ∈
    (⋃ 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:
exact Or.inl (Or.inl ⟨_, ⟨r, rfl⟩, _, ⟨s.mem_attach r, rfl⟩, hx⟩)

Premises used: Or.inl
-- Module: Mathlib.RingTheory.Finiteness.FiniteTypeLocal
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_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)
⊢ 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)))))

Tactic:
rw [Submonoid.powers_eq_closure, Submonoid.closure_le, Set.singleton_subset_iff]

Premises used: Set.singleton_subset_iff, Submonoid.powers_eq_closure, Submonoid.closure_le
-- Module: Mathlib.RingTheory.Finiteness.FiniteTypeLocal
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_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)
⊢ (↑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:
apply Algebra.subset_adjoin

Premises used: Algebra.subset_adjoin
-- Module: Mathlib.RingTheory.Finiteness.FiniteTypeLocal
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) ∈
    (⋃ 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:
Or.inl (Or.inr r.2)

Premises used: Set.union, Set.Mem, setOf, Or.inl, Or.inr, Subtype.property
-- Module: Mathlib.RingTheory.Finiteness.FiniteTypeLocal
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) ∈
    (⋃ 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:
exact Or.inl (Or.inr r.2)

Premises used: Or.inl, Or.inr, Subtype.property
-- Module: Mathlib.RingTheory.Finiteness.FiniteTypeLocal
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_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))
⊢ 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:
rw [ht]
-- Module: Mathlib.RingTheory.Finiteness.FiniteTypeLocal
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))) ⊤
    ((algebraMap S (Localization.Away (↑r : S)) : (a : S) → Localization.Away (↑r : S)) x : Localization.Away (↑r : S))

Tactic:
trivial
-- Module: Mathlib.RingTheory.Finiteness.FiniteTypeLocal
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)
obtain :
  ∀ (s_1 : Finset R) (h₁ : (↑s_1 : Set R) ⊆ s) (hs : Eq (α := Ideal R) (Ideal.span (↑s_1 : Set R)) ⊤), FiniteType R S
⊢ FiniteType R S

Tactic:
obtain ⟨s, h₁, hs⟩ := (Ideal.span_eq_top_iff_finite s).mp hs

Premises used: Ideal.span_eq_top_iff_finite, Iff.mp
-- Module: Mathlib.RingTheory.Finiteness.FiniteTypeLocal
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)) ⊤
⊢ ∀ (i : ↥s), FiniteType (Localization.Away (↑i : R)) (Localization.Away (↑i : R) ⊗[R] S)

Tactic:
replace h (i : s) := h i.val (h₁ i.property)
-- Module: Mathlib.RingTheory.Finiteness.FiniteTypeLocal
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))
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
⊢ FiniteType R S

Tactic:
set f := algebraMap R S

Premises used: Algebra.algebraMap
-- Module: Mathlib.RingTheory.Finiteness.FiniteTypeLocal
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))
out : Subalgebra.FG.{u_1, u_2} (R := R) (A := S) ⊤
⊢ FiniteType R S

Tactic:
constructor
-- Module: Mathlib.RingTheory.Finiteness.FiniteTypeLocal
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))
⊢ ∀ (r : ↥s), Subalgebra.FG (R := Localization.Away (↑r : R)) (A := Localization.Away (↑r : R) ⊗[R] S) ⊤

Tactic:
replace H := fun r => (h r).1
-- Module: Mathlib.RingTheory.Finiteness.FiniteTypeLocal
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) ⊤
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) ⊤
⊢ Subalgebra.FG.{u_1, u_2} (R := R) (A := S) ⊤

Tactic:
choose s₁ s₂ using H