awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : NoZeroDivisors S
inst_8 : Algebra.IsAlgebraic R S
a : A
h : IsAlgebraic S a
p_1 : S[X]
hp : p_1 ≠ 0
eval0 : Eq.{u_3 + 1} (α := A) ((aeval a : (a : S[X]) → A) p_1 : A) (0 : A)
hRS : FaithfulSMul R S
this_1 : NoZeroDivisors R
this_2 : Nontrivial R
this : IsDomain R
r : R
hr : r ≠ 0
int : ∀ z ∈ Finset.image p_1.coeff p_1.support, IsIntegral R (r • z)
p : (↥(Subalgebra.toSubring (integralClosure R S)))[X] :=
  (r • p_1).toSubring (Subalgebra.toSubring (integralClosure R S)) ⋯
⊢ IsAlgebraic.{u_2, u_3} (↥(integralClosure R S)) a

Tactic:
⟨p, ?_, ?_⟩

Premises used: IsAlgebraic, And.intro, Exists.intro
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : NoZeroDivisors S
inst_8 : Algebra.IsAlgebraic R S
a : A
h : IsAlgebraic S a
p_1 : S[X]
hp : p_1 ≠ 0
eval0 : Eq.{u_3 + 1} (α := A) ((aeval a : (a : S[X]) → A) p_1 : A) (0 : A)
hRS : FaithfulSMul R S
this_1 : NoZeroDivisors R
this_2 : Nontrivial R
this : IsDomain R
r : R
hr : r ≠ 0
int : ∀ z ∈ Finset.image p_1.coeff p_1.support, IsIntegral R (r • z)
p : (↥(Subalgebra.toSubring (integralClosure R S)))[X] :=
  (r • p_1).toSubring (Subalgebra.toSubring (integralClosure R S)) ⋯
refine_1 : p ≠ 0
refine_2 : Eq.{u_3 + 1} (α := A) ((aeval a : (a : (↥(integralClosure R S))[X]) → A) p : A) (0 : A)
⊢ IsAlgebraic.{u_2, u_3} (↥(integralClosure R S)) a

Tactic:
refine ⟨p, ?_, ?_⟩
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : NoZeroDivisors S
inst_8 : Algebra.IsAlgebraic R S
a : A
h : IsAlgebraic S a
p_1 : S[X]
hp : p_1 ≠ 0
eval0 : Eq.{u_3 + 1} (α := A) ((aeval a : (a : S[X]) → A) p_1 : A) (0 : A)
hRS : FaithfulSMul R S
this_1 : NoZeroDivisors R
this_2 : Nontrivial R
this : IsDomain R
r : R
hr : r ≠ 0
int : ∀ z ∈ Finset.image p_1.coeff p_1.support, IsIntegral R (r • z)
p : (↥(Subalgebra.toSubring (integralClosure R S)))[X] :=
  (r • p_1).toSubring (Subalgebra.toSubring (integralClosure R S)) ⋯
⊢ p ≠ 0

Tactic:
simpa only [← Polynomial.map_ne_zero_iff (f := Subring.subtype _) (p := p)
        Subtype.val_injective, p, map_toSubring, smul_ne_zero_iff] using And.intro hr hp

Premises used: Subtype.val_injective, smul_ne_zero_iff, And.intro, Polynomial.map_toSubring, Polynomial.map_ne_zero_iff
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : NoZeroDivisors S
inst_8 : Algebra.IsAlgebraic R S
a : A
h : IsAlgebraic S a
p_1 : S[X]
hp : p_1 ≠ 0
eval0 : Eq.{u_3 + 1} (α := A) ((aeval a : (a : S[X]) → A) p_1 : A) (0 : A)
hRS : FaithfulSMul R S
this_1 : NoZeroDivisors R
this_2 : Nontrivial R
this : IsDomain R
r : R
hr : r ≠ 0
int : ∀ z ∈ Finset.image p_1.coeff p_1.support, IsIntegral R (r • z)
p : (↥(Subalgebra.toSubring (integralClosure R S)))[X] :=
  (r • p_1).toSubring (Subalgebra.toSubring (integralClosure R S)) ⋯
