awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
s : Set R
span_eq : Eq (α := Ideal R) (Ideal.span s) ⊤
x y : R
eq :
  Eq (α := (a : (↑s : Type u_1)) → Away (↑a : R))
    ((algebraMap R ((a : (↑s : Type u_1)) → Away (↑a : R)) : (a : R) → (a : (↑s : Type u_1)) → Away (↑a : R)) x :
      (a : (↑s : Type u_1)) → Away (↑a : R))
    ((algebraMap R ((a : (↑s : Type u_1)) → Away (↑a : R)) : (a : R) → (a : (↑s : Type u_1)) → Away (↑a : R)) y :
      (a : (↑s : Type u_1)) → Away (↑a : R))
ne : ¬Eq (α := Ideal R) (Module.eqIdeal R x y) ⊤
r_1 : R
hrs : r_1 ∈ s
disj : Disjoint (↑(Module.eqIdeal R x y) : Set R) (↑(Submonoid.powers r_1) : Set R)
r : (↑s : Type u_1) := Subtype.mk (p := fun (x : R) ↦ x ∈ s) r_1 hrs
⊢ False
have have : ∀ (n : ℕ)
  (eq :
    (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers (↑r : R)) x)
              ((fun (x : ℕ) ↦ (↑r : R) ^ x) n) sorry) :
          R) *
        x =
      (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers (↑r : R)) x)
              ((fun (x : ℕ) ↦ (↑r : R) ^ x) n) sorry) :
          R) *
        y),
  False
Tactic: have ⟨⟨_, n, rfl⟩, eq⟩ := (IsLocalization.eq_iff_exists (.powers r.1) _).mp (congr_fun eq r)
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
s : Set R
span_eq : Eq (α := Ideal R) (Ideal.span s) ⊤
f : (a : (↑s : Type u_1)) → Away (↑a : R)
h :
  ∀ (a b : (↑s : Type u_1)),
    Eq (α := Away ((↑a : R) * (↑b : R)))
      ((Away.awayToAwayRight (↑a : R) (↑b : R) : (a_1 : Away (↑a : R)) → Away ((↑a : R) * (↑b : R))) (f a) :
        Away ((↑a : R) * (↑b : R)))
      ((Away.awayToAwayLeft (↑b : R) (↑a : R) : (a_1 : Away (↑b : R)) → Away ((↑a : R) * (↑b : R))) (f b) :
        Away ((↑a : R) * (↑b : R)))
⊢ ∃! r : R, ∀ (a : (↑s : Type u_1)), (algebraMap R (Away (↑a : R)) : (a_1 : R) → Away (↑a : R)) r = f a
have mem : Membership.mem (γ := Ideal R) (Ideal.span s) 1
Tactic: have mem := (Ideal.eq_top_iff_one _).mp span_eq
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
s : Set R
f : (a : (↑s : Type u_1)) → Away (↑a : R)
h :
  ∀ (a b : (↑s : Type u_1)),
    Eq (α := Away ((↑a : R) * (↑b : R)))
      ((Away.awayToAwayRight (↑a : R) (↑b : R) : (a_1 : Away (↑a : R)) → Away ((↑a : R) * (↑b : R))) (f a) :
        Away ((↑a : R) * (↑b : R)))
      ((Away.awayToAwayLeft (↑b : R) (↑a : R) : (a_1 : Away (↑b : R)) → Away ((↑a : R) * (↑b : R))) (f b) :
        Away ((↑a : R) * (↑b : R)))
mem : Membership.mem (γ := Ideal R) (Ideal.span s) 1
⊢ ∃! r : R, ∀ (a : (↑s : Type u_1)), (algebraMap R (Away (↑a : R)) : (a_1 : R) → Away (↑a : R)) r = f a
have inr : ∀
  (this :
    ∀ (s : Set R) (f : (a : (↑s : Type u_1)) → Away (↑a : R))
      (h :
        ∀ (a b : (↑s : Type u_1)),
          Eq (α := Away ((↑a : R) * (↑b : R)))
            ((Away.awayToAwayRight (↑a : R) (↑b : R) : (a_1 : Away (↑a : R)) → Away ((↑a : R) * (↑b : R))) (f a) :
              Away ((↑a : R) * (↑b : R)))
            ((Away.awayToAwayLeft (↑b : R) (↑a : R) : (a_1 : Away (↑b : R)) → Away ((↑a : R) * (↑b : R))) (f b) :
              Away ((↑a : R) * (↑b : R))))
      (mem : Membership.mem (γ := Ideal R) (Ideal.span s) 1) (finset_eq : ∃ (t : Finset R), (↑t : Set R) = s),
      ∃! r : R, ∀ (a : (↑s : Type u_1)), (algebraMap R (Away (↑a : R)) : (a_1 : R) → Away (↑a : R)) r = f a)
  (finset_eq : ¬∃ (t : Finset R), (↑t : Set R) = s),
  ∃! r : R, ∀ (a : (↑s : Type u_1)), (algebraMap R (Away (↑a : R)) : (a_1 : R) → Away (↑a : R)) r = f a
