-- Mathlib/RingTheory/Localization/Integral.lean
lemma isAlgebraic_of_isLocalization {R} [CommRing R] (M : Submonoid R) (S) [CommRing S]
    [Nontrivial R] [Algebra R S] [IsLocalization M S] : Algebra.IsAlgebraic R S

Proof state:
case neg.refine_1
R : Type u_5
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_6
inst✝³ : CommRing S
inst✝² : Nontrivial R
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : R
s : ↥M
hs : ¬↑s = 0
⊢ s • X - C x ≠ 0

Tactic:
intro e

Result:
case neg.refine_1
R : Type u_5
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_6
inst✝³ : CommRing S
inst✝² : Nontrivial R
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : R
s : ↥M
hs : ¬↑s = 0
e : s • X - C x = 0
⊢ False

Proof state:
R : Type u_5
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_6
inst✝³ : CommRing S
inst✝² : Nontrivial R
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : R
s : ↥M
hs : ↑s = 0
this : 0 = (algebraMap R S) x
⊢ (aeval (mk' S x s)) X = 0

Tactic:
simp [IsLocalization.mk'_eq_mul_mk'_one x, ← this]

Result:
no goals

Proof state:
case pos
R : Type u_5
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_6
inst✝³ : CommRing S
inst✝² : Nontrivial R
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : R
s : ↥M
hs : ↑s = 0
this : mk' S x s * (algebraMap R S) ↑s = (algebraMap R S) x
⊢ IsAlgebraic R (mk' S x s)

Tactic:
rw [hs, map_zero, mul_zero] at this

Result:
case pos
R : Type u_5
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_6
inst✝³ : CommRing S
inst✝² : Nontrivial R
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : R
s : ↥M
hs : ↑s = 0
this : 0 = (algebraMap R S) x
⊢ IsAlgebraic R (mk' S x s)

Proof state:
case isAlgebraic
R : Type u_5
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_6
inst✝³ : CommRing S
inst✝² : Nontrivial R
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
⊢ ∀ (x : S), IsAlgebraic R x

Tactic:
intro x

Result:
case isAlgebraic
R : Type u_5
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_6
inst✝³ : CommRing S
inst✝² : Nontrivial R
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : S
⊢ IsAlgebraic R x

Proof state:
case neg.refine_2
R : Type u_5
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_6
inst✝³ : CommRing S
inst✝² : Nontrivial R
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : R
s : ↥M
hs : ¬↑s = 0
⊢ (aeval (mk' S x s)) (s • X - C x) = 0

Tactic:
simp only [map_sub, Algebra.smul_def, Submonoid.smul_def,
  map_mul, AlgHom.commutes, aeval_X, IsLocalization.mk'_spec', aeval_C, sub_self]

Result:
no goals

Proof state:
R : Type u_5
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_6
inst✝³ : CommRing S
inst✝² : Nontrivial R
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
⊢ Algebra.IsAlgebraic R S

Tactic:
constructor

Result:
case isAlgebraic
R : Type u_5
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_6
inst✝³ : CommRing S
inst✝² : Nontrivial R
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
⊢ ∀ (x : S), IsAlgebraic R x

Proof state:
case isAlgebraic
R : Type u_5
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_6
inst✝³ : CommRing S
inst✝² : Nontrivial R
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : S
⊢ IsAlgebraic R x

Tactic:
obtain ⟨x, s, rfl⟩ := IsLocalization.mk'_surjective M x

Result:
case isAlgebraic.intro.intro
R : Type u_5
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_6
inst✝³ : CommRing S
inst✝² : Nontrivial R
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : R
s : ↥M
⊢ IsAlgebraic R (mk' S x s)

Proof state:
case neg.refine_1
R : Type u_5
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_6
inst✝³ : CommRing S
inst✝² : Nontrivial R
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : R
s : ↥M
hs : ¬↑s = 0
e : s • X - C x = 0
⊢ False

Tactic:
apply hs

Result:
case neg.refine_1
R : Type u_5
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_6
inst✝³ : CommRing S
inst✝² : Nontrivial R
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : R
s : ↥M
hs : ¬↑s = 0
e : s • X - C x = 0
⊢ ↑s = 0

Proof state:
case pos
R : Type u_5
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_6
inst✝³ : CommRing S
inst✝² : Nontrivial R
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : R
s : ↥M
hs : ↑s = 0
⊢ IsAlgebraic R (mk' S x s)

Tactic:
have := IsLocalization.mk'_spec S x s

Result:
case pos
R : Type u_5
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_6
inst✝³ : CommRing S
inst✝² : Nontrivial R
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : R
s : ↥M
hs : ↑s = 0
this : mk' S x s * (algebraMap R S) ↑s = (algebraMap R S) x
⊢ IsAlgebraic R (mk' S x s)

Proof state:
case neg
R : Type u_5
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_6
inst✝³ : CommRing S
inst✝² : Nontrivial R
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : R
s : ↥M
hs : ¬↑s = 0
⊢ IsAlgebraic R (mk' S x s)

Tactic:
refine ⟨s • X - C x, ?_, ?_⟩

Result:
case neg.refine_1
R : Type u_5
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_6
inst✝³ : CommRing S
inst✝² : Nontrivial R
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : R
s : ↥M
hs : ¬↑s = 0
⊢ s • X - C x ≠ 0

case neg.refine_2
R : Type u_5
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_6
inst✝³ : CommRing S
inst✝² : Nontrivial R
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : R
s : ↥M
hs : ¬↑s = 0
⊢ (aeval (mk' S x s)) (s • X - C x) = 0

Proof state:
case pos
R : Type u_5
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_6
inst✝³ : CommRing S
inst✝² : Nontrivial R
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : R
s : ↥M
hs : ↑s = 0
this : 0 = (algebraMap R S) x
⊢ IsAlgebraic R (mk' S x s)

Tactic:
exact ⟨X, X_ne_zero, by simp [IsLocalization.mk'_eq_mul_mk'_one x, ← this]⟩

Result:
no goals

Proof state:
case isAlgebraic.intro.intro
R : Type u_5
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_6
inst✝³ : CommRing S
inst✝² : Nontrivial R
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : R
s : ↥M
⊢ IsAlgebraic R (mk' S x s)

Tactic:
by_cases hs : (s : R) = 0

Result:
case pos
R : Type u_5
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_6
inst✝³ : CommRing S
inst✝² : Nontrivial R
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : R
s : ↥M
hs : ↑s = 0
⊢ IsAlgebraic R (mk' S x s)

case neg
R : Type u_5
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_6
inst✝³ : CommRing S
inst✝² : Nontrivial R
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : R
s : ↥M
hs : ¬↑s = 0
⊢ IsAlgebraic R (mk' S x s)