awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic (goal)
Goal:
R : Type u_5
S : Type u_6
T : Type u_7
U : Type u_8
inst : CommRing R
inst_1 : Ring S
inst_2 : CommRing T
inst_3 : Ring U
inst_4 : Algebra R S
inst_5 : Algebra T U
φ : R →+* T
ψ : S →+* U
h : RingHom.comp (algebraMap T U) φ = ψ.comp (algebraMap R S)
a : S
ha : IsIntegral R a
p : R[X]
hp : p.Monic ∧ eval₂ (algebraMap R S) a p = 0
rw :
  Eq.{u_8 + 1} (α := U) (eval ((ψ : (a : S) → U) a) (Polynomial.map (algebraMap T U) (Polynomial.map φ p)) : U) (0 : U)
rw₁ :
  Eq.{u_8 + 1} (α := U) (eval ((ψ : (a : S) → U) a) (Polynomial.map (RingHom.comp (algebraMap T U) φ) p) : U) (0 : U)
rw₂ : Eq.{u_8 + 1} (α := U) (eval ((ψ : (a : S) → U) a) (Polynomial.map (ψ.comp (algebraMap R S)) p) : U) (0 : U)
rw₃ :
  Eq.{u_8 + 1} (α := U) (eval ((ψ : (a : S) → U) a) (Polynomial.map ψ (Polynomial.map (algebraMap R S) p)) : U) (0 : U)