Tactic: wlog finset_eq : ∃ t : Finset R, t = s generalizing s
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
s : Set R
f : (a : (↑s : Type u_1)) → Away (↑a : R)
h :
  ∀ (a b : (↑s : Type u_1)),
    Eq (α := Away ((↑a : R) * (↑b : R)))
      ((Away.awayToAwayRight (↑a : R) (↑b : R) : (a_1 : Away (↑a : R)) → Away ((↑a : R) * (↑b : R))) (f a) :
        Away ((↑a : R) * (↑b : R)))
      ((Away.awayToAwayLeft (↑b : R) (↑a : R) : (a_1 : Away (↑b : R)) → Away ((↑a : R) * (↑b : R))) (f b) :
        Away ((↑a : R) * (↑b : R)))
mem : Membership.mem (γ := Ideal R) (Ideal.span s) 1
inr :
  ∀
    (this :
      ∀ (s : Set R) (f : (a : (↑s : Type u_1)) → Away (↑a : R))
        (h :
          ∀ (a b : (↑s : Type u_1)),
            Eq (α := Away ((↑a : R) * (↑b : R)))
              ((Away.awayToAwayRight (↑a : R) (↑b : R) : (a_1 : Away (↑a : R)) → Away ((↑a : R) * (↑b : R))) (f a) :
                Away ((↑a : R) * (↑b : R)))
              ((Away.awayToAwayLeft (↑b : R) (↑a : R) : (a_1 : Away (↑b : R)) → Away ((↑a : R) * (↑b : R))) (f b) :
                Away ((↑a : R) * (↑b : R))))
        (mem : Membership.mem (γ := Ideal R) (Ideal.span s) 1) (finset_eq : ∃ (t : Finset R), (↑t : Set R) = s),
        ∃! r : R, ∀ (a : (↑s : Type u_1)), (algebraMap R (Away (↑a : R)) : (a_1 : R) → Away (↑a : R)) r = f a)
    (finset_eq : ¬∃ (t : Finset R), (↑t : Set R) = s),
    ∃! r : R, ∀ (a : (↑s : Type u_1)), (algebraMap R (Away (↑a : R)) : (a_1 : R) → Away (↑a : R)) r = f a
⊢ ∃! r : R, ∀ (a : (↑s : Type u_1)), (algebraMap R (Away (↑a : R)) : (a_1 : R) → Away (↑a : R)) r = f a
have wlog : ∀ (s : Set R) (f : (a : (↑s : Type u_1)) → Away (↑a : R))
  (h :
    ∀ (a b : (↑s : Type u_1)),
      Eq (α := Away ((↑a : R) * (↑b : R)))
        ((Away.awayToAwayRight (↑a : R) (↑b : R) : (a_1 : Away (↑a : R)) → Away ((↑a : R) * (↑b : R))) (f a) :
          Away ((↑a : R) * (↑b : R)))
        ((Away.awayToAwayLeft (↑b : R) (↑a : R) : (a_1 : Away (↑b : R)) → Away ((↑a : R) * (↑b : R))) (f b) :
          Away ((↑a : R) * (↑b : R))))
  (mem : Membership.mem (γ := Ideal R) (Ideal.span s) 1) (finset_eq : ∃ (t : Finset R), (↑t : Set R) = s),
  ∃! r : R, ∀ (a : (↑s : Type u_1)), (algebraMap R (Away (↑a : R)) : (a_1 : R) → Away (↑a : R)) r = f a
