case intro.intro.intro
R : Type u_2
S : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
inst✝⁶ : CommRing S
L : Type u_1
inst✝⁵ : Field L
inst✝⁴ : Algebra R S
inst✝³ : Algebra S L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R S L
inst✝ : IsIntegralClosure S R L
h : Algebra.IsAlgebraic R L
inj : Function.Injective ↑(algebraMap R L)
a b : S
hb : b ≠ 0
c : { x // x ∈ integralClosure R L }
d : R
d_ne : d ≠ 0
hx : ↑(algebraMap S L) a / ↑(algebraMap S L) b * ↑(algebraMap R L) d = ↑c
⊢ ∃ c d x, d • a = b * c
R : Type u_2
S : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
inst✝⁶ : CommRing S
L : Type u_1
inst✝⁵ : Field L
inst✝⁴ : Algebra R S
inst✝³ : Algebra S L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R S L
inst✝ : IsIntegralClosure S R L
h : Algebra.IsAlgebraic R L
inj : Function.Injective ↑(algebraMap R L)
a b : S
hb : b ≠ 0
⊢ ∃ c d x, d • a = b * c
obtain ⟨c, d, d_ne, hx⟩ :=
  exists_integral_multiple (h (algebraMap _ L a / algebraMap _ L b))
    ((injective_iff_map_eq_zero _).mp inj)
case intro.intro.intro
R : Type u_2
S : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
inst✝⁶ : CommRing S
L : Type u_1
inst✝⁵ : Field L
inst✝⁴ : Algebra R S
inst✝³ : Algebra S L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R S L
inst✝ : IsIntegralClosure S R L
h : Algebra.IsAlgebraic R L
inj : Function.Injective ↑(algebraMap R L)
a b : S
hb : b ≠ 0
c : { x // x ∈ integralClosure R L }
d : R
d_ne : d ≠ 0
hx : ↑(algebraMap S L) a / ↑(algebraMap S L) b * ↑(algebraMap R L) d = ↑c
⊢ ↑(algebraMap S L) (d • a) = ↑(algebraMap S L) (b * mk' S ↑c (_ : ↑c ∈ integralClosure R L))
case intro.intro.intro
R : Type u_2
S : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
inst✝⁶ : CommRing S
L : Type u_1
inst✝⁵ : Field L
inst✝⁴ : Algebra R S
inst✝³ : Algebra S L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R S L
inst✝ : IsIntegralClosure S R L
h : Algebra.IsAlgebraic R L
inj : Function.Injective ↑(algebraMap R L)
a b : S
hb : b ≠ 0
c : { x // x ∈ integralClosure R L }
d : R
d_ne : d ≠ 0
hx : ↑(algebraMap S L) a / ↑(algebraMap S L) b * ↑(algebraMap R L) d = ↑c
⊢ ∃ c d x, d • a = b * c
refine'
  ⟨IsIntegralClosure.mk' S (c : L) c.2, d, d_ne, IsIntegralClosure.algebraMap_injective S R L _⟩
case intro.intro.intro
R : Type u_2
S : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
inst✝⁶ : CommRing S
L : Type u_1
inst✝⁵ : Field L
inst✝⁴ : Algebra R S
inst✝³ : Algebra S L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R S L
inst✝ : IsIntegralClosure S R L
h : Algebra.IsAlgebraic R L
inj : Function.Injective ↑(algebraMap R L)
a b : S
hb : b ≠ 0
c : { x // x ∈ integralClosure R L }
d : R
d_ne : d ≠ 0
hx : ↑(algebraMap S L) a / ↑(algebraMap S L) b * ↑(algebraMap R L) d = ↑c
⊢ ↑(algebraMap R L) d * ↑(algebraMap S L) a =
    ↑(algebraMap S L) b * (↑(algebraMap S L) a / ↑(algebraMap S L) b * ↑(algebraMap R L) d)
case intro.intro.intro
R : Type u_2
S : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
inst✝⁶ : CommRing S
L : Type u_1
inst✝⁵ : Field L
inst✝⁴ : Algebra R S
inst✝³ : Algebra S L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R S L
inst✝ : IsIntegralClosure S R L
h : Algebra.IsAlgebraic R L
inj : Function.Injective ↑(algebraMap R L)
a b : S
hb : b ≠ 0
c : { x // x ∈ integralClosure R L }
d : R
d_ne : d ≠ 0
hx : ↑(algebraMap S L) a / ↑(algebraMap S L) b * ↑(algebraMap R L) d = ↑c
⊢ ↑(algebraMap S L) (d • a) = ↑(algebraMap S L) (b * mk' S ↑c (_ : ↑c ∈ integralClosure R L))
simp only [Algebra.smul_def, RingHom.map_mul, IsIntegralClosure.algebraMap_mk', ← hx, ←
  IsScalarTower.algebraMap_apply]
case intro.intro.intro
R : Type u_2
S : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
inst✝⁶ : CommRing S
L : Type u_1
inst✝⁵ : Field L
inst✝⁴ : Algebra R S
inst✝³ : Algebra S L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R S L
inst✝ : IsIntegralClosure S R L
h : Algebra.IsAlgebraic R L
inj : Function.Injective ↑(algebraMap R L)
a b : S
hb : b ≠ 0
c : { x // x ∈ integralClosure R L }
d : R
d_ne : d ≠ 0
hx : ↑(algebraMap S L) a / ↑(algebraMap S L) b * ↑(algebraMap R L) d = ↑c
⊢ ↑(algebraMap S L) b ≠ 0
case intro.intro.intro
R : Type u_2
S : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
inst✝⁶ : CommRing S
L : Type u_1
inst✝⁵ : Field L
inst✝⁴ : Algebra R S
inst✝³ : Algebra S L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R S L
inst✝ : IsIntegralClosure S R L
h : Algebra.IsAlgebraic R L
inj : Function.Injective ↑(algebraMap R L)
a b : S
hb : b ≠ 0
c : { x // x ∈ integralClosure R L }
d : R
d_ne : d ≠ 0
hx : ↑(algebraMap S L) a / ↑(algebraMap S L) b * ↑(algebraMap R L) d = ↑c
⊢ ↑(algebraMap R L) d * ↑(algebraMap S L) a =
    ↑(algebraMap S L) b * (↑(algebraMap S L) a / ↑(algebraMap S L) b * ↑(algebraMap R L) d)
rw [← mul_assoc _ (_ / _), mul_div_cancel' (algebraMap S L a), mul_comm]
no goals
case intro.intro.intro
R : Type u_2
S : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
inst✝⁶ : CommRing S
L : Type u_1
inst✝⁵ : Field L
inst✝⁴ : Algebra R S
inst✝³ : Algebra S L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R S L
inst✝ : IsIntegralClosure S R L
h : Algebra.IsAlgebraic R L
inj : Function.Injective ↑(algebraMap R L)
a b : S
hb : b ≠ 0
c : { x // x ∈ integralClosure R L }
d : R
d_ne : d ≠ 0
hx : ↑(algebraMap S L) a / ↑(algebraMap S L) b * ↑(algebraMap R L) d = ↑c
⊢ ↑(algebraMap S L) b ≠ 0
exact mt ((injective_iff_map_eq_zero _).mp (IsIntegralClosure.algebraMap_injective S R L) _) hb