[GOAL]
h : IsField ℤ
a : ℤ
⊢ 2 * a = 1 → 1 = a + a
[PROOFSTEP]
rw [← two_mul]
[GOAL]
h : IsField ℤ
a : ℤ
⊢ 2 * a = 1 → 1 = 2 * a
[PROOFSTEP]
exact Eq.symm
[GOAL]
K✝ : Type u_1
L : Type u_2
inst✝² : Field K✝
inst✝¹ : Field L
nf : NumberField K✝
K : Type u_3
inst✝ : Field K
x : K
hx : x ∈ 𝓞 K
⊢ IsIntegral ℤ { val := x, property := hx }
[PROOFSTEP]
obtain ⟨P, hPm, hP⟩ := hx
[GOAL]
case intro.intro
K✝ : Type u_1
L : Type u_2
inst✝² : Field K✝
inst✝¹ : Field L
nf : NumberField K✝
K : Type u_3
inst✝ : Field K
x : K
P : Polynomial ℤ
hPm : Polynomial.Monic P
hP : Polynomial.eval₂ (algebraMap ℤ K) x P = 0
⊢ IsIntegral ℤ { val := x, property := (_ : ∃ p, Polynomial.Monic p ∧ Polynomial.eval₂ (algebraMap ℤ K) x p = 0) }
[PROOFSTEP]
refine' ⟨P, hPm, _⟩
[GOAL]
case intro.intro
K✝ : Type u_1
L : Type u_2
inst✝² : Field K✝
inst✝¹ : Field L
nf : NumberField K✝
K : Type u_3
inst✝ : Field K
x : K
P : Polynomial ℤ
hPm : Polynomial.Monic P
hP : Polynomial.eval₂ (algebraMap ℤ K) x P = 0
⊢ Polynomial.eval₂ (algebraMap ℤ { x // x ∈ 𝓞 K })
      { val := x, property := (_ : ∃ p, Polynomial.Monic p ∧ Polynomial.eval₂ (algebraMap ℤ K) x p = 0) } P =
    0
[PROOFSTEP]
rw [← Polynomial.aeval_def, ← Subalgebra.coe_eq_zero, Polynomial.aeval_subalgebra_coe, Polynomial.aeval_def,
  Subtype.coe_mk, hP]
[GOAL]
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
nf : NumberField K
inst✝ : Algebra K L
⊢ ↑((fun k => { val := ↑(algebraMap K L) ↑k, property := (_ : IsIntegral ℤ (↑(algebraMap K L) ↑k)) }) 1) = ↑1
[PROOFSTEP]
simp only [Subtype.coe_mk, Subalgebra.coe_one, map_one]
[GOAL]
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
nf : NumberField K
inst✝ : Algebra K L
x y : { x // x ∈ 𝓞 K }
⊢ ↑(OneHom.toFun
        { toFun := fun k => { val := ↑(algebraMap K L) ↑k, property := (_ : IsIntegral ℤ (↑(algebraMap K L) ↑k)) },
          map_one' :=
            (_ :
              (fun k => { val := ↑(algebraMap K L) ↑k, property := (_ : IsIntegral ℤ (↑(algebraMap K L) ↑k)) }) 1 = 1) }
        (x * y)) =
    ↑(OneHom.toFun
          { toFun := fun k => { val := ↑(algebraMap K L) ↑k, property := (_ : IsIntegral ℤ (↑(algebraMap K L) ↑k)) },
            map_one' :=
              (_ :
                (fun k => { val := ↑(algebraMap K L) ↑k, property := (_ : IsIntegral ℤ (↑(algebraMap K L) ↑k)) }) 1 =
                  1) }
          x *
        OneHom.toFun
          { toFun := fun k => { val := ↑(algebraMap K L) ↑k, property := (_ : IsIntegral ℤ (↑(algebraMap K L) ↑k)) },
            map_one' :=
              (_ :
                (fun k => { val := ↑(algebraMap K L) ↑k, property := (_ : IsIntegral ℤ (↑(algebraMap K L) ↑k)) }) 1 =
                  1) }
          y)
[PROOFSTEP]
simp only [Subalgebra.coe_mul, map_mul, Subtype.coe_mk]
[GOAL]
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
nf : NumberField K
inst✝ : Algebra K L
⊢ ↑(OneHom.toFun
        (↑{
            toOneHom :=
              {
                toFun := fun k =>
                  { val := ↑(algebraMap K L) ↑k, property := (_ : IsIntegral ℤ (↑(algebraMap K L) ↑k)) },
                map_one' :=
                  (_ :
                    (fun k => { val := ↑(algebraMap K L) ↑k, property := (_ : IsIntegral ℤ (↑(algebraMap K L) ↑k)) })
                        1 =
                      1) },
            map_mul' :=
              (_ :
                ∀ (x y : { x // x ∈ 𝓞 K }),
                  OneHom.toFun
                      {
                        toFun := fun k =>
                          { val := ↑(algebraMap K L) ↑k, property := (_ : IsIntegral ℤ (↑(algebraMap K L) ↑k)) },
                        map_one' :=
                          (_ :
                            (fun k =>
                                  { val := ↑(algebraMap K L) ↑k,
                                    property := (_ : IsIntegral ℤ (↑(algebraMap K L) ↑k)) })
                                1 =
                              1) }
                      (x * y) =
                    OneHom.toFun
                        {
                          toFun := fun k =>
                            { val := ↑(algebraMap K L) ↑k, property := (_ : IsIntegral ℤ (↑(algebraMap K L) ↑k)) },
                          map_one' :=
                            (_ :
                              (fun k =>
                                    { val := ↑(algebraMap K L) ↑k,
                                      property := (_ : IsIntegral ℤ (↑(algebraMap K L) ↑k)) })
                                  1 =
                                1) }
                        x *
                      OneHom.toFun
                        {
                          toFun := fun k =>
                            { val := ↑(algebraMap K L) ↑k, property := (_ : IsIntegral ℤ (↑(algebraMap K L) ↑k)) },
                          map_one' :=
                            (_ :
                              (fun k =>
                                    { val := ↑(algebraMap K L) ↑k,
                                      property := (_ : IsIntegral ℤ (↑(algebraMap K L) ↑k)) })
                                  1 =
                                1) }
                        y) })
        0) =
    ↑0
[PROOFSTEP]
simp only [Subtype.coe_mk, Subalgebra.coe_zero, map_zero]
[GOAL]
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
nf : NumberField K
inst✝ : Algebra K L
x y : { x // x ∈ 𝓞 K }
⊢ ↑(OneHom.toFun
        (↑{
            toOneHom :=
              {
                toFun := fun k =>
                  { val := ↑(algebraMap K L) ↑k, property := (_ : IsIntegral ℤ (↑(algebraMap K L) ↑k)) },
                map_one' :=
                  (_ :
                    (fun k => { val := ↑(algebraMap K L) ↑k, property := (_ : IsIntegral ℤ (↑(algebraMap K L) ↑k)) })
                        1 =
                      1) },
            map_mul' :=
              (_ :
                ∀ (x y : { x // x ∈ 𝓞 K }),
                  OneHom.toFun
                      {
                        toFun := fun k =>
                          { val := ↑(algebraMap K L) ↑k, property := (_ : IsIntegral ℤ (↑(algebraMap K L) ↑k)) },
                        map_one' :=
                          (_ :
                            (fun k =>
                                  { val := ↑(algebraMap K L) ↑k,
                                    property := (_ : IsIntegral ℤ (↑(algebraMap K L) ↑k)) })
                                1 =
                              1) }
                      (x * y) =
                    OneHom.toFun
                        {
                          toFun := fun k =>
                            { val := ↑(algebraMap K L) ↑k, property := (_ : IsIntegral ℤ (↑(algebraMap K L) ↑k)) },
                          map_one' :=
                            (_ :
                              (fun k =>
                                    { val := ↑(algebraMap K L) ↑k,
                                      property := (_ : IsIntegral ℤ (↑(algebraMap K L) ↑k)) })
                                  1 =
                                1) }
                        x *
                      OneHom.toFun
                        {
                          toFun := fun k =>
                            { val := ↑(algebraMap K L) ↑k, property := (_ : IsIntegral ℤ (↑(algebraMap K L) ↑k)) },
                          map_one' :=
                            (_ :
                              (fun k =>
                                    { val := ↑(algebraMap K L) ↑k,
                                      property := (_ : IsIntegral ℤ (↑(algebraMap K L) ↑k)) })
                                  1 =
                                1) }
                        y) })
        (x + y)) =
    ↑(OneHom.toFun
          (↑{
              toOneHom :=
                {
                  toFun := fun k =>
                    { val := ↑(algebraMap K L) ↑k, property := (_ : IsIntegral ℤ (↑(algebraMap K L) ↑k)) },
                  map_one' :=
                    (_ :
                      (fun k => { val := ↑(algebraMap K L) ↑k, property := (_ : IsIntegral ℤ (↑(algebraMap K L) ↑k)) })
                          1 =
                        1) },
              map_mul' :=
                (_ :
                  ∀ (x y : { x // x ∈ 𝓞 K }),
                    OneHom.toFun
                        {
                          toFun := fun k =>
                            { val := ↑(algebraMap K L) ↑k, property := (_ : IsIntegral ℤ (↑(algebraMap K L) ↑k)) },
                          map_one' :=
                            (_ :
                              (fun k =>
                                    { val := ↑(algebraMap K L) ↑k,
                                      property := (_ : IsIntegral ℤ (↑(algebraMap K L) ↑k)) })
                                  1 =
                                1) }
                        (x * y) =
                      OneHom.toFun
                          {
                            toFun := fun k =>
                              { val := ↑(algebraMap K L) ↑k, property := (_ : IsIntegral ℤ (↑(algebraMap K L) ↑k)) },
                            map_one' :=
                              (_ :
                                (fun k =>
                                      { val := ↑(algebraMap K L) ↑k,
                                        property := (_ : IsIntegral ℤ (↑(algebraMap K L) ↑k)) })
                                    1 =
                                  1) }
                          x *
                        OneHom.toFun
                          {
                            toFun := fun k =>
                              { val := ↑(algebraMap K L) ↑k, property := (_ : IsIntegral ℤ (↑(algebraMap K L) ↑k)) },
                            map_one' :=
                              (_ :
                                (fun k =>
                                      { val := ↑(algebraMap K L) ↑k,
                                        property := (_ : IsIntegral ℤ (↑(algebraMap K L) ↑k)) })
                                    1 =
                                  1) }
                          y) })
          x +
        OneHom.toFun
          (↑{
              toOneHom :=
                {
                  toFun := fun k =>
                    { val := ↑(algebraMap K L) ↑k, property := (_ : IsIntegral ℤ (↑(algebraMap K L) ↑k)) },
                  map_one' :=
                    (_ :
                      (fun k => { val := ↑(algebraMap K L) ↑k, property := (_ : IsIntegral ℤ (↑(algebraMap K L) ↑k)) })
                          1 =
                        1) },
              map_mul' :=
                (_ :
                  ∀ (x y : { x // x ∈ 𝓞 K }),
                    OneHom.toFun
                        {
                          toFun := fun k =>
                            { val := ↑(algebraMap K L) ↑k, property := (_ : IsIntegral ℤ (↑(algebraMap K L) ↑k)) },
                          map_one' :=
                            (_ :
                              (fun k =>
                                    { val := ↑(algebraMap K L) ↑k,
                                      property := (_ : IsIntegral ℤ (↑(algebraMap K L) ↑k)) })
                                  1 =
                                1) }
                        (x * y) =
                      OneHom.toFun
                          {
                            toFun := fun k =>
                              { val := ↑(algebraMap K L) ↑k, property := (_ : IsIntegral ℤ (↑(algebraMap K L) ↑k)) },
                            map_one' :=
                              (_ :
                                (fun k =>
                                      { val := ↑(algebraMap K L) ↑k,
                                        property := (_ : IsIntegral ℤ (↑(algebraMap K L) ↑k)) })
                                    1 =
                                  1) }
                          x *
                        OneHom.toFun
                          {
                            toFun := fun k =>
                              { val := ↑(algebraMap K L) ↑k, property := (_ : IsIntegral ℤ (↑(algebraMap K L) ↑k)) },
                            map_one' :=
                              (_ :
                                (fun k =>
                                      { val := ↑(algebraMap K L) ↑k,
                                        property := (_ : IsIntegral ℤ (↑(algebraMap K L) ↑k)) })
                                    1 =
                                  1) }
                          y) })
          y)
[PROOFSTEP]
simp only [map_add, Subalgebra.coe_add, Subtype.coe_mk]
[GOAL]
K : Type u_1
L : Type u_2
inst✝¹ : Field K
inst✝ : Field L
nf : NumberField K
⊢ ¬IsField { x // x ∈ 𝓞 K }
[PROOFSTEP]
have h_inj : Function.Injective (algebraMap ℤ (𝓞 K)) := RingHom.injective_int (algebraMap ℤ (𝓞 K))
[GOAL]
K : Type u_1
L : Type u_2
inst✝¹ : Field K
inst✝ : Field L
nf : NumberField K
h_inj : Injective ↑(algebraMap ℤ { x // x ∈ 𝓞 K })
⊢ ¬IsField { x // x ∈ 𝓞 K }
[PROOFSTEP]
intro hf
[GOAL]
K : Type u_1
L : Type u_2
inst✝¹ : Field K
inst✝ : Field L
nf : NumberField K
h_inj : Injective ↑(algebraMap ℤ { x // x ∈ 𝓞 K })
hf : IsField { x // x ∈ 𝓞 K }
⊢ False
[PROOFSTEP]
exact Int.not_isField (((IsIntegralClosure.isIntegral_algebra ℤ K).isField_iff_isField h_inj).mpr hf)
[GOAL]
K : Type u_1
L : Type u_2
inst✝¹ : Field K
inst✝ : Field L
nf : NumberField K
x : K
⊢ x ∈ Submodule.span ℤ (Set.range ↑(integralBasis K)) ↔ x ∈ 𝓞 K
[PROOFSTEP]
rw [integralBasis, Basis.localizationLocalization_span, Subalgebra.range_isScalarTower_toAlgHom,
  Subalgebra.mem_toSubmodule]
[GOAL]
⊢ FiniteDimensional ℚ ℚ
[PROOFSTEP]
convert (inferInstance : FiniteDimensional ℚ ℚ)
[GOAL]
f : Polynomial ℚ
hf : Fact (Irreducible f)
⊢ FiniteDimensional ℚ (AdjoinRoot f)
[PROOFSTEP]
convert (AdjoinRoot.powerBasis hf.out.ne_zero).finiteDimensional