Tactic: wlog finset_eq : ∃ t : Finset R, t = s generalizing s
Cleared hypotheses: s, f, h, mem
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
s : Set R
f : (a : (↑s : Type u_1)) → Away (↑a : R)
h :
  ∀ (a b : (↑s : Type u_1)),
    Eq (α := Away ((↑a : R) * (↑b : R)))
      ((Away.awayToAwayRight (↑a : R) (↑b : R) : (a_1 : Away (↑a : R)) → Away ((↑a : R) * (↑b : R))) (f a) :
        Away ((↑a : R) * (↑b : R)))
      ((Away.awayToAwayLeft (↑b : R) (↑a : R) : (a_1 : Away (↑b : R)) → Away ((↑a : R) * (↑b : R))) (f b) :
        Away ((↑a : R) * (↑b : R)))
mem : Membership.mem (γ := Ideal R) (Ideal.span s) 1
this :
  ∀ (s : Set R) (f : (a : (↑s : Type u_1)) → Away (↑a : R))
    (h :
      ∀ (a b : (↑s : Type u_1)),
        Eq (α := Away ((↑a : R) * (↑b : R)))
          ((Away.awayToAwayRight (↑a : R) (↑b : R) : (a_1 : Away (↑a : R)) → Away ((↑a : R) * (↑b : R))) (f a) :
            Away ((↑a : R) * (↑b : R)))
          ((Away.awayToAwayLeft (↑b : R) (↑a : R) : (a_1 : Away (↑b : R)) → Away ((↑a : R) * (↑b : R))) (f b) :
            Away ((↑a : R) * (↑b : R))))
    (mem : Membership.mem (γ := Ideal R) (Ideal.span s) 1) (finset_eq : ∃ (t : Finset R), (↑t : Set R) = s),
    ∃! r : R, ∀ (a : (↑s : Type u_1)), (algebraMap R (Away (↑a : R)) : (a_1 : R) → Away (↑a : R)) r = f a
finset_eq : ¬∃ (t : Finset R), (↑t : Set R) = s
⊢ ∃! r : R, ∀ (a : (↑s : Type u_1)), (algebraMap R (Away (↑a : R)) : (a_1 : R) → Away (↑a : R)) r = f a
have inr : ∀ (t : Finset R) (hts : (↑t : Set R) ⊆ s) (mem : Membership.mem (γ := Submodule R R) (Submodule.span R (↑t : Set R)) 1),
  ∃! r : R, ∀ (a : (↑s : Type u_1)), (algebraMap R (Away (↑a : R)) : (a_1 : R) → Away (↑a : R)) r = f a
Tactic: have ⟨t, hts, mem⟩ := Submodule.mem_span_finite_of_mem_span mem
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
s : Set R
f : (a : (↑s : Type u_1)) → Away (↑a : R)
h :
  ∀ (a b : (↑s : Type u_1)),
    Eq (α := Away ((↑a : R) * (↑b : R)))
      ((Away.awayToAwayRight (↑a : R) (↑b : R) : (a_1 : Away (↑a : R)) → Away ((↑a : R) * (↑b : R))) (f a) :
        Away ((↑a : R) * (↑b : R)))
      ((Away.awayToAwayLeft (↑b : R) (↑a : R) : (a_1 : Away (↑b : R)) → Away ((↑a : R) * (↑b : R))) (f b) :
        Away ((↑a : R) * (↑b : R)))
mem_1 : Membership.mem (γ := Ideal R) (Ideal.span s) 1
this :
  ∀ (s : Set R) (f : (a : (↑s : Type u_1)) → Away (↑a : R))
    (h :
      ∀ (a b : (↑s : Type u_1)),
        Eq (α := Away ((↑a : R) * (↑b : R)))
          ((Away.awayToAwayRight (↑a : R) (↑b : R) : (a_1 : Away (↑a : R)) → Away ((↑a : R) * (↑b : R))) (f a) :
            Away ((↑a : R) * (↑b : R)))
          ((Away.awayToAwayLeft (↑b : R) (↑a : R) : (a_1 : Away (↑b : R)) → Away ((↑a : R) * (↑b : R))) (f b) :
            Away ((↑a : R) * (↑b : R))))
    (mem : Membership.mem (γ := Ideal R) (Ideal.span s) 1) (finset_eq : ∃ (t : Finset R), (↑t : Set R) = s),
    ∃! r : R, ∀ (a : (↑s : Type u_1)), (algebraMap R (Away (↑a : R)) : (a_1 : R) → Away (↑a : R)) r = f a
