-- Mathlib/Algebra/Module/LocalizedModule/IsLocalization.lean
theorem isLocalizedModule_iff_isLocalization :
    IsLocalizedModule S (IsScalarTower.toAlgHom R A Aₛ).toLinearMap ↔
      IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ

Proof state:
case refine_3
R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
A : Type u_2
Aₛ : Type u_3
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : CommSemiring Aₛ
inst✝² : Algebra A Aₛ
inst✝¹ : Algebra R Aₛ
inst✝ : IsScalarTower R A Aₛ
x✝¹ x✝ : A
⊢ ((IsScalarTower.toAlgHom R A Aₛ).toLinearMap x✝¹ = (IsScalarTower.toAlgHom R A Aₛ).toLinearMap x✝ →
      ∃ c, c • x✝¹ = c • x✝) ↔
    (algebraMap A Aₛ) x✝¹ = (algebraMap A Aₛ) x✝ → ∃ c, ↑c * x✝¹ = ↑c * x✝

Tactic:
congr!

Result:
case refine_3.a.h'.a
R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
A : Type u_2
Aₛ : Type u_3
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : CommSemiring Aₛ
inst✝² : Algebra A Aₛ
inst✝¹ : Algebra R Aₛ
inst✝ : IsScalarTower R A Aₛ
x✝¹ x✝ : A
a✝ : (algebraMap A Aₛ) x✝¹ = (algebraMap A Aₛ) x✝
⊢ (∃ c, c • x✝¹ = c • x✝) ↔ ∃ c, ↑c * x✝¹ = ↑c * x✝

Proof state:
case refine_2
R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
A : Type u_2
Aₛ : Type u_3
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : CommSemiring Aₛ
inst✝² : Algebra A Aₛ
inst✝¹ : Algebra R Aₛ
inst✝ : IsScalarTower R A Aₛ
x✝ : Aₛ
⊢ (∃ x, x.2 • x✝ = (IsScalarTower.toAlgHom R A Aₛ).toLinearMap x.1) ↔
    ∃ x, x✝ * (algebraMap A Aₛ) ↑x.2 = (algebraMap A Aₛ) x.1

Tactic:
simp_rw [Prod.exists, Subtype.exists, Algebra.algebraMapSubmonoid]

Result:
case refine_2
R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
A : Type u_2
Aₛ : Type u_3
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : CommSemiring Aₛ
inst✝² : Algebra A Aₛ
inst✝¹ : Algebra R Aₛ
inst✝ : IsScalarTower R A Aₛ
x✝ : Aₛ
⊢ (∃ a a_1, ∃ (b : a_1 ∈ S), ⟨a_1, b⟩ • x✝ = (IsScalarTower.toAlgHom R A Aₛ).toLinearMap a) ↔
    ∃ a a_1, ∃ (_ : a_1 ∈ Submonoid.map (algebraMap R A) S), x✝ * (algebraMap A Aₛ) a_1 = (algebraMap A Aₛ) a

Proof state:
case refine_3.a.h'.a
R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
A : Type u_2
Aₛ : Type u_3
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : CommSemiring Aₛ
inst✝² : Algebra A Aₛ
inst✝¹ : Algebra R Aₛ
inst✝ : IsScalarTower R A Aₛ
x✝¹ x✝ : A
a✝ : (algebraMap A Aₛ) x✝¹ = (algebraMap A Aₛ) x✝
⊢ (∃ a, ∃ (b : a ∈ S), ⟨a, b⟩ • x✝¹ = ⟨a, b⟩ • x✝) ↔ ∃ a, ∃ (_ : a ∈ Submonoid.map (algebraMap R A) S), a * x✝¹ = a * x✝

Tactic:
simp [Algebra.smul_def]

Result:
no goals

Proof state:
R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
A : Type u_2
Aₛ : Type u_3
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : CommSemiring Aₛ
inst✝² : Algebra A Aₛ
inst✝¹ : Algebra R Aₛ
inst✝ : IsScalarTower R A Aₛ
⊢ IsLocalizedModule S (IsScalarTower.toAlgHom R A Aₛ).toLinearMap ↔ IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ

