-- Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean
theorem isField_of_isIntegral_of_isField {R S : Type*} [CommRing R] [CommRing S]
    [Algebra R S] [Algebra.IsIntegral R S]
    (hRS : Function.Injective (algebraMap R S)) (hS : IsField S) : IsField R

Proof state:
case intro
R : Type u_6
S : Type u_7
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Algebra.IsIntegral R S
hRS : Function.Injective ⇑(algebraMap R S)
hS : IsField S
this✝ : Nontrivial S
this : Nontrivial R
a : R
ha : a ≠ 0
a_inv : S
ha_inv : (algebraMap R S) a * a_inv = 1
⊢ ∃ b, a * b = 1

Tactic:
letI : Invertible a_inv := (Units.mkOfMulEqOne a_inv _ <| mul_comm _ a_inv ▸ ha_inv).invertible

Result:
case intro
R : Type u_6
S : Type u_7
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Algebra.IsIntegral R S
hRS : Function.Injective ⇑(algebraMap R S)
hS : IsField S
this✝¹ : Nontrivial S
this✝ : Nontrivial R
a : R
ha : a ≠ 0
a_inv : S
ha_inv : (algebraMap R S) a * a_inv = 1
this : Invertible a_inv := (Units.mkOfMulEqOne a_inv ((algebraMap R S) a) ⋯).invertible
⊢ ∃ b, a * b = 1

Proof state:
R : Type u_6
S : Type u_7
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Algebra.IsIntegral R S
hRS : Function.Injective ⇑(algebraMap R S)
hS : IsField S
this : Nontrivial S
⊢ IsField R

Tactic:
have := Module.nontrivial R S

Result:
R : Type u_6
S : Type u_7
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Algebra.IsIntegral R S
hRS : Function.Injective ⇑(algebraMap R S)
hS : IsField S
this✝ : Nontrivial S
this : Nontrivial R
⊢ IsField R

Proof state:
R : Type u_6
S : Type u_7
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Algebra.IsIntegral R S
hRS : Function.Injective ⇑(algebraMap R S)
hS : IsField S
this✝ : Nontrivial S
this : Nontrivial R
a : R
ha : a ≠ 0
⊢ ∃ b, a * b = 1

Tactic:
obtain ⟨a_inv, ha_inv⟩ := hS.mul_inv_cancel fun h ↦ ha (hRS (h.trans (RingHom.map_zero _).symm))

Result:
case intro
R : Type u_6
S : Type u_7
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Algebra.IsIntegral R S
hRS : Function.Injective ⇑(algebraMap R S)
hS : IsField S
this✝ : Nontrivial S
this : Nontrivial R
a : R
ha : a ≠ 0
a_inv : S
ha_inv : (algebraMap R S) a * a_inv = 1
⊢ ∃ b, a * b = 1

Proof state:
case h
R : Type u_6
S : Type u_7
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Algebra.IsIntegral R S
hRS : Function.Injective ⇑(algebraMap R S)
hS : IsField S
this✝¹ : Nontrivial S
this✝ : Nontrivial R
a : R
ha : a ≠ 0
a_inv : S
ha_inv : (algebraMap R S) a * a_inv = 1
this : Invertible a_inv := (Units.mkOfMulEqOne a_inv ((algebraMap R S) a) ⋯).invertible
p : R[X]
p_monic : p.Monic
hp : eval₂ (algebraMap R S) a_inv p = 0
⊢ (aeval ((algebraMap R S) a)) p.reverse = 0

Tactic:
rwa [← eval₂_reverse_eq_zero_iff] at hp

Result:
no goals

Proof state:
case intro.intro.intro
R : Type u_6
S : Type u_7
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Algebra.IsIntegral R S
hRS : Function.Injective ⇑(algebraMap R S)
hS : IsField S
this✝¹ : Nontrivial S
this✝ : Nontrivial R
a : R
ha : a ≠ 0
a_inv : S
ha_inv : (algebraMap R S) a * a_inv = 1
this : Invertible a_inv := (Units.mkOfMulEqOne a_inv ((algebraMap R S) a) ⋯).invertible
p : R[X]
p_monic : p.Monic
hp : eval₂ (algebraMap R S) a_inv p = 0
⊢ ∃ b, a * b = 1

Tactic:
use -p.reverse.divX.eval a

