awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
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
⊢ RingHomInvPair (↑φ : R →+* T) (↑φ.symm : T →+* R)

Tactic:
have : RingHomInvPair (φ : R →+* T) φ.symm := RingHomInvPair.of_ringEquiv _
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
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
this : RingHomInvPair (↑φ : R →+* T) (↑φ.symm : T →+* R)
⊢ Eq (α := T →+* S) (algebraMap T S) (RingHom.comp (algebraMap R S) φ.symm.toRingHom)

Tactic:
simp only [← h, RingHom.comp_assoc, RingEquiv.toRingHom_eq_coe, RingHomCompTriple.comp_eq]

Premises used: RingHomCompTriple.comp_eq, RingHom.comp_assoc, RingEquiv.toRingHom_eq_coe
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
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)

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]
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
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
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)
⊢ (r • t) • s = r • t • s

Tactic:
simp only [Algebra.smul_def, map_mul, h', mul_assoc]

Premises used: mul_assoc, map_mul, Algebra.smul_def
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
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
⊢ 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:
rfl
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
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_1 : Algebra T R := φ.symm.toRingHom.toAlgebra
this : IsScalarTower T R S := ⋯
⊢ IsIntegral R a

Tactic:
IsIntegral.tower_top ha

Premises used: IsIntegral.tower_top
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
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_1 : Algebra T R := φ.symm.toRingHom.toAlgebra
this : IsScalarTower T R S := ⋯
⊢ IsIntegral R a

Tactic:
exact IsIntegral.tower_top ha

Premises used: IsIntegral.tower_top
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
Goal:
B : Type u_5
C : Type u_6
F : Type u_7
inst : Ring B
inst_1 : Ring C
b : B
inst_2 : FunLike F B C
inst_3 : RingHomClass F B C
f : F
hb : IsIntegral ℤ b
⊢ IsIntegral.{0, u_6} ℤ (A := C) ((f : (a : B) → C) b : C)

Tactic:
hb.map (f : B →+* C).toIntAlgHom

Premises used: RingHom.toIntAlgHom, IsIntegral.map, RingHomClass.toRingHom
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
Goal:
R : Type u_1
B : Type u_3
inst : CommRing R
inst_1 : Ring B
inst_2 : Algebra R B
x : B
T : Subring R
hx : IsIntegral.{u_1, u_3} (↥T) x
⊢ IsIntegral R x

Tactic:
hx.tower_top

Premises used: IsIntegral.tower_top
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
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
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)
⊢ IsIntegral.{u_1, u_3} R (A := B) ((algebraMap A B : (a : A) → B) x : B)

Tactic:
rcases h with ⟨f, hf, hx⟩
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
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₂ (algebraMap R B) ((algebraMap A B : (a : A) → B) x) f = 0
⊢ IsIntegral.{u_1, u_3} R (A := B) ((algebraMap A B : (a : A) → B) x : B)

Tactic:
use f, hf
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
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)
right₃ right₄ : Eq.{u_3 + 1} (α := B) 0 0
⊢ eval₂ (algebraMap R B) ((algebraMap A B : (a : A) → B) x) f = 0

Tactic:
rw [IsScalarTower.algebraMap_eq R A B, ← hom_eval₂, hx, map_zero]

Premises used: Polynomial.hom_eval₂, map_zero, IsScalarTower.algebraMap_eq
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
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
hAB : Function.Injective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑(algebraMap A B) : (a : A) → B)
⊢ IsIntegral.{u_1, u_3} R (A := B) ((algebraMap A B : (a : A) → B) x : B) ↔ IsIntegral R x

Tactic:
isIntegral_algHom_iff (IsScalarTower.toAlgHom R A B) hAB

Premises used: IsScalarTower.toAlgHom, isIntegral_algHom_iff
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
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
mpr : (∃ (s : Set R), s.Finite ∧ IsIntegral.{u_1, u_3} (↥(Subring.closure s)) r) → IsIntegral R r
⊢ IsIntegral R r ↔ ∃ (s : Set R), s.Finite ∧ IsIntegral.{u_1, u_3} (↥(Subring.closure s)) r

Tactic:
constructor
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
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
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
⊢ ∃ (s : Set R), s.Finite ∧ IsIntegral.{u_1, u_3} (↥(Subring.closure s)) r

Tactic:
rcases hr with ⟨p, hmp, hpr⟩
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
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

Tactic:
⟨_, Finset.finite_toSet _, p.restriction, monic_restriction.2 hmp, ?_⟩

