-- Module: Mathlib.RingTheory.Localization.Away.Lemmas
Goal:
R : Type u_1
inst : CommRing R
s : Set R
hsone : Eq (α := Ideal R) (Ideal.span s) ⊤
Rₜ : (↑s : Type u_1) → Type u_2
inst_1 : (t : (↑s : Type u_1)) → CommRing (Rₜ t)
inst_2 : (t : (↑s : Type u_1)) → Algebra.{u_1, u_2} R (Rₜ t)
inst_3 : ∀ (t : (↑s : Type u_1)), Away.{u_1, u_2} (↑t : R) (Rₜ t)
p : (t : (↑s : Type u_1)) → Set (Rₜ t)
htone : ∀ (r : (↑s : Type u_1)), Eq (α := Ideal (Rₜ r)) (Ideal.span (p r)) ⊤
a : R
ha : a ∈ s
this : IsLocalization.{u_1, u_2} (Submonoid.powers a) (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha))
x : Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)
hx :
  Membership.mem (γ := Set (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)))
    (p (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)) x
h :
  HMul.hMul (β := Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)) x
      ((algebraMap R (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)) : (a_1 : R) → Rₜ ⟨a, ha⟩)
          (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers a) x)
                (a ^ ((sec a x).2 + 1)) ⋯) :
            R) :
        Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)) =
    (algebraMap R (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)) : (a_1 : R) → Rₜ ⟨a, ha⟩) (a * (sec a x).1)
h₁ :
  x *
      HPow.hPow (α := Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha))
        ((algebraMap R (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)) : (a_1 : R) → Rₜ ⟨a, ha⟩) a :
          Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha))
        ((sec a x).2 + 1) =
    (algebraMap R (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)) : (a_1 : R) → Rₜ ⟨a, ha⟩) (a * (sec a x).1)
h₂ :
  x *
      HPow.hPow (α := Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha))
        ((algebraMap R (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)) : (a_1 : R) → Rₜ ⟨a, ha⟩) a :
          Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha))
        ((sec a x).2 + 1) =
    HMul.hMul (α := Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)) (β :=
      Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha))
      ((algebraMap R (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)) : (a_1 : R) → Rₜ ⟨a, ha⟩) a :
        Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha))
      ((algebraMap R (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)) : (a_1 : R) → Rₜ ⟨a, ha⟩) (sec a x).1 :
        Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha))
h₃ :
  HMul.hMul (β := Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)) x
      ((algebraMap R (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)) : (a_1 : R) → Rₜ ⟨a, ha⟩)
          (a ^ ((sec a x).2 + 1)) :
        Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)) =
    HMul.hMul (α := Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)) (β :=
      Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha))
      ((algebraMap R (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)) : (a_1 : R) → Rₜ ⟨a, ha⟩) a :
        Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha))
      ((algebraMap R (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)) : (a_1 : R) → Rₜ ⟨a, ha⟩) (sec a x).1 :
        Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha))
h₄ :
  HMul.hMul (β := Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)) x
      ((algebraMap R (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)) : (a_1 : R) → Rₜ ⟨a, ha⟩)
          (a ^ (sec a x).2 * HPow.hPow (β := ℕ) a 1) :
        Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)) =
    HMul.hMul (α := Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)) (β :=
      Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha))
      ((algebraMap R (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)) : (a_1 : R) → Rₜ ⟨a, ha⟩) a :
        Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha))
      ((algebraMap R (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)) : (a_1 : R) → Rₜ ⟨a, ha⟩) (sec a x).1 :
        Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha))
h₅ :
  x *
      HMul.hMul (α := Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)) (β :=
        Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha))
        ((algebraMap R (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)) : (a_1 : R) → Rₜ ⟨a, ha⟩) (a ^ (sec a x).2) :
          Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha))
        ((algebraMap R (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)) : (a_1 : R) → Rₜ ⟨a, ha⟩)
            (HPow.hPow (β := ℕ) a 1) :
          Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)) =
    HMul.hMul (α := Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)) (β :=
      Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha))
      ((algebraMap R (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)) : (a_1 : R) → Rₜ ⟨a, ha⟩) a :
        Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha))
      ((algebraMap R (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)) : (a_1 : R) → Rₜ ⟨a, ha⟩) (sec a x).1 :
        Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha))
