-- Mathlib/RingTheory/Localization/Away/Lemmas.lean
lemma span_range_mulNumerator_eq_top {s : Set R}
    (hsone : Ideal.span s = ⊤) {Rₜ : s → Type*} [∀ t, CommRing (Rₜ t)] [∀ t, Algebra R (Rₜ t)]
    [∀ t, IsLocalization.Away t.val (Rₜ t)]
    {p : (t : s) → Set (Rₜ t)} (htone : ∀ (r : s), Ideal.span (p r) = ⊤) :
    Ideal.span (Set.range (IsLocalization.Away.mulNumerator s p)) = ⊤

Proof state:
case intro.intro.intro.mk.intro.intro.mk.intro
R : Type u_1
inst✝³ : CommRing R
s : Set R
hsone : Ideal.span s = ⊤
Rₜ : ↑s → Type u_2
inst✝² : (t : ↑s) → CommRing (Rₜ t)
inst✝¹ : (t : ↑s) → Algebra R (Rₜ t)
inst✝ : ∀ (t : ↑s), Away (↑t) (Rₜ t)
p : (t : ↑s) → Set (Rₜ t)
htone : ∀ (r : ↑s), Ideal.span (p r) = ⊤
a : R
ha : a ∈ s
this : IsLocalization (Submonoid.powers a) (Rₜ ⟨a, ha⟩)
h₁ : Ideal.span (p ⟨a, ha⟩) ≤ Ideal.span (⇑(algebraMap R (Rₜ ⟨a, ha⟩)) '' Set.range (mulNumerator s p))
y : R
hy : y ∈ Ideal.span (Set.range (mulNumerator s p))
m n : ℕ
hc : ↑⟨(fun x => a ^ x) n, ⋯⟩ * (↑⟨(fun x => a ^ x) m, ⋯⟩ * 1) = ↑⟨(fun x => a ^ x) n, ⋯⟩ * (↑1 * y)
⊢ a ∈ ↑(Ideal.span (Set.range (mulNumerator s p))).radical

Tactic:
simp only [← mul_assoc, OneMemClass.coe_one, one_mul, mul_one] at hc

Result:
case intro.intro.intro.mk.intro.intro.mk.intro
R : Type u_1
inst✝³ : CommRing R
s : Set R
hsone : Ideal.span s = ⊤
Rₜ : ↑s → Type u_2
inst✝² : (t : ↑s) → CommRing (Rₜ t)
inst✝¹ : (t : ↑s) → Algebra R (Rₜ t)
inst✝ : ∀ (t : ↑s), Away (↑t) (Rₜ t)
p : (t : ↑s) → Set (Rₜ t)
htone : ∀ (r : ↑s), Ideal.span (p r) = ⊤
a : R
ha : a ∈ s
this : IsLocalization (Submonoid.powers a) (Rₜ ⟨a, ha⟩)
h₁ : Ideal.span (p ⟨a, ha⟩) ≤ Ideal.span (⇑(algebraMap R (Rₜ ⟨a, ha⟩)) '' Set.range (mulNumerator s p))
y : R
hy : y ∈ Ideal.span (Set.range (mulNumerator s p))
m n : ℕ
hc : a ^ n * a ^ m = a ^ n * y
⊢ a ∈ ↑(Ideal.span (Set.range (mulNumerator s p))).radical

Proof state:
R : Type u_1
inst✝³ : CommRing R
s : Set R
hsone : Ideal.span s = ⊤
Rₜ : ↑s → Type u_2
inst✝² : (t : ↑s) → CommRing (Rₜ t)
inst✝¹ : (t : ↑s) → Algebra R (Rₜ t)
inst✝ : ∀ (t : ↑s), Away (↑t) (Rₜ t)
p : (t : ↑s) → Set (Rₜ t)
htone : ∀ (r : ↑s), Ideal.span (p r) = ⊤
a : R
ha : a ∈ s
this : IsLocalization (Submonoid.powers a) (Rₜ ⟨a, ha⟩)
x : Rₜ ⟨a, ha⟩
hx : x ∈ p ⟨a, ha⟩
⊢ x ∈ ↑(Ideal.span (⇑(algebraMap R (Rₜ ⟨a, ha⟩)) '' Set.range (mulNumerator s p)))

Tactic:
rw [SetLike.mem_coe, IsLocalization.mem_span_map (Submonoid.powers a)]