⊢ eval₂ (algebraMap T U) ((ψ : (a : S) → U) a) (Polynomial.map φ p) = 0
have rw₄ : eval₂ ψ ((ψ : (a : S) → U) a) (Polynomial.map (algebraMap R S) p) = 0
Tactic: rw [← eval_map, map_map, h, ← map_map, eval_map, eval₂_at_apply, eval_map, hp.2, ψ.map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic (goal)
Goal:
R : Type u_5
S : Type u_6
T : Type u_7
U : Type u_8
inst : CommRing R
inst_1 : Ring S
inst_2 : CommRing T
inst_3 : Ring U
inst_4 : Algebra R S
inst_5 : Algebra T U
φ : R →+* T
ψ : S →+* U
h : RingHom.comp (algebraMap T U) φ = ψ.comp (algebraMap R S)
a : S
ha : IsIntegral R a
p : R[X]
hp : p.Monic ∧ eval₂ (algebraMap R S) a p = 0
rw :
  Eq.{u_8 + 1} (α := U) (eval ((ψ : (a : S) → U) a) (Polynomial.map (algebraMap T U) (Polynomial.map φ p)) : U) (0 : U)
rw₁ :
  Eq.{u_8 + 1} (α := U) (eval ((ψ : (a : S) → U) a) (Polynomial.map (RingHom.comp (algebraMap T U) φ) p) : U) (0 : U)
rw₂ : Eq.{u_8 + 1} (α := U) (eval ((ψ : (a : S) → U) a) (Polynomial.map (ψ.comp (algebraMap R S)) p) : U) (0 : U)
rw₃ :
  Eq.{u_8 + 1} (α := U) (eval ((ψ : (a : S) → U) a) (Polynomial.map ψ (Polynomial.map (algebraMap R S) p)) : U) (0 : U)
rw₄ : eval₂ ψ ((ψ : (a : S) → U) a) (Polynomial.map (algebraMap R S) p) = 0
⊢ eval₂ (algebraMap T U) ((ψ : (a : S) → U) a) (Polynomial.map φ p) = 0
have rw₅ : Eq.{u_8 + 1} (α := U) ((ψ : (a : S) → U) (eval a (Polynomial.map (algebraMap R S) p)) : U) (0 : U)
Tactic: rw [← eval_map, map_map, h, ← map_map, eval_map, eval₂_at_apply, eval_map, hp.2, ψ.map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic (goal)
Goal:
R : Type u_5
S : Type u_6
T : Type u_7
U : Type u_8
inst : CommRing R
inst_1 : Ring S
inst_2 : CommRing T
inst_3 : Ring U
inst_4 : Algebra R S
inst_5 : Algebra T U
φ : R →+* T
ψ : S →+* U
h : RingHom.comp (algebraMap T U) φ = ψ.comp (algebraMap R S)
a : S
ha : IsIntegral R a
p : R[X]
hp : p.Monic ∧ eval₂ (algebraMap R S) a p = 0
rw :
  Eq.{u_8 + 1} (α := U) (eval ((ψ : (a : S) → U) a) (Polynomial.map (algebraMap T U) (Polynomial.map φ p)) : U) (0 : U)
rw₁ :
  Eq.{u_8 + 1} (α := U) (eval ((ψ : (a : S) → U) a) (Polynomial.map (RingHom.comp (algebraMap T U) φ) p) : U) (0 : U)
rw₂ : Eq.{u_8 + 1} (α := U) (eval ((ψ : (a : S) → U) a) (Polynomial.map (ψ.comp (algebraMap R S)) p) : U) (0 : U)
rw₃ :
  Eq.{u_8 + 1} (α := U) (eval ((ψ : (a : S) → U) a) (Polynomial.map ψ (Polynomial.map (algebraMap R S) p)) : U) (0 : U)
rw₄ : eval₂ ψ ((ψ : (a : S) → U) a) (Polynomial.map (algebraMap R S) p) = 0
rw₅ : Eq.{u_8 + 1} (α := U) ((ψ : (a : S) → U) (eval a (Polynomial.map (algebraMap R S) p)) : U) (0 : U)
⊢ eval₂ (algebraMap T U) ((ψ : (a : S) → U) a) (Polynomial.map φ p) = 0
have rw₆ : Eq.{u_8 + 1} (α := U) ((ψ : (a : S) → U) (eval₂ (algebraMap R S) a p) : U) (0 : U)
Tactic: rw [← eval_map, map_map, h, ← map_map, eval_map, eval₂_at_apply, eval_map, hp.2, ψ.map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic (goal)
Goal:
R : Type u_5
S : Type u_6
T : Type u_7
U : Type u_8
inst : CommRing R
inst_1 : Ring S
inst_2 : CommRing T
inst_3 : Ring U
inst_4 : Algebra R S
inst_5 : Algebra T U
φ : R →+* T
ψ : S →+* U
h : RingHom.comp (algebraMap T U) φ = ψ.comp (algebraMap R S)
a : S
ha : IsIntegral R a
p : R[X]
hp : p.Monic ∧ eval₂ (algebraMap R S) a p = 0
rw :
  Eq.{u_8 + 1} (α := U) (eval ((ψ : (a : S) → U) a) (Polynomial.map (algebraMap T U) (Polynomial.map φ p)) : U) (0 : U)
rw₁ :
  Eq.{u_8 + 1} (α := U) (eval ((ψ : (a : S) → U) a) (Polynomial.map (RingHom.comp (algebraMap T U) φ) p) : U) (0 : U)
rw₂ : Eq.{u_8 + 1} (α := U) (eval ((ψ : (a : S) → U) a) (Polynomial.map (ψ.comp (algebraMap R S)) p) : U) (0 : U)
rw₃ :
  Eq.{u_8 + 1} (α := U) (eval ((ψ : (a : S) → U) a) (Polynomial.map ψ (Polynomial.map (algebraMap R S) p)) : U) (0 : U)
rw₄ : eval₂ ψ ((ψ : (a : S) → U) a) (Polynomial.map (algebraMap R S) p) = 0
rw₅ : Eq.{u_8 + 1} (α := U) ((ψ : (a : S) → U) (eval a (Polynomial.map (algebraMap R S) p)) : U) (0 : U)
rw₆ : Eq.{u_8 + 1} (α := U) ((ψ : (a : S) → U) (eval₂ (algebraMap R S) a p) : U) (0 : U)
⊢ eval₂ (algebraMap T U) ((ψ : (a : S) → U) a) (Polynomial.map φ p) = 0
have rw₇ : Eq.{u_8 + 1} (α := U) ((ψ : (a : S) → U) 0 : U) (0 : U)
Tactic: rw [← eval_map, map_map, h, ← map_map, eval_map, eval₂_at_apply, eval_map, hp.2, ψ.map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic (goal)
Goal:
R : Type u_5
S : Type u_6
T : Type u_7
U : Type u_8
inst : CommRing R
inst_1 : Ring S
inst_2 : CommRing T
inst_3 : Ring U
inst_4 : Algebra R S
inst_5 : Algebra T U
φ : R →+* T
ψ : S →+* U
h : RingHom.comp (algebraMap T U) φ = ψ.comp (algebraMap R S)
a : S
ha : IsIntegral R a
p : R[X]
hp : p.Monic ∧ eval₂ (algebraMap R S) a p = 0
rw :
  Eq.{u_8 + 1} (α := U) (eval ((ψ : (a : S) → U) a) (Polynomial.map (algebraMap T U) (Polynomial.map φ p)) : U) (0 : U)
rw₁ :
  Eq.{u_8 + 1} (α := U) (eval ((ψ : (a : S) → U) a) (Polynomial.map (RingHom.comp (algebraMap T U) φ) p) : U) (0 : U)
rw₂ : Eq.{u_8 + 1} (α := U) (eval ((ψ : (a : S) → U) a) (Polynomial.map (ψ.comp (algebraMap R S)) p) : U) (0 : U)
rw₃ :
  Eq.{u_8 + 1} (α := U) (eval ((ψ : (a : S) → U) a) (Polynomial.map ψ (Polynomial.map (algebraMap R S) p)) : U) (0 : U)
rw₄ : eval₂ ψ ((ψ : (a : S) → U) a) (Polynomial.map (algebraMap R S) p) = 0
rw₅ : Eq.{u_8 + 1} (α := U) ((ψ : (a : S) → U) (eval a (Polynomial.map (algebraMap R S) p)) : U) (0 : U)
rw₆ : Eq.{u_8 + 1} (α := U) ((ψ : (a : S) → U) (eval₂ (algebraMap R S) a p) : U) (0 : U)
rw₇ : Eq.{u_8 + 1} (α := U) ((ψ : (a : S) → U) 0 : U) (0 : U)
⊢ eval₂ (algebraMap T U) ((ψ : (a : S) → U) a) (Polynomial.map φ p) = 0
have rw₈ : Eq.{u_8 + 1} (α := U) 0 0
Tactic: rw [← eval_map, map_map, h, ← map_map, eval_map, eval₂_at_apply, eval_map, hp.2, ψ.map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
x : B
hx : IsIntegral R x
p : R[X]
hp : p.Monic
hpx : eval₂ (algebraMap R B) x p = 0
⊢ eval₂ (algebraMap A B) x (Polynomial.map (algebraMap R A) p) = 0
have rw : Eq.{u_3 + 1} (α := B) ((aeval x : (a : A[X]) → B) (Polynomial.map (algebraMap R A) p) : B) (0 : B)
Tactic: rw [← aeval_def, aeval_map_algebraMap, aeval_def, hpx]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
x : B
hx : IsIntegral R x
p : R[X]
hp : p.Monic
hpx : eval₂ (algebraMap R B) x p = 0
rw : Eq.{u_3 + 1} (α := B) ((aeval x : (a : A[X]) → B) (Polynomial.map (algebraMap R A) p) : B) (0 : B)
⊢ eval₂ (algebraMap A B) x (Polynomial.map (algebraMap R A) p) = 0
have rw₁ : Eq.{u_3 + 1} (α := B) ((aeval x : (a : R[X]) → B) p : B) (0 : B)
Tactic: rw [← aeval_def, aeval_map_algebraMap, aeval_def, hpx]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
x : B
hx : IsIntegral R x
p : R[X]
hp : p.Monic
hpx : eval₂ (algebraMap R B) x p = 0
rw : Eq.{u_3 + 1} (α := B) ((aeval x : (a : A[X]) → B) (Polynomial.map (algebraMap R A) p) : B) (0 : B)
rw₁ : Eq.{u_3 + 1} (α := B) ((aeval x : (a : R[X]) → B) p : B) (0 : B)
rw₂ : eval₂ (algebraMap R B) x p = 0
⊢ eval₂ (algebraMap A B) x (Polynomial.map (algebraMap R A) p) = 0
have rw₃ : Eq.{u_3 + 1} (α := B) 0 0
Tactic: rw [← aeval_def, aeval_map_algebraMap, aeval_def, hpx]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic (goal)
Goal:
R : Type u_5
S : Type u_6
T : Type u_7
inst : CommRing R
inst_1 : Ring S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra T S
φ : R ≃+* T
h : Eq (α := R →+* S) (RingHom.comp (algebraMap T S) φ.toRingHom) (algebraMap R S)
a : S
⊢ IsIntegral R a ↔ IsIntegral T a
have mp : IsIntegral R a → IsIntegral T a
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic (goal)
Goal:
R : Type u_5
S : Type u_6
T : Type u_7
inst : CommRing R
inst_1 : Ring S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra T S
φ : R ≃+* T
h : Eq (α := R →+* S) (RingHom.comp (algebraMap T S) φ.toRingHom) (algebraMap R S)
a : S
mp : IsIntegral R a → IsIntegral T a
⊢ IsIntegral R a ↔ IsIntegral T a
have mpr : IsIntegral T a → IsIntegral R a
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic (goal)
Goal:
R : Type u_5
S : Type u_6
T : Type u_7
inst : CommRing R
inst_1 : Ring S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra T S
φ : R ≃+* T
h : Eq (α := R →+* S) (RingHom.comp (algebraMap T S) φ.toRingHom) (algebraMap R S)
a : S
ha : IsIntegral R a
this : Algebra R T := φ.toRingHom.toAlgebra
r : R
t : T
s : S
⊢ (r • t) • s = r • t • s
have simp : HMul.hMul (α := S) ((algebraMap T S : (a : T) → S) ((algebraMap R T : (a : R) → T) r : T) : S)
    (HMul.hMul (α := S) ((algebraMap T S : (a : T) → S) t : S) s) =
  HMul.hMul (α := S) ((RingHom.comp (algebraMap T S) φ.toRingHom : (a : R) → S) r : S)
    (HMul.hMul (α := S) ((algebraMap T S : (a : T) → S) t : S) s)
Tactic: simp only [Algebra.smul_def, map_mul, ← h, mul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic (hypothesis)
Goal:
R : Type u_5
S : Type u_6
T : Type u_7
inst : CommRing R
inst_1 : Ring S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra T S
φ : R ≃+* T
h : Eq (α := R →+* S) (RingHom.comp (algebraMap T S) φ.toRingHom) (algebraMap R S)
a : S
ha : IsIntegral T a
⊢ Eq (α := T →+* S) (algebraMap T S) (RingHom.comp (algebraMap R S) φ.symm.toRingHom)
have this : RingHomInvPair (↑φ : R →+* T) (↑φ.symm : T →+* R)
Tactic: have : RingHomInvPair (φ : R →+* T) φ.symm := RingHomInvPair.of_ringEquiv _
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic (hypothesis)
Goal:
R : Type u_5
S : Type u_6
T : Type u_7
inst : CommRing R
inst_1 : Ring S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra T S
φ : R ≃+* T
h : Eq (α := R →+* S) (RingHom.comp (algebraMap T S) φ.toRingHom) (algebraMap R S)
a : S
ha : IsIntegral T a
⊢ IsIntegral R a
have h' : Eq (α := T →+* S) (algebraMap T S) (RingHom.comp (algebraMap R S) φ.symm.toRingHom)
Tactic: have h' : (algebraMap T S) = (algebraMap R S).comp φ.symm.toRingHom := by
      have : RingHomInvPair (φ : R →+* T) φ.symm := RingHomInvPair.of_ringEquiv _
      simp only [← h, RingHom.comp_assoc, RingEquiv.toRingHom_eq_coe, RingHomCompTriple.comp_eq]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic (goal)
Goal:
R : Type u_5
S : Type u_6
T : Type u_7
inst : CommRing R
inst_1 : Ring S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra T S
φ : R ≃+* T
h : Eq (α := R →+* S) (RingHom.comp (algebraMap T S) φ.toRingHom) (algebraMap R S)
a : S
ha : IsIntegral T a
h' : Eq (α := T →+* S) (algebraMap T S) (RingHom.comp (algebraMap R S) φ.symm.toRingHom)
this : Algebra T R := φ.symm.toRingHom.toAlgebra
r : T
t : R
s : S
⊢ (r • t) • s = r • t • s
have simp : HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) ((algebraMap T R : (a : T) → R) r : R) : S)
    (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) t : S) s) =
  HMul.hMul (α := S) ((RingHom.comp (algebraMap R S) φ.symm.toRingHom : (a : T) → S) r : S)
    (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) t : S) s)
