awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.NumberField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
⊢ Eq (α := Algebra (𝓞 K) K) (instAlgebra K) (instAlgebra_1 K)

Tactic:
with_reducible_and_instances rfl
-- Module: Mathlib.NumberTheory.NumberField.Basic
Goal:
K : Type u_1
inst : Field K
x : 𝓞 K
⊢ (↑x : K) = (algebraMap (𝓞 K) K : (a : 𝓞 K) → K) x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.NumberField.Basic
Goal:
K : Type u_1
inst : Field K
x y : 𝓞 K
h : (↑x : K) = (↑y : K)
⊢ x = y

Tactic:
Subtype.ext h

Premises used: NumberField.RingOfIntegers, Subtype.ext
-- Module: Mathlib.NumberTheory.NumberField.Basic
Goal:
K : Type u_1
inst : Field K
x y : 𝓞 K
⊢ (↑x : K) = (↑y : K) ↔ x = y

Tactic:
NumberField.RingOfIntegers.ext_iff.symm

Premises used: NumberField.RingOfIntegers.ext_iff, Iff.symm
-- Module: Mathlib.NumberTheory.NumberField.Basic
Goal:
K : Type u_1
inst : Field K
x : K
hx : Membership.mem (γ := Subalgebra ℤ K) (integralClosure ℤ K) x
⊢ (algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
      (Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra ℤ K) (integralClosure ℤ K) x) x hx) =
    x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.NumberField.Basic
Goal:
K : Type u_1
inst : Field K
x : K
hx : Membership.mem (γ := Subalgebra ℤ K) (integralClosure ℤ K) x
⊢ (↑(Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra ℤ K) (integralClosure ℤ K) x) x hx) : K) = x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.NumberField.Basic
Goal:
K : Type u_1
inst : Field K
x y : K
hx : Membership.mem (γ := Subalgebra ℤ K) (integralClosure ℤ K) x
hy : Membership.mem (γ := Subalgebra ℤ K) (integralClosure ℤ K) y
⊢ Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra ℤ K) (integralClosure ℤ K) x) x hx =
      Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra ℤ K) (integralClosure ℤ K) x) y hy ↔
    x = y

Tactic:
simp
-- Module: Mathlib.NumberTheory.NumberField.Basic
Goal:
K : Type u_1
inst : Field K
⊢ Eq (α := ↥(integralClosure ℤ K))
    (Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra ℤ K) (integralClosure ℤ K) x) 1 ⋯) 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.NumberField.Basic
Goal:
K : Type u_1
inst : Field K
⊢ Eq (α := ↥(integralClosure ℤ K))
    (Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra ℤ K) (integralClosure ℤ K) x) 0 ⋯) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.NumberField.Basic
Goal:
K : Type u_1
inst : Field K
x y : K
hx : Membership.mem (γ := Subalgebra ℤ K) (integralClosure ℤ K) x
hy : Membership.mem (γ := Subalgebra ℤ K) (integralClosure ℤ K) y
⊢ Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra ℤ K) (integralClosure ℤ K) x) x hx +
      Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra ℤ K) (integralClosure ℤ K) x) y hy =
    Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra ℤ K) (integralClosure ℤ K) x) (x + y) ⋯

Tactic:
rfl

Premises used: Set.Mem, rfl
-- Module: Mathlib.NumberTheory.NumberField.Basic
Goal:
K : Type u_1
inst : Field K
x y : K
hx : Membership.mem (γ := Subalgebra ℤ K) (integralClosure ℤ K) x
hy : Membership.mem (γ := Subalgebra ℤ K) (integralClosure ℤ K) y
⊢ Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra ℤ K) (integralClosure ℤ K) x) x hx *
      Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra ℤ K) (integralClosure ℤ K) x) y hy =
    Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra ℤ K) (integralClosure ℤ K) x) (x * y) ⋯

Tactic:
rfl