Result:
R : Type u_1
inst✝³ : CommRing R
s : Set R
hsone : Ideal.span s = ⊤
Rₜ : ↑s → Type u_2
inst✝² : (t : ↑s) → CommRing (Rₜ t)
inst✝¹ : (t : ↑s) → Algebra R (Rₜ t)
inst✝ : ∀ (t : ↑s), Away (↑t) (Rₜ t)
p : (t : ↑s) → Set (Rₜ t)
htone : ∀ (r : ↑s), Ideal.span (p r) = ⊤
a : R
ha : a ∈ s
this : IsLocalization (Submonoid.powers a) (Rₜ ⟨a, ha⟩)
x : Rₜ ⟨a, ha⟩
hx : x ∈ p ⟨a, ha⟩
⊢ ∃ y ∈ Ideal.span (Set.range (mulNumerator s p)), ∃ z, x = mk' (Rₜ ⟨a, ha⟩) y z

Proof state:
R : Type u_1
inst✝³ : CommRing R
s : Set R
hsone : Ideal.span s = ⊤
Rₜ : ↑s → Type u_2
inst✝² : (t : ↑s) → CommRing (Rₜ t)
inst✝¹ : (t : ↑s) → Algebra R (Rₜ t)
inst✝ : ∀ (t : ↑s), Away (↑t) (Rₜ t)
p : (t : ↑s) → Set (Rₜ t)
htone : ∀ (r : ↑s), Ideal.span (p r) = ⊤
a : R
ha : a ∈ s
this : IsLocalization (Submonoid.powers a) (Rₜ ⟨a, ha⟩)
h₁ : Ideal.span (p ⟨a, ha⟩) ≤ Ideal.span (⇑(algebraMap R (Rₜ ⟨a, ha⟩)) '' Set.range (mulNumerator s p))
⊢ mk' (Rₜ ⟨a, ha⟩) 1 1 ∈ Ideal.span (⇑(algebraMap R (Rₜ ⟨a, ha⟩)) '' Set.range (mulNumerator s p))

