awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ IsIntegral R x ↔ IsIntegral R x.1 ∧ IsIntegral R x.2

Tactic:
⟨fun h ↦ ⟨h.map (AlgHom.fst R A B), h.map (AlgHom.snd R A B)⟩, fun h ↦ h.1.pair h.2⟩

Premises used: IsIntegral.pair, AlgHom.snd, And.right, IsIntegral.map, And.left, And.intro, Iff.intro, AlgHom.fst
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
S : Type u_2
inst : Field R
inst_1 : Ring S
inst_2 : IsDomain S
inst_3 : Algebra R S
x : S
int : IsIntegral R x
h0 : x ≠ 0
⊢ IsUnit x

Tactic:
have : FiniteDimensional R (R[x]) := .of_fg int.fg_adjoin_singleton
  (FiniteDimensional.isUnit R (K := R[x])
    (x := ⟨x, subset_adjoin rfl⟩) <| mt Subtype.ext_iff.mp h0).map (R[x]).val

Premises used: Subalgebra.val, Algebra.adjoin, mt, Subtype.ext_iff, FiniteDimensional.isUnit, Iff.mp, Module.Finite.of_fg, IsUnit.map, IsIntegral.fg_adjoin_singleton, Singleton.singleton
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
inst_4 : Algebra.IsIntegral R S
hR : IsField R
x : S
hx : x ≠ 0
this : Field R := hR.toField
obtain : ∀ (y : Sˣ) (hx : (↑y : S) ≠ 0), ∃ (b : S), (↑y : S) * b = 1
⊢ ∃ (b : S), x * b = 1

Tactic:
obtain ⟨y, rfl⟩ := (Algebra.IsIntegral.isIntegral (R := R) x).isUnit hx

Premises used: Algebra.IsIntegral.isIntegral, IsIntegral.isUnit, rfl
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
inst_4 : Algebra.IsIntegral R S
hR : IsField R
this : Field R := hR.toField
y : Sˣ
hx : (↑y : S) ≠ 0
⊢ ∃ (b : S), (↑y : S) * b = 1

Tactic:
⟨y.inv, y.val_inv⟩

Premises used: Exists.intro, Units.inv, Units.val_inv
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
inst_4 : Algebra.IsIntegral R S
hR : IsField R
this : Field R := hR.toField
y : Sˣ
hx : (↑y : S) ≠ 0
⊢ ∃ (b : S), (↑y : S) * b = 1

Tactic:
exact ⟨y.inv, y.val_inv⟩
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
S : Type u_2
inst : Field R
inst_1 : DivisionRing S
inst_2 : Algebra R S
x : S
int : IsIntegral R x
inl : ∀ (int : IsIntegral.{u_1, u_2} R (A := S) 0), Membership.mem (γ := Subalgebra R S) R[0] 0⁻¹
inr : ∀ (h0 : x ≠ 0), Membership.mem (γ := Subalgebra R S) R[x] x⁻¹
⊢ Membership.mem (γ := Subalgebra R S) R[x] x⁻¹

Tactic:
obtain rfl | h0 := eq_or_ne x 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
S : Type u_2
inst : Field R
inst_1 : DivisionRing S
inst_2 : Algebra R S
int : IsIntegral.{u_1, u_2} R (A := S) 0
inl : Membership.mem (γ := Subalgebra R S) R[0] 0
⊢ Membership.mem (γ := Subalgebra R S) R[0] 0⁻¹

Tactic:
rw [inv_zero]

Premises used: inv_zero
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
S : Type u_2
inst : Field R
inst_1 : DivisionRing S
inst_2 : Algebra R S
int : IsIntegral.{u_1, u_2} R (A := S) 0
⊢ Membership.mem (γ := Subalgebra R S) R[0] 0

Tactic:
Subalgebra.zero_mem _