refine_2 : eval a (map (algebraMap (↥(integralClosure R S)) A) p) = 0
refine_2₁ :
  eval a
      (map
        (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S A)
          (↑(Subalgebra.val (integralClosure R S)) : ↥(integralClosure R S) →+* S))
        p) =
    0
refine_2₂ :
  eval a (map (algebraMap S A) (map (↑(Subalgebra.val (integralClosure R S)) : ↥(integralClosure R S) →+* S) p)) = 0
refine_2₃ : eval a (map (algebraMap S A) (map (Subring.subtype (Subalgebra.toSubring (integralClosure R S))) p)) = 0
refine_2₄ : eval a (map (algebraMap S A) (r • p_1)) = 0
refine_2₅ : Eq.{u_3 + 1} (α := A) ((aeval a : (a : S[X]) → A) (r • p_1) : A) (0 : A)
refine_2₆ : Eq.{u_3 + 1} (α := A) ((AlgHom.restrictScalars R (aeval a) : (a : S[X]) → A) (r • p_1) : A) (0 : A)
refine_2₇ : HSMul.hSMul (β := A) r ((AlgHom.restrictScalars R (aeval a) : (a : S[X]) → A) p_1 : A) = 0
refine_2₈ : HSMul.hSMul (β := A) r ((aeval a : (a : S[X]) → A) p_1 : A) = 0
refine_2₉ : HSMul.hSMul (β := A) r 0 = 0
refine_2₁₀ refine_2₁₁ : Eq.{u_3 + 1} (α := A) 0 0
⊢ Eq.{u_3 + 1} (α := A) ((aeval a : (a : (↥(integralClosure R S))[X]) → A) p : A) (0 : A)

Tactic:
rw [← eval_map_algebraMap, Subalgebra.algebraMap_eq, ← map_map, ← Subalgebra.toSubring_subtype,
      map_toSubring, eval_map_algebraMap, ← AlgHom.restrictScalars_apply R,
      map_smul, AlgHom.restrictScalars_apply, eval0, smul_zero]

Premises used: smul_zero, Subalgebra.algebraMap_eq, AlgHom.restrictScalars_apply, Polynomial.eval_map_algebraMap, Subalgebra.toSubring_subtype, Polynomial.map_toSubring, Polynomial.map_map, map_smul
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : NoZeroDivisors S
inst_8 : Algebra.IsAlgebraic R S
a : A
h : IsAlgebraic S a
p_1 : S[X]
hp : p_1 ≠ 0
eval0 : Eq.{u_3 + 1} (α := A) ((aeval a : (a : S[X]) → A) p_1 : A) (0 : A)
hRS : FaithfulSMul R S
this_1 : NoZeroDivisors R
this_2 : Nontrivial R
this : IsDomain R
r : R
hr : r ≠ 0
int : ∀ z ∈ Finset.image p_1.coeff p_1.support, IsIntegral R (r • z)
p : (↥(Subalgebra.toSubring (integralClosure R S)))[X] :=
  (r • p_1).toSubring (Subalgebra.toSubring (integralClosure R S)) ⋯
⊢ IsAlgebraic.{u_2, u_3} (↥(integralClosure R S)) a

