-- Mathlib/RingTheory/Localization/AsSubring.lean
theorem mem_range_mapToFractionRing_iff (B : Type*) [CommRing B] [Algebra A B] [IsLocalization S B]
    (hS : S ≤ A⁰) (x : K) :
    x ∈ (mapToFractionRing K S B hS).range ↔
      ∃ (a s : A) (hs : s ∈ S), x = IsLocalization.mk' K a ⟨s, hS hs⟩ :=
  ⟨by
    rintro ⟨x, rfl⟩
    obtain ⟨a, s, rfl⟩ := IsLocalization.mk'_surjective S x
    use a, s, s.2
    apply IsLocalization.lift_mk', by
    rintro ⟨a, s, hs, rfl⟩
    use IsLocalization.mk' _ a ⟨s, hs⟩
    apply IsLocalization.lift_mk'⟩

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

Tactic:
rintro ⟨a, s, hs, rfl⟩

Result:
case intro.intro.intro
A : Type u_1
K : Type u_2
inst✝⁶ : CommRing A
S : Submonoid A
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsFractionRing A K
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
hS : S ≤ A⁰
a s : A
hs : s ∈ S
⊢ IsLocalization.mk' K a ⟨s, ⋯⟩ ∈ (mapToFractionRing K S B hS).range

Proof state:
case h
A : Type u_1
K : Type u_2
inst✝⁶ : CommRing A
S : Submonoid A
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsFractionRing A K
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
hS : S ≤ A⁰
a s : A
hs : s ∈ S
⊢ (mapToFractionRing K S B hS).toRingHom (IsLocalization.mk' B a ⟨s, hs⟩) = IsLocalization.mk' K a ⟨s, ⋯⟩

Tactic:
apply IsLocalization.lift_mk'

Result:
no goals

Proof state:
case intro.intro.intro
A : Type u_1
K : Type u_2
inst✝⁶ : CommRing A
S : Submonoid A
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsFractionRing A K
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
hS : S ≤ A⁰
a s : A
hs : s ∈ S
⊢ IsLocalization.mk' K a ⟨s, ⋯⟩ ∈ (mapToFractionRing K S B hS).range

Tactic:
use IsLocalization.mk' _ a ⟨s, hs⟩

Result:
case h
A : Type u_1
K : Type u_2
inst✝⁶ : CommRing A
S : Submonoid A
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsFractionRing A K
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
hS : S ≤ A⁰
a s : A
hs : s ∈ S
⊢ (mapToFractionRing K S B hS).toRingHom (IsLocalization.mk' B a ⟨s, hs⟩) = IsLocalization.mk' K a ⟨s, ⋯⟩

Proof state:
case intro.intro.intro
A : Type u_1
K : Type u_2
inst✝⁶ : CommRing A
S : Submonoid A
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsFractionRing A K
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
hS : S ≤ A⁰
a : A
s : ↥S
⊢ ∃ a_1 s_1,
    ∃ (hs : s_1 ∈ S),
      (mapToFractionRing K S B hS).toRingHom (IsLocalization.mk' B a s) = IsLocalization.mk' K a_1 ⟨s_1, ⋯⟩

Tactic:
use a, s, s.2

Result:
case h
A : Type u_1
K : Type u_2
inst✝⁶ : CommRing A
S : Submonoid A
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsFractionRing A K
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
hS : S ≤ A⁰
a : A
s : ↥S
⊢ (mapToFractionRing K S B hS).toRingHom (IsLocalization.mk' B a s) = IsLocalization.mk' K a ⟨↑s, ⋯⟩

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

Tactic:
obtain ⟨a, s, rfl⟩ := IsLocalization.mk'_surjective S x

Result:
case intro.intro.intro
A : Type u_1
K : Type u_2
inst✝⁶ : CommRing A
S : Submonoid A
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsFractionRing A K
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
hS : S ≤ A⁰
a : A
s : ↥S
⊢ ∃ a_1 s_1,
    ∃ (hs : s_1 ∈ S),
      (mapToFractionRing K S B hS).toRingHom (IsLocalization.mk' B a s) = IsLocalization.mk' K a_1 ⟨s_1, ⋯⟩

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

Tactic:
rintro ⟨x, rfl⟩

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

Proof state:
case h
A : Type u_1
K : Type u_2
inst✝⁶ : CommRing A
S : Submonoid A
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsFractionRing A K
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
hS : S ≤ A⁰
a : A
s : ↥S
⊢ (mapToFractionRing K S B hS).toRingHom (IsLocalization.mk' B a s) = IsLocalization.mk' K a ⟨↑s, ⋯⟩

Tactic:
apply IsLocalization.lift_mk'

Result:
no goals