-- 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_1 :
  (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
r' : R
eq :
  (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)))
    r'
right :
  ∀ (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

Tactic:
exact (congr_arg _ (uniq _ fun b ↦ eq ⟨b, .inr b.2⟩).symm).trans (eq ⟨a, .inl rfl⟩)

Premises used: Subtype.mk, congr_arg, Or.inl, Eq.symm, Subtype.val, Or.inr, rfl, Eq.trans, Subtype.property