Tactic:
have : IsAlgebraic (integralClosure R S) a := by
    refine ⟨p, ?_, ?_⟩
    · simpa only [← Polynomial.map_ne_zero_iff (f := Subring.subtype _) (p := p)
        Subtype.val_injective, p, map_toSubring, smul_ne_zero_iff] using And.intro hr hp
    rw [← eval_map_algebraMap, Subalgebra.algebraMap_eq, ← map_map, ← Subalgebra.toSubring_subtype,
      map_toSubring, eval_map_algebraMap, ← AlgHom.restrictScalars_apply R,
      map_smul, AlgHom.restrictScalars_apply, eval0, smul_zero]
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : NoZeroDivisors S
inst_8 : Algebra.IsAlgebraic R S
a : A
h : IsAlgebraic S a
p_1 : S[X]
hp : p_1 ≠ 0
eval0 : Eq.{u_3 + 1} (α := A) ((aeval a : (a : S[X]) → A) p_1 : A) (0 : A)
hRS : FaithfulSMul R S
this_1 : NoZeroDivisors R
this_2 : Nontrivial R
this_3 : IsDomain R
r : R
hr : r ≠ 0
int : ∀ z ∈ Finset.image p_1.coeff p_1.support, IsIntegral R (r • z)
p : (↥(Subalgebra.toSubring (integralClosure R S)))[X] :=
  (r • p_1).toSubring (Subalgebra.toSubring (integralClosure R S)) ⋯
this : IsAlgebraic.{u_2, u_3} (↥(integralClosure R S)) a
⊢ IsAlgebraic R a

Tactic:
restrictScalars_of_isIntegral _ this

Premises used: IsAlgebraic.restrictScalars_of_isIntegral
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : NoZeroDivisors S
inst_8 : Algebra.IsAlgebraic R S
a : A
h : IsAlgebraic S a
p_1 : S[X]
hp : p_1 ≠ 0
eval0 : Eq.{u_3 + 1} (α := A) ((aeval a : (a : S[X]) → A) p_1 : A) (0 : A)
hRS : FaithfulSMul R S
this_1 : NoZeroDivisors R
this_2 : Nontrivial R
this_3 : IsDomain R
r : R
hr : r ≠ 0
int : ∀ z ∈ Finset.image p_1.coeff p_1.support, IsIntegral R (r • z)
p : (↥(Subalgebra.toSubring (integralClosure R S)))[X] :=
  (r • p_1).toSubring (Subalgebra.toSubring (integralClosure R S)) ⋯
this : IsAlgebraic.{u_2, u_3} (↥(integralClosure R S)) a
⊢ IsAlgebraic R a

Tactic:
exact restrictScalars_of_isIntegral _ this

Premises used: IsAlgebraic.restrictScalars_of_isIntegral
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : NoZeroDivisors S
inst_8 : Algebra.IsAlgebraic R S
a : A
h : IsAlgebraic S a
p : S[X]
hp : p ≠ 0
eval0 : Eq.{u_3 + 1} (α := A) ((aeval a : (a : S[X]) → A) p : A) (0 : A)
hRS : FaithfulSMul R S
this_1 : NoZeroDivisors R
this_2 : Nontrivial R
this : IsDomain R
pos pos₁ pos₂ pos₃ :
  ∀ (r : R) (hr : r ≠ 0) (int : ∀ z ∈ Finset.image p.coeff p.support, IsIntegral R (r • z)), IsAlgebraic R a
pos₄ :
  ∀ (r : R) (hr : r ≠ 0) (int : ∀ z ∈ Finset.image p.coeff p.support, IsIntegral R (r • z))
    (this : IsAlgebraic.{u_2, u_3} (↥(integralClosure R S)) a), IsAlgebraic R a
⊢ IsAlgebraic R a