Premises used: Set.Mem, Subalgebra.zero_mem
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
S : Type u_2
inst : Field R
inst_1 : DivisionRing S
inst_2 : Algebra R S
int : IsIntegral.{u_1, u_2} R (A := S) 0
⊢ Membership.mem (γ := Subalgebra R S) R[0] 0

Tactic:
exact Subalgebra.zero_mem _

Premises used: Subalgebra.zero_mem
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
S : Type u_2
inst : Field R
inst_1 : DivisionRing S
inst_2 : Algebra R S
x : S
int : IsIntegral R x
h0 : x ≠ 0
⊢ FiniteDimensional.{u_1, u_2} R ↥R[x]

Tactic:
have : FiniteDimensional R (R[x]) := .of_fg int.fg_adjoin_singleton
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
S : Type u_2
inst : Field R
inst_1 : DivisionRing S
inst_2 : Algebra R S
x : S
int : IsIntegral R x
h0 : x ≠ 0
this : FiniteDimensional.{u_1, u_2} R ↥R[x]
inr : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ Membership.mem (γ := Subalgebra R S) R[x] x⁻¹

Tactic:
obtain ⟨⟨y, hy⟩, h1⟩ := FiniteDimensional.exists_mul_eq_one R
    (K := R[x]) (x := ⟨x, subset_adjoin rfl⟩) (mt Subtype.ext_iff.mp h0)

Premises used: mt, Subtype.ext_iff, FiniteDimensional.exists_mul_eq_one, Iff.mp
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
S : Type u_2
inst : Field R
inst_1 : DivisionRing S
inst_2 : Algebra R S
x : S
int : IsIntegral R x
h0 : x ≠ 0
this : FiniteDimensional.{u_1, u_2} R ↥R[x]
y : S
hy : Membership.mem (γ := Subalgebra R S) R[x] y
h1 : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
inr inr₁ inr₂ inr₃ :
  Membership.mem (γ := Subalgebra R S) R[x]
    (↑(Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) y hy) : S)
⊢ Membership.mem (γ := Subalgebra R S) R[x] x⁻¹

Tactic:
rwa [← mul_left_cancel₀ h0 ((Subtype.ext_iff.mp h1).trans (mul_inv_cancel₀ h0).symm)]

Premises used: mul_inv_cancel₀, mul_left_cancel₀, Subtype.ext_iff, Iff.mp, Eq.symm, Eq.trans
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
S : Type u_2
inst : Field R
inst_1 : DivisionRing S
inst_2 : Algebra R S
x : S
A : Subalgebra R S
int : IsIntegral R x
hx : x ∈ A
⊢ x⁻¹ ∈ A

Tactic:
adjoin_le (Set.singleton_subset_iff.mpr hx) int.inv_mem_adjoin

Premises used: Iff.mpr, Set.singleton_subset_iff, Algebra.adjoin_le, IsIntegral.inv_mem_adjoin
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
S : Type u_2
inst : Field R
inst_1 : DivisionRing S
inst_2 : Algebra R S
x : S
A : Subalgebra R S
inst_3 : Algebra.IsIntegral.{u_1, u_2} R ↥A
hx : x ∈ A
⊢ x⁻¹ ∈ A

Tactic:
((isIntegral_algHom_iff A.val Subtype.val_injective).mpr <|
    Algebra.IsIntegral.isIntegral (⟨x, hx⟩ : A)).inv_mem hx

Premises used: Iff.mpr, Algebra.IsIntegral.isIntegral, Set.Mem, Subtype.val_injective, Subalgebra.val, isIntegral_algHom_iff, Subtype.mk, IsIntegral.inv_mem
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
S : Type u_2
inst : Field R
inst_1 : DivisionRing S
inst_2 : Algebra R S
x : S
int : IsIntegral R x
⊢ IsIntegral R x⁻¹

Tactic:
.of_mem_of_fg _ int.fg_adjoin_singleton _ int.inv_mem_adjoin