Premises used: Set.Mem, rfl
-- Module: Mathlib.NumberTheory.NumberField.Basic
Goal:
K : Type u_1
inst : Field K
x y : K
hx : Membership.mem (γ := Subalgebra ℤ K) (integralClosure ℤ K) x
hy : Membership.mem (γ := Subalgebra ℤ K) (integralClosure ℤ K) y
⊢ Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra ℤ K) (integralClosure ℤ K) x) x hx -
      Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra ℤ K) (integralClosure ℤ K) x) y hy =
    Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra ℤ K) (integralClosure ℤ K) x) (x - y) ⋯

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.NumberField.Basic
Goal:
K : Type u_1
inst : Field K
x : K
hx : Membership.mem (γ := Subalgebra ℤ K) (integralClosure ℤ K) x
⊢ -Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra ℤ K) (integralClosure ℤ K) x) x hx =
    Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra ℤ K) (integralClosure ℤ K) x) (-x) ⋯

Tactic:
rfl

Premises used: Set.Mem, rfl
-- Module: Mathlib.NumberTheory.NumberField.Basic
Goal:
K_1 : Type u_1
L_1 : Type u_2
inst : Field K_1
inst_1 : Field L_1
K : Type u_3
L : Type u_4
inst_2 : Field K
inst_3 : Field L
f : K →+* L
h :
  Eq.{u_4 + 1} (α := L)
    ((↑(Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := Subalgebra ℤ L) (integralClosure ℤ L) x)
            ((f : (a : K) → L) (↑1 : K)) ⋯) :
        L) :
      L)
    ((↑1 : L) : L)
⊢ Eq.{u_4 + 1} (α := 𝓞 L)
    (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := Subalgebra ℤ L) (integralClosure ℤ L) x)
        ((f : (a : K) → L) (↑1 : K)) ⋯ :
      ↥(integralClosure ℤ L))
    (1 : 𝓞 L)

Tactic:
ext
-- Module: Mathlib.NumberTheory.NumberField.Basic
Goal:
K_1 : Type u_1
L_1 : Type u_2
inst : Field K_1
inst_1 : Field L_1
K : Type u_3
L : Type u_4
inst_2 : Field K
inst_3 : Field L
f : K →+* L
⊢ Eq.{u_4 + 1} (α := L)
    ((↑(Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := Subalgebra ℤ L) (integralClosure ℤ L) x)
            ((f : (a : K) → L) (↑1 : K)) ⋯) :
        L) :
      L)
    ((↑1 : L) : L)

Tactic:
simp only [map_mk, map_one]

Premises used: map_one, NumberField.RingOfIntegers.map_mk
-- Module: Mathlib.NumberTheory.NumberField.Basic
Goal:
K_1 : Type u_1
L_1 : Type u_2
inst : Field K_1
inst_1 : Field L_1
K : Type u_3
L : Type u_4
inst_2 : Field K
inst_3 : Field L
f : K →+* L
x y : 𝓞 K
h :
  (↑(Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := Subalgebra ℤ L) (integralClosure ℤ L) x)
          ((f : (a : K) → L) (↑(x * y) : K)) ⋯) :
      L) =
    (↑(HMul.hMul (α := 𝓞 L) (β := 𝓞 L)
          (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := Subalgebra ℤ L) (integralClosure ℤ L) x)
              ((f : (a : K) → L) (↑x : K)) ⋯ :
            ↥(integralClosure ℤ L))
          (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := Subalgebra ℤ L) (integralClosure ℤ L) x)
              ((f : (a : K) → L) (↑y : K)) ⋯ :
            ↥(integralClosure ℤ L))) :
      L)
⊢ Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := Subalgebra ℤ L) (integralClosure ℤ L) x)
      ((f : (a : K) → L) (↑(x * y) : K)) ⋯ =
    HMul.hMul (α := 𝓞 L) (β := 𝓞 L)
      (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := Subalgebra ℤ L) (integralClosure ℤ L) x)
          ((f : (a : K) → L) (↑x : K)) ⋯ :
        ↥(integralClosure ℤ L))
      (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := Subalgebra ℤ L) (integralClosure ℤ L) x)
          ((f : (a : K) → L) (↑y : K)) ⋯ :
        ↥(integralClosure ℤ L))

Tactic:
ext
-- Module: Mathlib.NumberTheory.NumberField.Basic
Goal:
K_1 : Type u_1
L_1 : Type u_2
inst : Field K_1
inst_1 : Field L_1
K : Type u_3
L : Type u_4
inst_2 : Field K
inst_3 : Field L
f : K →+* L
x y : 𝓞 K
⊢ (↑(Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := Subalgebra ℤ L) (integralClosure ℤ L) x)
          ((f : (a : K) → L) (↑(x * y) : K)) ⋯) :
      L) =
    (↑(HMul.hMul (α := 𝓞 L) (β := 𝓞 L)
          (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := Subalgebra ℤ L) (integralClosure ℤ L) x)
              ((f : (a : K) → L) (↑x : K)) ⋯ :
            ↥(integralClosure ℤ L))
          (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := Subalgebra ℤ L) (integralClosure ℤ L) x)
              ((f : (a : K) → L) (↑y : K)) ⋯ :
            ↥(integralClosure ℤ L))) :
      L)