Premises used: Iff.mpr, Polynomial.monic_restriction, Polynomial.restriction, And.intro, Exists.intro, Finset.finite_toSet
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
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 : eval₂ (algebraMap (↥(Subring.closure (↑p.coeffs : Set R))) B) r p.restriction = 0
⊢ ∃ (s : Set R), s.Finite ∧ IsIntegral.{u_1, u_3} (↥(Subring.closure s)) r

Tactic:
refine ⟨_, Finset.finite_toSet _, p.restriction, monic_restriction.2 hmp, ?_⟩
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
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
mp₄ mp₅ : Eq.{u_3 + 1} (α := B) 0 0
⊢ eval₂ (algebraMap (↥(Subring.closure (↑p.coeffs : Set R))) B) r p.restriction = 0

Tactic:
rw [← aeval_def, ← aeval_map_algebraMap R r p.restriction, map_restriction, aeval_def, hpr]

Premises used: Polynomial.aeval_map_algebraMap, Polynomial.restriction, Polynomial.aeval_def, Polynomial.map_restriction
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
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
mpr : ∀ (s : Set R), s.Finite → ∀ (hsr : IsIntegral.{u_1, u_3} (↥(Subring.closure s)) r), IsIntegral R r
⊢ IsIntegral R r

Tactic:
rcases hr with ⟨s, _, hsr⟩
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
Goal:
R : Type u_1
B : Type u_3
inst : CommRing R
inst_1 : Ring B
inst_2 : Algebra R B
r : B
s : Set R
left : s.Finite
hsr : IsIntegral.{u_1, u_3} (↥(Subring.closure s)) r
⊢ IsIntegral R r

Tactic:
hsr.of_subring _

Premises used: IsIntegral.of_subring
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
Goal:
R : Type u_1
B : Type u_3
inst : CommRing R
inst_1 : Ring B
inst_2 : Algebra R B
r : B
s : Set R
left : s.Finite
hsr : IsIntegral.{u_1, u_3} (↥(Subring.closure s)) r
⊢ IsIntegral R r

Tactic:
exact hsr.of_subring _

Premises used: IsIntegral.of_subring
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
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[])

Tactic:
⟨{1}, Submodule.ext fun x => ?_⟩

Premises used: Submodule.FG, Exists.intro, Singleton.singleton, OfNat.ofNat, Submodule.ext
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
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
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
⊢ FG.{u_1, u_2} (R := R) (M := A) ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) R[])

Tactic:
refine ⟨{1}, Submodule.ext fun x => ?_⟩
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
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
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
empty₂ :
  Membership.mem (γ := Submodule R A) 1 x ↔
    Membership.mem (γ := Submodule R A)
      ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) ⊥ : Submodule R A) x
empty₃ empty₄ : Membership.mem (γ := Submodule R A) 1 x ↔ Membership.mem (γ := Submodule R A) 1 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

Tactic:
rw [Algebra.adjoin_empty, Finset.coe_singleton, ← one_eq_span, Algebra.toSubmodule_bot]

Premises used: Finset.coe_singleton, Algebra.toSubmodule_bot, Algebra.adjoin_empty, Submodule.one_eq_span
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
s_1 : Set A
a : A
s : Set A
h : a ∉ s
hs : s.Finite
ih :
  ∀ (his : ∀ x ∈ s, IsIntegral R x),
    FG.{u_1, u_2} (R := R) (M := A)
      ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (Algebra.adjoin R s))
his : ∀ x ∈ Insert.insert a s, IsIntegral R x
insert :
  (HMul.hMul (α := Submodule R A) (β := Submodule R A)
      ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (Algebra.adjoin R s) : Submodule R A)
      ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) R[a] : Submodule R A)).FG
⊢ FG.{u_1, u_2} (R := R) (M := A)
    ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (Algebra.adjoin R (Insert.insert a s)))

Tactic:
rw [← Set.union_singleton, Algebra.adjoin_union_coe_submodule]

Premises used: Algebra.adjoin_union_coe_submodule, Set.union_singleton
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
s_1 : Set A
a : A
s : Set A
h : a ∉ s
hs : s.Finite
ih :
  ∀ (his : ∀ x ∈ s, IsIntegral R x),
    FG.{u_1, u_2} (R := R) (M := A)
      ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (Algebra.adjoin R s))
his : ∀ x ∈ insert a s, IsIntegral R x
⊢ (HMul.hMul (α := Submodule R A) (β := Submodule R A)
      ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (Algebra.adjoin R s) : Submodule R A)
      ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) R[a] : Submodule R A)).FG

