awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
S : Type u_4
inst : CommRing S
g : S[X]
mon : g.Monic
I : Ideal S[X]
h : g ∈ I
nth_rw :
  Eq (α := S[X] ⧸ I)
    (∑ i ∈ Finset.range (g.natDegree + 1),
      HMul.hMul (α := S[X] ⧸ I)
        ((RingHom.comp (Ideal.Quotient.mk I) (algebraMap S S[X]) : (a : S) → S[X] ⧸ I) (g.coeff i) : S[X] ⧸ I)
        (HPow.hPow (α := S[X] ⧸ I) ((Ideal.Quotient.mk I : (a : S[X]) → S[X] ⧸ I) X : S[X] ⧸ I) i))
    ((Ideal.Quotient.mk I : (a : S[X]) → S[X] ⧸ I)
      (∑ i ∈ Finset.range (g.natDegree + 1),
        HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (g.coeff i) : S[X]) (HPow.hPow (α := S[X]) X i)))
⊢ Eq (α := S[X] ⧸ I)
    (∑ i ∈ Finset.range (g.natDegree + 1),
        HMul.hMul (α := S[X] ⧸ I)
          ((RingHom.comp (Ideal.Quotient.mk I) (algebraMap S S[X]) : (a : S) → S[X] ⧸ I) (g.coeff i) : S[X] ⧸ I)
          (HPow.hPow (α := S[X] ⧸ I) ((Ideal.Quotient.mk I : (a : S[X]) → S[X] ⧸ I) X : S[X] ⧸ I) i) :
      S[X] ⧸ I)
    ((Ideal.Quotient.mk I : (a : S[X]) → S[X] ⧸ I) g : S[X] ⧸ I)

Tactic:
nth_rw 3 [(as_sum_range_C_mul_X_pow g)]

Premises used: Polynomial.as_sum_range_C_mul_X_pow
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
S : Type u_4
inst : CommRing S
g : S[X]
mon : g.Monic
I : Ideal S[X]
h : g ∈ I
⊢ Eq (α := S[X] ⧸ I)
    (∑ i ∈ Finset.range (g.natDegree + 1),
      HMul.hMul (α := S[X] ⧸ I)
        ((RingHom.comp (Ideal.Quotient.mk I) (algebraMap S S[X]) : (a : S) → S[X] ⧸ I) (g.coeff i) : S[X] ⧸ I)
        (HPow.hPow (α := S[X] ⧸ I) ((Ideal.Quotient.mk I : (a : S[X]) → S[X] ⧸ I) X : S[X] ⧸ I) i))
    ((Ideal.Quotient.mk I : (a : S[X]) → S[X] ⧸ I)
      (∑ i ∈ Finset.range (g.natDegree + 1),
        HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (g.coeff i) : S[X]) (HPow.hPow (α := S[X]) X i)))

Tactic:
simp only [map_sum, algebraMap_eq, RingHom.coe_comp, Function.comp_apply, map_mul, map_pow]

Premises used: map_pow, map_sum, map_mul, RingHom.coe_comp, Function.comp_apply, Polynomial.algebraMap_eq
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
S : Type u_4
inst : CommRing S
g : S[X]
mon : g.Monic
I : Ideal S[X]
h : g ∈ I
⊢ RingHom.IsIntegralElem (RingHom.comp (Ideal.Quotient.mk I) (algebraMap S S[X]))
    ((Ideal.Quotient.mk I : (a : S[X]) → S[X] ⧸ I) X)

Tactic:
exact ⟨g, mon, by
  rw [← (Ideal.Quotient.eq_zero_iff_mem.mpr h), eval₂_eq_sum_range]
  nth_rw 3 [(as_sum_range_C_mul_X_pow g)]
  simp only [map_sum, algebraMap_eq, RingHom.coe_comp, Function.comp_apply, map_mul, map_pow]⟩
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
S : Type u_4
inst : CommRing S
g : S[X]
mon : g.Monic
I : Ideal S[X]
h : g ∈ I
h₁ :
  ∀ (g : S[X] ⧸ I),
    Membership.mem (γ := Subalgebra S (S[X] ⧸ I)) S[((Ideal.Quotient.mkₐ S I : (a : S[X]) → S[X] ⧸ I) X : S[X] ⧸ I)] g ↔
      Membership.mem (γ := Subalgebra S (S[X] ⧸ I)) ⊤ g
