-- 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 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
⊢ y * (algebraMap S T) ↑((algebraMap R S) x, ⟨(algebraMap R S) ↑s, ⋯⟩).2 =
    (algebraMap S T) ((algebraMap R S) x, ⟨(algebraMap R S) ↑s, ⋯⟩).1

Tactic:
simpa [← IsScalarTower.algebraMap_apply] using e

Result:
no goals

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₂
a : ↥N
e : ↑a * (y₁ * ↑s₂) = ↑a * (y₂ * ↑s₁)
⊢ ↑1 * (↑a * (y₁ * ↑s₂)) = ↑1 * (↑a * (y₂ * ↑s₁))

Tactic:
convert e using 1 <;> simp

Result:
no goals

Proof state:
case intro.mk.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
x₁ x₂ : S
y₁ : R
s₁ : ↥M
e₁ : x₁ * (algebraMap R S) ↑(y₁, s₁).2 = (algebraMap R S) (y₁, s₁).1
y₂ : R
s₂ : ↥M
e₂ : x₂ * (algebraMap R S) ↑(y₂, s₂).2 = (algebraMap R S) (y₂, s₂).1
⊢ (algebraMap S T) x₁ = (algebraMap S T) x₂ → ∃ a, (algebraMap R S) ↑a * x₁ = (algebraMap R S) ↑a * x₂

Tactic:
dsimp only at e₁ e₂ ⊢

Result:
case intro.mk.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
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₂
⊢ (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₂
h₁ :
  (algebraMap S T) x₁ * (algebraMap S T) ((algebraMap R S) ↑s₁) =
      (algebraMap S T) x₂ * (algebraMap S T) ((algebraMap R S) ↑s₁) ↔
    (algebraMap S T) x₁ = (algebraMap S T) x₂
h₂ :
  (algebraMap S T) x₁ * (algebraMap S T) ((algebraMap R S) ↑s₁) * (algebraMap S T) ((algebraMap R S) ↑s₂) =
      (algebraMap S T) x₂ * (algebraMap S T) ((algebraMap R S) ↑s₁) * (algebraMap S T) ((algebraMap R S) ↑s₂) ↔
    (algebraMap S T) x₁ * (algebraMap S T) ((algebraMap R S) ↑s₁) =
      (algebraMap S T) x₂ * (algebraMap S T) ((algebraMap R S) ↑s₁)
this : (algebraMap S T) x₁ = (algebraMap S T) x₂ → ∃ a, (algebraMap R S) ↑a * x₁ = (algebraMap R S) ↑a * x₂
⊢ (algebraMap S T) x₁ = (algebraMap S T) x₂ → ∃ a, (algebraMap R S) ↑a * x₁ = (algebraMap R S) ↑a * x₂

Tactic:
simpa only [mul_comm] using this

Result:
no goals

Proof state:
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

Tactic:
refine ⟨⟨algebraMap R S x, _, _, s.prop, rfl⟩, ?_⟩

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
⊢ y * (algebraMap S T) ↑((algebraMap R S) x, ⟨(algebraMap R S) ↑s, ⋯⟩).2 =
    (algebraMap S T) ((algebraMap R S) x, ⟨(algebraMap R S) ↑s, ⋯⟩).1

Proof state:
case intro.mk.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
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₂
⊢ (∃ c, ↑c * (y₁ * ↑s₂) = ↑c * (y₂ * ↑s₁)) → ∃ a c, ↑c * (↑a * (y₁ * ↑s₂)) = ↑c * (↑a * (y₂ * ↑s₁))

Tactic:
intro ⟨a, e⟩

Result:
case intro.mk.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
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₂
a : ↥N
e : ↑a * (y₁ * ↑s₂) = ↑a * (y₂ * ↑s₁)
⊢ ∃ a c, ↑c * (↑a * (y₁ * ↑s₂)) = ↑c * (↑a * (y₂ * ↑s₁))

Proof state:
case intro.mk.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
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₂
⊢ (algebraMap R T) (y₁ * ↑s₂) = (algebraMap R T) (y₂ * ↑s₁) →
    ∃ a, (algebraMap R S) (↑a * (y₁ * ↑s₂)) = (algebraMap R S) (↑a * (y₂ * ↑s₁))

Tactic:
simp_rw [IsLocalization.eq_iff_exists N T, IsLocalization.eq_iff_exists M S]

Result:
case intro.mk.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
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₂
⊢ (∃ c, ↑c * (y₁ * ↑s₂) = ↑c * (y₂ * ↑s₁)) → ∃ a c, ↑c * (↑a * (y₁ * ↑s₂)) = ↑c * (↑a * (y₂ * ↑s₁))

Proof state:
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⟩

Tactic:
exact (IsScalarTower.algebraMap_apply _ _ _ _).symm

Result:
no goals