finset_eq : ¬∃ (t : Finset R), (↑t : Set R) = s
t : Finset R
hts : (↑t : Set R) ⊆ s
mem : Membership.mem (γ := Submodule R R) (Submodule.span R (↑t : Set R)) 1
⊢ ∃! r : R, ∀ (a : (↑s : Type u_1)), (algebraMap R (Away (↑a : R)) : (a_1 : R) → Away (↑a : R)) r = f a
have inr : ∀ (r : R)
  (eq :
    ∀ (a : (↑(↑t : Set R) : Type u_1)),
      Eq (α := Away (↑a : R)) ((algebraMap R (Away (↑a : R)) : (a_1 : R) → Away (↑a : R)) r : Away (↑a : R))
        (f (Subtype.mk (p := fun (x : R) ↦ x ∈ s) (↑a : R) sorry) :
          Away (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ s) (↑a : R) sorry) : R)))
  (uniq :
    ∀ (y : R),
      (fun (r : R) ↦
            ∀ (a : (↑(↑t : Set R) : Type u_1)),
              Eq (α := Away (↑a : R)) ((algebraMap R (Away (↑a : R)) : (a_1 : R) → Away (↑a : R)) r : Away (↑a : R))
                (f (Subtype.mk (p := fun (x : R) ↦ x ∈ s) (↑a : R) sorry) :
                  Away (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ s) (↑a : R) sorry) : R)))
          y →
        y = r),
  ∃! r : R, ∀ (a : (↑s : Type u_1)), (algebraMap R (Away (↑a : R)) : (a_1 : R) → Away (↑a : R)) r = f a
Tactic: have ⟨r, eq, uniq⟩ := this t (fun a ↦ f ⟨a, hts a.2⟩)
      (fun a b ↦ h ⟨a, hts a.2⟩ ⟨b, hts b.2⟩) mem ⟨_, rfl⟩
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
s : Set R
f : (a : (↑s : Type u_1)) → Away (↑a : R)
h :
  ∀ (a b : (↑s : Type u_1)),
    Eq (α := Away ((↑a : R) * (↑b : R)))
      ((Away.awayToAwayRight (↑a : R) (↑b : R) : (a_1 : Away (↑a : R)) → Away ((↑a : R) * (↑b : R))) (f a) :
        Away ((↑a : R) * (↑b : R)))
      ((Away.awayToAwayLeft (↑b : R) (↑a : R) : (a_1 : Away (↑b : R)) → Away ((↑a : R) * (↑b : R))) (f b) :
        Away ((↑a : R) * (↑b : R)))
mem_1 : Membership.mem (γ := Ideal R) (Ideal.span s) 1
this :
  ∀ (s : Set R) (f : (a : (↑s : Type u_1)) → Away (↑a : R))
    (h :
      ∀ (a b : (↑s : Type u_1)),
        Eq (α := Away ((↑a : R) * (↑b : R)))
          ((Away.awayToAwayRight (↑a : R) (↑b : R) : (a_1 : Away (↑a : R)) → Away ((↑a : R) * (↑b : R))) (f a) :
            Away ((↑a : R) * (↑b : R)))
          ((Away.awayToAwayLeft (↑b : R) (↑a : R) : (a_1 : Away (↑b : R)) → Away ((↑a : R) * (↑b : R))) (f b) :
            Away ((↑a : R) * (↑b : R))))
    (mem : Membership.mem (γ := Ideal R) (Ideal.span s) 1) (finset_eq : ∃ (t : Finset R), (↑t : Set R) = s),
    ∃! r : R, ∀ (a : (↑s : Type u_1)), (algebraMap R (Away (↑a : R)) : (a_1 : R) → Away (↑a : R)) r = f a
finset_eq : ¬∃ (t : Finset R), (↑t : Set R) = s
t : Finset R
hts : (↑t : Set R) ⊆ s
mem : Membership.mem (γ := Submodule R R) (Submodule.span R (↑t : Set R)) 1
r : R
eq :
  (fun (r : R) ↦
      ∀ (a : (↑(↑t : Set R) : Type u_1)),
        Eq (α := Away (↑a : R)) ((algebraMap R (Away (↑a : R)) : (a_1 : R) → Away (↑a : R)) r : Away (↑a : R))
          (f (Subtype.mk (p := fun (x : R) ↦ x ∈ s) (↑a : R) ⋯) :
            Away (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ s) (↑a : R) ⋯) : R)))
    r
uniq :
  ∀ (y : R),
    (fun (r : R) ↦
          ∀ (a : (↑(↑t : Set R) : Type u_1)),
            Eq (α := Away (↑a : R)) ((algebraMap R (Away (↑a : R)) : (a_1 : R) → Away (↑a : R)) r : Away (↑a : R))
              (f (Subtype.mk (p := fun (x : R) ↦ x ∈ s) (↑a : R) ⋯) :
                Away (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ s) (↑a : R) ⋯) : R)))
        y →
      y = r