⊢ Eq (α := Subalgebra S (S[X] ⧸ I)) S[((Ideal.Quotient.mkₐ S I : (a : S[X]) → S[X] ⧸ I) X : S[X] ⧸ I)] ⊤

Tactic:
ext g
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
S : Type u_4
inst : CommRing S
g_1 : S[X]
mon : g_1.Monic
I : Ideal S[X]
h : g_1 ∈ I
g : S[X] ⧸ I
h₁ :
  Membership.mem (γ := Subalgebra S (S[X] ⧸ I)) S[((Ideal.Quotient.mkₐ S I : (a : S[X]) → S[X] ⧸ I) X : S[X] ⧸ I)] g →
    Membership.mem (γ := Subalgebra S (S[X] ⧸ I)) ⊤ g
h₂ :
  Membership.mem (γ := Subalgebra S (S[X] ⧸ I)) ⊤ g →
    Membership.mem (γ := Subalgebra S (S[X] ⧸ I)) S[((Ideal.Quotient.mkₐ S I : (a : S[X]) → S[X] ⧸ I) X : S[X] ⧸ I)] g
⊢ Membership.mem (γ := Subalgebra S (S[X] ⧸ I)) S[((Ideal.Quotient.mkₐ S I : (a : S[X]) → S[X] ⧸ I) X : S[X] ⧸ I)] g ↔
    Membership.mem (γ := Subalgebra S (S[X] ⧸ I)) ⊤ g

Tactic:
constructor
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
S : Type u_4
inst : CommRing S
g_1 : S[X]
mon : g_1.Monic
I : Ideal S[X]
h : g_1 ∈ I
g : S[X] ⧸ I
⊢ Membership.mem (γ := Subalgebra S (S[X] ⧸ I)) S[((Ideal.Quotient.mkₐ S I : (a : S[X]) → S[X] ⧸ I) X : S[X] ⧸ I)] g →
    Membership.mem (γ := Subalgebra S (S[X] ⧸ I)) ⊤ g

Tactic:
simp only [Algebra.mem_top, implies_true]

Premises used: Algebra.mem_top, implies_true
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
S : Type u_4
inst : CommRing S
g_1 : S[X]
mon : g_1.Monic
I : Ideal S[X]
h : g_1 ∈ I
g : S[X] ⧸ I
h_1 : Membership.mem (γ := Subalgebra S (S[X] ⧸ I)) ⊤ g
h₁ :
  ∀ (g' : S[X]) (hg : (Ideal.Quotient.mkₐ S I : (a : S[X]) → S[X] ⧸ I) g' = g),
    Membership.mem (γ := Subalgebra S (S[X] ⧸ I)) S[((Ideal.Quotient.mkₐ S I : (a : S[X]) → S[X] ⧸ I) X : S[X] ⧸ I)] g
⊢ Membership.mem (γ := Subalgebra S (S[X] ⧸ I)) S[((Ideal.Quotient.mkₐ S I : (a : S[X]) → S[X] ⧸ I) X : S[X] ⧸ I)] g

Tactic:
obtain ⟨g', hg⟩ := Ideal.Quotient.mkₐ_surjective S I g

