-- Mathlib/RingTheory/Localization/LocalizationLocalization.lean
theorem localization_localization_isLocalization_of_has_all_units [IsLocalization N T]
    (H : ∀ x : S, IsUnit x → x ∈ N) : IsLocalization (N.comap (algebraMap R S)) T

Proof state:
R : Type u_1
inst✝⁸ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
N : Submonoid S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
H : ∀ (x : S), IsUnit x → x ∈ N
⊢ IsLocalization (Submonoid.comap (algebraMap R S) N) T

Tactic:
convert localization_localization_isLocalization M N T using 1

Result:
case h.e'_3
R : Type u_1
inst✝⁸ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
N : Submonoid S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
H : ∀ (x : S), IsUnit x → x ∈ N
⊢ Submonoid.comap (algebraMap R S) N = localizationLocalizationSubmodule M N

Proof state:
case h.e'_3.e_S
R : Type u_1
inst✝⁸ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
N : Submonoid S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
H : ∀ (x : S), IsUnit x → x ∈ N
⊢ Submonoid.map (algebraMap R S) M ≤ N

Tactic:
rintro _ ⟨x, hx, rfl⟩

Result:
case h.e'_3.e_S.intro.intro
R : Type u_1
inst✝⁸ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
N : Submonoid S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
H : ∀ (x : S), IsUnit x → x ∈ N
x : R
hx : x ∈ ↑M
⊢ (algebraMap R S) x ∈ N

Proof state:
case h.e'_3
R : Type u_1
inst✝⁸ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
N : Submonoid S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
H : ∀ (x : S), IsUnit x → x ∈ N
⊢ Submonoid.comap (algebraMap R S) N = Submonoid.comap (algebraMap R S) (N ⊔ Submonoid.map (algebraMap R S) M)

Tactic:
congr

Result:
case h.e'_3.e_S
R : Type u_1
inst✝⁸ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
N : Submonoid S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
H : ∀ (x : S), IsUnit x → x ∈ N
⊢ N = N ⊔ Submonoid.map (algebraMap R S) M

Proof state:
case h.e'_3.e_S
R : Type u_1
inst✝⁸ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
N : Submonoid S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
H : ∀ (x : S), IsUnit x → x ∈ N
⊢ N = N ⊔ Submonoid.map (algebraMap R S) M

Tactic:
symm

Result:
case h.e'_3.e_S
R : Type u_1
inst✝⁸ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
N : Submonoid S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
H : ∀ (x : S), IsUnit x → x ∈ N
⊢ N ⊔ Submonoid.map (algebraMap R S) M = N

Proof state:
case h.e'_3
R : Type u_1
inst✝⁸ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
N : Submonoid S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
H : ∀ (x : S), IsUnit x → x ∈ N
⊢ Submonoid.comap (algebraMap R S) N = localizationLocalizationSubmodule M N

Tactic:
dsimp [localizationLocalizationSubmodule]

Result:
case h.e'_3
R : Type u_1
inst✝⁸ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
N : Submonoid S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
H : ∀ (x : S), IsUnit x → x ∈ N
⊢ Submonoid.comap (algebraMap R S) N = Submonoid.comap (algebraMap R S) (N ⊔ Submonoid.map (algebraMap R S) M)

Proof state:
case h.e'_3.e_S.intro.intro
R : Type u_1
inst✝⁸ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
N : Submonoid S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
H : ∀ (x : S), IsUnit x → x ∈ N
x : R
hx : x ∈ ↑M
⊢ (algebraMap R S) x ∈ N

Tactic:
exact H _ (IsLocalization.map_units _ ⟨x, hx⟩)

Result:
no goals

Proof state:
case h.e'_3.e_S
R : Type u_1
inst✝⁸ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
N : Submonoid S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
H : ∀ (x : S), IsUnit x → x ∈ N
⊢ N ⊔ Submonoid.map (algebraMap R S) M = N

Tactic:
rw [sup_eq_left]

Result:
case h.e'_3.e_S
R : Type u_1
inst✝⁸ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
N : Submonoid S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
H : ∀ (x : S), IsUnit x → x ∈ N
⊢ Submonoid.map (algebraMap R S) M ≤ N