Tactic: simp only [Algebra.smul_def, map_mul, h', mul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
x : A
h : IsIntegral R x
⊢ IsIntegral.{u_1, u_3} R (A := B) ((algebraMap A B : (a : A) → B) x : B)
have rcases : ∀ (f : R[X]) (hf : f.Monic) (hx : eval₂ (algebraMap R A) x f = 0),
  IsIntegral.{u_1, u_3} R (A := B) ((algebraMap A B : (a : A) → B) x : B)
Tactic: rcases h with ⟨f, hf, hx⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
x : A
f : R[X]
hf : f.Monic
hx : eval₂ (algebraMap R A) x f = 0
⊢ IsIntegral.{u_1, u_3} R (A := B) ((algebraMap A B : (a : A) → B) x : B)
have right : eval₂ (algebraMap R B) ((algebraMap A B : (a : A) → B) x) f = 0
Tactic: use f, hf
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
x : A
f : R[X]
hf : f.Monic
hx : eval₂ (algebraMap R A) x f = 0
⊢ eval₂ (algebraMap R B) ((algebraMap A B : (a : A) → B) x) f = 0
have right : eval₂ (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap A B) (algebraMap R A))
    ((algebraMap A B : (a : A) → B) x) f =
  0
Tactic: rw [IsScalarTower.algebraMap_eq R A B, ← hom_eval₂, hx, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
x : A
f : R[X]
hf : f.Monic
hx : eval₂ (algebraMap R A) x f = 0
right :
  eval₂ (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap A B) (algebraMap R A))
      ((algebraMap A B : (a : A) → B) x) f =
    0
