-- Mathlib/RingTheory/Algebraic/Basic.lean
theorem IsLocalization.isAlgebraic [Nontrivial R] (M : Submonoid R) [IsLocalization M S] :
    Algebra.IsAlgebraic R S where
  isAlgebraic x

Proof state:
R : Type u
S : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Nontrivial R
M : Submonoid R
inst✝ : IsLocalization M S
x : S
⊢ IsAlgebraic R x

Tactic:
obtain rfl | hx := eq_or_ne x 0

Result:
case inl
R : Type u
S : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Nontrivial R
M : Submonoid R
inst✝ : IsLocalization M S
⊢ IsAlgebraic R 0

case inr
R : Type u
S : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Nontrivial R
M : Submonoid R
inst✝ : IsLocalization M S
x : S
hx : x ≠ 0
⊢ IsAlgebraic R x

Proof state:
case inr
R : Type u
S : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Nontrivial R
M : Submonoid R
inst✝ : IsLocalization M S
x : S
hx : x ≠ 0
⊢ IsAlgebraic R x

Tactic:
have ⟨⟨r, m⟩, h⟩ := surj M x

Result:
case inr
R : Type u
S : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Nontrivial R
M : Submonoid R
inst✝ : IsLocalization M S
x : S
hx : x ≠ 0
r : R
m : ↥M
h : x * (algebraMap R S) ↑(r, m).2 = (algebraMap R S) (r, m).1
⊢ IsAlgebraic R x

Proof state:
case inr
R : Type u
S : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Nontrivial R
M : Submonoid R
inst✝ : IsLocalization M S
x : S
hx : x ≠ 0
r : R
m : ↥M
h : x * (algebraMap R S) ↑(r, m).2 = (algebraMap R S) (r, m).1
⊢ IsAlgebraic R x

Tactic:
refine ⟨C m.1 * X - C r, fun eq ↦ hx ?_, by simpa [sub_eq_zero, mul_comm x] using h⟩

Result:
case inr
R : Type u
S : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Nontrivial R
M : Submonoid R
inst✝ : IsLocalization M S
x : S
hx : x ≠ 0
r : R
m : ↥M
h : x * (algebraMap R S) ↑(r, m).2 = (algebraMap R S) (r, m).1
eq : C ↑m * X - C r = 0
⊢ x = 0

Proof state:
case inr
R : Type u
S : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Nontrivial R
M : Submonoid R
inst✝ : IsLocalization M S
x : S
hx : x ≠ 0
r : R
m : ↥M
h : x * (algebraMap R S) ↑(r, m).2 = (algebraMap R S) (r, m).1
eq : C ↑m * X - C r = 0
⊢ x = 0

Tactic:
rwa [← eq_mk'_iff_mul_eq, show r = 0 by simpa using congr(coeff $eq 0), mk'_zero] at h

Result:
no goals

Proof state:
case inl
R : Type u
S : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Nontrivial R
M : Submonoid R
inst✝ : IsLocalization M S
⊢ IsAlgebraic R 0

Tactic:
exact isAlgebraic_zero

Result:
no goals

Proof state:
R : Type u
S : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Nontrivial R
M : Submonoid R
inst✝ : IsLocalization M S
x : S
hx : x ≠ 0
r : R
m : ↥M
h : x = mk' S (r, m).1 (r, m).2
eq : C ↑m * X - C r = 0
⊢ r = 0

Tactic:
simpa using congr(coeff $eq 0)

Result:
no goals

Proof state:
R : Type u
S : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Nontrivial R
M : Submonoid R
inst✝ : IsLocalization M S
x : S
hx : x ≠ 0
r : R
m : ↥M
h : x * (algebraMap R S) ↑(r, m).2 = (algebraMap R S) (r, m).1
⊢ (aeval x) (C ↑m * X - C r) = 0

Tactic:
simpa [sub_eq_zero, mul_comm x] using h

Result:
no goals