awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
f : R →+* S
a b : R
H :
  Function.Surjective.{u_1 + 1, u_2 + 1} (α := Away (a * b)) (β := Away (M := S) ((f : (a : R) → S) (a * b) : S))
    (⇑(awayMap f (a * b)) : (a_1 : Away (a * b)) → Away ((f : (a : R) → S) (a * b)))
rw :
  ∀
    (H :
      ∀ (a_1 : S),
        ∃ (b_1 : R) (m : ℕ), (f : (a : R) → S) b_1 = HPow.hPow (α := S) ((f : (a : R) → S) (a * b) : S) m * a_1)
    (a_1 : Away (M := S) ((f : (a : R) → S) a : S)),
    ∃ (b_1 : Away a) (m : ℕ),
      (awayMap f a : (a_2 : Away a) → Away ((f : (a : R) → S) a)) b_1 =
        HPow.hPow (α := Away (M := S) ((f : (a : R) → S) a : S))
            ((awayMap f a : (a_2 : Away a) → Away ((f : (a : R) → S) a))
                ((algebraMap R (Away a) : (a_2 : R) → Away a) b) :
              Away (M := S) ((f : (a : R) → S) a : S))
            m *
          a_1
⊢ Function.Surjective.{u_1 + 1, u_2 + 1} (α :=
    Away (M := Away a) ((algebraMap R (Away a) : (a_1 : R) → Away a) b : Away a)) (β :=
    Away (M := Away (M := S) ((f : (a : R) → S) a : S))
      ((awayMap f a : (a_1 : Away a) → Away ((f : (a : R) → S) a)) ((algebraMap R (Away a) : (a_1 : R) → Away a) b) :
        Away (M := S) ((f : (a : R) → S) a : S)))
    (⇑(awayMap (awayMap f a) ((algebraMap R (Away a) : (a_1 : R) → Away a) b)) :
      (a_1 : Away ((algebraMap R (Away a) : (a_1 : R) → Away a) b)) →
        Away
          ((awayMap f a : (a_2 : Away a) → Away ((f : (a : R) → S) a))
            ((algebraMap R (Away a) : (a_2 : R) → Away a) b)))

Tactic:
rw [awayMap_surjective_iff] at H ⊢

Premises used: Localization.awayMap_surjective_iff
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
f : R →+* S
a b : R
H : ∀ (a_1 : S), ∃ (b_1 : R) (m : ℕ), (f : (a : R) → S) b_1 = HPow.hPow (α := S) ((f : (a : R) → S) (a * b) : S) m * a_1
this :
  ∀ (s : S) (n : ℕ),
    ∃ (c : R) (l : ℕ) (m : ℕ) (k : ℕ),
      (f : (a : R) → S) (a ^ (k + n) * c) = HMul.hMul (α := S) ((f : (a : R) → S) (a ^ (k + l) * b ^ m) : S) s
⊢ ∀ (a_1 : Away (M := S) ((f : (a : R) → S) a : S)),
    ∃ (b_1 : Away a) (m : ℕ),
      (awayMap f a : (a_2 : Away a) → Away ((f : (a : R) → S) a)) b_1 =
        HPow.hPow (α := Away (M := S) ((f : (a : R) → S) a : S))
            ((awayMap f a : (a_2 : Away a) → Away ((f : (a : R) → S) a))
                ((algebraMap R (Away a) : (a_2 : R) → Away a) b) :
              Away (M := S) ((f : (a : R) → S) a : S))
            m *
          a_1