Tactic:
rw [isLocalizedModule_iff, isLocalization_iff]

Result:
R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
A : Type u_2
Aₛ : Type u_3
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : CommSemiring Aₛ
inst✝² : Algebra A Aₛ
inst✝¹ : Algebra R Aₛ
inst✝ : IsScalarTower R A Aₛ
⊢ ((∀ (x : ↥S), IsUnit ((algebraMap R (Module.End R Aₛ)) ↑x)) ∧
      (∀ (y : Aₛ), ∃ x, x.2 • y = (IsScalarTower.toAlgHom R A Aₛ).toLinearMap x.1) ∧
        ∀ {x₁ x₂ : A},
          (IsScalarTower.toAlgHom R A Aₛ).toLinearMap x₁ = (IsScalarTower.toAlgHom R A Aₛ).toLinearMap x₂ →
            ∃ c, c • x₁ = c • x₂) ↔
    (∀ (y : ↥(Algebra.algebraMapSubmonoid A S)), IsUnit ((algebraMap A Aₛ) ↑y)) ∧
      (∀ (z : Aₛ), ∃ x, z * (algebraMap A Aₛ) ↑x.2 = (algebraMap A Aₛ) x.1) ∧
        ∀ {x y : A}, (algebraMap A Aₛ) x = (algebraMap A Aₛ) y → ∃ c, ↑c * x = ↑c * y

Proof state:
case refine_1
R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
A : Type u_2
Aₛ : Type u_3
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : CommSemiring Aₛ
inst✝² : Algebra A Aₛ
inst✝¹ : Algebra R Aₛ
inst✝ : IsScalarTower R A Aₛ
⊢ (∀ (x : ↥S), IsUnit ((algebraMap R (Module.End R Aₛ)) ↑x)) ↔
    ∀ (y : ↥(Algebra.algebraMapSubmonoid A S)), IsUnit ((algebraMap A Aₛ) ↑y)

Tactic:
simp_rw [← (Algebra.lmul R Aₛ).commutes, Algebra.lmul_isUnit_iff, Subtype.forall,
  Algebra.algebraMapSubmonoid, ← SetLike.mem_coe, Submonoid.coe_map,
  Set.forall_mem_image, ← IsScalarTower.algebraMap_apply]

Result:
no goals

Proof state:
R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
A : Type u_2
Aₛ : Type u_3
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : CommSemiring Aₛ
inst✝² : Algebra A Aₛ
inst✝¹ : Algebra R Aₛ
inst✝ : IsScalarTower R A Aₛ
⊢ ((∀ (x : ↥S), IsUnit ((algebraMap R (Module.End R Aₛ)) ↑x)) ∧
      (∀ (y : Aₛ), ∃ x, x.2 • y = (IsScalarTower.toAlgHom R A Aₛ).toLinearMap x.1) ∧
        ∀ {x₁ x₂ : A},
          (IsScalarTower.toAlgHom R A Aₛ).toLinearMap x₁ = (IsScalarTower.toAlgHom R A Aₛ).toLinearMap x₂ →
            ∃ c, c • x₁ = c • x₂) ↔
    (∀ (y : ↥(Algebra.algebraMapSubmonoid A S)), IsUnit ((algebraMap A Aₛ) ↑y)) ∧
      (∀ (z : Aₛ), ∃ x, z * (algebraMap A Aₛ) ↑x.2 = (algebraMap A Aₛ) x.1) ∧
        ∀ {x y : A}, (algebraMap A Aₛ) x = (algebraMap A Aₛ) y → ∃ c, ↑c * x = ↑c * y