Tactic:
rw [IsLocalization.mk'_one]

Result:
R : Type u_1
inst✝³ : CommRing R
s : Set R
hsone : Ideal.span s = ⊤
Rₜ : ↑s → Type u_2
inst✝² : (t : ↑s) → CommRing (Rₜ t)
inst✝¹ : (t : ↑s) → Algebra R (Rₜ t)
inst✝ : ∀ (t : ↑s), Away (↑t) (Rₜ t)
p : (t : ↑s) → Set (Rₜ t)
htone : ∀ (r : ↑s), Ideal.span (p r) = ⊤
a : R
ha : a ∈ s
this : IsLocalization (Submonoid.powers a) (Rₜ ⟨a, ha⟩)
h₁ : Ideal.span (p ⟨a, ha⟩) ≤ Ideal.span (⇑(algebraMap R (Rₜ ⟨a, ha⟩)) '' Set.range (mulNumerator s p))
⊢ (algebraMap R (Rₜ ⟨a, ha⟩)) 1 ∈ Ideal.span (⇑(algebraMap R (Rₜ ⟨a, ha⟩)) '' Set.range (mulNumerator s p))

Proof state:
R : Type u_1
inst✝³ : CommRing R
s : Set R
hsone : Ideal.span s = ⊤
Rₜ : ↑s → Type u_2
inst✝² : (t : ↑s) → CommRing (Rₜ t)
inst✝¹ : (t : ↑s) → Algebra R (Rₜ t)
inst✝ : ∀ (t : ↑s), Away (↑t) (Rₜ t)
p : (t : ↑s) → Set (Rₜ t)
htone : ∀ (r : ↑s), Ideal.span (p r) = ⊤
a : R
ha : a ∈ s
⊢ a ∈ ↑(Ideal.span (Set.range (mulNumerator s p))).radical

Tactic:
haveI : IsLocalization (Submonoid.powers a) (Rₜ ⟨a, ha⟩) :=
  inferInstanceAs <| IsLocalization.Away (⟨a, ha⟩ : s).val (Rₜ ⟨a, ha⟩)

Result:
R : Type u_1
inst✝³ : CommRing R
s : Set R
hsone : Ideal.span s = ⊤
Rₜ : ↑s → Type u_2
inst✝² : (t : ↑s) → CommRing (Rₜ t)
inst✝¹ : (t : ↑s) → Algebra R (Rₜ t)
inst✝ : ∀ (t : ↑s), Away (↑t) (Rₜ t)
p : (t : ↑s) → Set (Rₜ t)
htone : ∀ (r : ↑s), Ideal.span (p r) = ⊤
a : R
ha : a ∈ s
this : IsLocalization (Submonoid.powers a) (Rₜ ⟨a, ha⟩)
⊢ a ∈ ↑(Ideal.span (Set.range (mulNumerator s p))).radical

Proof state:
case intro.intro.intro.mk.intro
R : Type u_1
inst✝³ : CommRing R
s : Set R
hsone : Ideal.span s = ⊤
Rₜ : ↑s → Type u_2
inst✝² : (t : ↑s) → CommRing (Rₜ t)
inst✝¹ : (t : ↑s) → Algebra R (Rₜ t)
inst✝ : ∀ (t : ↑s), Away (↑t) (Rₜ t)
p : (t : ↑s) → Set (Rₜ t)
htone : ∀ (r : ↑s), Ideal.span (p r) = ⊤
a : R
ha : a ∈ s
this : IsLocalization (Submonoid.powers a) (Rₜ ⟨a, ha⟩)
h₁ : Ideal.span (p ⟨a, ha⟩) ≤ Ideal.span (⇑(algebraMap R (Rₜ ⟨a, ha⟩)) '' Set.range (mulNumerator s p))
y : R
hy : y ∈ Ideal.span (Set.range (mulNumerator s p))
m : ℕ
hyz : mk' (Rₜ ⟨a, ha⟩) 1 1 = mk' (Rₜ ⟨a, ha⟩) y ⟨(fun x => a ^ x) m, ⋯⟩
⊢ a ∈ ↑(Ideal.span (Set.range (mulNumerator s p))).radical

Tactic:
rw [IsLocalization.eq] at hyz

Result:
case intro.intro.intro.mk.intro
R : Type u_1
inst✝³ : CommRing R
s : Set R
hsone : Ideal.span s = ⊤
Rₜ : ↑s → Type u_2
inst✝² : (t : ↑s) → CommRing (Rₜ t)
inst✝¹ : (t : ↑s) → Algebra R (Rₜ t)
inst✝ : ∀ (t : ↑s), Away (↑t) (Rₜ t)
p : (t : ↑s) → Set (Rₜ t)
htone : ∀ (r : ↑s), Ideal.span (p r) = ⊤
a : R
ha : a ∈ s
this : IsLocalization (Submonoid.powers a) (Rₜ ⟨a, ha⟩)
h₁ : Ideal.span (p ⟨a, ha⟩) ≤ Ideal.span (⇑(algebraMap R (Rₜ ⟨a, ha⟩)) '' Set.range (mulNumerator s p))
y : R
hy : y ∈ Ideal.span (Set.range (mulNumerator s p))
m : ℕ
hyz : ∃ c, ↑c * (↑⟨(fun x => a ^ x) m, ⋯⟩ * 1) = ↑c * (↑1 * y)
⊢ a ∈ ↑(Ideal.span (Set.range (mulNumerator s p))).radical

Proof state:
R : Type u_1
inst✝³ : CommRing R
s : Set R
hsone : Ideal.span s = ⊤
Rₜ : ↑s → Type u_2
inst✝² : (t : ↑s) → CommRing (Rₜ t)
inst✝¹ : (t : ↑s) → Algebra R (Rₜ t)
inst✝ : ∀ (t : ↑s), Away (↑t) (Rₜ t)
p : (t : ↑s) → Set (Rₜ t)
htone : ∀ (r : ↑s), Ideal.span (p r) = ⊤
a : R
ha : a ∈ s
this : IsLocalization (Submonoid.powers a) (Rₜ ⟨a, ha⟩)
h₁ : Ideal.span (p ⟨a, ha⟩) ≤ Ideal.span (⇑(algebraMap R (Rₜ ⟨a, ha⟩)) '' Set.range (mulNumerator s p))
⊢ (algebraMap R (Rₜ ⟨a, ha⟩)) 1 ∈ Ideal.span (⇑(algebraMap R (Rₜ ⟨a, ha⟩)) '' Set.range (mulNumerator s p))

Tactic:
apply h₁

Result:
case a
R : Type u_1
inst✝³ : CommRing R
s : Set R
hsone : Ideal.span s = ⊤
Rₜ : ↑s → Type u_2
inst✝² : (t : ↑s) → CommRing (Rₜ t)
inst✝¹ : (t : ↑s) → Algebra R (Rₜ t)
inst✝ : ∀ (t : ↑s), Away (↑t) (Rₜ t)
p : (t : ↑s) → Set (Rₜ t)
htone : ∀ (r : ↑s), Ideal.span (p r) = ⊤
a : R
ha : a ∈ s
this : IsLocalization (Submonoid.powers a) (Rₜ ⟨a, ha⟩)
h₁ : Ideal.span (p ⟨a, ha⟩) ≤ Ideal.span (⇑(algebraMap R (Rₜ ⟨a, ha⟩)) '' Set.range (mulNumerator s p))
⊢ (algebraMap R (Rₜ ⟨a, ha⟩)) 1 ∈ Ideal.span (p ⟨a, ha⟩)