Tactic:
simp only [map_mk, map_mul]

Premises used: map_mul, NumberField.RingOfIntegers.map_mk
-- Module: Mathlib.NumberTheory.NumberField.Basic
Goal:
K_1 : Type u_1
L_1 : Type u_2
inst : Field K_1
inst_1 : Field L_1
K : Type u_3
L : Type u_4
inst_2 : Field K
inst_3 : Field L
f : K →+* L
h :
  Eq.{u_4 + 1} (α := L)
    ((↑(Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := Subalgebra ℤ L) (integralClosure ℤ L) x)
            ((f : (a : K) → L) (↑0 : K)) ⋯) :
        L) :
      L)
    ((↑0 : L) : L)
⊢ Eq.{u_4 + 1} (α := 𝓞 L)
    (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := Subalgebra ℤ L) (integralClosure ℤ L) x)
        ((f : (a : K) → L) (↑0 : K)) ⋯ :
      ↥(integralClosure ℤ L))
    (0 : 𝓞 L)

Tactic:
ext
-- Module: Mathlib.NumberTheory.NumberField.Basic
Goal:
K_1 : Type u_1
L_1 : Type u_2
inst : Field K_1
inst_1 : Field L_1
K : Type u_3
L : Type u_4
inst_2 : Field K
inst_3 : Field L
f : K →+* L
⊢ Eq.{u_4 + 1} (α := L)
    ((↑(Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := Subalgebra ℤ L) (integralClosure ℤ L) x)
            ((f : (a : K) → L) (↑0 : K)) ⋯) :
        L) :
      L)
    ((↑0 : L) : L)

Tactic:
simp only [map_mk, map_zero]

Premises used: map_zero, NumberField.RingOfIntegers.map_mk
-- Module: Mathlib.NumberTheory.NumberField.Basic
Goal:
K_1 : Type u_1
L_1 : Type u_2
inst : Field K_1
inst_1 : Field L_1
K : Type u_3
L : Type u_4
inst_2 : Field K
inst_3 : Field L
f : K →+* L
x y : 𝓞 K
h :
  (↑(Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := Subalgebra ℤ L) (integralClosure ℤ L) x)
          ((f : (a : K) → L) (↑(x + y) : K)) ⋯) :
      L) =
    (↑(HAdd.hAdd (α := 𝓞 L) (β := 𝓞 L)
          (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := Subalgebra ℤ L) (integralClosure ℤ L) x)
              ((f : (a : K) → L) (↑x : K)) ⋯ :
            ↥(integralClosure ℤ L))
          (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := Subalgebra ℤ L) (integralClosure ℤ L) x)
              ((f : (a : K) → L) (↑y : K)) ⋯ :
            ↥(integralClosure ℤ L))) :
      L)
⊢ Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := Subalgebra ℤ L) (integralClosure ℤ L) x)
      ((f : (a : K) → L) (↑(x + y) : K)) ⋯ =
    HAdd.hAdd (α := 𝓞 L) (β := 𝓞 L)
      (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := Subalgebra ℤ L) (integralClosure ℤ L) x)
          ((f : (a : K) → L) (↑x : K)) ⋯ :
        ↥(integralClosure ℤ L))
      (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := Subalgebra ℤ L) (integralClosure ℤ L) x)
          ((f : (a : K) → L) (↑y : K)) ⋯ :
        ↥(integralClosure ℤ L))

