awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (goal)
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)) ⋯
⊢ Eq.{u_3 + 1} (α := A) ((aeval a : (a : (↥(integralClosure R S))[X]) → A) p : A) (0 : A)
have refine_2 : eval a (map (algebraMap (↥(integralClosure R S)) A) p) = 0
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]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (goal)
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
⊢ Eq.{u_3 + 1} (α := A) ((aeval a : (a : (↥(integralClosure R S))[X]) → A) p : A) (0 : A)
have refine_2₁ : eval a
    (map
      (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S A)
        (↑(Subalgebra.val (integralClosure R S)) : ↥(integralClosure R S) →+* S))
      p) =
  0
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]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (goal)
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
⊢ Eq.{u_3 + 1} (α := A) ((aeval a : (a : (↥(integralClosure R S))[X]) → A) p : A) (0 : A)
have refine_2₂ : eval a (map (algebraMap S A) (map (↑(Subalgebra.val (integralClosure R S)) : ↥(integralClosure R S) →+* S) p)) = 0
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]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (goal)
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
⊢ Eq.{u_3 + 1} (α := A) ((aeval a : (a : (↥(integralClosure R S))[X]) → A) p : A) (0 : A)
have refine_2₃ : eval a (map (algebraMap S A) (map (Subring.subtype (Subalgebra.toSubring (integralClosure R S))) p)) = 0
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]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (goal)
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
⊢ Eq.{u_3 + 1} (α := A) ((aeval a : (a : (↥(integralClosure R S))[X]) → A) p : A) (0 : A)
have refine_2₄ : eval a (map (algebraMap S A) (r • p_1)) = 0
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]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (goal)
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
⊢ Eq.{u_3 + 1} (α := A) ((aeval a : (a : (↥(integralClosure R S))[X]) → A) p : A) (0 : A)
have refine_2₅ : Eq.{u_3 + 1} (α := A) ((aeval a : (a : S[X]) → A) (r • p_1) : 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]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (goal)
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)
⊢ Eq.{u_3 + 1} (α := A) ((aeval a : (a : (↥(integralClosure R S))[X]) → A) p : A) (0 : A)
have refine_2₆ : Eq.{u_3 + 1} (α := A) ((AlgHom.restrictScalars R (aeval a) : (a : S[X]) → A) (r • p_1) : 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]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (goal)
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)
⊢ Eq.{u_3 + 1} (α := A) ((aeval a : (a : (↥(integralClosure R S))[X]) → A) p : A) (0 : A)
have refine_2₇ : HSMul.hSMul (β := A) r ((AlgHom.restrictScalars R (aeval a) : (a : S[X]) → A) p_1 : A) = 0
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]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (goal)
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
⊢ Eq.{u_3 + 1} (α := A) ((aeval a : (a : (↥(integralClosure R S))[X]) → A) p : A) (0 : A)
have refine_2₈ : HSMul.hSMul (β := A) r ((aeval a : (a : S[X]) → A) p_1 : A) = 0
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]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (goal)
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
⊢ Eq.{u_3 + 1} (α := A) ((aeval a : (a : (↥(integralClosure R S))[X]) → A) p : A) (0 : A)
have refine_2₉ : HSMul.hSMul (β := A) r 0 = 0
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]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (goal)
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
⊢ Eq.{u_3 + 1} (α := A) ((aeval a : (a : (↥(integralClosure R S))[X]) → A) p : A) (0 : A)
have refine_2₁₀ : Eq.{u_3 + 1} (α := A) 0 0
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]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (hypothesis)
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 R a
have this₁ : 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]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (goal)
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
⊢ IsAlgebraic R a
have pos : ∀ (r : R) (hr : r ≠ 0) (int : ∀ z ∈ Finset.image p.coeff p.support, IsIntegral R (r • z)), 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
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (goal)
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
⊢ IsAlgebraic R a
have 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
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
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (goal)
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
⊢ IsAlgebraic R a
have inl : Subsingleton A → IsAlgebraic R a
Tactic: cases subsingleton_or_nontrivial A