Tactic:
simpa [Function.Surjective, (IsLocalization.mk'_surjective (.powers (f a))).forall, ← map_pow,
      (IsLocalization.mk'_surjective (.powers a)).exists, Submonoid.mem_powers_iff, pow_add,
      Localization.awayMap, IsLocalization.Away.map, IsLocalization.map_mk', ← mul_assoc,
      IsLocalization.mk'_eq_iff_eq, ← map_mul, IsLocalization.eq_iff_exists (.powers (f a)),
      IsLocalization.mul_mk'_eq_mk'_of_mul]

Premises used: IsLocalization.map_mk', IsLocalization.mk'_surjective, Function.Surjective.forall, Function.Surjective.exists, mul_assoc, pow_add, map_pow, IsLocalization.mk'_eq_iff_eq, map_mul, IsLocalization.Away.map, Submonoid.powers, Localization.awayMap, Submonoid.mem_powers_iff, IsLocalization.mul_mk'_eq_mk'_of_mul, DFunLike.coe, Function.Surjective, IsLocalization.eq_iff_exists
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
f : R →+* S
a b : R
H : ∀ (a_1 : S), ∃ (b_1 : R) (m : ℕ), (f : (a : R) → S) b_1 = HPow.hPow (α := S) ((f : (a : R) → S) (a * b) : S) m * a_1
suffices :
  ∀ (s : S) (n : ℕ),
    ∃ (c : R) (l : ℕ) (m : ℕ) (k : ℕ),
      (f : (a : R) → S) (a ^ (k + n) * c) = HMul.hMul (α := S) ((f : (a : R) → S) (a ^ (k + l) * b ^ m) : S) s
⊢ ∀ (a_1 : Away (M := S) ((f : (a : R) → S) a : S)),
    ∃ (b_1 : Away a) (m : ℕ),
      (awayMap f a : (a_2 : Away a) → Away ((f : (a : R) → S) a)) b_1 =
        HPow.hPow (α := Away (M := S) ((f : (a : R) → S) a : S))
            ((awayMap f a : (a_2 : Away a) → Away ((f : (a : R) → S) a))
                ((algebraMap R (Away a) : (a_2 : R) → Away a) b) :
              Away (M := S) ((f : (a : R) → S) a : S))
            m *
          a_1

Tactic:
suffices ∀ (s : S) (n : ℕ), ∃ c l m k, f (a ^ (k + n) * c) =
      f (a ^ (k + l) * b ^ m) * s by
    simpa [Function.Surjective, (IsLocalization.mk'_surjective (.powers (f a))).forall, ← map_pow,
      (IsLocalization.mk'_surjective (.powers a)).exists, Submonoid.mem_powers_iff, pow_add,
      Localization.awayMap, IsLocalization.Away.map, IsLocalization.map_mk', ← mul_assoc,
      IsLocalization.mk'_eq_iff_eq, ← map_mul, IsLocalization.eq_iff_exists (.powers (f a)),
      IsLocalization.mul_mk'_eq_mk'_of_mul]
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
f : R →+* S
a b : R
H : ∀ (a_1 : S), ∃ (b_1 : R) (m : ℕ), (f : (a : R) → S) b_1 = HPow.hPow (α := S) ((f : (a : R) → S) (a * b) : S) m * a_1
s : S
n : ℕ
obtain :
  ∀ (c : R) (m : ℕ) (e : (f : (a : R) → S) c = HPow.hPow (α := S) ((f : (a : R) → S) (a * b) : S) m * s),
    ∃ (c : R) (l : ℕ) (m : ℕ) (k : ℕ),
      (f : (a : R) → S) (a ^ (k + n) * c) = HMul.hMul (α := S) ((f : (a : R) → S) (a ^ (k + l) * b ^ m) : S) s
⊢ ∃ (c : R) (l : ℕ) (m : ℕ) (k : ℕ),
    (f : (a : R) → S) (a ^ (k + n) * c) = HMul.hMul (α := S) ((f : (a : R) → S) (a ^ (k + l) * b ^ m) : S) s

Tactic:
obtain ⟨c, m, e⟩ := H s
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
f : R →+* S
a b : R
H : ∀ (a_1 : S), ∃ (b_1 : R) (m : ℕ), (f : (a : R) → S) b_1 = HPow.hPow (α := S) ((f : (a : R) → S) (a * b) : S) m * a_1
s : S
n : ℕ
c : R
m : ℕ
e : (f : (a : R) → S) c = HPow.hPow (α := S) ((f : (a : R) → S) (a * b) : S) m * s
simp :
  HPow.hPow (α := S) ((f : (a : R) → S) a : S) n *
      (HMul.hMul (α := S) (β := S) ((f : (a : R) → S) a : S) ((f : (a : R) → S) b : S) ^ m * s) =
    HPow.hPow (α := S) ((f : (a : R) → S) a : S) n * HPow.hPow (α := S) ((f : (a : R) → S) a : S) m *
        HPow.hPow (α := S) ((f : (a : R) → S) b : S) m *
      s
⊢ (f : (a : R) → S) (a ^ (0 + n) * c) = HMul.hMul (α := S) ((f : (a : R) → S) (a ^ (0 + (n + m)) * b ^ m) : S) s

Tactic:
simp [e, pow_add]

Premises used: pow_add
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
f : R →+* S
a b : R
H : ∀ (a_1 : S), ∃ (b_1 : R) (m : ℕ), (f : (a : R) → S) b_1 = HPow.hPow (α := S) ((f : (a : R) → S) (a * b) : S) m * a_1
s : S
n : ℕ
c : R
m : ℕ
e : (f : (a : R) → S) c = HPow.hPow (α := S) ((f : (a : R) → S) (a * b) : S) m * s
⊢ HPow.hPow (α := S) ((f : (a : R) → S) a : S) n *
      (HMul.hMul (α := S) (β := S) ((f : (a : R) → S) a : S) ((f : (a : R) → S) b : S) ^ m * s) =
    HPow.hPow (α := S) ((f : (a : R) → S) a : S) n * HPow.hPow (α := S) ((f : (a : R) → S) a : S) m *
        HPow.hPow (α := S) ((f : (a : R) → S) b : S) m *
      s

Tactic:
ring
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
f : R →+* S
a b : R
H : ∀ (a_1 : S), ∃ (b_1 : R) (m : ℕ), (f : (a : R) → S) b_1 = HPow.hPow (α := S) ((f : (a : R) → S) (a * b) : S) m * a_1
s : S
n : ℕ
c : R
m : ℕ
e : (f : (a : R) → S) c = HPow.hPow (α := S) ((f : (a : R) → S) (a * b) : S) m * s
⊢ ∃ (c : R) (l : ℕ) (m : ℕ) (k : ℕ),
    (f : (a : R) → S) (a ^ (k + n) * c) = HMul.hMul (α := S) ((f : (a : R) → S) (a ^ (k + l) * b ^ m) : S) s

Tactic:
exact ⟨c, n + m, m, 0, by simp [e, pow_add]; ring⟩
-- Module: Mathlib.RingTheory.Localization.Away.Basic
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))
this : Eq (α := Ideal R) (Module.eqIdeal R x y) ⊤
⊢ x = y

Tactic:
simpa [Module.eqIdeal] using (Ideal.eq_top_iff_one _).mp this

Premises used: Ideal.eq_top_iff_one, Iff.mp, Module.eqIdeal
-- Module: Mathlib.RingTheory.Localization.Away.Basic
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))
suffices : Eq (α := Ideal R) (Module.eqIdeal R x y) ⊤
⊢ x = y