Premises used: IsIntegral.of_mem_of_fg, IsIntegral.fg_adjoin_singleton, IsIntegral.inv_mem_adjoin
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
S : Type u_2
inst : Field R
inst_1 : DivisionRing S
inst_2 : Algebra R S
x : S
A : Subalgebra R S
int : IsIntegral R x
inv_mem : x⁻¹ ∈ A
rw : x⁻¹⁻¹ ∈ A
⊢ x ∈ A

Tactic:
rw [← inv_inv x]

Premises used: inv_inv
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
S : Type u_2
inst : Field R
inst_1 : DivisionRing S
inst_2 : Algebra R S
x : S
A : Subalgebra R S
int : IsIntegral R x
inv_mem : x⁻¹ ∈ A
⊢ x⁻¹⁻¹ ∈ A

Tactic:
int.inv.inv_mem inv_mem

Premises used: Set.Mem, IsIntegral.inv_mem, IsIntegral.inv
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
S : Type u_2
inst : Field R
inst_1 : DivisionRing S
inst_2 : Algebra R S
x : S
A : Subalgebra R S
int : IsIntegral R x
inv_mem : x⁻¹ ∈ A
⊢ x⁻¹⁻¹ ∈ A

Tactic:
exact int.inv.inv_mem inv_mem

Premises used: IsIntegral.inv_mem, IsIntegral.inv
-- 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
inst_3 : Algebra.IsIntegral R A
h' : FiniteType R A
s : Finset A
hs : Eq (α := Subalgebra R A) (adjoin R (↑s : Set A)) ⊤
⊢ FG.{u_1, u_2} (R := R) (M := A) ⊤

Tactic:
apply hs ▸ fg_adjoin_of_finite s.finite_toSet fun x _ ↦ Algebra.IsIntegral.isIntegral x
-- 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
⊢ Module.Finite R A ↔ Algebra.IsIntegral R A ∧ FiniteType R A

Tactic:
⟨fun _ ↦ ⟨⟨.of_finite R⟩, inferInstance⟩, fun ⟨h, _⟩ ↦ h.finite⟩

Premises used: Algebra.IsIntegral.finite, inferInstance, And.intro, Iff.intro, Module.Finite, _private.0.Algebra.finite_iff_isIntegral_and_finiteType.match_1, IsIntegral.of_finite, Algebra.IsIntegral.mk
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
h : f.IsIntegral
h' : f.FiniteType
⊢ f.Finite

Tactic:
let _ := f.toAlgebra
  let _ : Algebra.IsIntegral R S := ⟨h⟩
  Algebra.IsIntegral.finite (h' := h')

Premises used: Algebra.IsIntegral.finite, RingHom.Finite, Algebra.IsIntegral.mk, RingHom.toAlgebra
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
⊢ f.Finite ↔ f.IsIntegral ∧ f.FiniteType

Tactic:
⟨fun h ↦ ⟨h.to_isIntegral, h.to_finiteType⟩, fun ⟨h, h'⟩ ↦ h.to_finite h'⟩

Premises used: _private.0.RingHom.finite_iff_isIntegral_and_finiteType.match_1, RingHom.Finite.to_isIntegral, And.intro, Iff.intro, RingHom.Finite.to_finiteType, RingHom.Finite, RingHom.IsIntegral.to_finite
-- 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
r : A
⊢ Membership.mem (γ := Subalgebra R A) (integralClosure R A) r ↔
    ∃ (M : Subalgebra R A),
      FG.{u_1, u_2} (R := R) (M := A) ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) M) ∧ r ∈ M

Tactic:
⟨fun hr =>
    ⟨Algebra.adjoin R {r}, hr.fg_adjoin_singleton, Algebra.subset_adjoin rfl⟩,
    fun ⟨M, Hf, hrM⟩ => .of_mem_of_fg M Hf _ hrM⟩