Tactic:
classical
  have ⟨r, hr, int⟩ := Algebra.IsAlgebraic.exists_integral_multiples R (p.support.image (coeff p))
  let p := (r • p).toSubring (integralClosure R S).toSubring fun s hs ↦ by
    obtain ⟨n, hn, rfl⟩ := mem_coeffs_iff.mp hs
    exact int _ (Finset.mem_image_of_mem _ <| support_smul _ _ hn)
  have : IsAlgebraic (integralClosure R S) a := by
    refine ⟨p, ?_, ?_⟩
    · simpa only [← Polynomial.map_ne_zero_iff (f := Subring.subtype _) (p := p)
        Subtype.val_injective, p, map_toSubring, smul_ne_zero_iff] using And.intro hr hp
    rw [← eval_map_algebraMap, Subalgebra.algebraMap_eq, ← map_map, ← Subalgebra.toSubring_subtype,
      map_toSubring, eval_map_algebraMap, ← AlgHom.restrictScalars_apply R,
      map_smul, AlgHom.restrictScalars_apply, eval0, smul_zero]
  exact restrictScalars_of_isIntegral _ this
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : NoZeroDivisors S
alg : Algebra.IsAlgebraic R S
a : A
h : IsIntegral S a
inl : Subsingleton A → IsAlgebraic R a
inr : Nontrivial A → IsAlgebraic R a
⊢ IsAlgebraic R a

Tactic:
cases subsingleton_or_nontrivial A

Premises used: subsingleton_or_nontrivial
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : NoZeroDivisors S
alg : Algebra.IsAlgebraic R S
a : A
h : IsIntegral S a
h_1 : Subsingleton A
⊢ Nontrivial R

Tactic:
have := Algebra.IsAlgebraic.nontrivial R S
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : NoZeroDivisors S
alg : Algebra.IsAlgebraic R S
a : A
h : IsIntegral S a
h_1 : Subsingleton A
this : Nontrivial R
⊢ IsAlgebraic R a

Tactic:
Subsingleton.elim a 0 ▸ isAlgebraic_zero

Premises used: Eq.rec, isAlgebraic_zero, Subsingleton.elim, OfNat.ofNat, Eq.symm
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : NoZeroDivisors S
alg : Algebra.IsAlgebraic R S
a : A
h : IsIntegral S a
h_1 : Subsingleton A
this : Nontrivial R
⊢ IsAlgebraic R a

Tactic:
exact Subsingleton.elim a 0 ▸ isAlgebraic_zero
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : NoZeroDivisors S
alg : Algebra.IsAlgebraic R S
a : A
h : IsIntegral S a
h_1 : Nontrivial A
⊢ Nontrivial S

Tactic:
have := Module.nontrivial S A
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : NoZeroDivisors S
alg : Algebra.IsAlgebraic R S
a : A
h : IsIntegral S a
h_1 : Nontrivial A
this : Nontrivial S
⊢ IsAlgebraic R a

Tactic:
h.isAlgebraic.restrictScalars _

Premises used: IsAlgebraic.restrictScalars, IsIntegral.isAlgebraic
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : NoZeroDivisors S
alg : Algebra.IsAlgebraic R S
a : A
h : IsIntegral S a
h_1 : Nontrivial A
this : Nontrivial S
⊢ IsAlgebraic R a

Tactic:
exact h.isAlgebraic.restrictScalars _

Premises used: IsAlgebraic.restrictScalars, IsIntegral.isAlgebraic
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
A : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
a : A
ha : IsAlgebraic R a
p : R[X]
h : p ≠ 0
eval0 : Eq.{u_3 + 1} (α := A) ((aeval a : (a : R[X]) → A) p : A) (0 : A)
⊢ Eq.{u_3 + 1} (α := A) ((aeval (-a) : (a : R[X]) → A) ((algEquivAevalNegX : (a : R[X]) → R[X]) p : R[X]) : A) (0 : A)

Tactic:
simpa [← comp_eq_aeval, aeval_comp]

Premises used: Polynomial.aeval_comp, Polynomial.comp_eq_aeval
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
A : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
a : A
ha : IsAlgebraic R a
r : R
⊢ IsAlgebraic R (r • a)

Tactic:
have ⟨_, hp, eval0⟩ := ha
  ⟨_, scaleRoots_ne_zero hp r, Algebra.smul_def r a ▸ scaleRoots_aeval_eq_zero eval0⟩

