-- Mathlib/RingTheory/EssentialFiniteness.lean
lemma essFiniteType_cond_iff (σ : Finset S) :
    IsLocalization ((IsUnit.submonoid S).comap (algebraMap (adjoin R (σ : Set S)) S)) S ↔
    (∀ s : S, ∃ t ∈ Algebra.adjoin R (σ : Set S),
      IsUnit t ∧ s * t ∈ Algebra.adjoin R (σ : Set S))

Proof state:
case mp
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Finset S
hσ : IsLocalization (Submonoid.comap (algebraMap (↥(adjoin R ↑σ)) S) (IsUnit.submonoid S)) S
⊢ ∀ (s : S), ∃ t ∈ adjoin R ↑σ, IsUnit t ∧ s * t ∈ adjoin R ↑σ

Tactic:
intro s

Result:
case mp
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Finset S
hσ : IsLocalization (Submonoid.comap (algebraMap (↥(adjoin R ↑σ)) S) (IsUnit.submonoid S)) S
s : S
⊢ ∃ t ∈ adjoin R ↑σ, IsUnit t ∧ s * t ∈ adjoin R ↑σ

Proof state:
case mpr.surj'
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Finset S
hσ : ∀ (s : S), ∃ t ∈ adjoin R ↑σ, IsUnit t ∧ s * t ∈ adjoin R ↑σ
⊢ ∀ (z : S), ∃ x, z * (algebraMap (↥(adjoin R ↑σ)) S) ↑x.2 = (algebraMap (↥(adjoin R ↑σ)) S) x.1

Tactic:
intro s

Result:
case mpr.surj'
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Finset S
hσ : ∀ (s : S), ∃ t ∈ adjoin R ↑σ, IsUnit t ∧ s * t ∈ adjoin R ↑σ
s : S
⊢ ∃ x, s * (algebraMap (↥(adjoin R ↑σ)) S) ↑x.2 = (algebraMap (↥(adjoin R ↑σ)) S) x.1

Proof state:
case mpr.exists_of_eq
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Finset S
hσ : ∀ (s : S), ∃ t ∈ adjoin R ↑σ, IsUnit t ∧ s * t ∈ adjoin R ↑σ
x y : ↥(adjoin R ↑σ)
e : (algebraMap (↥(adjoin R ↑σ)) S) x = (algebraMap (↥(adjoin R ↑σ)) S) y
⊢ ∃ c, ↑c * x = ↑c * y

Tactic:
exact ⟨1, by simpa using Subtype.ext e⟩

Result:
no goals

Proof state:
case mpr.surj'
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Finset S
hσ : ∀ (s : S), ∃ t ∈ adjoin R ↑σ, IsUnit t ∧ s * t ∈ adjoin R ↑σ
s : S
⊢ ∃ x, s * (algebraMap (↥(adjoin R ↑σ)) S) ↑x.2 = (algebraMap (↥(adjoin R ↑σ)) S) x.1

Tactic:
obtain ⟨t, ht, ht', h⟩ := hσ s

Result:
case mpr.surj'.intro.intro.intro
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Finset S
hσ : ∀ (s : S), ∃ t ∈ adjoin R ↑σ, IsUnit t ∧ s * t ∈ adjoin R ↑σ
s t : S
ht : t ∈ adjoin R ↑σ
ht' : IsUnit t
h : s * t ∈ adjoin R ↑σ
⊢ ∃ x, s * (algebraMap (↥(adjoin R ↑σ)) S) ↑x.2 = (algebraMap (↥(adjoin R ↑σ)) S) x.1

Proof state:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Finset S
⊢ IsLocalization (Submonoid.comap (algebraMap (↥(adjoin R ↑σ)) S) (IsUnit.submonoid S)) S ↔
    ∀ (s : S), ∃ t ∈ adjoin R ↑σ, IsUnit t ∧ s * t ∈ adjoin R ↑σ

Tactic:
constructor <;> intro hσ

Result:
case mp
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Finset S
hσ : IsLocalization (Submonoid.comap (algebraMap (↥(adjoin R ↑σ)) S) (IsUnit.submonoid S)) S
⊢ ∀ (s : S), ∃ t ∈ adjoin R ↑σ, IsUnit t ∧ s * t ∈ adjoin R ↑σ

case mpr
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Finset S
hσ : ∀ (s : S), ∃ t ∈ adjoin R ↑σ, IsUnit t ∧ s * t ∈ adjoin R ↑σ
⊢ IsLocalization (Submonoid.comap (algebraMap (↥(adjoin R ↑σ)) S) (IsUnit.submonoid S)) S

Proof state:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Finset S
hσ : ∀ (s : S), ∃ t ∈ adjoin R ↑σ, IsUnit t ∧ s * t ∈ adjoin R ↑σ
x y : ↥(adjoin R ↑σ)
e : (algebraMap (↥(adjoin R ↑σ)) S) x = (algebraMap (↥(adjoin R ↑σ)) S) y
⊢ ↑1 * x = ↑1 * y

Tactic:
simpa using Subtype.ext e

Result:
no goals

Proof state:
case mpr
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Finset S
hσ : ∀ (s : S), ∃ t ∈ adjoin R ↑σ, IsUnit t ∧ s * t ∈ adjoin R ↑σ
⊢ IsLocalization (Submonoid.comap (algebraMap (↥(adjoin R ↑σ)) S) (IsUnit.submonoid S)) S

Tactic:
constructor

Result:
case mpr.map_units'
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Finset S
hσ : ∀ (s : S), ∃ t ∈ adjoin R ↑σ, IsUnit t ∧ s * t ∈ adjoin R ↑σ
⊢ ∀ (y : ↥(Submonoid.comap (algebraMap (↥(adjoin R ↑σ)) S) (IsUnit.submonoid S))),
    IsUnit ((algebraMap (↥(adjoin R ↑σ)) S) ↑y)

