case intro.intro
R : Type u_1
A : Type u_3
B : Type u_2
S : Type ?u.811467
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : R →+* S
x : A
y : B
p : R[X]
hp : Monic p
hp' : eval₂ (_root_.algebraMap R B) y p = 0
⊢ IsIntegral A (x ⊗ₜ[R] y)
R : Type u_1
A : Type u_3
B : Type u_2
S : Type ?u.811467
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : R →+* S
x : A
y : B
h : IsIntegral R y
⊢ IsIntegral A (x ⊗ₜ[R] y)
obtain ⟨p, hp, hp'⟩ := h
case intro.intro.refine'_1
R : Type u_1
A : Type u_3
B : Type u_2
S : Type ?u.811467
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : R →+* S
x : A
y : B
p : R[X]
hp : Monic p
hp' : eval₂ (_root_.algebraMap R B) y p = 0
⊢ Monic (scaleRoots (Polynomial.map (_root_.algebraMap R A) p) x)

case intro.intro.refine'_2
R : Type u_1
A : Type u_3
B : Type u_2
S : Type ?u.811467
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : R →+* S
x : A
y : B
p : R[X]
hp : Monic p
hp' : eval₂ (_root_.algebraMap R B) y p = 0
⊢ eval₂ (_root_.algebraMap A (A ⊗[R] B)) (x ⊗ₜ[R] y) (scaleRoots (Polynomial.map (_root_.algebraMap R A) p) x) = 0
case intro.intro
R : Type u_1
A : Type u_3
B : Type u_2
S : Type ?u.811467
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : R →+* S
x : A
y : B
p : R[X]
hp : Monic p
hp' : eval₂ (_root_.algebraMap R B) y p = 0
⊢ IsIntegral A (x ⊗ₜ[R] y)
refine' ⟨(p.map (_root_.algebraMap R A)).scaleRoots x, _, _⟩
case h.e'_2.h.e'_6
R : Type u_1
A : Type u_3
B : Type u_2
S : Type ?u.811467
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : R →+* S
x : A
y : B
p : R[X]
hp : Monic p
hp' : eval₂ (_root_.algebraMap R B) y p = 0
⊢ x ⊗ₜ[R] y = ↑Algebra.TensorProduct.includeLeftRingHom x * ?intro.intro.refine'_2.convert_2

case h.e'_3
R : Type u_1
A : Type u_3
B : Type u_2
S : Type ?u.811467
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : R →+* S
x : A
y : B
p : R[X]
hp : Monic p
hp' : eval₂ (_root_.algebraMap R B) y p = 0
⊢ 0 =
    ↑Algebra.TensorProduct.includeLeftRingHom x ^ natDegree (Polynomial.map (_root_.algebraMap R A) p) *
      eval₂ Algebra.TensorProduct.includeLeftRingHom ?intro.intro.refine'_2.convert_2
        (Polynomial.map (_root_.algebraMap R A) p)

case intro.intro.refine'_2.convert_2
R : Type u_1
A : Type u_3
B : Type u_2
S : Type ?u.811467
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : R →+* S
x : A
y : B
p : R[X]
hp : Monic p
hp' : eval₂ (_root_.algebraMap R B) y p = 0
⊢ A ⊗[R] B
case intro.intro.refine'_2
R : Type u_1
A : Type u_3
B : Type u_2
S : Type ?u.811467
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : R →+* S
x : A
y : B
p : R[X]
hp : Monic p
hp' : eval₂ (_root_.algebraMap R B) y p = 0
⊢ eval₂ (_root_.algebraMap A (A ⊗[R] B)) (x ⊗ₜ[R] y) (scaleRoots (Polynomial.map (_root_.algebraMap R A) p) x) = 0
convert Polynomial.scaleRoots_eval₂_mul (R := A ⊗[R] B) (S := A)
    Algebra.TensorProduct.includeLeftRingHom (?_) x
case h.e'_2.h.e'_6
R : Type u_1
A : Type u_3
B : Type u_2
S : Type ?u.811467
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : R →+* S
x : A
y : B
p : R[X]
hp : Monic p
hp' : eval₂ (_root_.algebraMap R B) y p = 0
⊢ x ⊗ₜ[R] y = ↑Algebra.TensorProduct.includeLeftRingHom x * 1 ⊗ₜ[R] y