Tactic:
FG.mul
      (ih fun i hi => his i <| Set.mem_insert_of_mem a hi)
      (his a <| Set.mem_insert a s).fg_adjoin_singleton

Premises used: Set.mem_insert_of_mem, Submodule.FG.mul, Set.mem_insert, IsIntegral.fg_adjoin_singleton
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
s_1 : Set A
a : A
s : Set A
h : a ∉ s
hs : s.Finite
ih :
  ∀ (his : ∀ x ∈ s, IsIntegral R x),
    FG.{u_1, u_2} (R := R) (M := A)
      ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (Algebra.adjoin R s))
his : ∀ x ∈ insert a s, IsIntegral R x
⊢ (HMul.hMul (α := Submodule R A) (β := Submodule R A)
      ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (Algebra.adjoin R s) : Submodule R A)
      ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) R[a] : Submodule R A)).FG

Tactic:
exact FG.mul
      (ih fun i hi => his i <| Set.mem_insert_of_mem a hi)
      (his a <| Set.mem_insert a s).fg_adjoin_singleton

Premises used: Set.mem_insert_of_mem, Submodule.FG.mul, Set.mem_insert, IsIntegral.fg_adjoin_singleton
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
s : Set A
hfs : s.Finite
his : ∀ x ∈ s, IsIntegral R x
empty :
  ∀ (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[])
insert :
  ∀ {a : A} {s : Set A},
    a ∉ s →
      s.Finite →
        ∀
          (ih :
            ∀ (his : ∀ x ∈ s, IsIntegral R x),
              FG.{u_1, u_2} (R := R) (M := A)
                ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (Algebra.adjoin R s)))
          (his : ∀ x ∈ Insert.insert a s, IsIntegral R x),
          FG.{u_1, u_2} (R := R) (M := A)
            ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (Algebra.adjoin R (Insert.insert a s)))
⊢ FG.{u_1, u_2} (R := R) (M := A) ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (Algebra.adjoin R s))

Tactic:
induction s, hfs using Set.Finite.induction_on with
  | empty =>
    refine ⟨{1}, Submodule.ext fun x => ?_⟩
    rw [Algebra.adjoin_empty, Finset.coe_singleton, ← one_eq_span, Algebra.toSubmodule_bot]
  | @insert a s _ _ ih =>
    rw [← Set.union_singleton, Algebra.adjoin_union_coe_submodule]
    exact FG.mul
      (ih fun i hi => his i <| Set.mem_insert_of_mem a hi)
      (his a <| Set.mem_insert a s).fg_adjoin_singleton

Premises used: Finset.coe_singleton, Algebra.toSubmodule_bot, Insert.insert, Algebra.adjoin_union_coe_submodule, Set.union_singleton, Algebra.adjoin_empty, Submodule.one_eq_span
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
s : Set A
hf : s.Finite
hi : ∀ x ∈ s, IsIntegral R x
⊢ Module.Finite.{u_1, u_2} R ↥(adjoin R s)

Tactic:
.of_fg <| fg_adjoin_of_finite hf hi

Premises used: iInf, Set.Mem, Set.iInter, setOf, Algebra.adjoin, fg_adjoin_of_finite, Module.Finite.of_fg
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
Goal:
R : Type u_1
B : Type u_3
inst : CommRing R
inst_1 : Ring B
inst_2 : Algebra R B
x : B
hi : IsIntegral R x
⊢ Module.Finite.{u_1, u_3} R ↥R[x]

Tactic:
.of_fg hi.fg_adjoin_singleton

Premises used: iInf, Set.Mem, Set.iInter, setOf, Algebra.adjoin, Module.Finite.of_fg, IsIntegral.fg_adjoin_singleton
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : IsNoetherianRing R
s : Finset A
hs : ∀ x ∈ s, IsIntegral R x
⊢ IsNoetherian.{u_1, u_2} R ↥(Algebra.adjoin R (↑s : Set A))

Tactic:
isNoetherian_of_fg_of_noetherian _ (fg_adjoin_of_finite s.finite_toSet hs)

Premises used: iInf, Set.Mem, Set.iInter, setOf, Algebra.adjoin, fg_adjoin_of_finite, isNoetherian_of_fg_of_noetherian, Finset.finite_toSet
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : Algebra R B
x : A × B
hx₁ : IsIntegral R x.1
hx₂ : IsIntegral R x.2
obtain : ∀ (p₁ : R[X]) (hp₁Monic : p₁.Monic) (hp₁Eval : eval₂ (algebraMap R A) x.1 p₁ = 0), IsIntegral R x
⊢ IsIntegral R x