⊢ eval₂ (algebraMap R B) ((algebraMap A B : (a : A) → B) x) f = 0
have right₁ : Eq.{u_3 + 1} (α := B) ((algebraMap A B : (a : A) → B) (eval₂ (algebraMap R A) x f) : B) (0 : B)
Tactic: rw [IsScalarTower.algebraMap_eq R A B, ← hom_eval₂, hx, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
x : A
f : R[X]
hf : f.Monic
hx : eval₂ (algebraMap R A) x f = 0
right :
  eval₂ (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap A B) (algebraMap R A))
      ((algebraMap A B : (a : A) → B) x) f =
    0
right₁ : Eq.{u_3 + 1} (α := B) ((algebraMap A B : (a : A) → B) (eval₂ (algebraMap R A) x f) : B) (0 : B)
⊢ eval₂ (algebraMap R B) ((algebraMap A B : (a : A) → B) x) f = 0
have right₂ : Eq.{u_3 + 1} (α := B) ((algebraMap A B : (a : A) → B) 0 : B) (0 : B)
Tactic: rw [IsScalarTower.algebraMap_eq R A B, ← hom_eval₂, hx, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
x : A
f : R[X]
hf : f.Monic
hx : eval₂ (algebraMap R A) x f = 0
right :
  eval₂ (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap A B) (algebraMap R A))
      ((algebraMap A B : (a : A) → B) x) f =
    0