case h.e'_3
R : Type u_1
A : Type u_3
B : Type u_2
S : Type ?u.811467
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : R →+* S
x : A
y : B
p : R[X]
hp : Monic p
hp' : eval₂ (_root_.algebraMap R B) y p = 0
⊢ 0 =
    ↑Algebra.TensorProduct.includeLeftRingHom x ^ natDegree (Polynomial.map (_root_.algebraMap R A) p) *
      eval₂ Algebra.TensorProduct.includeLeftRingHom (1 ⊗ₜ[R] y) (Polynomial.map (_root_.algebraMap R A) p)
case h.e'_2.h.e'_6
R : Type u_1
A : Type u_3
B : Type u_2
S : Type ?u.811467
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : R →+* S
x : A
y : B
p : R[X]
hp : Monic p
hp' : eval₂ (_root_.algebraMap R B) y p = 0
⊢ x ⊗ₜ[R] y = ↑Algebra.TensorProduct.includeLeftRingHom x * ?intro.intro.refine'_2.convert_2

case h.e'_3
R : Type u_1
A : Type u_3
B : Type u_2
S : Type ?u.811467
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : R →+* S
x : A
y : B
p : R[X]
hp : Monic p
hp' : eval₂ (_root_.algebraMap R B) y p = 0
⊢ 0 =
    ↑Algebra.TensorProduct.includeLeftRingHom x ^ natDegree (Polynomial.map (_root_.algebraMap R A) p) *
      eval₂ Algebra.TensorProduct.includeLeftRingHom ?intro.intro.refine'_2.convert_2
        (Polynomial.map (_root_.algebraMap R A) p)

case intro.intro.refine'_2.convert_2
R : Type u_1
A : Type u_3
B : Type u_2
S : Type ?u.811467
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : R →+* S
x : A
y : B
p : R[X]
hp : Monic p
hp' : eval₂ (_root_.algebraMap R B) y p = 0
⊢ A ⊗[R] B
any_goals exact 1 ⊗ₜ y
case intro.intro.refine'_1
R : Type u_1
A : Type u_3
B : Type u_2
S : Type ?u.811467
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : R →+* S
x : A
y : B
p : R[X]
hp : Monic p
hp' : eval₂ (_root_.algebraMap R B) y p = 0
⊢ Monic (Polynomial.map (_root_.algebraMap R A) p)
case intro.intro.refine'_1
R : Type u_1
A : Type u_3
B : Type u_2
S : Type ?u.811467
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : R →+* S
x : A
y : B
p : R[X]
hp : Monic p
hp' : eval₂ (_root_.algebraMap R B) y p = 0
⊢ Monic (scaleRoots (Polynomial.map (_root_.algebraMap R A) p) x)
rw [Polynomial.monic_scaleRoots_iff]
no goals
case intro.intro.refine'_1
R : Type u_1
A : Type u_3
B : Type u_2
S : Type ?u.811467
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : R →+* S
x : A
y : B
p : R[X]
hp : Monic p
hp' : eval₂ (_root_.algebraMap R B) y p = 0
⊢ Monic (Polynomial.map (_root_.algebraMap R A) p)
exact hp.map _
no goals
case intro.intro.refine'_2.convert_2
R : Type u_1
A : Type u_3
B : Type u_2
S : Type ?u.811467
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : R →+* S
x : A
y : B
p : R[X]
hp : Monic p
hp' : eval₂ (_root_.algebraMap R B) y p = 0
⊢ A ⊗[R] B
exact 1 ⊗ₜ y
no goals
case h.e'_2.h.e'_6
R : Type u_1
A : Type u_3
B : Type u_2
S : Type ?u.811467
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : R →+* S
x : A
y : B
p : R[X]
hp : Monic p
hp' : eval₂ (_root_.algebraMap R B) y p = 0
⊢ x ⊗ₜ[R] y = ↑Algebra.TensorProduct.includeLeftRingHom x * 1 ⊗ₜ[R] y
simp only [Algebra.TensorProduct.includeLeftRingHom_apply,
  Algebra.TensorProduct.tmul_mul_tmul, mul_one, one_mul]
case h.e'_3
R : Type u_1
A : Type u_3
B : Type u_2
S : Type ?u.811467
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : R →+* S
x : A
y : B
p : R[X]
hp : Monic p
hp' : eval₂ (_root_.algebraMap R B) y p = 0
⊢ 0 =
    (x ^ natDegree (Polynomial.map (_root_.algebraMap R A) p)) ⊗ₜ[R] 1 *
      eval₂ Algebra.TensorProduct.includeLeftRingHom (1 ⊗ₜ[R] y) (Polynomial.map (_root_.algebraMap R A) p)