Premises used: Ideal.Quotient.mkₐ_surjective
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
S : Type u_4
inst : CommRing S
g_1 : S[X]
mon : g_1.Monic
I : Ideal S[X]
h : g_1 ∈ I
g : S[X] ⧸ I
h_1 : Membership.mem (γ := Subalgebra S (S[X] ⧸ I)) ⊤ g
g' : S[X]
hg : (Ideal.Quotient.mkₐ S I : (a : S[X]) → S[X] ⧸ I) g' = g
nth_rw :
  Eq.{u_4 + 1} (α := S[X] ⧸ I)
    (∑ x ∈ Finset.range (g'.natDegree + 1),
      (Ideal.Quotient.mkₐ S I : (a : S[X]) → S[X] ⧸ I)
        (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (g'.coeff x) : S[X]) (HPow.hPow (α := S[X]) X x)))
    (∑ i ∈ Finset.range (g'.natDegree + 1),
      g'.coeff i • HPow.hPow (α := S[X] ⧸ I) ((Ideal.Quotient.mkₐ S I : (a : S[X]) → S[X] ⧸ I) X : S[X] ⧸ I) i)
⊢ g = ((aeval ((Ideal.Quotient.mkₐ S I : (a : S[X]) → S[X] ⧸ I) X) : S[X] →ₐ[S] S[X] ⧸ I) : (a : S[X]) → S[X] ⧸ I) g'

Tactic:
nth_rw 1 [← hg, aeval_eq_sum_range' (lt_add_one _),
          as_sum_range_C_mul_X_pow g', map_sum]

Premises used: lt_add_one, map_sum, Polynomial.as_sum_range_C_mul_X_pow, Polynomial.aeval_eq_sum_range'
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
S : Type u_4
inst : CommRing S
g_1 : S[X]
mon : g_1.Monic
I : Ideal S[X]
h : g_1 ∈ I
g : S[X] ⧸ I
h_1 : Membership.mem (γ := Subalgebra S (S[X] ⧸ I)) ⊤ g
g' : S[X]
hg : (Ideal.Quotient.mkₐ S I : (a : S[X]) → S[X] ⧸ I) g' = g
⊢ Eq.{u_4 + 1} (α := S[X] ⧸ I)
    (∑ x ∈ Finset.range (g'.natDegree + 1),
      (Ideal.Quotient.mkₐ S I : (a : S[X]) → S[X] ⧸ I)
        (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (g'.coeff x) : S[X]) (HPow.hPow (α := S[X]) X x)))
    (∑ i ∈ Finset.range (g'.natDegree + 1),
      g'.coeff i • HPow.hPow (α := S[X] ⧸ I) ((Ideal.Quotient.mkₐ S I : (a : S[X]) → S[X] ⧸ I) X : S[X] ⧸ I) i)

Tactic:
simp only [Polynomial.C_mul', ← map_pow, map_smul]

Premises used: Polynomial.C_mul', map_pow, map_smul
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
S : Type u_4
inst : CommRing S
g_1 : S[X]
mon : g_1.Monic
I : Ideal S[X]
h : g_1 ∈ I
g : S[X] ⧸ I
h_1 : Membership.mem (γ := Subalgebra S (S[X] ⧸ I)) ⊤ g
g' : S[X]
hg : (Ideal.Quotient.mkₐ S I : (a : S[X]) → S[X] ⧸ I) g' = g
⊢ g = ((aeval ((Ideal.Quotient.mkₐ S I : (a : S[X]) → S[X] ⧸ I) X) : S[X] →ₐ[S] S[X] ⧸ I) : (a : S[X]) → S[X] ⧸ I) g'

Tactic:
have : g = (Polynomial.aeval ((Ideal.Quotient.mkₐ S I) X)) g' := by
        nth_rw 1 [← hg, aeval_eq_sum_range' (lt_add_one _),
          as_sum_range_C_mul_X_pow g', map_sum]
        simp only [Polynomial.C_mul', ← map_pow, map_smul]
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
S : Type u_4
inst : CommRing S
g_1 : S[X]
mon : g_1.Monic
I : Ideal S[X]
h : g_1 ∈ I
g : S[X] ⧸ I
h_1 : Membership.mem (γ := Subalgebra S (S[X] ⧸ I)) ⊤ g
g' : S[X]
hg : (Ideal.Quotient.mkₐ S I : (a : S[X]) → S[X] ⧸ I) g' = g
this :
  g = ((aeval ((Ideal.Quotient.mkₐ S I : (a : S[X]) → S[X] ⧸ I) X) : S[X] →ₐ[S] S[X] ⧸ I) : (a : S[X]) → S[X] ⧸ I) g'
⊢ Membership.mem (γ := Subalgebra S (S[X] ⧸ I)) S[((Ideal.Quotient.mkₐ S I : (a : S[X]) → S[X] ⧸ I) X : S[X] ⧸ I)] g

Tactic:
this ▸ (aeval_mem_adjoin_singleton S ((Ideal.Quotient.mk I) Polynomial.X))

Premises used: Ideal.Quotient.mk, Eq.rec, Polynomial.aeval_mem_adjoin_singleton, Eq.symm, Polynomial.X, DFunLike.coe
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
S : Type u_4
inst : CommRing S
g_1 : S[X]
mon : g_1.Monic
I : Ideal S[X]
h : g_1 ∈ I
g : S[X] ⧸ I
h_1 : Membership.mem (γ := Subalgebra S (S[X] ⧸ I)) ⊤ g
g' : S[X]
hg : (Ideal.Quotient.mkₐ S I : (a : S[X]) → S[X] ⧸ I) g' = g
this :
  g = ((aeval ((Ideal.Quotient.mkₐ S I : (a : S[X]) → S[X] ⧸ I) X) : S[X] →ₐ[S] S[X] ⧸ I) : (a : S[X]) → S[X] ⧸ I) g'
⊢ Membership.mem (γ := Subalgebra S (S[X] ⧸ I)) S[((Ideal.Quotient.mkₐ S I : (a : S[X]) → S[X] ⧸ I) X : S[X] ⧸ I)] g

Tactic:
exact this ▸ (aeval_mem_adjoin_singleton S ((Ideal.Quotient.mk I) Polynomial.X))
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
S : Type u_4
inst : CommRing S
g : S[X]
mon : g.Monic
I : Ideal S[X]
h : g ∈ I
⊢ Eq (α := Subalgebra S (S[X] ⧸ I)) S[((Ideal.Quotient.mkₐ S I : (a : S[X]) → S[X] ⧸ I) X : S[X] ⧸ I)] ⊤

Tactic:
have eq_top : Algebra.adjoin S {(Ideal.Quotient.mkₐ S I) X} = ⊤ := by
    ext g
    constructor
    · simp only [Algebra.mem_top, implies_true]
    · intro _
      obtain ⟨g', hg⟩ := Ideal.Quotient.mkₐ_surjective S I g
      have : g = (Polynomial.aeval ((Ideal.Quotient.mkₐ S I) X)) g' := by
        nth_rw 1 [← hg, aeval_eq_sum_range' (lt_add_one _),
          as_sum_range_C_mul_X_pow g', map_sum]
        simp only [Polynomial.C_mul', ← map_pow, map_smul]
      exact this ▸ (aeval_mem_adjoin_singleton S ((Ideal.Quotient.mk I) Polynomial.X))
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
S : Type u_4
inst : CommRing S
g : S[X]
mon : g.Monic
I : Ideal S[X]
h : g ∈ I
eq_top : Eq (α := Subalgebra S (S[X] ⧸ I)) S[((Ideal.Quotient.mkₐ S I : (a : S[X]) → S[X] ⧸ I) X : S[X] ⧸ I)] ⊤
⊢ RingHom.IsIntegral (AlgHom.toRingHom (AlgHom.comp (Ideal.Quotient.mkₐ S I) (Algebra.ofId S S[X])))

Tactic:
fun a ↦ (eq_top ▸ adjoin_le_integralClosure <| mon.quotient_isIntegralElem h)
    Algebra.mem_top

Premises used: RingHom.IsIntegral
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
S : Type u_4
inst : CommRing S
g : S[X]
mon : g.Monic
I : Ideal S[X]
h : g ∈ I
eq_top : Eq (α := Subalgebra S (S[X] ⧸ I)) S[((Ideal.Quotient.mkₐ S I : (a : S[X]) → S[X] ⧸ I) X : S[X] ⧸ I)] ⊤
⊢ RingHom.IsIntegral (AlgHom.toRingHom (AlgHom.comp (Ideal.Quotient.mkₐ S I) (Algebra.ofId S S[X])))

Tactic:
exact fun a ↦ (eq_top ▸ adjoin_le_integralClosure <| mon.quotient_isIntegralElem h)
    Algebra.mem_top
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
val : A
h : Membership.mem (γ := Subalgebra R A) (integralClosure R A) val
⊢ IsIntegral R (A := A)
    ((algebraMap (↥(integralClosure R A)) A : (a : ↥(integralClosure R A)) → A)
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (integralClosure R A) x) val h) :
      A)

Tactic:
h

Premises used: Set.Mem, setOf, RingHom.IsIntegralElem, IsIntegral
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
val : A
h : Membership.mem (γ := Subalgebra R A) (integralClosure R A) val
⊢ IsIntegral R (A := A)
    ((algebraMap (↥(integralClosure R A)) A : (a : ↥(integralClosure R A)) → A)
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (integralClosure R A) x) val h) :
      A)

Tactic:
exact h
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R B
inst_4 : Algebra A B
inst_5 : IsIntegralClosure A R B
inst_6 : Algebra R A
inst_7 : IsScalarTower R A B
x : A
⊢ IsIntegral R x

Tactic:
(isIntegral_algebraMap_iff (algebraMap_injective A R B)).mp <|
    show IsIntegral R (algebraMap A B x) from isIntegral_iff.mpr ⟨x, rfl⟩

Premises used: Iff.mpr, IsIntegralClosure.isIntegral_iff, IsIntegralClosure.algebraMap_injective, isIntegral_algebraMap_iff, Exists.intro, Iff.mp, rfl
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R B
inst_4 : Algebra A B
inst_5 : IsIntegralClosure A R B
inst_6 : Algebra R A
inst_7 : IsScalarTower R A B
⊢ Algebra.IsIntegral R A

Tactic:
⟨fun x => IsIntegralClosure.isIntegral R B x⟩

Premises used: IsIntegralClosure.isIntegral, Algebra.IsIntegral.mk
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R B
inst_4 : Algebra A B
inst_5 : IsIntegralClosure A R B
inst_6 : Module R A
inst_7 : IsScalarTower R A B
inst_8 : IsTorsionFree R B
⊢ IsTorsionFree R A

Tactic:
Function.Injective.moduleIsTorsionFree _ (IsIntegralClosure.algebraMap_injective A R B)
      fun _ _ => ?_

Premises used: IsIntegralClosure.algebraMap_injective, Function.Injective.moduleIsTorsionFree
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R B
inst_4 : Algebra A B
inst_5 : IsIntegralClosure A R B
inst_6 : Module R A
inst_7 : IsScalarTower R A B
inst_8 : IsTorsionFree R B
_ :
  ∀ (x : R) (x_1 : A),
    (algebraMap A B : (a : A) → B) (x • x_1) = HSMul.hSMul (β := B) x ((algebraMap A B : (a : A) → B) x_1 : B)
⊢ IsTorsionFree R A

Tactic:
refine
    Function.Injective.moduleIsTorsionFree _ (IsIntegralClosure.algebraMap_injective A R B)
      fun _ _ => ?_

Premises used: IsIntegralClosure.algebraMap_injective, Function.Injective.moduleIsTorsionFree
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R B
inst_4 : Algebra A B
inst_5 : IsIntegralClosure A R B
inst_6 : Module R A
inst_7 : IsScalarTower R A B
inst_8 : IsTorsionFree R B
x : R
x_1 : A
⊢ (algebraMap A B : (a : A) → B) (x • x_1) = HSMul.hSMul (β := B) x ((algebraMap A B : (a : A) → B) x_1 : B)

Tactic:
simp only [Algebra.algebraMap_eq_smul_one, IsScalarTower.smul_assoc]

Premises used: Algebra.algebraMap_eq_smul_one, IsScalarTower.smul_assoc
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R B
inst_4 : Algebra A B
inst_5 : IsIntegralClosure A R B
x : B
hx : IsIntegral R x
⊢ (algebraMap A B : (a : A) → B) (mk' A x hx) = x

Tactic:
Classical.choose_spec (isIntegral_iff.mp hx)

Premises used: IsIntegralClosure.isIntegral_iff, IsIntegralClosure.mk', Classical.choose_spec, Iff.mp
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R B
inst_4 : Algebra A B
inst_5 : IsIntegralClosure A R B
h : IsIntegral.{u_1, u_3} R (A := B) 1
rw : Eq.{u_3 + 1} (α := B) (1 : B) ((algebraMap A B : (a : A) → B) 1 : B)
rw₁ rw₂ : Eq.{u_3 + 1} (α := B) 1 1
⊢ Eq.{u_3 + 1} (α := B) ((algebraMap A B : (a : A) → B) (mk' A 1 h) : B) ((algebraMap A B : (a : A) → B) 1 : B)

Tactic:
rw [algebraMap_mk', map_one]

Premises used: IsIntegralClosure.algebraMap_mk', map_one
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R B
inst_4 : Algebra A B
inst_5 : IsIntegralClosure A R B
h : IsIntegral.{u_1, u_3} R (A := B) 0
rw : Eq.{u_3 + 1} (α := B) (0 : B) ((algebraMap A B : (a : A) → B) 0 : B)
rw₁ rw₂ : Eq.{u_3 + 1} (α := B) 0 0
⊢ Eq.{u_3 + 1} (α := B) ((algebraMap A B : (a : A) → B) (mk' A 0 h) : B) ((algebraMap A B : (a : A) → B) 0 : B)

Tactic:
rw [algebraMap_mk', map_zero]

Premises used: map_zero, IsIntegralClosure.algebraMap_mk'
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R B
inst_4 : Algebra A B
inst_5 : IsIntegralClosure A R B
x y : B
hx : IsIntegral R x
hy : IsIntegral R y
⊢ Eq.{u_3 + 1} (α := B) ((algebraMap A B : (a : A) → B) (mk' A (x + y) ⋯) : B)
    ((algebraMap A B : (a : A) → B) (mk' A x hx + mk' A y hy) : B)

Tactic:
simp only [algebraMap_mk', map_add]

Premises used: map_add, IsIntegralClosure.algebraMap_mk'
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R B
inst_4 : Algebra A B
inst_5 : IsIntegralClosure A R B
x y : B
hx : IsIntegral R x
hy : IsIntegral R y
⊢ Eq.{u_3 + 1} (α := B) ((algebraMap A B : (a : A) → B) (mk' A (x * y) ⋯) : B)
    ((algebraMap A B : (a : A) → B) (mk' A x hx * mk' A y hy) : B)

Tactic:
simp only [algebraMap_mk', map_mul]

Premises used: map_mul, IsIntegralClosure.algebraMap_mk'
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R B
inst_4 : Algebra A B
inst_5 : IsIntegralClosure A R B
inst_6 : Algebra R A
inst_7 : IsScalarTower R A B
x : R
h : IsIntegral.{u_1, u_3} R (A := B) ((algebraMap R B : (a : R) → B) x : B)
rw :
  Eq.{u_3 + 1} (α := B) ((algebraMap R B : (a : R) → B) x : B)
    ((algebraMap A B : (a : A) → B) ((algebraMap R A : (a : R) → A) x : A) : B)
rw₁ rw₂ : Eq.{u_3 + 1} (α := B) ((algebraMap R B : (a : R) → B) x : B) ((algebraMap R B : (a : R) → B) x : B)
⊢ Eq.{u_3 + 1} (α := B) ((algebraMap A B : (a : A) → B) (mk' A ((algebraMap R B : (a : R) → B) x) h) : B)
    ((algebraMap A B : (a : A) → B) ((algebraMap R A : (a : R) → A) x : A) : B)

Tactic:
rw [algebraMap_mk', ← IsScalarTower.algebraMap_apply]

Premises used: IsIntegralClosure.algebraMap_mk', IsScalarTower.algebraMap_apply
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R B
inst_4 : Algebra A B
inst_5 : IsIntegralClosure A R B
inst_6 : Algebra R A
inst_7 : IsScalarTower R A B
inst_8 : IsDomain A
hR : IsField R
⊢ IsField A

Tactic:
have := IsIntegralClosure.isIntegral_algebra R (A := A) B
  isField_of_isIntegral_of_isField' hR

Premises used: IsIntegralClosure.isIntegral_algebra, isField_of_isIntegral_of_isField'
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R B
inst_4 : Algebra A B
inst_5 : IsIntegralClosure A R B
S : Type u_4
inst_6 : CommRing S
inst_7 : Algebra A S
inst_8 : Algebra R S
f : B ≃ₐ[R] S
h :
  ∀ (x : A),
    Eq.{u_4 + 1} (α := S) ((algebraMap A S : (a : A) → S) x : S)
      ((f : (a : B) → S) ((algebraMap A B : (a : A) → B) x : B) : S)
x : S
⊢ IsIntegral R x ↔ ∃ (y : A), (algebraMap A S : (a : A) → S) y = x

Tactic:
simp [← isIntegral_algEquiv f.symm,
    IsIntegralClosure.isIntegral_iff (A := A), h, ← f.symm.injective.eq_iff]

Premises used: AlgEquiv.symm, IsIntegralClosure.isIntegral_iff, Function.Injective.eq_iff, isIntegral_algEquiv, AlgEquiv.injective
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R B
inst_4 : Algebra A B
inst_5 : IsIntegralClosure A R B
S : Type u_4
inst_6 : CommRing S
inst_7 : Algebra R S
inst_8 : Algebra S B
inst_9 : IsScalarTower R S B
inst_10 : Algebra R A
inst_11 : IsScalarTower R A B
isIntegral : Algebra.IsIntegral R S
⊢ mk'.{u_1, u_2, u_3} (R := R) A (B := B) ((algebraMap S B : (a : S) → B) 1 : B) ⋯ = 1

Tactic:
simp only [map_one, mk'_one]

Premises used: map_one
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R B
inst_4 : Algebra A B
inst_5 : IsIntegralClosure A R B
S : Type u_4
inst_6 : CommRing S
inst_7 : Algebra R S
inst_8 : Algebra S B
inst_9 : IsScalarTower R S B
inst_10 : Algebra R A
inst_11 : IsScalarTower R A B
isIntegral : Algebra.IsIntegral R S
x y : S
simp_rw :
  mk'.{u_1, u_2, u_3} (R := R) A (B := B) ((algebraMap S B : (a : S) → B) (x * y) : B) ⋯ =
    mk'.{u_1, u_2, u_3} (R := R) A
      (HMul.hMul (α := B) (β := B) ((algebraMap S B : (a : S) → B) x : B) ((algebraMap S B : (a : S) → B) y : B)) ⋯
⊢ mk'.{u_1, u_2, u_3} (R := R) A (B := B) ((algebraMap S B : (a : S) → B) (x * y) : B) ⋯ =
    mk'.{u_1, u_2, u_3} (R := R) A (B := B) ((algebraMap S B : (a : S) → B) x : B) ⋯ *
      mk'.{u_1, u_2, u_3} (R := R) A (B := B) ((algebraMap S B : (a : S) → B) y : B) ⋯

Tactic:
simp_rw [← mk'_mul, map_mul]

Premises used: map_mul, IsIntegralClosure.mk'_mul
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R B
inst_4 : Algebra A B
inst_5 : IsIntegralClosure A R B
S : Type u_4
inst_6 : CommRing S
inst_7 : Algebra R S
inst_8 : Algebra S B
inst_9 : IsScalarTower R S B
inst_10 : Algebra R A
inst_11 : IsScalarTower R A B
isIntegral : Algebra.IsIntegral R S
⊢ mk'.{u_1, u_2, u_3} (R := R) A (B := B) ((algebraMap S B : (a : S) → B) 0 : B) ⋯ = 0

Tactic:
simp only [map_zero, mk'_zero]

Premises used: map_zero
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R B
inst_4 : Algebra A B
inst_5 : IsIntegralClosure A R B
S : Type u_4
inst_6 : CommRing S
inst_7 : Algebra R S
inst_8 : Algebra S B
inst_9 : IsScalarTower R S B
inst_10 : Algebra R A
inst_11 : IsScalarTower R A B
isIntegral : Algebra.IsIntegral R S
x y : S
simp_rw :
  mk'.{u_1, u_2, u_3} (R := R) A (B := B) ((algebraMap S B : (a : S) → B) (x + y) : B) ⋯ =
    mk'.{u_1, u_2, u_3} (R := R) A
      (HAdd.hAdd (α := B) (β := B) ((algebraMap S B : (a : S) → B) x : B) ((algebraMap S B : (a : S) → B) y : B)) ⋯
⊢ mk'.{u_1, u_2, u_3} (R := R) A (B := B) ((algebraMap S B : (a : S) → B) (x + y) : B) ⋯ =
    mk'.{u_1, u_2, u_3} (R := R) A (B := B) ((algebraMap S B : (a : S) → B) x : B) ⋯ +
      mk'.{u_1, u_2, u_3} (R := R) A (B := B) ((algebraMap S B : (a : S) → B) y : B) ⋯

Tactic:
simp_rw [← mk'_add, map_add]

Premises used: map_add, IsIntegralClosure.mk'_add
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R B
inst_4 : Algebra A B
inst_5 : IsIntegralClosure A R B
S : Type u_4
inst_6 : CommRing S
inst_7 : Algebra R S
inst_8 : Algebra S B
inst_9 : IsScalarTower R S B
inst_10 : Algebra R A
inst_11 : IsScalarTower R A B
isIntegral : Algebra.IsIntegral R S
x : R
simp_rw :
  mk'.{u_1, u_2, u_3} (R := R) A (B := B) ((algebraMap R B : (a : R) → B) x : B) ⋯ = (algebraMap R A : (a : R) → A) x
⊢ mk'.{u_1, u_2, u_3} (R := R) A (B := B) ((algebraMap S B : (a : S) → B) ((algebraMap R S : (a : R) → S) x : S) : B)
      ⋯ =
    (algebraMap R A : (a : R) → A) x

Tactic:
simp_rw [← IsScalarTower.algebraMap_apply, mk'_algebraMap]

Premises used: IsScalarTower.algebraMap_apply