-- Mathlib/RingTheory/IntegralClosure/IsIntegral/Basic.lean
theorem IsIntegral.pair {x : A × B} (hx₁ : IsIntegral R x.1) (hx₂ : IsIntegral R x.2) :
    IsIntegral R x

Proof state:
case intro.intro.intro.intro
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
x : A × B
p₁ : R[X]
hp₁Monic : p₁.Monic
hp₁Eval : (aeval x.1) p₁ = 0
p₂ : R[X]
hp₂Monic : p₂.Monic
hp₂Eval : (aeval x.2) p₂ = 0
⊢ (aeval x) (p₁ * p₂) = 0

Tactic:
rw [aeval_prod_apply, aeval_mul, hp₁Eval, zero_mul, aeval_mul, hp₂Eval, mul_zero,
  Prod.zero_eq_mk]

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
x : A × B
hx₁ : IsIntegral R x.1
hx₂ : IsIntegral R x.2
⊢ IsIntegral R x

Tactic:
obtain ⟨p₁, ⟨hp₁Monic, hp₁Eval⟩⟩ := hx₁

Result:
case intro.intro
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
x : A × B
hx₂ : IsIntegral R x.2
p₁ : R[X]
hp₁Monic : p₁.Monic
hp₁Eval : eval₂ (algebraMap R A) x.1 p₁ = 0
⊢ IsIntegral R x

Proof state:
case intro.intro.intro.intro
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
x : A × B
p₁ : R[X]
hp₁Monic : p₁.Monic
hp₁Eval : eval₂ (algebraMap R A) x.1 p₁ = 0
p₂ : R[X]
hp₂Monic : p₂.Monic
hp₂Eval : eval₂ (algebraMap R B) x.2 p₂ = 0
⊢ IsIntegral R x

Tactic:
refine ⟨p₁ * p₂, ⟨hp₁Monic.mul hp₂Monic, ?_⟩⟩

Result:
case intro.intro.intro.intro
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
x : A × B
p₁ : R[X]
hp₁Monic : p₁.Monic
hp₁Eval : eval₂ (algebraMap R A) x.1 p₁ = 0
p₂ : R[X]
hp₂Monic : p₂.Monic
hp₂Eval : eval₂ (algebraMap R B) x.2 p₂ = 0
⊢ eval₂ (algebraMap R (A × B)) x (p₁ * p₂) = 0

Proof state:
case intro.intro.intro.intro
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
x : A × B
p₁ : R[X]
hp₁Monic : p₁.Monic
hp₁Eval : eval₂ (algebraMap R A) x.1 p₁ = 0
p₂ : R[X]
hp₂Monic : p₂.Monic
hp₂Eval : eval₂ (algebraMap R B) x.2 p₂ = 0
⊢ eval₂ (algebraMap R (A × B)) x (p₁ * p₂) = 0

Tactic:
rw [← aeval_def] at *

Result:
case intro.intro.intro.intro
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
x : A × B
p₁ : R[X]
hp₁Monic : p₁.Monic
hp₁Eval : (aeval x.1) p₁ = 0
p₂ : R[X]
hp₂Monic : p₂.Monic
hp₂Eval : (aeval x.2) p₂ = 0
⊢ (aeval x) (p₁ * p₂) = 0

Proof state:
case intro.intro
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
x : A × B
hx₂ : IsIntegral R x.2
p₁ : R[X]
hp₁Monic : p₁.Monic
hp₁Eval : eval₂ (algebraMap R A) x.1 p₁ = 0
⊢ IsIntegral R x

Tactic:
obtain ⟨p₂, ⟨hp₂Monic, hp₂Eval⟩⟩ := hx₂

Result:
case intro.intro.intro.intro
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
x : A × B
p₁ : R[X]
hp₁Monic : p₁.Monic
hp₁Eval : eval₂ (algebraMap R A) x.1 p₁ = 0
p₂ : R[X]
hp₂Monic : p₂.Monic
hp₂Eval : eval₂ (algebraMap R B) x.2 p₂ = 0
⊢ IsIntegral R x