⊢ ∃! r : R, ∀ (a : (↑s : Type u_1)), (algebraMap R (Away (↑a : R)) : (a_1 : R) → Away (↑a : R)) r = f a
have inr : ∀ (a : (↑s : Type u_1)), (algebraMap R (Away (↑a : R)) : (a_1 : R) → Away (↑a : R)) r = f a
Tactic: refine ⟨r, fun a ↦ ?_, fun _ eq ↦ uniq _ fun a ↦ eq ⟨a, hts a.2⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
s : Set R
f : (a : (↑s : Type u_1)) → Away (↑a : R)
h :
  ∀ (a b : (↑s : Type u_1)),
    Eq (α := Away ((↑a : R) * (↑b : R)))
      ((Away.awayToAwayRight (↑a : R) (↑b : R) : (a_1 : Away (↑a : R)) → Away ((↑a : R) * (↑b : R))) (f a) :
        Away ((↑a : R) * (↑b : R)))
      ((Away.awayToAwayLeft (↑b : R) (↑a : R) : (a_1 : Away (↑b : R)) → Away ((↑a : R) * (↑b : R))) (f b) :
        Away ((↑a : R) * (↑b : R)))
mem_1 : Membership.mem (γ := Ideal R) (Ideal.span s) 1
this :
  ∀ (s : Set R) (f : (a : (↑s : Type u_1)) → Away (↑a : R))
    (h :
      ∀ (a b : (↑s : Type u_1)),
        Eq (α := Away ((↑a : R) * (↑b : R)))
          ((Away.awayToAwayRight (↑a : R) (↑b : R) : (a_1 : Away (↑a : R)) → Away ((↑a : R) * (↑b : R))) (f a) :
            Away ((↑a : R) * (↑b : R)))
          ((Away.awayToAwayLeft (↑b : R) (↑a : R) : (a_1 : Away (↑b : R)) → Away ((↑a : R) * (↑b : R))) (f b) :
            Away ((↑a : R) * (↑b : R))))
    (mem : Membership.mem (γ := Ideal R) (Ideal.span s) 1) (finset_eq : ∃ (t : Finset R), (↑t : Set R) = s),
    ∃! r : R, ∀ (a : (↑s : Type u_1)), (algebraMap R (Away (↑a : R)) : (a_1 : R) → Away (↑a : R)) r = f a
finset_eq : ¬∃ (t : Finset R), (↑t : Set R) = s
t : Finset R
hts : (↑t : Set R) ⊆ s
mem : Membership.mem (γ := Submodule R R) (Submodule.span R (↑t : Set R)) 1
r : R
eq :
  (fun (r : R) ↦
      ∀ (a : (↑(↑t : Set R) : Type u_1)),
        Eq (α := Away (↑a : R)) ((algebraMap R (Away (↑a : R)) : (a_1 : R) → Away (↑a : R)) r : Away (↑a : R))
          (f (Subtype.mk (p := fun (x : R) ↦ x ∈ s) (↑a : R) ⋯) :
            Away (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ s) (↑a : R) ⋯) : R)))
    r
uniq :
  ∀ (y : R),
    (fun (r : R) ↦
          ∀ (a : (↑(↑t : Set R) : Type u_1)),
            Eq (α := Away (↑a : R)) ((algebraMap R (Away (↑a : R)) : (a_1 : R) → Away (↑a : R)) r : Away (↑a : R))
              (f (Subtype.mk (p := fun (x : R) ↦ x ∈ s) (↑a : R) ⋯) :
                Away (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ s) (↑a : R) ⋯) : R)))
        y →
      y = r
a : (↑s : Type u_1)
⊢ (algebraMap R (Away (↑a : R)) : (a_1 : R) → Away (↑a : R)) r = f a
have hts₁ : insert (↑a : R) (↑t : Set R) ⊆ s
Tactic: replace hts := Set.insert_subset a.2 hts
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
s : Set R
f : (a : (↑s : Type u_1)) → Away (↑a : R)
h :
  ∀ (a b : (↑s : Type u_1)),
    Eq (α := Away ((↑a : R) * (↑b : R)))
      ((Away.awayToAwayRight (↑a : R) (↑b : R) : (a_1 : Away (↑a : R)) → Away ((↑a : R) * (↑b : R))) (f a) :
        Away ((↑a : R) * (↑b : R)))
      ((Away.awayToAwayLeft (↑b : R) (↑a : R) : (a_1 : Away (↑b : R)) → Away ((↑a : R) * (↑b : R))) (f b) :
        Away ((↑a : R) * (↑b : R)))