Premises used: IsAlgebraic, Eq.rec, Polynomial.scaleRoots_aeval_eq_zero, Polynomial.scaleRoots_ne_zero, _private.0.IsAlgebraic.smul.match_1, And.intro, Exists.intro, Polynomial.scaleRoots, HSMul.hSMul, Algebra.smul_def, Eq.symm
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
A : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
a : A
ha : IsAlgebraic R a
n : ℕ
⊢ IsAlgebraic R (n • a)

Tactic:
Nat.cast_smul_eq_nsmul R n a ▸ ha.smul _

Premises used: IsAlgebraic.smul, Eq.rec, Nat.cast_smul_eq_nsmul
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
A : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
a : A
ha : IsAlgebraic R a
n : ℤ
⊢ IsAlgebraic R (n • a)

Tactic:
Int.cast_smul_eq_zsmul R n a ▸ ha.smul _

Premises used: IsAlgebraic.smul, Eq.rec, Int.cast_smul_eq_zsmul
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
s : S
a : A
ha : IsAlgebraic R a
inst_5 : FaithfulSMul R S
rw : IsAlgebraic S (HSMul.hSMul (β := TensorProduct R S A) s (1 ⊗ₜ[R] a))
⊢ IsAlgebraic S (A := TensorProduct R S A) (s ⊗ₜ[R] a)

Tactic:
rw [← mul_one s, ← smul_eq_mul, ← TensorProduct.smul_tmul']

Premises used: TensorProduct.smul_tmul', smul_eq_mul, mul_one
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
s : S
a : A
ha : IsAlgebraic R a
inst_5 : FaithfulSMul R S
have :
  ∀ (p : R[X]) (h : p ≠ 0) (eval0 : Eq.{u_3 + 1} (α := A) ((aeval a : (a : R[X]) → A) p : A) (0 : A)),
    IsAlgebraic S (HSMul.hSMul (β := TensorProduct R S A) s (1 ⊗ₜ[R] a))
⊢ IsAlgebraic S (HSMul.hSMul (β := TensorProduct R S A) s (1 ⊗ₜ[R] a))

Tactic:
have ⟨p, h, eval0⟩ := ha
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
s : S
a : A
ha : IsAlgebraic R a
inst_5 : FaithfulSMul R S
p : R[X]
h : p ≠ 0
eval0 : Eq.{u_3 + 1} (α := A) ((aeval a : (a : R[X]) → A) p : A) (0 : A)
⊢ IsAlgebraic S (HSMul.hSMul (β := TensorProduct R S A) s (1 ⊗ₜ[R] a))

Tactic:
.smul ⟨p.map (algebraMap R S),
    (Polynomial.map_ne_zero_iff <| FaithfulSMul.algebraMap_injective ..).mpr h, ?_⟩ _

Premises used: Iff.mpr, Algebra.algebraMap, IsAlgebraic.smul, FaithfulSMul.algebraMap_injective, And.intro, Exists.intro, Polynomial.map, Polynomial.map_ne_zero_iff
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
s : S
a : A
ha : IsAlgebraic R a
inst_5 : FaithfulSMul R S
p : R[X]
h : p ≠ 0
eval0 : Eq.{u_3 + 1} (α := A) ((aeval a : (a : R[X]) → A) p : A) (0 : A)
refine :
  Eq (α := TensorProduct R S A)
    ((aeval (1 ⊗ₜ[R] a) : (a : S[X]) → TensorProduct R S A) (map (algebraMap R S) p) : TensorProduct R S A)
    (0 : TensorProduct R S A)
⊢ IsAlgebraic S (HSMul.hSMul (β := TensorProduct R S A) s (1 ⊗ₜ[R] a))

Tactic:
refine .smul ⟨p.map (algebraMap R S),
    (Polynomial.map_ne_zero_iff <| FaithfulSMul.algebraMap_injective ..).mpr h, ?_⟩ _
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
s : S
a : A
ha : IsAlgebraic R a
inst_5 : FaithfulSMul R S
p : R[X]
h : p ≠ 0
eval0 : Eq.{u_3 + 1} (α := A) ((aeval a : (a : R[X]) → A) p : A) (0 : A)
a₁ :
  ∀ (x : R),
    Eq (α := TensorProduct R S A)
      ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S (TensorProduct R S A)) (algebraMap R S) :
            (a : R) → TensorProduct R S A)
          x :
        TensorProduct R S A)
      ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
              (↑Algebra.TensorProduct.includeRight : A →+* TensorProduct R S A) (algebraMap R A) :
            (a : R) → TensorProduct R S A)
          x :
        TensorProduct R S A)