right₁ : Eq.{u_3 + 1} (α := B) ((algebraMap A B : (a : A) → B) (eval₂ (algebraMap R A) x f) : B) (0 : B)
right₂ : Eq.{u_3 + 1} (α := B) ((algebraMap A B : (a : A) → B) 0 : B) (0 : B)
⊢ eval₂ (algebraMap R B) ((algebraMap A B : (a : A) → B) x) f = 0
have right₃ : Eq.{u_3 + 1} (α := B) 0 0
Tactic: rw [IsScalarTower.algebraMap_eq R A B, ← hom_eval₂, hx, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic (goal)
Goal:
R : Type u_1
B : Type u_3
inst : CommRing R
inst_1 : Ring B
inst_2 : Algebra R B
r : B
⊢ IsIntegral R r ↔ ∃ (s : Set R), s.Finite ∧ IsIntegral.{u_1, u_3} (↥(Subring.closure s)) r
have mp : IsIntegral R r → ∃ (s : Set R), s.Finite ∧ IsIntegral.{u_1, u_3} (↥(Subring.closure s)) r
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic (goal)
Goal:
R : Type u_1
B : Type u_3
inst : CommRing R
inst_1 : Ring B
inst_2 : Algebra R B
r : B
mp : IsIntegral R r → ∃ (s : Set R), s.Finite ∧ IsIntegral.{u_1, u_3} (↥(Subring.closure s)) r
⊢ IsIntegral R r ↔ ∃ (s : Set R), s.Finite ∧ IsIntegral.{u_1, u_3} (↥(Subring.closure s)) r
have mpr : (∃ (s : Set R), s.Finite ∧ IsIntegral.{u_1, u_3} (↥(Subring.closure s)) r) → IsIntegral R r
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic (goal)
Goal:
R : Type u_1
B : Type u_3
inst : CommRing R
inst_1 : Ring B
inst_2 : Algebra R B
r : B
hr : IsIntegral R r
⊢ ∃ (s : Set R), s.Finite ∧ IsIntegral.{u_1, u_3} (↥(Subring.closure s)) r
have mp : ∀ (p : R[X]) (hmp : p.Monic) (hpr : eval₂ (algebraMap R B) r p = 0),
  ∃ (s : Set R), s.Finite ∧ IsIntegral.{u_1, u_3} (↥(Subring.closure s)) r
Tactic: rcases hr with ⟨p, hmp, hpr⟩
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic (goal)
Goal:
R : Type u_1
B : Type u_3
inst : CommRing R
inst_1 : Ring B
inst_2 : Algebra R B
r : B
p : R[X]
hmp : p.Monic
hpr : eval₂ (algebraMap R B) r p = 0
⊢ ∃ (s : Set R), s.Finite ∧ IsIntegral.{u_1, u_3} (↥(Subring.closure s)) r
have mp : eval₂ (algebraMap (↥(Subring.closure (↑p.coeffs : Set R))) B) r p.restriction = 0
Tactic: refine ⟨_, Finset.finite_toSet _, p.restriction, monic_restriction.2 hmp, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic (goal)
Goal:
R : Type u_1
B : Type u_3
inst : CommRing R
inst_1 : Ring B
inst_2 : Algebra R B
r : B
p : R[X]
hmp : p.Monic
hpr : eval₂ (algebraMap R B) r p = 0
⊢ eval₂ (algebraMap (↥(Subring.closure (↑p.coeffs : Set R))) B) r p.restriction = 0
have mp : Eq.{u_3 + 1} (α := B) ((aeval r : (a : (↥(Subring.closure (↑p.coeffs : Set R)))[X]) → B) p.restriction : B) (0 : B)
Tactic: rw [← aeval_def, ← aeval_map_algebraMap R r p.restriction, map_restriction, aeval_def, hpr]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic (goal)
Goal:
R : Type u_1
B : Type u_3
inst : CommRing R
inst_1 : Ring B
inst_2 : Algebra R B
r : B
p : R[X]
hmp : p.Monic
hpr : eval₂ (algebraMap R B) r p = 0
mp : Eq.{u_3 + 1} (α := B) ((aeval r : (a : (↥(Subring.closure (↑p.coeffs : Set R)))[X]) → B) p.restriction : B) (0 : B)
⊢ eval₂ (algebraMap (↥(Subring.closure (↑p.coeffs : Set R))) B) r p.restriction = 0
have mp₁ : Eq.{u_3 + 1} (α := B)
  ((aeval r : (a : R[X]) → B) (Polynomial.map (algebraMap (↥(Subring.closure (↑p.coeffs : Set R))) R) p.restriction) :
    B)
  (0 : B)
Tactic: rw [← aeval_def, ← aeval_map_algebraMap R r p.restriction, map_restriction, aeval_def, hpr]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic (goal)
Goal:
R : Type u_1
B : Type u_3
inst : CommRing R
inst_1 : Ring B
inst_2 : Algebra R B
r : B
p : R[X]
hmp : p.Monic
hpr : eval₂ (algebraMap R B) r p = 0
mp : Eq.{u_3 + 1} (α := B) ((aeval r : (a : (↥(Subring.closure (↑p.coeffs : Set R)))[X]) → B) p.restriction : B) (0 : B)
mp₁ :
  Eq.{u_3 + 1} (α := B)
    ((aeval r : (a : R[X]) → B) (Polynomial.map (algebraMap (↥(Subring.closure (↑p.coeffs : Set R))) R) p.restriction) :
      B)
    (0 : B)
⊢ eval₂ (algebraMap (↥(Subring.closure (↑p.coeffs : Set R))) B) r p.restriction = 0
have mp₂ : Eq.{u_3 + 1} (α := B) ((aeval r : (a : R[X]) → B) p : B) (0 : B)
Tactic: rw [← aeval_def, ← aeval_map_algebraMap R r p.restriction, map_restriction, aeval_def, hpr]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic (goal)
Goal:
R : Type u_1
B : Type u_3
inst : CommRing R
inst_1 : Ring B
inst_2 : Algebra R B
r : B
p : R[X]
hmp : p.Monic
hpr : eval₂ (algebraMap R B) r p = 0
mp : Eq.{u_3 + 1} (α := B) ((aeval r : (a : (↥(Subring.closure (↑p.coeffs : Set R)))[X]) → B) p.restriction : B) (0 : B)
mp₁ :
  Eq.{u_3 + 1} (α := B)
    ((aeval r : (a : R[X]) → B) (Polynomial.map (algebraMap (↥(Subring.closure (↑p.coeffs : Set R))) R) p.restriction) :
      B)
    (0 : B)
mp₂ : Eq.{u_3 + 1} (α := B) ((aeval r : (a : R[X]) → B) p : B) (0 : B)
mp₃ : eval₂ (algebraMap R B) r p = 0
⊢ eval₂ (algebraMap (↥(Subring.closure (↑p.coeffs : Set R))) B) r p.restriction = 0
have mp₄ : Eq.{u_3 + 1} (α := B) 0 0
Tactic: rw [← aeval_def, ← aeval_map_algebraMap R r p.restriction, map_restriction, aeval_def, hpr]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic (goal)
Goal:
R : Type u_1
B : Type u_3
inst : CommRing R
inst_1 : Ring B
inst_2 : Algebra R B
r : B
hr : ∃ (s : Set R), s.Finite ∧ IsIntegral.{u_1, u_3} (↥(Subring.closure s)) r
⊢ IsIntegral R r
have mpr : ∀ (s : Set R), s.Finite → ∀ (hsr : IsIntegral.{u_1, u_3} (↥(Subring.closure s)) r), IsIntegral R r
Tactic: rcases hr with ⟨s, _, hsr⟩
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
s : Set A
his : ∀ (x : A), Membership.mem (γ := Set A) ∅ x → IsIntegral R x
⊢ FG.{u_1, u_2} (R := R) (M := A) ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) R[])
have empty : ∀ (x : A),
  Membership.mem (γ := Submodule R A) (span R (↑{1} : Set A)) x ↔
    Membership.mem (γ := Submodule R A)
      ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) R[] : Submodule R A) x