Premises used: Algebra.subset_adjoin, Algebra.adjoin, Membership.mem, integralClosure, And.intro, Iff.intro, Exists.intro, IsIntegral.of_mem_of_fg, IsIntegral.fg_adjoin_singleton, Singleton.singleton, rfl, _private.0.mem_integralClosure_iff_mem_fg.match_1
-- 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
x : A
hx : IsIntegral R x
rw : {x} ⊆ (↑(integralClosure R A) : Set A)
⊢ LE.le (α := Subalgebra R A) R[x] (integralClosure R A)

Tactic:
rw [Algebra.adjoin_le_iff]

Premises used: Algebra.adjoin_le_iff
-- 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
x : A
hx : IsIntegral R x
simp : Membership.mem (γ := Subalgebra R A) (integralClosure R A) x
⊢ {x} ⊆ (↑(integralClosure R A) : Set A)

Tactic:
simp only [SetLike.mem_coe, Set.singleton_subset_iff]

Premises used: Set.singleton_subset_iff, SetLike.mem_coe
-- 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
x : A
hx : IsIntegral R x
⊢ Membership.mem (γ := Subalgebra R A) (integralClosure R A) x

Tactic:
hx

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
x : A
hx : IsIntegral R x
⊢ Membership.mem (γ := Subalgebra R A) (integralClosure R A) x

Tactic:
exact hx
-- 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
S : Subalgebra R A
⊢ S ≤ integralClosure R A ↔ Algebra.IsIntegral.{u_1, u_2} R ↥S

Tactic:
SetLike.forall.symm.trans <|
    (forall_congr' fun x =>
      show IsIntegral R (algebraMap S A x) ↔ IsIntegral R x from
        isIntegral_algebraMap_iff Subtype.coe_injective).trans
      Algebra.isIntegral_def.symm

Premises used: Algebra.isIntegral_def, Set.Mem, setOf, SetLike.forall, Subtype.coe_injective, RingHom.IsIntegralElem, isIntegral_algebraMap_iff, IsIntegral, forall_congr', Iff.trans, Iff.symm
-- 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
S : Set A
hS : ∀ x ∈ S, IsIntegral R x
⊢ Algebra.IsIntegral.{u_1, u_2} R ↥(Algebra.adjoin R S)

Tactic:
le_integralClosure_iff_isIntegral.mp <| adjoin_le hS

Premises used: le_integralClosure_iff_isIntegral, Algebra.adjoin_le, Iff.mp
-- 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
rw : LE.le (α := Subalgebra R A) ⊤ (integralClosure R A) ↔ Algebra.IsIntegral R A
rw₁ : Algebra.IsIntegral.{u_1, u_2} R ↥⊤ ↔ Algebra.IsIntegral R A
rw₂ rw₃ : Algebra.IsIntegral R A ↔ Algebra.IsIntegral R A
⊢ Eq (α := Subalgebra R A) (integralClosure R A) ⊤ ↔ Algebra.IsIntegral R A

Tactic:
rw [← top_le_iff, le_integralClosure_iff_isIntegral,
      (Subalgebra.topEquiv (R := R) (A := A)).isIntegral_iff]

Premises used: AlgEquiv.isIntegral_iff, le_integralClosure_iff_isIntegral, top_le_iff, Subalgebra.topEquiv
-- 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
S T : Subalgebra R A
simp_rw : S ⊔ T ≤ integralClosure R A ↔ S ≤ integralClosure R A ∧ T ≤ integralClosure R A
⊢ Algebra.IsIntegral.{u_1, u_2} R ↥(S ⊔ T) ↔ Algebra.IsIntegral.{u_1, u_2} R ↥S ∧ Algebra.IsIntegral.{u_1, u_2} R ↥T

Tactic:
simp_rw [← le_integralClosure_iff_isIntegral, sup_le_iff]