⊢ Eq (α := R →+* TensorProduct R S A)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S (TensorProduct R S A)) (algebraMap R S))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (↑Algebra.TensorProduct.includeRight : A →+* TensorProduct R S A) (algebraMap R A))

Tactic:
ext
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
s : S
a : A
ha : IsAlgebraic R a
inst_5 : FaithfulSMul R S
p : R[X]
h : p ≠ 0
eval0 : Eq.{u_3 + 1} (α := A) ((aeval a : (a : R[X]) → A) p : A) (0 : A)
x : R
⊢ Eq (α := TensorProduct R S A)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S (TensorProduct R S A)) (algebraMap R S) :
          (a : R) → TensorProduct R S A)
        x :
      TensorProduct R S A)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
            (↑Algebra.TensorProduct.includeRight : A →+* TensorProduct R S A) (algebraMap R A) :
          (a : R) → TensorProduct R S A)
        x :
      TensorProduct R S A)

Tactic:
simp
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
s : S
a : A
ha : IsAlgebraic R a
inst_5 : FaithfulSMul R S
p : R[X]
h : p ≠ 0
eval0 : Eq.{u_3 + 1} (α := A) ((aeval a : (a : R[X]) → A) p : A) (0 : A)
rw :
  Eq (α := TensorProduct R S A)
    (((aeval ((Algebra.TensorProduct.includeRight : (a : A) → TensorProduct R S A) a) :
            S[X] →ₐ[S] TensorProduct R S A) :
          (a : S[X]) → TensorProduct R S A)
        (map (algebraMap R S) p) :
      TensorProduct R S A)
    (0 : TensorProduct R S A)
rw₁ :
  Eq (α := TensorProduct R S A)
    (((aeval (((↑Algebra.TensorProduct.includeRight : A →+* TensorProduct R S A) : (a : A) → TensorProduct R S A) a) :
            S[X] →ₐ[S] TensorProduct R S A) :
          (a : S[X]) → TensorProduct R S A)
        (map (algebraMap R S) p) :
      TensorProduct R S A)
    (0 : TensorProduct R S A)
rw₂ :
  Eq (α := TensorProduct R S A)
    (((↑Algebra.TensorProduct.includeRight : A →+* TensorProduct R S A) : (a : A) → TensorProduct R S A)
        ((aeval a : (a : R[X]) → A) p) :
      TensorProduct R S A)
    (0 : TensorProduct R S A)
rw₃ :
  Eq (α := TensorProduct R S A)
    (((↑Algebra.TensorProduct.includeRight : A →+* TensorProduct R S A) : (a : A) → TensorProduct R S A) 0) 0
rw₄ rw₅ : Eq (α := TensorProduct R S A) 0 0
⊢ Eq (α := TensorProduct R S A)
    ((aeval (1 ⊗ₜ[R] a) : (a : S[X]) → TensorProduct R S A) (map (algebraMap R S) p) : TensorProduct R S A)
    (0 : TensorProduct R S A)

Tactic:
rw [← Algebra.TensorProduct.includeRight_apply, ← AlgHom.coe_toRingHom (A := A),
    ← map_aeval_eq_aeval_map (by ext; simp), eval0, map_zero]