h₆ :
  HMul.hMul (β := Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha))
      (HMul.hMul (β := Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)) x
        ((algebraMap R (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)) : (a_1 : R) → Rₜ ⟨a, ha⟩) (a ^ (sec a x).2) :
          Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)))
      ((algebraMap R (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)) : (a_1 : R) → Rₜ ⟨a, ha⟩)
          (HPow.hPow (β := ℕ) a 1) :
        Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)) =
    HMul.hMul (α := Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)) (β :=
      Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha))
      ((algebraMap R (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)) : (a_1 : R) → Rₜ ⟨a, ha⟩) a :
        Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha))
      ((algebraMap R (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)) : (a_1 : R) → Rₜ ⟨a, ha⟩) (sec a x).1 :
        Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha))
h₇ :
  HMul.hMul (α := Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)) (β :=
      Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha))
      ((algebraMap R (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)) : (a_1 : R) → Rₜ ⟨a, ha⟩) (sec a x).1 :
        Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha))
      ((algebraMap R (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)) : (a_1 : R) → Rₜ ⟨a, ha⟩)
          (HPow.hPow (β := ℕ) a 1) :
        Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)) =
    HMul.hMul (α := Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)) (β :=
      Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha))
      ((algebraMap R (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)) : (a_1 : R) → Rₜ ⟨a, ha⟩) a :
        Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha))
      ((algebraMap R (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)) : (a_1 : R) → Rₜ ⟨a, ha⟩) (sec a x).1 :
        Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha))
h₈ :
  HMul.hMul (α := Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)) (β :=
      Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha))
      ((algebraMap R (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)) : (a_1 : R) → Rₜ ⟨a, ha⟩)
          (HPow.hPow (β := ℕ) a 1) :
        Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha))
      ((algebraMap R (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)) : (a_1 : R) → Rₜ ⟨a, ha⟩) (sec a x).1 :
        Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)) =
    HMul.hMul (α := Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)) (β :=
      Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha))
      ((algebraMap R (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)) : (a_1 : R) → Rₜ ⟨a, ha⟩) a :
        Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha))
      ((algebraMap R (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)) : (a_1 : R) → Rₜ ⟨a, ha⟩) (sec a x).1 :
        Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha))
h₉ h₁₀ :
  HMul.hMul (α := Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)) (β :=
      Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha))
      ((algebraMap R (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)) : (a_1 : R) → Rₜ ⟨a, ha⟩) a :
        Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha))
      ((algebraMap R (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)) : (a_1 : R) → Rₜ ⟨a, ha⟩) (sec a x).1 :
        Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)) =
    HMul.hMul (α := Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)) (β :=
      Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha))
      ((algebraMap R (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)) : (a_1 : R) → Rₜ ⟨a, ha⟩) a :
        Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha))
      ((algebraMap R (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)) : (a_1 : R) → Rₜ ⟨a, ha⟩) (sec a x).1 :
        Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha))
⊢ x =
    mk' (M := Submonoid.powers a) (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)) (a * (sec a x).1)
      (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers a) x) (a ^ ((sec a x).2 + 1))
        ⋯)

Tactic:
rw [IsLocalization.eq_mk'_iff_mul_eq, map_pow, map_mul, ← map_pow, pow_add, map_mul,
      ← mul_assoc, IsLocalization.Away.sec_spec a x, mul_comm, pow_one]

Premises used: IsLocalization.Away.sec_spec, mul_assoc, pow_add, map_pow, map_mul, pow_one, mul_comm, IsLocalization.eq_mk'_iff_mul_eq