Tactic:
ext
-- Module: Mathlib.NumberTheory.NumberField.Basic
Goal:
K_1 : Type u_1
L_1 : Type u_2
inst : Field K_1
inst_1 : Field L_1
K : Type u_3
L : Type u_4
inst_2 : Field K
inst_3 : Field L
f : K →+* L
x y : 𝓞 K
⊢ (↑(Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := Subalgebra ℤ L) (integralClosure ℤ L) x)
          ((f : (a : K) → L) (↑(x + y) : K)) ⋯) :
      L) =
    (↑(HAdd.hAdd (α := 𝓞 L) (β := 𝓞 L)
          (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := Subalgebra ℤ L) (integralClosure ℤ L) x)
              ((f : (a : K) → L) (↑x : K)) ⋯ :
            ↥(integralClosure ℤ L))
          (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := Subalgebra ℤ L) (integralClosure ℤ L) x)
              ((f : (a : K) → L) (↑y : K)) ⋯ :
            ↥(integralClosure ℤ L))) :
      L)

Tactic:
simp only [map_mk, map_add]

Premises used: map_add, NumberField.RingOfIntegers.map_mk
-- Module: Mathlib.NumberTheory.NumberField.Basic
Goal:
K : Type u_3
L : Type u_4
inst : Field K
inst_1 : Field L
f : K →+* L
x : 𝓞 K
⊢ Eq.{u_4 + 1} (α := L) ((↑((mapRingHom f : (a : 𝓞 K) → 𝓞 L) x) : L) : L) ((f : (a : K) → L) (↑x : K) : L)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.NumberField.Basic
Goal:
K : Type u_3
L : Type u_4
inst : Field K
inst_1 : Field L
e : K ≃+* L
x : 𝓞 K
⊢ Eq.{u_4 + 1} (α := L) ((↑((mapRingEquiv e : (a : 𝓞 K) → 𝓞 L) x) : L) : L) ((e : (a : K) → L) (↑x : K) : L)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.NumberField.Basic
Goal:
K : Type u_3
L : Type u_4
inst : Field K
inst_1 : Field L
e : K ≃+* L
x : 𝓞 L
⊢ Eq.{u_3 + 1} (α := K) ((↑(((mapRingEquiv e).symm : (a : 𝓞 L) → 𝓞 K) x) : K) : K) ((e.symm : (a : L) → K) (↑x : L) : K)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.NumberField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
⊢ Eq (α := Algebra (𝓞 K) (𝓞 K)) (Algebra.id (𝓞 K)) (inst_ringOfIntegersAlgebra K K)

Tactic:
rfl

Premises used: NumberField.RingOfIntegers.mapRingHom, NumberField.RingOfIntegers, rfl
-- Module: Mathlib.NumberTheory.NumberField.Basic
Goal:
K_1 : Type u_1
L_1 : Type u_2
inst : Field K_1
inst_1 : Field L_1
k : Type u_3
K : Type u_4
L : Type u_5
inst_2 : Field k
inst_3 : Field K
inst_4 : Field L
inst_5 : Algebra k K
inst_6 : Algebra k L
inst_7 : Algebra K L
inst_8 : IsScalarTower k K L
⊢ IsScalarTower.{u_3, u_4, u_5} (𝓞 k) (𝓞 K) (𝓞 L)

Tactic:
IsScalarTower.of_algHom (mapAlgHom (IsScalarTower.toAlgHom k K L))

Premises used: IsScalarTower.toAlgHom, NumberField.RingOfIntegers.mapAlgHom, IsScalarTower.of_algHom
-- Module: Mathlib.NumberTheory.NumberField.Basic
Goal:
K : Type u_1
inst : Field K
⊢ Injective (α := 𝓞 K) (β := K) (⇑(algebraMap (𝓞 K) K) : (a : 𝓞 K) → K)

Tactic:
FaithfulSMul.algebraMap_injective _ _

Premises used: FaithfulSMul.algebraMap_injective
-- Module: Mathlib.NumberTheory.NumberField.Basic
Goal:
K : Type u_1
inst : Field K
x : 𝓞 K
⊢ Eq (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) x : K) (0 : K) ↔ x = 0

Tactic:
map_eq_zero_iff _ coe_injective

Premises used: NumberField.RingOfIntegers.coe_injective, map_eq_zero_iff
-- Module: Mathlib.NumberTheory.NumberField.Basic
Goal:
K : Type u_1
inst : Field K
x : 𝓞 K
⊢ Ne (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) x : K) (0 : K) ↔ x ≠ 0

Tactic:
map_ne_zero_iff _ coe_injective

Premises used: NumberField.RingOfIntegers.coe_injective, map_ne_zero_iff
-- Module: Mathlib.NumberTheory.NumberField.Basic
Goal:
K : Type u_1
inst : Field K
x : 𝓞 K
⊢ Eq (α := Polynomial ℤ) (minpoly ℤ (↑x : K)) (minpoly ℤ x)