Premises used: AlgHom.coe_toRingHom, Algebra.TensorProduct.includeRight_apply, map_zero, Polynomial.map_aeval_eq_aeval_map
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : NoZeroDivisors R
a b : S
ha : IsAlgebraic R a
hb : IsAlgebraic R b
have : ∀ (ra : R) (a0 : ra ≠ 0) (int_a : IsIntegral R (ra • a)), IsAlgebraic R (a * b)
⊢ IsAlgebraic R (a * b)

Tactic:
have ⟨ra, a0, int_a⟩ := ha.exists_integral_multiple
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : NoZeroDivisors R
a b : S
ha : IsAlgebraic R a
hb : IsAlgebraic R b
ra : R
a0 : ra ≠ 0
int_a : IsIntegral R (ra • a)
have : ∀ (rb : R) (b0 : rb ≠ 0) (int_b : IsIntegral R (rb • b)), IsAlgebraic R (a * b)
⊢ IsAlgebraic R (a * b)

Tactic:
have ⟨rb, b0, int_b⟩ := hb.exists_integral_multiple
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : NoZeroDivisors R
a b : S
ha : IsAlgebraic R a
hb : IsAlgebraic R b
ra : R
a0 : ra ≠ 0
int_a : IsIntegral R (ra • a)
rb : R
b0 : rb ≠ 0
int_b : IsIntegral R (rb • b)
⊢ IsAlgebraic R (a * b)

Tactic:
IsAlgebraic.iff_exists_smul_integral.mpr ⟨_, mul_ne_zero a0 b0, ?_⟩

Premises used: Iff.mpr, IsAlgebraic.iff_exists_smul_integral, And.intro, Exists.intro, mul_ne_zero
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : NoZeroDivisors R
a b : S
ha : IsAlgebraic R a
hb : IsAlgebraic R b
ra : R
a0 : ra ≠ 0
int_a : IsIntegral R (ra • a)
rb : R
b0 : rb ≠ 0
int_b : IsIntegral R (rb • b)
refine : IsIntegral R ((ra * rb) • (a * b))
⊢ IsAlgebraic R (a * b)

Tactic:
refine IsAlgebraic.iff_exists_smul_integral.mpr ⟨_, mul_ne_zero a0 b0, ?_⟩

Premises used: Iff.mpr, IsAlgebraic.iff_exists_smul_integral, And.intro, Exists.intro, mul_ne_zero
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : NoZeroDivisors R
a b : S
ha : IsAlgebraic R a
hb : IsAlgebraic R b
ra : R
a0 : ra ≠ 0
int_a : IsIntegral R (ra • a)
rb : R
b0 : rb ≠ 0
int_b : IsIntegral R (rb • b)
simp_rw : IsIntegral R (ra • a * rb • b)
⊢ IsIntegral R ((ra * rb) • (a * b))

Tactic:
simp_rw [Algebra.smul_def, map_mul, mul_mul_mul_comm, ← Algebra.smul_def]

Premises used: mul_mul_mul_comm, map_mul, Algebra.smul_def
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : NoZeroDivisors R
a b : S
ha : IsAlgebraic R a
hb : IsAlgebraic R b
ra : R
a0 : ra ≠ 0
int_a : IsIntegral R (ra • a)
rb : R
b0 : rb ≠ 0
int_b : IsIntegral R (rb • b)
⊢ IsIntegral R (ra • a * rb • b)

Tactic:
int_a.mul int_b

Premises used: IsIntegral.mul
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : NoZeroDivisors R
a b : S
ha : IsAlgebraic R a
hb : IsAlgebraic R b
ra : R
a0 : ra ≠ 0
int_a : IsIntegral R (ra • a)
rb : R
b0 : rb ≠ 0
int_b : IsIntegral R (rb • b)
⊢ IsIntegral R (ra • a * rb • b)

Tactic:
exact int_a.mul int_b

Premises used: IsIntegral.mul