Premises used: le_integralClosure_iff_isIntegral, sup_le_iff
-- 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
ι : Sort u_5
S : ι → Subalgebra R A
simp_rw : iSup S ≤ integralClosure R A ↔ ∀ (i : ι), S i ≤ integralClosure R A
⊢ Algebra.IsIntegral.{u_1, u_2} R ↥(iSup S) ↔ ∀ (i : ι), Algebra.IsIntegral.{u_1, u_2} R ↥(S i)

Tactic:
simp_rw [← le_integralClosure_iff_isIntegral, iSup_le_iff]

Premises used: le_integralClosure_iff_isIntegral, iSup_le_iff
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
A : Type u_2
S : Type u_4
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing S
inst_3 : Algebra R A
inst_4 : Algebra R S
f : A ≃ₐ[R] S
h :
  ∀ (y : S),
    y ∈ Subalgebra.map (↑f : A →ₐ[R] S) (integralClosure R A) ↔
      Membership.mem (γ := Subalgebra R S) (integralClosure R S) y
⊢ Subalgebra.map (↑f : A →ₐ[R] S) (integralClosure R A) = integralClosure R S

Tactic:
ext y
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
A : Type u_2
S : Type u_4
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing S
inst_3 : Algebra R A
inst_4 : Algebra R S
f : A ≃ₐ[R] S
y : S
h :
  (∃ (x : A), Membership.mem (γ := Subalgebra R A) (integralClosure R A) x ∧ ((↑f : A →ₐ[R] S) : (a : A) → S) x = y) ↔
    Membership.mem (γ := Subalgebra R S) (integralClosure R S) y
⊢ y ∈ Subalgebra.map (↑f : A →ₐ[R] S) (integralClosure R A) ↔
    Membership.mem (γ := Subalgebra R S) (integralClosure R S) y

Tactic:
rw [Subalgebra.mem_map]

Premises used: Subalgebra.mem_map
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
A : Type u_2
S : Type u_4
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing S
inst_3 : Algebra R A
inst_4 : Algebra R S
f : A ≃ₐ[R] S
y : S
h :
  (∃ (x : A), Membership.mem (γ := Subalgebra R A) (integralClosure R A) x ∧ ((↑f : A →ₐ[R] S) : (a : A) → S) x = y) →
    Membership.mem (γ := Subalgebra R S) (integralClosure R S) y
h₁ :
  Membership.mem (γ := Subalgebra R S) (integralClosure R S) y →
    ∃ (x : A), Membership.mem (γ := Subalgebra R A) (integralClosure R A) x ∧ ((↑f : A →ₐ[R] S) : (a : A) → S) x = y
⊢ (∃ (x : A), Membership.mem (γ := Subalgebra R A) (integralClosure R A) x ∧ ((↑f : A →ₐ[R] S) : (a : A) → S) x = y) ↔
    Membership.mem (γ := Subalgebra R S) (integralClosure R S) y

Tactic:
constructor
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
A : Type u_2
S : Type u_4
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing S
inst_3 : Algebra R A
inst_4 : Algebra R S
f : A ≃ₐ[R] S
x : A
hx : Membership.mem (γ := Subalgebra R A) (integralClosure R A) x
⊢ Membership.mem (α := S) (γ := Subalgebra R S) (integralClosure R S) (((↑f : A →ₐ[R] S) : (a : A) → S) x : S)

Tactic:
hx.map f

Premises used: Set.Mem, setOf, RingHom.IsIntegralElem, IsIntegral, IsIntegral.map
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
A : Type u_2
S : Type u_4
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing S
inst_3 : Algebra R A
inst_4 : Algebra R S
f : A ≃ₐ[R] S
x : A
hx : Membership.mem (γ := Subalgebra R A) (integralClosure R A) x
⊢ Membership.mem (α := S) (γ := Subalgebra R S) (integralClosure R S) (((↑f : A →ₐ[R] S) : (a : A) → S) x : S)

Tactic:
exact hx.map f

