-- Mathlib/RingTheory/Localization/AsSubring.lean
theorem mem_range_mapToFractionRing_iff_ofField (B : Type*) [CommRing B] [Algebra A B]
    [IsLocalization S B] (x : K) :
    x ∈ (mapToFractionRing K S B hS).range ↔
      ∃ (a s : A) (_ : s ∈ S), x = algebraMap A K a * (algebraMap A K s)⁻¹

Proof state:
case h.e'_2.h.e'_2.h.h.e'_2.h.h.e'_2.h.h.e'_3
A : Type u_1
K : Type u_2
inst✝⁶ : CommRing A
S : Submonoid A
hS : S ≤ A⁰
inst✝⁵ : Field K
inst✝⁴ : Algebra A K
inst✝³ : IsFractionRing A K
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
x : K
x✝² x✝¹ : A
x✝ : x✝¹ ∈ S
⊢ (algebraMap A K) x✝² * ((algebraMap A K) x✝¹)⁻¹ = IsLocalization.mk' K x✝² ⟨x✝¹, ⋯⟩

Tactic:
congr

Result:
case h.e'_2.h.e'_2.h.h.e'_2.h.h.e'_2.h.h.e'_3.e_a
A : Type u_1
K : Type u_2
inst✝⁶ : CommRing A
S : Submonoid A
hS : S ≤ A⁰
inst✝⁵ : Field K
inst✝⁴ : Algebra A K
inst✝³ : IsFractionRing A K
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
x : K
x✝² x✝¹ : A
x✝ : x✝¹ ∈ S
⊢ ((algebraMap A K) x✝¹)⁻¹ =
    ↑((IsUnit.liftRight ((IsLocalization.toLocalizationMap A⁰ K).toMap.restrict A⁰) ⋯) ⟨x✝¹, ⋯⟩)⁻¹

Proof state:
A : Type u_1
K : Type u_2
inst✝⁶ : CommRing A
S : Submonoid A
hS : S ≤ A⁰
inst✝⁵ : Field K
inst✝⁴ : Algebra A K
inst✝³ : IsFractionRing A K
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
x : K
⊢ (∃ a s, ∃ (hs : s ∈ S), x = IsLocalization.mk' K a ⟨s, ⋯⟩) ↔
    ∃ a s, ∃ (_ : s ∈ S), x = (algebraMap A K) a * ((algebraMap A K) s)⁻¹

Tactic:
convert Iff.rfl

Result:
case h.e'_2.h.e'_2.h.h.e'_2.h.h.e'_2.h.h.e'_3
A : Type u_1
K : Type u_2
inst✝⁶ : CommRing A
S : Submonoid A
hS : S ≤ A⁰
inst✝⁵ : Field K
inst✝⁴ : Algebra A K
inst✝³ : IsFractionRing A K
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
x : K
x✝² x✝¹ : A
x✝ : x✝¹ ∈ S
⊢ (algebraMap A K) x✝² * ((algebraMap A K) x✝¹)⁻¹ = IsLocalization.mk' K x✝² ⟨x✝¹, ⋯⟩

Proof state:
case h.e'_2.h.e'_2.h.h.e'_2.h.h.e'_2.h.h.e'_3.e_a
A : Type u_1
K : Type u_2
inst✝⁶ : CommRing A
S : Submonoid A
hS : S ≤ A⁰
inst✝⁵ : Field K
inst✝⁴ : Algebra A K
inst✝³ : IsFractionRing A K
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
x : K
x✝² x✝¹ : A
x✝ : x✝¹ ∈ S
⊢ ((algebraMap A K) x✝¹)⁻¹ =
    ↑((IsUnit.liftRight ((IsLocalization.toLocalizationMap A⁰ K).toMap.restrict A⁰) ⋯) ⟨x✝¹, ⋯⟩)⁻¹

Tactic:
rw [Units.val_inv_eq_inv_val]

Result:
case h.e'_2.h.e'_2.h.h.e'_2.h.h.e'_2.h.h.e'_3.e_a
A : Type u_1
K : Type u_2
inst✝⁶ : CommRing A
S : Submonoid A
hS : S ≤ A⁰
inst✝⁵ : Field K
inst✝⁴ : Algebra A K
inst✝³ : IsFractionRing A K
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
x : K
x✝² x✝¹ : A
x✝ : x✝¹ ∈ S
⊢ ((algebraMap A K) x✝¹)⁻¹ =
    (↑((IsUnit.liftRight ((IsLocalization.toLocalizationMap A⁰ K).toMap.restrict A⁰) ⋯) ⟨x✝¹, ⋯⟩))⁻¹

Proof state:
A : Type u_1
K : Type u_2
inst✝⁶ : CommRing A
S : Submonoid A
hS : S ≤ A⁰
inst✝⁵ : Field K
inst✝⁴ : Algebra A K
inst✝³ : IsFractionRing A K
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
x : K
⊢ x ∈ (mapToFractionRing K S B hS).range ↔ ∃ a s, ∃ (_ : s ∈ S), x = (algebraMap A K) a * ((algebraMap A K) s)⁻¹

Tactic:
rw [mem_range_mapToFractionRing_iff]

Result:
A : Type u_1
K : Type u_2
inst✝⁶ : CommRing A
S : Submonoid A
hS : S ≤ A⁰
inst✝⁵ : Field K
inst✝⁴ : Algebra A K
inst✝³ : IsFractionRing A K
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
x : K
⊢ (∃ a s, ∃ (hs : s ∈ S), x = IsLocalization.mk' K a ⟨s, ⋯⟩) ↔
    ∃ a s, ∃ (_ : s ∈ S), x = (algebraMap A K) a * ((algebraMap A K) s)⁻¹

Proof state:
case h.e'_2.h.e'_2.h.h.e'_2.h.h.e'_2.h.h.e'_3.e_a
A : Type u_1
K : Type u_2
inst✝⁶ : CommRing A
S : Submonoid A
hS : S ≤ A⁰
inst✝⁵ : Field K
inst✝⁴ : Algebra A K
inst✝³ : IsFractionRing A K
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
x : K
x✝² x✝¹ : A
x✝ : x✝¹ ∈ S
⊢ ((algebraMap A K) x✝¹)⁻¹ =
    (↑((IsUnit.liftRight ((IsLocalization.toLocalizationMap A⁰ K).toMap.restrict A⁰) ⋯) ⟨x✝¹, ⋯⟩))⁻¹

Tactic:
rfl

Result:
no goals