mem : Membership.mem (γ := Ideal R) (Ideal.span s) 1
finset_eq : ∃ (t : Finset R), (↑t : Set R) = s
⊢ ∃! r : R, ∀ (a : (↑s : Type u_1)), (algebraMap R (Away (↑a : R)) : (a_1 : R) → Away (↑a : R)) r = f a
have span_eq : Eq (α := Ideal R) (Ideal.span s) ⊤
Tactic: have span_eq := (Ideal.eq_top_iff_one _).mpr mem
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
s : Set R
f : (a : (↑s : Type u_1)) → Away (↑a : R)
h :
  ∀ (a b : (↑s : Type u_1)),
    Eq (α := Away ((↑a : R) * (↑b : R)))
      ((Away.awayToAwayRight (↑a : R) (↑b : R) : (a_1 : Away (↑a : R)) → Away ((↑a : R) * (↑b : R))) (f a) :
        Away ((↑a : R) * (↑b : R)))
      ((Away.awayToAwayLeft (↑b : R) (↑a : R) : (a_1 : Away (↑b : R)) → Away ((↑a : R) * (↑b : R))) (f b) :
        Away ((↑a : R) * (↑b : R)))
mem : Membership.mem (γ := Ideal R) (Ideal.span s) 1
finset_eq : ∃ (t : Finset R), (↑t : Set R) = s
span_eq : Eq (α := Ideal R) (Ideal.span s) ⊤
⊢ ∃! r : R, ∀ (a : (↑s : Type u_1)), (algebraMap R (Away (↑a : R)) : (a_1 : R) → Away (↑a : R)) r = f a
have refine : ∃ (x : R), ∀ (a : (↑s : Type u_1)), (algebraMap R (Away (↑a : R)) : (a_1 : R) → Away (↑a : R)) x = f a
Tactic: refine existsUnique_of_exists_of_unique ?_ fun x y hx hy ↦
    algebraMap_injective_of_span_eq_top s span_eq (funext fun a ↦ (hx a).trans (hy a).symm)
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
s : Set R
f : (a : (↑s : Type u_1)) → Away (↑a : R)
h :
  ∀ (a b : (↑s : Type u_1)),
    Eq (α := Away ((↑a : R) * (↑b : R)))
      ((Away.awayToAwayRight (↑a : R) (↑b : R) : (a_1 : Away (↑a : R)) → Away ((↑a : R) * (↑b : R))) (f a) :
        Away ((↑a : R) * (↑b : R)))
      ((Away.awayToAwayLeft (↑b : R) (↑a : R) : (a_1 : Away (↑b : R)) → Away ((↑a : R) * (↑b : R))) (f b) :
        Away ((↑a : R) * (↑b : R)))
mem : Membership.mem (γ := Ideal R) (Ideal.span s) 1
finset_eq : ∃ (t : Finset R), (↑t : Set R) = s
span_eq : Eq (α := Ideal R) (Ideal.span s) ⊤
⊢ ∃ (x : R), ∀ (a : (↑s : Type u_1)), (algebraMap R (Away (↑a : R)) : (a_1 : R) → Away (↑a : R)) x = f a
have obtain : ∀ (s : Finset R) (f : (a : (↑(↑s : Set R) : Type u_1)) → Away (↑a : R))
  (h :
    ∀ (a b : (↑(↑s : Set R) : Type u_1)),
      Eq (α := Away ((↑a : R) * (↑b : R)))
        ((Away.awayToAwayRight (↑a : R) (↑b : R) : (a_1 : Away (↑a : R)) → Away ((↑a : R) * (↑b : R))) (f a) :
          Away ((↑a : R) * (↑b : R)))
        ((Away.awayToAwayLeft (↑b : R) (↑a : R) : (a_1 : Away (↑b : R)) → Away ((↑a : R) * (↑b : R))) (f b) :
          Away ((↑a : R) * (↑b : R))))
  (mem : Membership.mem (γ := Ideal R) (Ideal.span (↑s : Set R)) 1)
  (span_eq : Eq (α := Ideal R) (Ideal.span (↑s : Set R)) ⊤),
  ∃ (x : R), ∀ (a : (↑(↑s : Set R) : Type u_1)), (algebraMap R (Away (↑a : R)) : (a_1 : R) → Away (↑a : R)) x = f a