Result:
case h
R : Type u_6
S : Type u_7
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Algebra.IsIntegral R S
hRS : Function.Injective ⇑(algebraMap R S)
hS : IsField S
this✝¹ : Nontrivial S
this✝ : Nontrivial R
a : R
ha : a ≠ 0
a_inv : S
ha_inv : (algebraMap R S) a * a_inv = 1
this : Invertible a_inv := (Units.mkOfMulEqOne a_inv ((algebraMap R S) a) ⋯).invertible
p : R[X]
p_monic : p.Monic
hp : eval₂ (algebraMap R S) a_inv p = 0
⊢ a * -eval a p.reverse.divX = 1

Proof state:
case h
R : Type u_6
S : Type u_7
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Algebra.IsIntegral R S
hRS : Function.Injective ⇑(algebraMap R S)
hS : IsField S
this✝¹ : Nontrivial S
this✝ : Nontrivial R
a : R
ha : a ≠ 0
a_inv : S
ha_inv : (algebraMap R S) a * a_inv = 1
this : Invertible a_inv := (Units.mkOfMulEqOne a_inv ((algebraMap R S) a) ⋯).invertible
p : R[X]
p_monic : p.Monic
hp : eval₂ (algebraMap R S) a_inv p = 0
⊢ a * -eval a p.reverse.divX = 1

Tactic:
nth_rewrite 1 [mul_neg, ← eval_X (x := a), ← eval_mul, ← p_monic, ← coeff_zero_reverse,
  ← add_eq_zero_iff_neg_eq, ← eval_C (a := p.reverse.coeff 0), ← eval_add, X_mul_divX_add,
  ← (injective_iff_map_eq_zero' _).mp hRS, ← aeval_algebraMap_apply_eq_algebraMap_eval]

Result:
case h
R : Type u_6
S : Type u_7
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Algebra.IsIntegral R S
hRS : Function.Injective ⇑(algebraMap R S)
hS : IsField S
this✝¹ : Nontrivial S
this✝ : Nontrivial R
a : R
ha : a ≠ 0
a_inv : S
ha_inv : (algebraMap R S) a * a_inv = 1
this : Invertible a_inv := (Units.mkOfMulEqOne a_inv ((algebraMap R S) a) ⋯).invertible
p : R[X]
p_monic : p.Monic
hp : eval₂ (algebraMap R S) a_inv p = 0
⊢ (aeval ((algebraMap R S) a)) p.reverse = 0

Proof state:
R : Type u_6
S : Type u_7
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Algebra.IsIntegral R S
hRS : Function.Injective ⇑(algebraMap R S)
hS : IsField S
this✝ : Nontrivial S
this : Nontrivial R
⊢ IsField R

Tactic:
refine ⟨⟨0, 1, zero_ne_one⟩, mul_comm, fun {a} ha ↦ ?_⟩

Result:
R : Type u_6
S : Type u_7
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Algebra.IsIntegral R S
hRS : Function.Injective ⇑(algebraMap R S)
hS : IsField S
this✝ : Nontrivial S
this : Nontrivial R
a : R
ha : a ≠ 0
⊢ ∃ b, a * b = 1

Proof state:
case intro
R : Type u_6
S : Type u_7
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Algebra.IsIntegral R S
hRS : Function.Injective ⇑(algebraMap R S)
hS : IsField S
this✝¹ : Nontrivial S
this✝ : Nontrivial R
a : R
ha : a ≠ 0
a_inv : S
ha_inv : (algebraMap R S) a * a_inv = 1
this : Invertible a_inv := (Units.mkOfMulEqOne a_inv ((algebraMap R S) a) ⋯).invertible
⊢ ∃ b, a * b = 1

Tactic:
obtain ⟨p, p_monic, hp⟩ := Algebra.IsIntegral.isIntegral (R := R) a_inv

Result:
case intro.intro.intro
R : Type u_6
S : Type u_7
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Algebra.IsIntegral R S
hRS : Function.Injective ⇑(algebraMap R S)
hS : IsField S
this✝¹ : Nontrivial S
this✝ : Nontrivial R
a : R
ha : a ≠ 0
a_inv : S
ha_inv : (algebraMap R S) a * a_inv = 1
this : Invertible a_inv := (Units.mkOfMulEqOne a_inv ((algebraMap R S) a) ⋯).invertible
p : R[X]
p_monic : p.Monic
hp : eval₂ (algebraMap R S) a_inv p = 0
⊢ ∃ b, a * b = 1

Proof state:
R : Type u_6
S : Type u_7
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Algebra.IsIntegral R S
hRS : Function.Injective ⇑(algebraMap R S)
hS : IsField S
⊢ IsField R

Tactic:
have := hS.nontrivial

Result:
R : Type u_6
S : Type u_7
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Algebra.IsIntegral R S
hRS : Function.Injective ⇑(algebraMap R S)
hS : IsField S
this : Nontrivial S
⊢ IsField R