-- Mathlib/RingTheory/Localization/LocalizationLocalization.lean
theorem isLocalization_of_submonoid_le (M N : Submonoid R) (h : M ≤ N) [IsLocalization M S]
    [IsLocalization N T] [Algebra S T] [IsScalarTower R S T] :
    IsLocalization (N.map (algebraMap R S)) T :=
  { map_units'

Proof state:
case mk.intro.intro
R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
M N : Submonoid R
h : M ≤ N
inst✝³ : IsLocalization M S
inst✝² : IsLocalization N T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
y : R
hy : y ∈ ↑N
⊢ IsUnit ((algebraMap S T) ↑⟨(algebraMap R S) y, ⋯⟩)

Tactic:
convert IsLocalization.map_units T ⟨y, hy⟩

Result:
case h.e'_3
R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
M N : Submonoid R
h : M ≤ N
inst✝³ : IsLocalization M S
inst✝² : IsLocalization N T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
y : R
hy : y ∈ ↑N
⊢ (algebraMap S T) ↑⟨(algebraMap R S) y, ⋯⟩ = (algebraMap R T) ↑⟨y, hy⟩

Proof state:
R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
M N : Submonoid R
h : M ≤ N
inst✝³ : IsLocalization M S
inst✝² : IsLocalization N T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
y : T
⊢ ∃ x, y * (algebraMap S T) ↑x.2 = (algebraMap S T) x.1

Tactic:
obtain ⟨⟨x, s⟩, e⟩ := IsLocalization.surj N y

Result:
case intro.mk
R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
M N : Submonoid R
h : M ≤ N
inst✝³ : IsLocalization M S
inst✝² : IsLocalization N T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
y : T
x : R
s : ↥N
e : y * (algebraMap R T) ↑(x, s).2 = (algebraMap R T) (x, s).1
⊢ ∃ x, y * (algebraMap S T) ↑x.2 = (algebraMap S T) x.1

Proof state:
R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
M N : Submonoid R
h : M ≤ N
inst✝³ : IsLocalization M S
inst✝² : IsLocalization N T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
x₁ x₂ : S
y₁ : R
s₁ : ↥M
e₁ : x₁ * (algebraMap R S) ↑s₁ = (algebraMap R S) y₁
y₂ : R
s₂ : ↥M
e₂ : x₂ * (algebraMap R S) ↑s₂ = (algebraMap R S) y₂
this :
  (algebraMap R T) (y₁ * ↑s₂) = (algebraMap R T) (y₂ * ↑s₁) →
    ∃ a, (algebraMap R S) (↑a * (y₁ * ↑s₂)) = (algebraMap R S) (↑a * (y₂ * ↑s₁))
h₁ :
  (algebraMap S T) x₁ * (algebraMap R T) ↑⟨↑s₁, ⋯⟩ = (algebraMap S T) x₂ * (algebraMap R T) ↑⟨↑s₁, ⋯⟩ ↔
    (algebraMap S T) x₁ = (algebraMap S T) x₂
⊢ (algebraMap S T) x₁ = (algebraMap S T) x₂ → ∃ a, (algebraMap R S) ↑a * x₁ = (algebraMap R S) ↑a * x₂

Tactic:
have h₂ := @IsUnit.mul_left_inj T _ _ ((algebraMap S T x₁) * (algebraMap R T s₁))
  ((algebraMap S T x₂) * (algebraMap R T s₁))
  (IsLocalization.map_units T ⟨(s₂ : R), h s₂.prop⟩)

Result:
R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
M N : Submonoid R
h : M ≤ N
inst✝³ : IsLocalization M S
inst✝² : IsLocalization N T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
x₁ x₂ : S
y₁ : R
s₁ : ↥M
e₁ : x₁ * (algebraMap R S) ↑s₁ = (algebraMap R S) y₁
y₂ : R
s₂ : ↥M
e₂ : x₂ * (algebraMap R S) ↑s₂ = (algebraMap R S) y₂
this :
  (algebraMap R T) (y₁ * ↑s₂) = (algebraMap R T) (y₂ * ↑s₁) →
    ∃ a, (algebraMap R S) (↑a * (y₁ * ↑s₂)) = (algebraMap R S) (↑a * (y₂ * ↑s₁))
h₁ :
  (algebraMap S T) x₁ * (algebraMap R T) ↑⟨↑s₁, ⋯⟩ = (algebraMap S T) x₂ * (algebraMap R T) ↑⟨↑s₁, ⋯⟩ ↔
    (algebraMap S T) x₁ = (algebraMap S T) x₂
h₂ :
  (algebraMap S T) x₁ * (algebraMap R T) ↑s₁ * (algebraMap R T) ↑⟨↑s₂, ⋯⟩ =
      (algebraMap S T) x₂ * (algebraMap R T) ↑s₁ * (algebraMap R T) ↑⟨↑s₂, ⋯⟩ ↔
    (algebraMap S T) x₁ * (algebraMap R T) ↑s₁ = (algebraMap S T) x₂ * (algebraMap R T) ↑s₁
⊢ (algebraMap S T) x₁ = (algebraMap S T) x₂ → ∃ a, (algebraMap R S) ↑a * x₁ = (algebraMap R S) ↑a * x₂

Proof state:
R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
M N : Submonoid R
h : M ≤ N
inst✝³ : IsLocalization M S
inst✝² : IsLocalization N T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
x₁ x₂ : S
y₁ : R
s₁ : ↥M
e₁ : x₁ * (algebraMap R S) ↑s₁ = (algebraMap R S) y₁
y₂ : R
s₂ : ↥M
e₂ : x₂ * (algebraMap R S) ↑s₂ = (algebraMap R S) y₂
this :
  (algebraMap R T) (y₁ * ↑s₂) = (algebraMap R T) (y₂ * ↑s₁) →
    ∃ a, (algebraMap R S) (↑a * (y₁ * ↑s₂)) = (algebraMap R S) (↑a * (y₂ * ↑s₁))
⊢ (algebraMap S T) x₁ = (algebraMap S T) x₂ → ∃ a, (algebraMap R S) ↑a * x₁ = (algebraMap R S) ↑a * x₂

Tactic:
have h₁ := @IsUnit.mul_left_inj T _ _ (algebraMap S T x₁) (algebraMap S T x₂)
  (IsLocalization.map_units T ⟨(s₁ : R), h s₁.prop⟩)

Result:
R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
M N : Submonoid R
h : M ≤ N
inst✝³ : IsLocalization M S
inst✝² : IsLocalization N T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
x₁ x₂ : S
y₁ : R
s₁ : ↥M
e₁ : x₁ * (algebraMap R S) ↑s₁ = (algebraMap R S) y₁
y₂ : R
s₂ : ↥M
e₂ : x₂ * (algebraMap R S) ↑s₂ = (algebraMap R S) y₂
this :
  (algebraMap R T) (y₁ * ↑s₂) = (algebraMap R T) (y₂ * ↑s₁) →
    ∃ a, (algebraMap R S) (↑a * (y₁ * ↑s₂)) = (algebraMap R S) (↑a * (y₂ * ↑s₁))
h₁ :
  (algebraMap S T) x₁ * (algebraMap R T) ↑⟨↑s₁, ⋯⟩ = (algebraMap S T) x₂ * (algebraMap R T) ↑⟨↑s₁, ⋯⟩ ↔
    (algebraMap S T) x₁ = (algebraMap S T) x₂
⊢ (algebraMap S T) x₁ = (algebraMap S T) x₂ → ∃ a, (algebraMap R S) ↑a * x₁ = (algebraMap R S) ↑a * x₂