Premises used: IsIntegral.map
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
A : Type u_2
S : Type u_4
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing S
inst_3 : Algebra R A
inst_4 : Algebra R S
f : A ≃ₐ[R] S
y : S
hy : Membership.mem (γ := Subalgebra R S) (integralClosure R S) y
right : ((↑f : A →ₐ[R] S) : (a : A) → S) ((f.symm : (a : S) → A) y : A) = y
⊢ ∃ (x : A), Membership.mem (γ := Subalgebra R A) (integralClosure R A) x ∧ ((↑f : A →ₐ[R] S) : (a : A) → S) x = y

Tactic:
use f.symm y, hy.map (f.symm : S →ₐ[R] A)

Premises used: AlgEquiv.toAlgHom, AlgEquiv.symm, IsIntegral.map, DFunLike.coe
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
A : Type u_2
S : Type u_4
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing S
inst_3 : Algebra R A
inst_4 : Algebra R S
f : A ≃ₐ[R] S
y : S
hy : Membership.mem (γ := Subalgebra R S) (integralClosure R S) y
⊢ ((↑f : A →ₐ[R] S) : (a : A) → S) ((f.symm : (a : S) → A) y : A) = y

Tactic:
simp
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
A : Type u_2
S : Type u_4
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing S
inst_3 : Algebra R A
inst_4 : Algebra R S
f : A →ₐ[R] S
x : ↥(integralClosure R A)
⊢ Eq.{u_4 + 1} (α := S) ((↑((f.mapIntegralClosure : (a : ↥(integralClosure R A)) → ↥(integralClosure R S)) x) : S) : S)
    ((f : (a : A) → S) (↑x : A) : S)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
A : Type u_2
S : Type u_4
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing S
inst_3 : Algebra R A
inst_4 : Algebra R S
f : A ≃ₐ[R] S
x : ↥(integralClosure R A)
⊢ Eq.{u_4 + 1} (α := S) ((↑((f.mapIntegralClosure : (a : ↥(integralClosure R A)) → ↥(integralClosure R S)) x) : S) : S)
    ((f : (a : A) → S) (↑x : A) : S)

Tactic:
rfl

Premises used: rfl
-- 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
x : ↥(integralClosure R A)
p : R[X]
hpm : p.Monic
hpx : eval₂ (algebraMap R A) (↑x : A) p = 0
rwa :
  ∀ (hpx : Eq.{u_2 + 1} (α := A) ((aeval (↑x : A) : (a : R[X]) → A) p : A) (0 : A)),
    (↑(eval₂ (algebraMap R ↥(integralClosure R A)) x p) : A) = (↑0 : A)
rwa₁ :
  ∀
    (hpx :
      Eq.{u_2 + 1} (α := A)
        (((aeval ((Subalgebra.val (integralClosure R A) : (a : ↥(integralClosure R A)) → A) x) : R[X] →ₐ[R] A) :
              (a : R[X]) → A)
            p :
          A)
        (0 : A)),
    (↑(eval₂ (algebraMap R ↥(integralClosure R A)) x p) : A) = (↑0 : A)
rwa₂ rwa₃ rwa₄ rwa₅ :
  ∀
    (hpx :
      Eq (α := A)
        ((Subalgebra.val (integralClosure R A) : (a : ↥(integralClosure R A)) → A)
            ((aeval x : (a : R[X]) → ↥(integralClosure R A)) p : ↥(integralClosure R A)) :
          A)
        (0 : A)),
    (↑(eval₂ (algebraMap R ↥(integralClosure R A)) x p) : A) = (↑0 : A)
⊢ (↑(eval₂ (algebraMap R ↥(integralClosure R A)) x p) : A) = (↑0 : A)

Tactic:
rwa [← aeval_def, ← Subalgebra.val_apply, aeval_algHom_apply] at hpx

