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)))) ⊤
⊢ Membership.mem (γ := Ideal S) ⊤ 1

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_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)))) ⊤
obtain :
  ∀ (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)),
    FiniteType R S
⊢ FiniteType R S

Tactic:
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)

Premises used: Finsupp.mem_span_iff_linearCombination, SetLike.coe, Iff.mp, OfNat.ofNat
-- 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)
h :
  Eq (α := Subalgebra R S)
    (adjoin R (↑(s.attach.biUnion sf ∪ s ∪ Finset.image (⇑l : (a : (↑(↑s : Set S) : Type u_2)) → S) l.support) : Set S))
    ⊤
⊢ FiniteType R S

Tactic:
use s.attach.biUnion sf ∪ s ∪ l.support.image l

Premises used: Finsupp.support, Finset.biUnion, Finset.attach, DFunLike.coe, Finset.image
-- 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)
h :
  LE.le (α := Subalgebra R S) ⊤
    (adjoin R (↑(s.attach.biUnion sf ∪ s ∪ Finset.image (⇑l : (a : (↑(↑s : Set S) : Type u_2)) → S) l.support) : Set S))
⊢ Eq (α := Subalgebra R S)
    (adjoin R (↑(s.attach.biUnion sf ∪ s ∪ Finset.image (⇑l : (a : (↑(↑s : Set S) : Type u_2)) → S) l.support) : Set S))
    ⊤

Tactic:
rw [_root_.eq_top_iff]

Premises used: eq_top_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
apply :
  (↑s : Set S) ⊆
    (↑(adjoin R
          (↑(s.attach.biUnion sf ∪ s ∪ Finset.image (⇑l : (a : (↑(↑s : Set S) : Type u_2)) → S) l.support) : Set S)) :
      Set S)
apply₁ :
  ∀ (i : (↑(↑s : Set S) : Type u_2)),
    Membership.mem (α := S) (γ := Subalgebra R S)
      (adjoin R
        (↑(s.attach.biUnion sf ∪ s ∪ Finset.image (⇑l : (a : (↑(↑s : Set S) : Type u_2)) → S) l.support) : Set S))
      ((l : (a : (↑(↑s : Set S) : Type u_2)) → S) i : S)
apply₂ :
  ∀ (r : (↑(↑s : Set S) : Type u_2)),
    ∃ (n : ℕ),
      Membership.mem (γ := Subalgebra R S)
        (adjoin R
          (↑(s.attach.biUnion sf ∪ s ∪ Finset.image (⇑l : (a : (↑(↑s : Set S) : Type u_2)) → S) l.support) : Set S))
        ((↑r : S) ^ n • x)
⊢ Membership.mem (γ := Subalgebra R S)
    (adjoin R (↑(s.attach.biUnion sf ∪ s ∪ Finset.image (⇑l : (a : (↑(↑s : Set S) : Type u_2)) → S) l.support) : Set S))
    x

Tactic:
apply Subalgebra.mem_of_span_eq_top_of_smul_pow_mem _ (s : Set S) l hl _ _ x _