Tactic:
minpoly.algebraMap_eq RingOfIntegers.coe_injective x

Premises used: NumberField.RingOfIntegers.coe_injective, minpoly.algebraMap_eq
-- Module: Mathlib.NumberTheory.NumberField.Basic
Goal:
K : Type u_1
inst : Field K
x : 𝓞 K
⊢ IsIntegral ℤ (A := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) x : K)

Tactic:
x.2

Premises used: Set.Mem, setOf, RingHom.IsIntegralElem, IsIntegral, Subtype.property
-- Module: Mathlib.NumberTheory.NumberField.Basic
Goal:
K : Type u_1
inst : Field K
x : 𝓞 K
obtain :
  ∀ (P : Polynomial ℤ) (hPm : P.Monic)
    (hP : Polynomial.eval₂ (algebraMap ℤ K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) x) P = 0), IsIntegral ℤ x
⊢ IsIntegral ℤ x

Tactic:
obtain ⟨P, hPm, hP⟩ := x.isIntegral_coe

Premises used: NumberField.RingOfIntegers.isIntegral_coe
-- Module: Mathlib.NumberTheory.NumberField.Basic
Goal:
K : Type u_1
inst : Field K
x : 𝓞 K
P : Polynomial ℤ
hPm : P.Monic
hP : Polynomial.eval₂ (algebraMap ℤ K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) x) P = 0
⊢ IsIntegral ℤ x

Tactic:
⟨P, hPm, ?_⟩

Premises used: RingHom.IsIntegralElem, IsIntegral, And.intro, Exists.intro
-- Module: Mathlib.NumberTheory.NumberField.Basic
Goal:
K : Type u_1
inst : Field K
x : 𝓞 K
P : Polynomial ℤ
hPm : P.Monic
hP : Polynomial.eval₂ (algebraMap ℤ K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) x) P = 0
refine : Polynomial.eval₂ (algebraMap ℤ (𝓞 K)) x P = 0
⊢ IsIntegral ℤ x

Tactic:
refine ⟨P, hPm, ?_⟩
-- Module: Mathlib.NumberTheory.NumberField.Basic
Goal:
K : Type u_1
inst : Field K
x : 𝓞 K
P : Polynomial ℤ
hPm : P.Monic
hP : Polynomial.eval₂ (algebraMap ℤ K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) x) P = 0
rwa :
  ∀
    (hP :
      Polynomial.eval₂
          (@RingHom.comp _ (𝓞 K) _ _ Semiring.toNonAssocSemiring _ (algebraMap (𝓞 K) K) (algebraMap ℤ (𝓞 K)))
          ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) x) P =
        0),
    Polynomial.eval₂ (algebraMap ℤ (𝓞 K)) x P = 0
rwa₁ :
  ∀ (hP : Eq (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (Polynomial.eval₂ (algebraMap ℤ (𝓞 K)) x P) : K) (0 : K)),
    Polynomial.eval₂ (algebraMap ℤ (𝓞 K)) x P = 0
rwa₂ rwa₃ rwa₄ rwa₅ :
  ∀ (hP : Polynomial.eval₂ (algebraMap ℤ (𝓞 K)) x P = 0), Polynomial.eval₂ (algebraMap ℤ (𝓞 K)) x P = 0
⊢ Polynomial.eval₂ (algebraMap ℤ (𝓞 K)) x P = 0

Tactic:
rwa [IsScalarTower.algebraMap_eq (S := 𝓞 K), ← Polynomial.hom_eval₂, coe_eq_zero_iff] at hP

Premises used: Polynomial.hom_eval₂, NumberField.RingOfIntegers.coe_eq_zero_iff, IsScalarTower.algebraMap_eq, NumberField.RingOfIntegers
-- Module: Mathlib.NumberTheory.NumberField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : NumberField K
⊢ IsFractionRing (𝓞 K) K

Tactic:
integralClosure.isFractionRing_of_finite_extension ℚ _

Premises used: Set.Mem, Rat, integralClosure.isFractionRing_of_finite_extension, NumberField.RingOfIntegers
-- Module: Mathlib.NumberTheory.NumberField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
⊢ IsIntegralClosure (𝓞 K) ℤ K