Premises used: Subalgebra.val_apply, Polynomial.aeval_def, Polynomial.aeval_algHom_apply
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing A
inst_2 : Ring B
inst_3 : CommRing S
inst_4 : Algebra R A
inst_5 : Algebra R B
f_1 f : R →+* S
⊢ Algebra.IsIntegral.{u_1, u_2} R ↥(integralClosure R A)

Tactic:
⟨integralClosure.isIntegral⟩

Premises used: integralClosure.isIntegral, Algebra.IsIntegral.mk
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
B : Type u_3
inst : CommRing R
inst_1 : Ring B
inst_2 : Algebra R B
x y : B
r : R
hr : HMul.hMul (α := B) ((algebraMap R B : (a : R) → B) r : B) y = 1
hx : IsIntegral R (x * y)
obtain : ∀ (p : R[X]) (p_monic : p.Monic) (hp : eval₂ (algebraMap R B) (x * y) p = 0), IsIntegral R x
⊢ IsIntegral R x

Tactic:
obtain ⟨p, p_monic, hp⟩ := hx
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
B : Type u_3
inst : CommRing R
inst_1 : Ring B
inst_2 : Algebra R B
x y : B
r : R
hr : HMul.hMul (α := B) ((algebraMap R B : (a : R) → B) r : B) y = 1
p : R[X]
p_monic : p.Monic
hp : eval₂ (algebraMap R B) (x * y) p = 0
⊢ IsIntegral R x

Tactic:
⟨scaleRoots p r, (monic_scaleRoots_iff r).2 p_monic, ?_⟩

Premises used: Iff.mpr, RingHom.IsIntegralElem, IsIntegral, And.intro, Exists.intro, Polynomial.scaleRoots, Polynomial.monic_scaleRoots_iff
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
B : Type u_3
inst : CommRing R
inst_1 : Ring B
inst_2 : Algebra R B
x y : B
r : R
hr : HMul.hMul (α := B) ((algebraMap R B : (a : R) → B) r : B) y = 1
p : R[X]
p_monic : p.Monic
hp : eval₂ (algebraMap R B) (x * y) p = 0
refine : eval₂ (algebraMap R B) x (p.scaleRoots r) = 0
⊢ IsIntegral R x

Tactic:
refine ⟨scaleRoots p r, (monic_scaleRoots_iff r).2 p_monic, ?_⟩
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
B : Type u_3
inst : CommRing R
inst_1 : Ring B
inst_2 : Algebra R B
x y : B
r : R
hr : HMul.hMul (α := B) ((algebraMap R B : (a : R) → B) r : B) y = 1
p : R[X]
p_monic : p.Monic
hp : eval₂ (algebraMap R B) (x * y) p = 0
⊢ Eq.{u_3 + 1} (α := B)
    ((aeval (HMul.hMul (α := B) ((algebraMap R B : (a : R) → B) r : B) (x * y)) : (a : R[X]) → B) (p.scaleRoots r) : B)
    (0 : B)

Tactic:
scaleRoots_aeval_eq_zero hp

Premises used: Polynomial.scaleRoots_aeval_eq_zero
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
B : Type u_3
inst : CommRing R
inst_1 : Ring B
inst_2 : Algebra R B
x y : B
r : R
hr : HMul.hMul (α := B) ((algebraMap R B : (a : R) → B) r : B) y = 1
p : R[X]
p_monic : p.Monic
hp : eval₂ (algebraMap R B) (x * y) p = 0
h :
  Eq (α := (p : R[X]) → B) (eval₂ (algebraMap R B) x)
    (⇑(aeval (HMul.hMul (α := B) ((algebraMap R B : (a : R) → B) r : B) (x * y))) : (a : R[X]) → B)
⊢ eval₂ (algebraMap R B) x (p.scaleRoots r) = 0

Tactic:
convert! scaleRoots_aeval_eq_zero hp

Premises used: Polynomial.scaleRoots_aeval_eq_zero