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)
⊢ FiniteType R S
have 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)) ⊤
Tactic: use s.attach.biUnion sf ∪ s ∪ l.support.image l
-- 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)
⊢ 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))
    ⊤
have 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))
Tactic: rw [_root_.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 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
⊢ 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
have 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)
Tactic: apply Subalgebra.mem_of_span_eq_top_of_smul_pow_mem _ (s : Set S) l hl _ _ x _
-- 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
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)
⊢ 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
have 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)
Tactic: apply Subalgebra.mem_of_span_eq_top_of_smul_pow_mem _ (s : Set S) l hl _ _ x _
-- 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
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)
⊢ 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
have 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)
Tactic: apply Subalgebra.mem_of_span_eq_top_of_smul_pow_mem _ (s : Set S) l hl _ _ x _
-- 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 x : S
hx : x ∈ (↑s : 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)
have a : x ∈ (↑(s.attach.biUnion sf ∪ 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_1 x : S
hx : x ∈ (↑s : Set S)
⊢ x ∈ (↑(s.attach.biUnion sf ∪ s ∪ Finset.image (⇑l : (a : (↑(↑s : Set S) : Type u_2)) → S) l.support) : Set S)
have 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)
Tactic: rw [Finset.coe_union, Finset.coe_union]
-- 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
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)
have 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)
Tactic: by_cases h : l i = 0
-- 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
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)
⊢ 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)
have 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)
Tactic: by_cases h : l i = 0
-- 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
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) (γ := 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)
have 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
Tactic: rw [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 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) (γ := 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)
have 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)
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
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 ∪ 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)
have 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)
Tactic: rw [Finset.coe_union, Finset.coe_image]
-- 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)
⊢ ∃ (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)
have 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)
Tactic: rw [Finset.coe_union, Finset.coe_union, Finset.coe_biUnion]
-- 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)
⊢ ∃ (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)
have 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)
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] }]
-- 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)
⊢ ∃ (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_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)
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 : 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)
⊢ ∃ (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_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)))))
Tactic: refine IsLocalization.exists_smul_mem_of_mem_adjoin
      (Submonoid.powers (r : S)) x (t r) (Algebra.adjoin R _) ?_ ?_ ?_