case mpr.surj'
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Finset S
hσ : ∀ (s : S), ∃ t ∈ adjoin R ↑σ, IsUnit t ∧ s * t ∈ adjoin R ↑σ
⊢ ∀ (z : S), ∃ x, z * (algebraMap (↥(adjoin R ↑σ)) S) ↑x.2 = (algebraMap (↥(adjoin R ↑σ)) S) x.1

case mpr.exists_of_eq
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Finset S
hσ : ∀ (s : S), ∃ t ∈ adjoin R ↑σ, IsUnit t ∧ s * t ∈ adjoin R ↑σ
⊢ ∀ {x y : ↥(adjoin R ↑σ)}, (algebraMap (↥(adjoin R ↑σ)) S) x = (algebraMap (↥(adjoin R ↑σ)) S) y → ∃ c, ↑c * x = ↑c * y

Proof state:
case mpr.surj'.intro.intro.intro
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Finset S
hσ : ∀ (s : S), ∃ t ∈ adjoin R ↑σ, IsUnit t ∧ s * t ∈ adjoin R ↑σ
s t : S
ht : t ∈ adjoin R ↑σ
ht' : IsUnit t
h : s * t ∈ adjoin R ↑σ
⊢ ∃ x, s * (algebraMap (↥(adjoin R ↑σ)) S) ↑x.2 = (algebraMap (↥(adjoin R ↑σ)) S) x.1

Tactic:
exact ⟨⟨⟨_, h⟩, ⟨t, ht⟩, ht'⟩, rfl⟩

Result:
no goals

Proof state:
case mpr.exists_of_eq
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Finset S
hσ : ∀ (s : S), ∃ t ∈ adjoin R ↑σ, IsUnit t ∧ s * t ∈ adjoin R ↑σ
⊢ ∀ {x y : ↥(adjoin R ↑σ)}, (algebraMap (↥(adjoin R ↑σ)) S) x = (algebraMap (↥(adjoin R ↑σ)) S) y → ∃ c, ↑c * x = ↑c * y

Tactic:
intros x y e

Result:
case mpr.exists_of_eq
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Finset S
hσ : ∀ (s : S), ∃ t ∈ adjoin R ↑σ, IsUnit t ∧ s * t ∈ adjoin R ↑σ
x y : ↥(adjoin R ↑σ)
e : (algebraMap (↥(adjoin R ↑σ)) S) x = (algebraMap (↥(adjoin R ↑σ)) S) y
⊢ ∃ c, ↑c * x = ↑c * y

Proof state:
case mp.intro.mk.mk.mk.mk
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Finset S
hσ : IsLocalization (Submonoid.comap (algebraMap (↥(adjoin R ↑σ)) S) (IsUnit.submonoid S)) S
s x : S
hx : x ∈ adjoin R ↑σ
t : S
ht : t ∈ adjoin R ↑σ
ht' : ⟨t, ht⟩ ∈ Submonoid.comap (algebraMap (↥(adjoin R ↑σ)) S) (IsUnit.submonoid S)
h :
  s * (algebraMap (↥(adjoin R ↑σ)) S) ↑(⟨x, hx⟩, ⟨⟨t, ht⟩, ht'⟩).2 =
    (algebraMap (↥(adjoin R ↑σ)) S) (⟨x, hx⟩, ⟨⟨t, ht⟩, ht'⟩).1
⊢ ∃ t ∈ adjoin R ↑σ, IsUnit t ∧ s * t ∈ adjoin R ↑σ

Tactic:
exact ⟨t, ht, ht', h ▸ hx⟩

Result:
no goals

Proof state:
case mpr.map_units'
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Finset S
hσ : ∀ (s : S), ∃ t ∈ adjoin R ↑σ, IsUnit t ∧ s * t ∈ adjoin R ↑σ
⊢ ∀ (y : ↥(Submonoid.comap (algebraMap (↥(adjoin R ↑σ)) S) (IsUnit.submonoid S))),
    IsUnit ((algebraMap (↥(adjoin R ↑σ)) S) ↑y)

Tactic:
exact fun y ↦ y.prop

Result:
no goals

Proof state:
case mp
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Finset S
hσ : IsLocalization (Submonoid.comap (algebraMap (↥(adjoin R ↑σ)) S) (IsUnit.submonoid S)) S
s : S
⊢ ∃ t ∈ adjoin R ↑σ, IsUnit t ∧ s * t ∈ adjoin R ↑σ

Tactic:
obtain ⟨⟨⟨x, hx⟩, ⟨t, ht⟩, ht'⟩, h⟩ := hσ.2 s

Result:
case mp.intro.mk.mk.mk.mk
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Finset S
hσ : IsLocalization (Submonoid.comap (algebraMap (↥(adjoin R ↑σ)) S) (IsUnit.submonoid S)) S
s x : S
hx : x ∈ adjoin R ↑σ
t : S
ht : t ∈ adjoin R ↑σ
ht' : ⟨t, ht⟩ ∈ Submonoid.comap (algebraMap (↥(adjoin R ↑σ)) S) (IsUnit.submonoid S)
h :
  s * (algebraMap (↥(adjoin R ↑σ)) S) ↑(⟨x, hx⟩, ⟨⟨t, ht⟩, ht'⟩).2 =
    (algebraMap (↥(adjoin R ↑σ)) S) (⟨x, hx⟩, ⟨⟨t, ht⟩, ht'⟩).1
⊢ ∃ t ∈ adjoin R ↑σ, IsUnit t ∧ s * t ∈ adjoin R ↑σ