Tactic: obtain ⟨s, rfl⟩ := finset_eq
Cleared hypotheses: s, f, h, mem, finset_eq, span_eq
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
s : Finset R
f : (a : (↑(↑s : Set R) : Type u_1)) → Away (↑a : R)
h :
  ∀ (a b : (↑(↑s : Set R) : Type u_1)),
    Eq (α := Away ((↑a : R) * (↑b : R)))
      ((Away.awayToAwayRight (↑a : R) (↑b : R) : (a_1 : Away (↑a : R)) → Away ((↑a : R) * (↑b : R))) (f a) :
        Away ((↑a : R) * (↑b : R)))
      ((Away.awayToAwayLeft (↑b : R) (↑a : R) : (a_1 : Away (↑b : R)) → Away ((↑a : R) * (↑b : R))) (f b) :
        Away ((↑a : R) * (↑b : R)))
mem : Membership.mem (γ := Ideal R) (Ideal.span (↑s : Set R)) 1
span_eq : Eq (α := Ideal R) (Ideal.span (↑s : Set R)) ⊤
⊢ ∃ (x : R), ∀ (a : (↑(↑s : Set R) : Type u_1)), (algebraMap R (Away (↑a : R)) : (a_1 : R) → Away (↑a : R)) x = f a
have choose : ∀ (n : (a : (↑(↑s : Set R) : Type u_1)) → ℕ) (r : (a : (↑(↑s : Set R) : Type u_1)) → R)
  (eq :
    ∀ (a : (↑(↑s : Set R) : Type u_1)),
      f a * HPow.hPow (α := Away (↑a : R)) ((algebraMap R (Away (↑a : R)) : (a_1 : R) → Away (↑a : R)) (↑a : R)) (n a) =
        (algebraMap R (Away (↑a : R)) : (a_1 : R) → Away (↑a : R)) (r a)),
  ∃ (x : R), ∀ (a : (↑(↑s : Set R) : Type u_1)), (algebraMap R (Away (↑a : R)) : (a_1 : R) → Away (↑a : R)) x = f a
Tactic: choose n r eq using fun a ↦ Away.surj a.1 (f a)
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
s : Finset R
f : (a : (↑(↑s : Set R) : Type u_1)) → Away (↑a : R)
h :
  ∀ (a b : (↑(↑s : Set R) : Type u_1)),
    Eq (α := Away ((↑a : R) * (↑b : R)))
      ((Away.awayToAwayRight (↑a : R) (↑b : R) : (a_1 : Away (↑a : R)) → Away ((↑a : R) * (↑b : R))) (f a) :
        Away ((↑a : R) * (↑b : R)))
      ((Away.awayToAwayLeft (↑b : R) (↑a : R) : (a_1 : Away (↑b : R)) → Away ((↑a : R) * (↑b : R))) (f b) :
        Away ((↑a : R) * (↑b : R)))
mem : Membership.mem (γ := Ideal R) (Ideal.span (↑s : Set R)) 1
span_eq : Eq (α := Ideal R) (Ideal.span (↑s : Set R)) ⊤
n : (a : (↑(↑s : Set R) : Type u_1)) → ℕ
r_1 : (a : (↑(↑s : Set R) : Type u_1)) → R
eq :
  ∀ (a : (↑(↑s : Set R) : Type u_1)),
    f a * HPow.hPow (α := Away (↑a : R)) ((algebraMap R (Away (↑a : R)) : (a_1 : R) → Away (↑a : R)) (↑a : R)) (n a) =
      (algebraMap R (Away (↑a : R)) : (a_1 : R) → Away (↑a : R)) (r_1 a)
N : ℕ := s.attach.sup n
r : (a : (↑(↑s : Set R) : Type u_1)) → R := fun (a : (↑(↑s : Set R) : Type u_1)) ↦ (↑a : R) ^ (N - n a) * r_1 a
a : (↑(↑s : Set R) : Type u_1)
⊢ HMul.hMul (β := Away (↑a : R)) (f a)
      ((algebraMap R (Away (↑a : R)) : (a_1 : R) → Away (↑a : R)) ((↑a : R) ^ N) : Away (↑a : R)) =
    (algebraMap R (Away (↑a : R)) : (a_1 : R) → Away (↑a : R)) (r a)
