-- 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_1 : (↑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)
hts : insert (↑a : R) (↑t : Set R) ⊆ s
inr inr₁ inr₂ :
  ∀ (r' : R)
    (eq :
      ∀ (a_1 : (↑({(↑a : R)} ∪ (↑t : Set R)) : Type u_1)),
        Eq (α := Away (↑a_1 : R)) ((algebraMap R (Away (↑a_1 : R)) : (a_2 : R) → Away (↑a_1 : R)) r' : Away (↑a_1 : R))
          (f (Subtype.mk (p := fun (x : R) ↦ x ∈ s) (↑a_1 : R) ⋯) :
            Away (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ s) (↑a_1 : R) ⋯) : R))),
    (∀ (y : R),
        (fun (r : R) ↦
              ∀ (a_1 : (↑({(↑a : R)} ∪ (↑t : Set R)) : Type u_1)),
                Eq (α := Away (↑a_1 : R))
                  ((algebraMap R (Away (↑a_1 : R)) : (a_2 : R) → Away (↑a_1 : R)) r : Away (↑a_1 : R))
                  (f (Subtype.mk (p := fun (x : R) ↦ x ∈ s) (↑a_1 : R) ⋯) :
                    Away (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ s) (↑a_1 : R) ⋯) : R)))
            y →
          y = r') →
      (algebraMap R (Away (↑a : R)) : (a_1 : R) → Away (↑a : R)) r = f a
⊢ (algebraMap R (Away (↑a : R)) : (a_1 : R) → Away (↑a : R)) r = f a

Tactic:
classical
    have ⟨r', eq, _⟩ := this ({a.1} ∪ t) (fun a ↦ f ⟨a, hts a.2⟩) (fun a b ↦
      h ⟨a, hts a.2⟩ ⟨b, hts b.2⟩) (Ideal.span_mono (fun _ ↦ .inr) mem) ⟨{a.1} ∪ t, by simp⟩
    exact (congr_arg _ (uniq _ fun b ↦ eq ⟨b, .inr b.2⟩).symm).trans (eq ⟨a, .inl rfl⟩)