Premises used: SetLike.coe, Subalgebra.mem_of_span_eq_top_of_smul_pow_mem
-- 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 x : S
hx : x ∈ (↑s : Set S)
a : x ∈ (↑(s.attach.biUnion sf ∪ s ∪ Finset.image (⇑l : (a : (↑(↑s : Set S) : Type u_2)) → S) l.support) : Set S)
⊢ x ∈
    (↑(adjoin R
          (↑(s.attach.biUnion sf ∪ 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 x : S
hx : x ∈ (↑s : Set S)
a :
  x ∈
    (↑(s.attach.biUnion sf) : Set S) ∪ (↑s : Set S) ∪
      (↑(Finset.image (⇑l : (a : (↑(↑s : Set S) : Type u_2)) → S) l.support) : Set S)
⊢ x ∈ (↑(s.attach.biUnion sf ∪ s ∪ Finset.image (⇑l : (a : (↑(↑s : Set S) : Type u_2)) → S) l.support) : Set S)

Tactic:
rw [Finset.coe_union, Finset.coe_union]

Premises used: Finset.coe_union
-- 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 x : S
hx : x ∈ (↑s : Set S)
⊢ x ∈
    (↑(s.attach.biUnion sf) : 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 hx)

Premises used: Set.union, Set.Mem, setOf, Or.inl, Or.inr
-- 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 x : S
hx : x ∈ (↑s : Set S)
⊢ x ∈
    (↑(s.attach.biUnion sf) : 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 hx)

Premises used: Or.inl, Or.inr
-- 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
i : (↑(↑s : Set S) : Type u_2)
pos :
  ∀ (h : Eq (α := S) ((l : (a : (↑(↑s : Set S) : Type u_2)) → S) i : S) (0 : S)),
    Membership.mem (α := S) (γ := Subalgebra R S)
      (adjoin R
        (↑(s.attach.biUnion sf ∪ s ∪ Finset.image (⇑l : (a : (↑(↑s : Set S) : Type u_2)) → S) l.support) : Set S))
      ((l : (a : (↑(↑s : Set S) : Type u_2)) → S) i : S)
neg :
  ∀ (h : ¬Eq (α := S) ((l : (a : (↑(↑s : Set S) : Type u_2)) → S) i : S) (0 : S)),
    Membership.mem (α := S) (γ := Subalgebra R S)
      (adjoin R
        (↑(s.attach.biUnion sf ∪ s ∪ Finset.image (⇑l : (a : (↑(↑s : Set S) : Type u_2)) → S) l.support) : Set S))
      ((l : (a : (↑(↑s : Set S) : Type u_2)) → S) i : S)
⊢ Membership.mem (α := S) (γ := Subalgebra R S)
    (adjoin R (↑(s.attach.biUnion sf ∪ s ∪ Finset.image (⇑l : (a : (↑(↑s : Set S) : Type u_2)) → S) l.support) : Set S))
    ((l : (a : (↑(↑s : Set S) : Type u_2)) → S) i : S)

Tactic:
by_cases h : l i = 0

Premises used: DFunLike.coe
-- 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
i : (↑(↑s : Set S) : Type u_2)
h : Eq (α := S) ((l : (a : (↑(↑s : Set S) : Type u_2)) → S) i : S) (0 : S)
pos :
  Membership.mem (γ := Subalgebra R S)
    (adjoin R (↑(s.attach.biUnion sf ∪ s ∪ Finset.image (⇑l : (a : (↑(↑s : Set S) : Type u_2)) → S) l.support) : Set S))
    0
⊢ Membership.mem (α := S) (γ := Subalgebra R S)
    (adjoin R (↑(s.attach.biUnion sf ∪ s ∪ Finset.image (⇑l : (a : (↑(↑s : Set S) : Type u_2)) → S) l.support) : Set S))
    ((l : (a : (↑(↑s : Set S) : Type u_2)) → S) i : S)

Tactic:
rw [h]
-- 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
i : (↑(↑s : Set S) : Type u_2)
h : Eq (α := S) ((l : (a : (↑(↑s : Set S) : Type u_2)) → S) i : S) (0 : S)
⊢ Membership.mem (γ := Subalgebra R S)
    (adjoin R (↑(s.attach.biUnion sf ∪ s ∪ Finset.image (⇑l : (a : (↑(↑s : Set S) : Type u_2)) → S) l.support) : Set S))
    0

Tactic:
zero_mem _

Premises used: ZeroMemClass.zero_mem
-- 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
i : (↑(↑s : Set S) : Type u_2)
h : Eq (α := S) ((l : (a : (↑(↑s : Set S) : Type u_2)) → S) i : S) (0 : S)
⊢ Membership.mem (γ := Subalgebra R S)
    (adjoin R (↑(s.attach.biUnion sf ∪ s ∪ Finset.image (⇑l : (a : (↑(↑s : Set S) : Type u_2)) → S) l.support) : Set S))
    0

Tactic:
exact zero_mem _

Premises used: ZeroMemClass.zero_mem
-- 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
i : (↑(↑s : Set S) : Type u_2)
h : ¬Eq (α := S) ((l : (a : (↑(↑s : Set S) : Type u_2)) → S) i : S) (0 : S)
neg :
  Membership.mem (α := S)
    (↑(s.attach.biUnion sf ∪ s ∪ Finset.image (⇑l : (a : (↑(↑s : Set S) : Type u_2)) → S) l.support) : Set S)
    ((l : (a : (↑(↑s : Set S) : Type u_2)) → S) i : S)
⊢ Membership.mem (α := S) (γ := Subalgebra R S)
    (adjoin R (↑(s.attach.biUnion sf ∪ s ∪ Finset.image (⇑l : (a : (↑(↑s : Set S) : Type u_2)) → S) l.support) : Set S))
    ((l : (a : (↑(↑s : Set S) : Type u_2)) → S) i : 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
i : (↑(↑s : Set S) : Type u_2)
h : ¬Eq (α := S) ((l : (a : (↑(↑s : Set S) : Type u_2)) → S) i : S) (0 : S)
neg :
  Membership.mem (α := S)
    ((↑(s.attach.biUnion sf ∪ s) : Set S) ∪
      (⇑l : (a : (↑(↑s : Set S) : Type u_2)) → S) '' (↑l.support : Set (↑(↑s : Set S) : Type u_2)))
    ((l : (a : (↑(↑s : Set S) : Type u_2)) → S) i : S)
⊢ Membership.mem (α := S)
    (↑(s.attach.biUnion sf ∪ s ∪ Finset.image (⇑l : (a : (↑(↑s : Set S) : Type u_2)) → S) l.support) : Set S)
    ((l : (a : (↑(↑s : Set S) : Type u_2)) → S) i : S)

Tactic:
rw [Finset.coe_union, Finset.coe_image]

Premises used: Finset.coe_image, Finset.coe_union
-- 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
i : (↑(↑s : Set S) : Type u_2)
h : ¬Eq (α := S) ((l : (a : (↑(↑s : Set S) : Type u_2)) → S) i : S) (0 : S)
⊢ Membership.mem (α := S)
    ((↑(s.attach.biUnion sf ∪ s) : Set S) ∪
      (⇑l : (a : (↑(↑s : Set S) : Type u_2)) → S) '' (↑l.support : Set (↑(↑s : Set S) : Type u_2)))
    ((l : (a : (↑(↑s : Set S) : Type u_2)) → S) i : S)

Tactic:
Or.inr (Set.mem_image_of_mem _ (Finsupp.mem_support_iff.mpr h))

Premises used: Iff.mpr, Finsupp.mem_support_iff, Set.union, Set.Mem, setOf, Set.mem_image_of_mem, Or.inr
-- 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
i : (↑(↑s : Set S) : Type u_2)
h : ¬Eq (α := S) ((l : (a : (↑(↑s : Set S) : Type u_2)) → S) i : S) (0 : S)
⊢ Membership.mem (α := S)
    ((↑(s.attach.biUnion sf ∪ s) : Set S) ∪
      (⇑l : (a : (↑(↑s : Set S) : Type u_2)) → S) '' (↑l.support : Set (↑(↑s : Set S) : Type u_2)))
    ((l : (a : (↑(↑s : Set S) : Type u_2)) → S) i : S)

Tactic:
exact Or.inr (Set.mem_image_of_mem _ (Finsupp.mem_support_iff.mpr h))

Premises used: Iff.mpr, Finsupp.mem_support_iff, Set.mem_image_of_mem, Or.inr
-- 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 :
  ∃ (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)
⊢ ∃ (n : ℕ),
    Membership.mem (γ := Subalgebra R S)
      (adjoin R
        (↑(s.attach.biUnion sf ∪ s ∪ Finset.image (⇑l : (a : (↑(↑s : Set S) : Type u_2)) → S) l.support) : Set S))
      ((↑r : S) ^ n • x)

Tactic:
rw [Finset.coe_union, Finset.coe_union, Finset.coe_biUnion]

Premises used: Finset.coe_biUnion, Finset.coe_union
-- 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)
x_1 : Set S
⊢ (∃ (n : ℕ), Membership.mem (γ := Subalgebra R S) (adjoin R x_1) ((↑r : S) ^ n • x)) ↔
    ∃ (m : ↥(Submonoid.powers (↑r : S))), Membership.mem (γ := Subalgebra R S) (adjoin R x_1) ((↑m : S) • x)

Tactic:
simp [Submonoid.mem_powers_iff]

Premises used: Submonoid.mem_powers_iff