case h.e'_3
R : Type u_1
A : Type u_3
B : Type u_2
S : Type ?u.811467
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : R →+* S
x : A
y : B
p : R[X]
hp : Monic p
hp' : eval₂ (_root_.algebraMap R B) y p = 0
⊢ 0 =
    ↑Algebra.TensorProduct.includeLeftRingHom x ^ natDegree (Polynomial.map (_root_.algebraMap R A) p) *
      eval₂ Algebra.TensorProduct.includeLeftRingHom (1 ⊗ₜ[R] y) (Polynomial.map (_root_.algebraMap R A) p)
simp only [Algebra.TensorProduct.includeLeftRingHom_apply, Algebra.TensorProduct.tmul_pow,
  one_pow]
case h.e'_3.h.e'_6
R : Type u_1
A : Type u_3
B : Type u_2
S : Type ?u.811467
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : R →+* S
x : A
y : B
p : R[X]
hp : Monic p
hp' : eval₂ (_root_.algebraMap R B) y p = 0
⊢ eval₂ Algebra.TensorProduct.includeLeftRingHom (1 ⊗ₜ[R] y) (Polynomial.map (_root_.algebraMap R A) p) = 0
case h.e'_3
R : Type u_1
A : Type u_3
B : Type u_2
S : Type ?u.811467
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : R →+* S
x : A
y : B
p : R[X]
hp : Monic p
hp' : eval₂ (_root_.algebraMap R B) y p = 0
⊢ 0 =
    (x ^ natDegree (Polynomial.map (_root_.algebraMap R A) p)) ⊗ₜ[R] 1 *
      eval₂ Algebra.TensorProduct.includeLeftRingHom (1 ⊗ₜ[R] y) (Polynomial.map (_root_.algebraMap R A) p)
convert (MulZeroClass.mul_zero (M₀ := A ⊗[R] B) _).symm
case h.e'_3.h.e'_6
R : Type u_1
A : Type u_3
B : Type u_2
S : Type ?u.811467
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : R →+* S
x : A
y : B
p : R[X]
hp : Monic p
hp' : eval₂ (_root_.algebraMap R B) y p = 0
⊢ eval₂ (↑Algebra.TensorProduct.includeRight) (1 ⊗ₜ[R] y) (Polynomial.map (_root_.algebraMap R B) p) = 0
case h.e'_3.h.e'_6
R : Type u_1
A : Type u_3
B : Type u_2
S : Type ?u.811467
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : R →+* S
x : A
y : B
p : R[X]
hp : Monic p
hp' : eval₂ (_root_.algebraMap R B) y p = 0
⊢ eval₂ Algebra.TensorProduct.includeLeftRingHom (1 ⊗ₜ[R] y) (Polynomial.map (_root_.algebraMap R A) p) = 0
erw [Polynomial.eval₂_map, Algebra.TensorProduct.includeLeft_comp_algebraMap,
  ← Polynomial.eval₂_map]
case h.e'_3
R : Type u_1
A : Type u_3
B : Type u_2
S : Type ?u.811467
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : R →+* S
x : A
y : B
p : R[X]
hp : Monic p
hp' : eval₂ (_root_.algebraMap R B) y p = 0
⊢ 0 = ↑↑Algebra.TensorProduct.includeRight (eval y (Polynomial.map (_root_.algebraMap R B) p))
case h.e'_3.h.e'_6
R : Type u_1
A : Type u_3
B : Type u_2
S : Type ?u.811467
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : R →+* S
x : A
y : B
p : R[X]
hp : Monic p
hp' : eval₂ (_root_.algebraMap R B) y p = 0
⊢ eval₂ (↑Algebra.TensorProduct.includeRight) (1 ⊗ₜ[R] y) (Polynomial.map (_root_.algebraMap R B) p) = 0
convert Polynomial.eval₂_at_apply
  (Algebra.TensorProduct.includeRight : B →ₐ[R] A ⊗[R] B).toRingHom y
no goals
case h.e'_3
R : Type u_1
A : Type u_3
B : Type u_2
S : Type ?u.811467
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : R →+* S
x : A
y : B
p : R[X]
hp : Monic p
hp' : eval₂ (_root_.algebraMap R B) y p = 0
⊢ 0 = ↑↑Algebra.TensorProduct.includeRight (eval y (Polynomial.map (_root_.algebraMap R B) p))
rw [Polynomial.eval_map, hp', _root_.map_zero]