Tactic:
refine and_congr ?_ (and_congr (forall_congr' fun _ ↦ ?_) (forall₂_congr fun _ _ ↦ ?_))

Result:
case refine_1
R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
A : Type u_2
Aₛ : Type u_3
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : CommSemiring Aₛ
inst✝² : Algebra A Aₛ
inst✝¹ : Algebra R Aₛ
inst✝ : IsScalarTower R A Aₛ
⊢ (∀ (x : ↥S), IsUnit ((algebraMap R (Module.End R Aₛ)) ↑x)) ↔
    ∀ (y : ↥(Algebra.algebraMapSubmonoid A S)), IsUnit ((algebraMap A Aₛ) ↑y)

case refine_2
R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
A : Type u_2
Aₛ : Type u_3
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : CommSemiring Aₛ
inst✝² : Algebra A Aₛ
inst✝¹ : Algebra R Aₛ
inst✝ : IsScalarTower R A Aₛ
x✝ : Aₛ
⊢ (∃ x, x.2 • x✝ = (IsScalarTower.toAlgHom R A Aₛ).toLinearMap x.1) ↔
    ∃ x, x✝ * (algebraMap A Aₛ) ↑x.2 = (algebraMap A Aₛ) x.1

case refine_3
R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
A : Type u_2
Aₛ : Type u_3
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : CommSemiring Aₛ
inst✝² : Algebra A Aₛ
inst✝¹ : Algebra R Aₛ
inst✝ : IsScalarTower R A Aₛ
x✝¹ x✝ : A
⊢ ((IsScalarTower.toAlgHom R A Aₛ).toLinearMap x✝¹ = (IsScalarTower.toAlgHom R A Aₛ).toLinearMap x✝ →
      ∃ c, c • x✝¹ = c • x✝) ↔
    (algebraMap A Aₛ) x✝¹ = (algebraMap A Aₛ) x✝ → ∃ c, ↑c * x✝¹ = ↑c * x✝

Proof state:
case refine_3.a.h'.a
R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
A : Type u_2
Aₛ : Type u_3
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : CommSemiring Aₛ
inst✝² : Algebra A Aₛ
inst✝¹ : Algebra R Aₛ
inst✝ : IsScalarTower R A Aₛ
x✝¹ x✝ : A
a✝ : (algebraMap A Aₛ) x✝¹ = (algebraMap A Aₛ) x✝
⊢ (∃ c, c • x✝¹ = c • x✝) ↔ ∃ c, ↑c * x✝¹ = ↑c * x✝

Tactic:
simp_rw [Subtype.exists, Algebra.algebraMapSubmonoid]

Result:
case refine_3.a.h'.a
R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
A : Type u_2
Aₛ : Type u_3
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : CommSemiring Aₛ
inst✝² : Algebra A Aₛ
inst✝¹ : Algebra R Aₛ
inst✝ : IsScalarTower R A Aₛ
x✝¹ x✝ : A
a✝ : (algebraMap A Aₛ) x✝¹ = (algebraMap A Aₛ) x✝
⊢ (∃ a, ∃ (b : a ∈ S), ⟨a, b⟩ • x✝¹ = ⟨a, b⟩ • x✝) ↔ ∃ a, ∃ (_ : a ∈ Submonoid.map (algebraMap R A) S), a * x✝¹ = a * x✝

Proof state:
case refine_2
R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
A : Type u_2
Aₛ : Type u_3
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : CommSemiring Aₛ
inst✝² : Algebra A Aₛ
inst✝¹ : Algebra R Aₛ
inst✝ : IsScalarTower R A Aₛ
x✝ : Aₛ
⊢ (∃ a a_1, ∃ (b : a_1 ∈ S), ⟨a_1, b⟩ • x✝ = (IsScalarTower.toAlgHom R A Aₛ).toLinearMap a) ↔
    ∃ a a_1, ∃ (_ : a_1 ∈ Submonoid.map (algebraMap R A) S), x✝ * (algebraMap A Aₛ) a_1 = (algebraMap A Aₛ) a

Tactic:
simp [← IsScalarTower.algebraMap_apply, Submonoid.mk_smul, Algebra.smul_def, mul_comm]

Result:
no goals