Tactic:
obtain ⟨p₁, ⟨hp₁Monic, hp₁Eval⟩⟩ := hx₁
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : 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
obtain : ∀ (p₂ : R[X]) (hp₂Monic : p₂.Monic) (hp₂Eval : eval₂ (algebraMap R B) x.2 p₂ = 0), IsIntegral R x
⊢ IsIntegral R x

Tactic:
obtain ⟨p₂, ⟨hp₂Monic, hp₂Eval⟩⟩ := hx₂
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : 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:
⟨p₁ * p₂, ⟨hp₁Monic.mul hp₂Monic, ?_⟩⟩

Premises used: HMul.hMul, RingHom.IsIntegralElem, IsIntegral, And.intro, Exists.intro, Polynomial.Monic.mul
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : 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
refine : eval₂ (algebraMap R (A × B)) x (p₁ * p₂) = 0
⊢ IsIntegral R x

Tactic:
refine ⟨p₁ * p₂, ⟨hp₁Monic.mul hp₂Monic, ?_⟩⟩
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : 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
rw :
  ∀ (hp₁Eval : Eq.{u_2 + 1} (α := A) ((aeval x.1 : (a : R[X]) → A) p₁ : A) (0 : A)) (p₂ : R[X]) (hp₂Monic : p₂.Monic)
    (hp₂Eval : Eq.{u_3 + 1} (α := B) ((aeval x.2 : (a : R[X]) → B) p₂ : B) (0 : B)),
    Eq (α := A × B) ((aeval x : (a : R[X]) → A × B) (p₁ * p₂) : A × B) (0 : A × B)
⊢ eval₂ (algebraMap R (A × B)) x (p₁ * p₂) = 0

Tactic:
rw [← aeval_def] at *

Premises used: Polynomial.aeval_def
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : Algebra R B
x : A × B
p₁ : R[X]
hp₁Monic : p₁.Monic
hp₁Eval : Eq.{u_2 + 1} (α := A) ((aeval x.1 : (a : R[X]) → A) p₁ : A) (0 : A)
p₂ : R[X]
hp₂Monic : p₂.Monic
hp₂Eval : Eq.{u_3 + 1} (α := B) ((aeval x.2 : (a : R[X]) → B) p₂ : B) (0 : B)
rw :
  Eq (α := A × B) (((aeval x.1 : (a : R[X]) → A) (p₁ * p₂), (aeval x.2 : (a : R[X]) → B) (p₁ * p₂)) : A × B) (0 : A × B)
rw₁ :
  Eq (α := A × B)
    ((HMul.hMul (α := A) (β := A) ((aeval x.1 : (a : R[X]) → A) p₁ : A) ((aeval x.1 : (a : R[X]) → A) p₂ : A),
        (aeval x.2 : (a : R[X]) → B) (p₁ * p₂)) :
      A × B)
    (0 : A × B)
rw₂ :
  Eq (α := A × B)
    ((HMul.hMul (α := A) (β := A) (0 : A) ((aeval x.1 : (a : R[X]) → A) p₂ : A),
        (aeval x.2 : (a : R[X]) → B) (p₁ * p₂)) :
      A × B)
    (0 : A × B)
rw₃ : Eq (α := A × B) ((0, (aeval x.2 : (a : R[X]) → B) (p₁ * p₂)) : A × B) (0 : A × B)
rw₄ :
  Eq (α := A × B)
    (0, HMul.hMul (α := B) (β := B) ((aeval x.2 : (a : R[X]) → B) p₁ : B) ((aeval x.2 : (a : R[X]) → B) p₂ : B)) 0
rw₅ : Eq (α := A × B) (0, HMul.hMul (α := B) (β := B) ((aeval x.2 : (a : R[X]) → B) p₁ : B) (0 : B)) 0
rw₆ : Eq (α := A × B) (0, 0) 0
rw₇ rw₈ : Eq (α := A × B) (0, 0) (0, 0)
⊢ Eq (α := A × B) ((aeval x : (a : R[X]) → A × B) (p₁ * p₂) : A × B) (0 : A × B)

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

Premises used: MulZeroClass.zero_mul, Polynomial.aeval_prod_apply, Polynomial.aeval_mul, MulZeroClass.mul_zero, Prod.zero_eq_mk