have rw : HMul.hMul (β := Away (↑a : R)) (f a)
    ((algebraMap R (Away (↑a : R)) : (a_1 : R) → Away (↑a : R)) ((↑a : R) ^ N) : Away (↑a : R)) =
  HMul.hMul (α := Away (↑a : R)) (β := Away (↑a : R))
    ((algebraMap R (Away (↑a : R)) : (a_1 : R) → Away (↑a : R)) ((↑a : R) ^ (N - n a)) : Away (↑a : R))
    ((algebraMap R (Away (↑a : R)) : (a_1 : R) → Away (↑a : R)) (r_1 a) : Away (↑a : R))
Tactic: rw [map_mul, ← eq, mul_left_comm, ← map_pow, ← map_mul, ← pow_add,
      Nat.sub_add_cancel (Finset.le_sup <| s.mem_attach a)]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
s : Finset R
f : (a : (↑(↑s : Set R) : Type u_1)) → Away (↑a : R)
h :
  ∀ (a b : (↑(↑s : Set R) : Type u_1)),
    Eq (α := Away ((↑a : R) * (↑b : R)))
      ((Away.awayToAwayRight (↑a : R) (↑b : R) : (a_1 : Away (↑a : R)) → Away ((↑a : R) * (↑b : R))) (f a) :
        Away ((↑a : R) * (↑b : R)))
      ((Away.awayToAwayLeft (↑b : R) (↑a : R) : (a_1 : Away (↑b : R)) → Away ((↑a : R) * (↑b : R))) (f b) :
        Away ((↑a : R) * (↑b : R)))
mem : Membership.mem (γ := Ideal R) (Ideal.span (↑s : Set R)) 1
span_eq : Eq (α := Ideal R) (Ideal.span (↑s : Set R)) ⊤
n : (a : (↑(↑s : Set R) : Type u_1)) → ℕ
r_1 : (a : (↑(↑s : Set R) : Type u_1)) → R
eq :
  ∀ (a : (↑(↑s : Set R) : Type u_1)),
    f a * HPow.hPow (α := Away (↑a : R)) ((algebraMap R (Away (↑a : R)) : (a_1 : R) → Away (↑a : R)) (↑a : R)) (n a) =
      (algebraMap R (Away (↑a : R)) : (a_1 : R) → Away (↑a : R)) (r_1 a)
N : ℕ := s.attach.sup n
r : (a : (↑(↑s : Set R) : Type u_1)) → R := fun (a : (↑(↑s : Set R) : Type u_1)) ↦ (↑a : R) ^ (N - n a) * r_1 a
a : (↑(↑s : Set R) : Type u_1)
rw :
  HMul.hMul (β := Away (↑a : R)) (f a)
      ((algebraMap R (Away (↑a : R)) : (a_1 : R) → Away (↑a : R)) ((↑a : R) ^ N) : Away (↑a : R)) =
    HMul.hMul (α := Away (↑a : R)) (β := Away (↑a : R))
      ((algebraMap R (Away (↑a : R)) : (a_1 : R) → Away (↑a : R)) ((↑a : R) ^ (N - n a)) : Away (↑a : R))
      ((algebraMap R (Away (↑a : R)) : (a_1 : R) → Away (↑a : R)) (r_1 a) : Away (↑a : R))
⊢ HMul.hMul (β := Away (↑a : R)) (f a)
      ((algebraMap R (Away (↑a : R)) : (a_1 : R) → Away (↑a : R)) ((↑a : R) ^ N) : Away (↑a : R)) =
    (algebraMap R (Away (↑a : R)) : (a_1 : R) → Away (↑a : R)) (r a)
have rw₁ : HMul.hMul (β := Away (↑a : R)) (f a)
    ((algebraMap R (Away (↑a : R)) : (a_1 : R) → Away (↑a : R)) ((↑a : R) ^ N) : Away (↑a : R)) =
  HMul.hMul (α := Away (↑a : R))
    ((algebraMap R (Away (↑a : R)) : (a_1 : R) → Away (↑a : R)) ((↑a : R) ^ (N - n a)) : Away (↑a : R))
    (f a * HPow.hPow (α := Away (↑a : R)) ((algebraMap R (Away (↑a : R)) : (a_1 : R) → Away (↑a : R)) (↑a : R)) (n a))
Tactic: rw [map_mul, ← eq, mul_left_comm, ← map_pow, ← map_mul, ← pow_add,
      Nat.sub_add_cancel (Finset.le_sup <| s.mem_attach a)]