Tactic:
integralClosure.isIntegralClosure _ _

Premises used: Set.Mem, integralClosure.isIntegralClosure, NumberField.RingOfIntegers
-- Module: Mathlib.NumberTheory.NumberField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
⊢ Algebra.IsIntegral.{0, u_1} ℤ (𝓞 K)

Tactic:
IsIntegralClosure.isIntegral_algebra ℤ K

Premises used: IsIntegralClosure.isIntegral_algebra, Int
-- Module: Mathlib.NumberTheory.NumberField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : NumberField K
⊢ IsIntegrallyClosed.{u_1} (𝓞 K)

Tactic:
integralClosure.isIntegrallyClosedOfFiniteExtension ℚ

Premises used: integralClosure.isIntegrallyClosedOfFiniteExtension, Set.Mem, Rat, NumberField.RingOfIntegers
-- Module: Mathlib.NumberTheory.NumberField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : CharZero K
⊢ CharZero.{u_1} (𝓞 K)

Tactic:
.of_module K

Premises used: CharZero.of_module
-- Module: Mathlib.NumberTheory.NumberField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : NumberField K
⊢ IsNoetherian.{0, u_1} ℤ (𝓞 K)

Tactic:
IsIntegralClosure.isNoetherian _ ℚ K _

Premises used: Rat, IsIntegralClosure.isNoetherian
-- Module: Mathlib.NumberTheory.NumberField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : NumberField K
⊢ AddGroup.FG.{u_1} (𝓞 K)

Tactic:
Finite.iff_addGroup_fg.mp <| IsNoetherian.finite ℤ (𝓞 K)

Premises used: Int, Iff.mp, Module.Finite.iff_addGroup_fg, NumberField.RingOfIntegers, Module.IsNoetherian.finite
-- Module: Mathlib.NumberTheory.NumberField.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Injective.{1, u_1 + 1} (α := ℤ) (β := 𝓞 K) (⇑(algebraMap ℤ (𝓞 K)) : (a : ℤ) → 𝓞 K)

Tactic:
have h_inj : Function.Injective (algebraMap ℤ (𝓞 K)) := RingHom.injective_int (algebraMap ℤ (𝓞 K))
-- Module: Mathlib.NumberTheory.NumberField.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h_inj : Injective.{1, u_1 + 1} (α := ℤ) (β := 𝓞 K) (⇑(algebraMap ℤ (𝓞 K)) : (a : ℤ) → 𝓞 K)
hf : IsField.{u_1} (𝓞 K)
⊢ False

Tactic:
Int.not_isField
    (((IsIntegralClosure.isIntegral_algebra ℤ K).isField_iff_isField h_inj).mpr hf)

Premises used: Iff.mpr, Int.not_isField, Algebra.IsIntegral.isField_iff_isField
-- Module: Mathlib.NumberTheory.NumberField.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h_inj : Injective.{1, u_1 + 1} (α := ℤ) (β := 𝓞 K) (⇑(algebraMap ℤ (𝓞 K)) : (a : ℤ) → 𝓞 K)
hf : IsField.{u_1} (𝓞 K)
⊢ False

Tactic:
exact Int.not_isField
    (((IsIntegralClosure.isIntegral_algebra ℤ K).isField_iff_isField h_inj).mpr hf)

Premises used: Iff.mpr, Int.not_isField, Algebra.IsIntegral.isField_iff_isField
-- Module: Mathlib.NumberTheory.NumberField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : NumberField K
I : Ideal (𝓞 K)
hI : I.IsMaximal
⊢ NeZero I

Tactic:
⟨Ring.ne_bot_of_isMaximal_of_not_isField hI <| RingOfIntegers.not_isField K⟩

Premises used: NumberField.RingOfIntegers.not_isField, NeZero.mk, Ring.ne_bot_of_isMaximal_of_not_isField
-- Module: Mathlib.NumberTheory.NumberField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : NumberField K
⊢ IsDedekindDomain.{u_1} (𝓞 K)

Tactic:
IsIntegralClosure.isDedekindDomain ℤ ℚ K _

Premises used: Rat, Int, IsIntegralClosure.isDedekindDomain
-- Module: Mathlib.NumberTheory.NumberField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : NumberField K
⊢ Free.{0, u_1} ℤ (𝓞 K)