Tactic: refine ⟨{1}, Submodule.ext fun x => ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
s : Set A
his : ∀ (x : A), Membership.mem (γ := Set A) ∅ x → IsIntegral R x
x : A
⊢ Membership.mem (γ := Submodule R A) (span R (↑{1} : Set A)) x ↔
    Membership.mem (γ := Submodule R A)
      ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) R[] : Submodule R A) x
have empty : Membership.mem (γ := Submodule R A) (span R (↑{1} : Set A)) x ↔
  Membership.mem (γ := Submodule R A)
    ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) ⊥ : Submodule R A) x
Tactic: rw [Algebra.adjoin_empty, Finset.coe_singleton, ← one_eq_span, Algebra.toSubmodule_bot]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
s : Set A
his : ∀ (x : A), Membership.mem (γ := Set A) ∅ x → IsIntegral R x
x : A
empty :
  Membership.mem (γ := Submodule R A) (span R (↑{1} : Set A)) x ↔
    Membership.mem (γ := Submodule R A)
      ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) ⊥ : Submodule R A) x
⊢ Membership.mem (γ := Submodule R A) (span R (↑{1} : Set A)) x ↔
    Membership.mem (γ := Submodule R A)
      ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) R[] : Submodule R A) x
have empty₁ : Membership.mem (γ := Submodule R A) (R ∙ 1) x ↔
  Membership.mem (γ := Submodule R A)
    ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) ⊥ : Submodule R A) x
Tactic: rw [Algebra.adjoin_empty, Finset.coe_singleton, ← one_eq_span, Algebra.toSubmodule_bot]