Tactic:
suffices Module.eqIdeal R x y = ⊤ by simpa [Module.eqIdeal] using (Ideal.eq_top_iff_one _).mp this
-- Module: Mathlib.RingTheory.Localization.Away.Basic
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))
by_contra : ∀ (ne : ¬Eq (α := Ideal R) (Module.eqIdeal R x y) ⊤), False
⊢ Eq (α := Ideal R) (Module.eqIdeal R x y) ⊤

Tactic:
by_contra ne
-- Module: Mathlib.RingTheory.Localization.Away.Basic
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) ⊤
have :
  ∀ (r : R) (hrs : r ∈ s) (disj : Disjoint (↑(Module.eqIdeal R x y) : Set R) (↑(Submonoid.powers r) : Set R)), False
⊢ False

Tactic:
have ⟨r, hrs, disj⟩ := Ideal.exists_disjoint_powers_of_span_eq_top s span_eq _ ne
-- Module: Mathlib.RingTheory.Localization.Away.Basic
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
have :
  ∀ (n : ℕ)
    (eq :
      (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers (↑r : R)) x)
                ((fun (x : ℕ) ↦ (↑r : R) ^ x) n) ⋯) :
            R) *
          x =
        (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers (↑r : R)) x)
                ((fun (x : ℕ) ↦ (↑r : R) ^ x) n) ⋯) :
            R) *
          y),
    False
⊢ False

Tactic:
have ⟨⟨_, n, rfl⟩, eq⟩ := (IsLocalization.eq_iff_exists (.powers r.1) _).mp (congr_fun eq r)
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
s : Set R
span_eq : Eq (α := Ideal R) (Ideal.span s) ⊤
x y : R
eq_1 :
  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
n : ℕ
eq :
  (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers (↑r : R)) x)
            ((fun (x : ℕ) ↦ (↑r : R) ^ x) n) ⋯) :
        R) *
      x =
    (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers (↑r : R)) x)
            ((fun (x : ℕ) ↦ (↑r : R) ^ x) n) ⋯) :
        R) *
      y
⊢ False

Tactic:
Set.disjoint_left.mp disj eq ⟨n, rfl⟩

Premises used: Set.disjoint_left, Exists.intro, Iff.mp, rfl
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
s : Set R
span_eq : Eq (α := Ideal R) (Ideal.span s) ⊤
x y : R
eq_1 :
  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
n : ℕ
eq :
  (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers (↑r : R)) x)
            ((fun (x : ℕ) ↦ (↑r : R) ^ x) n) ⋯) :
        R) *
      x =
    (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers (↑r : R)) x)
            ((fun (x : ℕ) ↦ (↑r : R) ^ x) n) ⋯) :
        R) *
      y
⊢ False

Tactic:
exact Set.disjoint_left.mp disj eq ⟨n, rfl⟩

Premises used: Set.disjoint_left, Exists.intro, Iff.mp, rfl
-- Module: Mathlib.RingTheory.Localization.Away.Basic
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)))
⊢ Membership.mem (γ := Ideal R) (Ideal.span s) 1

Tactic:
have mem := (Ideal.eq_top_iff_one _).mp span_eq
-- Module: Mathlib.RingTheory.Localization.Away.Basic
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
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
⊢ ∃! 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

Premises used: Finset
-- Module: Mathlib.RingTheory.Localization.Away.Basic
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
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
⊢ ∃! 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
-- Module: Mathlib.RingTheory.Localization.Away.Basic
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
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) ⋯) :
            Away (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ s) (↑a : 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
⊢ ∃! 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⟩
-- Module: Mathlib.RingTheory.Localization.Away.Basic
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

Tactic:
⟨r, fun a ↦ ?_, fun _ eq ↦ uniq _ fun a ↦ eq ⟨a, hts a.2⟩⟩

Premises used: Subtype.mk, ExistsUnique, And.intro, Exists.intro, Subtype.val, Subtype.property