Tactic:
IsIntegralClosure.module_free ℤ ℚ K (𝓞 K)

Premises used: Rat, Int, NumberField.RingOfIntegers, IsIntegralClosure.module_free
-- Module: Mathlib.NumberTheory.NumberField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : NumberField K
⊢ IsLocalization (R := 𝓞 K) (Algebra.algebraMapSubmonoid (𝓞 K) ℤ⁰) K

Tactic:
IsIntegralClosure.isLocalization_of_isSeparable ℤ ℚ K (𝓞 K)

Premises used: Rat, Int, NumberField.RingOfIntegers, IsIntegralClosure.isLocalization_of_isSeparable
-- Module: Mathlib.NumberTheory.NumberField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : NumberField K
M : Type u_3
inst_3 : AddZeroClass M
f : M →+ K
h : ∀ (x : M), IsIntegral.{0, u_1} ℤ (A := K) ((f : (a : M) → K) x : K)
simp : Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra ℤ K) (integralClosure ℤ K) x) 0 ⋯ = 0
⊢ restrict (⇑f : (a : M) → K) h 0 = 0

Tactic:
simp only [restrict, map_zero]

Premises used: NumberField.RingOfIntegers.restrict, map_zero
-- Module: Mathlib.NumberTheory.NumberField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : NumberField K
M : Type u_3
inst_3 : AddZeroClass M
f : M →+ K
h : ∀ (x : M), IsIntegral.{0, u_1} ℤ (A := K) ((f : (a : M) → K) x : K)
⊢ Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra ℤ K) (integralClosure ℤ K) x) 0 ⋯ = 0

Tactic:
rfl
-- Module: Mathlib.NumberTheory.NumberField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : NumberField K
M : Type u_3
inst_3 : AddZeroClass M
f : M →+ K
h : ∀ (x : M), IsIntegral.{0, u_1} ℤ (A := K) ((f : (a : M) → K) x : K)
x y : M
simp :
  Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra ℤ K) (integralClosure ℤ K) x)
      (HAdd.hAdd (α := K) (β := K) ((f : (a : M) → K) x : K) ((f : (a : M) → K) y : K)) ⋯ =
    HAdd.hAdd (α := 𝓞 K) (β := 𝓞 K)
      (Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra ℤ K) (integralClosure ℤ K) x)
          ((f : (a : M) → K) x) ⋯ :
        ↥(integralClosure ℤ K))
      (Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra ℤ K) (integralClosure ℤ K) x)
          ((f : (a : M) → K) y) ⋯ :
        ↥(integralClosure ℤ K))
⊢ restrict (⇑f : (a : M) → K) h (x + y) = restrict (⇑f : (a : M) → K) h x + restrict (⇑f : (a : M) → K) h y

Tactic:
simp only [restrict, map_add]

Premises used: NumberField.RingOfIntegers.restrict, map_add
-- Module: Mathlib.NumberTheory.NumberField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : NumberField K
M : Type u_3
inst_3 : AddZeroClass M
f : M →+ K
h : ∀ (x : M), IsIntegral.{0, u_1} ℤ (A := K) ((f : (a : M) → K) x : K)
x y : M
⊢ Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra ℤ K) (integralClosure ℤ K) x)
      (HAdd.hAdd (α := K) (β := K) ((f : (a : M) → K) x : K) ((f : (a : M) → K) y : K)) ⋯ =
    HAdd.hAdd (α := 𝓞 K) (β := 𝓞 K)
      (Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra ℤ K) (integralClosure ℤ K) x)
          ((f : (a : M) → K) x) ⋯ :
        ↥(integralClosure ℤ K))
      (Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra ℤ K) (integralClosure ℤ K) x)
          ((f : (a : M) → K) y) ⋯ :
        ↥(integralClosure ℤ K))

Tactic:
rfl
-- Module: Mathlib.NumberTheory.NumberField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : NumberField K
M : Type u_3
inst_3 : MulOneClass M
f : M →* K
h : ∀ (x : M), IsIntegral.{0, u_1} ℤ (A := K) ((f : (a : M) → K) x : K)
simp : Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra ℤ K) (integralClosure ℤ K) x) 1 ⋯ = 1
⊢ restrict (⇑f : (a : M) → K) h 1 = 1

Tactic:
simp only [restrict, map_one]

Premises used: NumberField.RingOfIntegers.restrict, map_one