[GOAL]
R : Type u_1
A : Type u_2
K : Type u_3
inst✝¹⁶ : CommRing R
inst✝¹⁵ : CommRing A
inst✝¹⁴ : Field K
inst✝¹³ : IsDomain A
inst✝¹² : Algebra A K
inst✝¹¹ : IsFractionRing A K
L : Type u_4
inst✝¹⁰ : Field L
C : Type u_5
inst✝⁹ : CommRing C
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra A L
inst✝⁶ : IsScalarTower A K L
inst✝⁵ : Algebra C L
inst✝⁴ : IsIntegralClosure C A L
inst✝³ : Algebra A C
inst✝² : IsScalarTower A C L
inst✝¹ : IsSeparable K L
inst✝ : NoZeroSMulDivisors A L
⊢ IsLocalization (algebraMapSubmonoid C A⁰) L
[PROOFSTEP]
haveI : IsDomain C := (IsIntegralClosure.equiv A C L (integralClosure A L)).toMulEquiv.isDomain (integralClosure A L)
[GOAL]
R : Type u_1
A : Type u_2
K : Type u_3
inst✝¹⁶ : CommRing R
inst✝¹⁵ : CommRing A
inst✝¹⁴ : Field K
inst✝¹³ : IsDomain A
inst✝¹² : Algebra A K
inst✝¹¹ : IsFractionRing A K
L : Type u_4
inst✝¹⁰ : Field L
C : Type u_5
inst✝⁹ : CommRing C
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra A L
inst✝⁶ : IsScalarTower A K L
inst✝⁵ : Algebra C L
inst✝⁴ : IsIntegralClosure C A L
inst✝³ : Algebra A C
inst✝² : IsScalarTower A C L
inst✝¹ : IsSeparable K L
inst✝ : NoZeroSMulDivisors A L
this : IsDomain C
⊢ IsLocalization (algebraMapSubmonoid C A⁰) L
[PROOFSTEP]
haveI : NoZeroSMulDivisors A C := IsIntegralClosure.noZeroSMulDivisors A L
[GOAL]
R : Type u_1
A : Type u_2
K : Type u_3
inst✝¹⁶ : CommRing R
inst✝¹⁵ : CommRing A
inst✝¹⁴ : Field K
inst✝¹³ : IsDomain A
inst✝¹² : Algebra A K
inst✝¹¹ : IsFractionRing A K
L : Type u_4
inst✝¹⁰ : Field L
C : Type u_5
inst✝⁹ : CommRing C
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra A L
inst✝⁶ : IsScalarTower A K L
inst✝⁵ : Algebra C L
inst✝⁴ : IsIntegralClosure C A L
inst✝³ : Algebra A C
inst✝² : IsScalarTower A C L
inst✝¹ : IsSeparable K L
inst✝ : NoZeroSMulDivisors A L
this✝ : IsDomain C
this : NoZeroSMulDivisors A C
⊢ IsLocalization (algebraMapSubmonoid C A⁰) L
[PROOFSTEP]
refine' ⟨_, fun z => _, fun {x y} => ⟨fun h => ⟨1, _⟩, _⟩⟩
[GOAL]
case refine'_1
R : Type u_1
A : Type u_2
K : Type u_3
inst✝¹⁶ : CommRing R
inst✝¹⁵ : CommRing A
inst✝¹⁴ : Field K
inst✝¹³ : IsDomain A
inst✝¹² : Algebra A K
inst✝¹¹ : IsFractionRing A K
L : Type u_4
inst✝¹⁰ : Field L
C : Type u_5
inst✝⁹ : CommRing C
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra A L
inst✝⁶ : IsScalarTower A K L
inst✝⁵ : Algebra C L
inst✝⁴ : IsIntegralClosure C A L
inst✝³ : Algebra A C
inst✝² : IsScalarTower A C L
inst✝¹ : IsSeparable K L
inst✝ : NoZeroSMulDivisors A L
this✝ : IsDomain C
this : NoZeroSMulDivisors A C
⊢ ∀ (y : { x // x ∈ algebraMapSubmonoid C A⁰ }), IsUnit (↑(algebraMap C L) ↑y)
[PROOFSTEP]
rintro ⟨_, x, hx, rfl⟩
[GOAL]
case refine'_1.mk.intro.intro
R : Type u_1
A : Type u_2
K : Type u_3
inst✝¹⁶ : CommRing R
inst✝¹⁵ : CommRing A
inst✝¹⁴ : Field K
inst✝¹³ : IsDomain A
inst✝¹² : Algebra A K
inst✝¹¹ : IsFractionRing A K
L : Type u_4
inst✝¹⁰ : Field L
C : Type u_5
inst✝⁹ : CommRing C
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra A L
inst✝⁶ : IsScalarTower A K L
inst✝⁵ : Algebra C L
inst✝⁴ : IsIntegralClosure C A L
inst✝³ : Algebra A C
inst✝² : IsScalarTower A C L
inst✝¹ : IsSeparable K L
inst✝ : NoZeroSMulDivisors A L
this✝ : IsDomain C
this : NoZeroSMulDivisors A C
x : A
hx : x ∈ ↑A⁰
⊢ IsUnit
    (↑(algebraMap C L)
      ↑{ val := ↑(algebraMap A C) x, property := (_ : ∃ a, a ∈ ↑A⁰ ∧ ↑(algebraMap A C) a = ↑(algebraMap A C) x) })
[PROOFSTEP]
rw [isUnit_iff_ne_zero, map_ne_zero_iff _ (IsIntegralClosure.algebraMap_injective C A L), Subtype.coe_mk,
  map_ne_zero_iff _ (NoZeroSMulDivisors.algebraMap_injective A C)]
[GOAL]
case refine'_1.mk.intro.intro
R : Type u_1
A : Type u_2
K : Type u_3
inst✝¹⁶ : CommRing R
inst✝¹⁵ : CommRing A
inst✝¹⁴ : Field K
inst✝¹³ : IsDomain A
inst✝¹² : Algebra A K
inst✝¹¹ : IsFractionRing A K
L : Type u_4
inst✝¹⁰ : Field L
C : Type u_5
inst✝⁹ : CommRing C
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra A L
inst✝⁶ : IsScalarTower A K L
inst✝⁵ : Algebra C L
inst✝⁴ : IsIntegralClosure C A L
inst✝³ : Algebra A C
inst✝² : IsScalarTower A C L
inst✝¹ : IsSeparable K L
inst✝ : NoZeroSMulDivisors A L
this✝ : IsDomain C
this : NoZeroSMulDivisors A C
x : A
hx : x ∈ ↑A⁰
⊢ x ≠ 0
[PROOFSTEP]
exact mem_nonZeroDivisors_iff_ne_zero.mp hx
[GOAL]
case refine'_2
R : Type u_1
A : Type u_2
K : Type u_3
inst✝¹⁶ : CommRing R
inst✝¹⁵ : CommRing A
inst✝¹⁴ : Field K
inst✝¹³ : IsDomain A
inst✝¹² : Algebra A K
inst✝¹¹ : IsFractionRing A K
L : Type u_4
inst✝¹⁰ : Field L
C : Type u_5
inst✝⁹ : CommRing C
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra A L
inst✝⁶ : IsScalarTower A K L
inst✝⁵ : Algebra C L
inst✝⁴ : IsIntegralClosure C A L
inst✝³ : Algebra A C
inst✝² : IsScalarTower A C L
inst✝¹ : IsSeparable K L
inst✝ : NoZeroSMulDivisors A L
this✝ : IsDomain C
this : NoZeroSMulDivisors A C
z : L
⊢ ∃ x, z * ↑(algebraMap C L) ↑x.snd = ↑(algebraMap C L) x.fst
[PROOFSTEP]
obtain ⟨m, hm⟩ := IsIntegral.exists_multiple_integral_of_isLocalization A⁰ z (IsSeparable.isIntegral K z)
[GOAL]
case refine'_2.intro
R : Type u_1
A : Type u_2
K : Type u_3
inst✝¹⁶ : CommRing R
inst✝¹⁵ : CommRing A
inst✝¹⁴ : Field K
inst✝¹³ : IsDomain A
inst✝¹² : Algebra A K
inst✝¹¹ : IsFractionRing A K
L : Type u_4
inst✝¹⁰ : Field L
C : Type u_5
inst✝⁹ : CommRing C
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra A L
inst✝⁶ : IsScalarTower A K L
inst✝⁵ : Algebra C L
inst✝⁴ : IsIntegralClosure C A L
inst✝³ : Algebra A C
inst✝² : IsScalarTower A C L
inst✝¹ : IsSeparable K L
inst✝ : NoZeroSMulDivisors A L
this✝ : IsDomain C
this : NoZeroSMulDivisors A C
z : L
m : { x // x ∈ A⁰ }
hm : IsIntegral A (m • z)
⊢ ∃ x, z * ↑(algebraMap C L) ↑x.snd = ↑(algebraMap C L) x.fst
[PROOFSTEP]
obtain ⟨x, hx⟩ : ∃ x, algebraMap C L x = m • z := IsIntegralClosure.isIntegral_iff.mp hm
[GOAL]
case refine'_2.intro.intro
R : Type u_1
A : Type u_2
K : Type u_3
inst✝¹⁶ : CommRing R
inst✝¹⁵ : CommRing A
inst✝¹⁴ : Field K
inst✝¹³ : IsDomain A
inst✝¹² : Algebra A K
inst✝¹¹ : IsFractionRing A K
L : Type u_4
inst✝¹⁰ : Field L
C : Type u_5
inst✝⁹ : CommRing C
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra A L
inst✝⁶ : IsScalarTower A K L
inst✝⁵ : Algebra C L
inst✝⁴ : IsIntegralClosure C A L
inst✝³ : Algebra A C
inst✝² : IsScalarTower A C L
inst✝¹ : IsSeparable K L
inst✝ : NoZeroSMulDivisors A L
this✝ : IsDomain C
this : NoZeroSMulDivisors A C
z : L
m : { x // x ∈ A⁰ }
hm : IsIntegral A (m • z)
x : C
hx : ↑(algebraMap C L) x = m • z
⊢ ∃ x, z * ↑(algebraMap C L) ↑x.snd = ↑(algebraMap C L) x.fst
[PROOFSTEP]
refine' ⟨⟨x, algebraMap A C m, m, SetLike.coe_mem m, rfl⟩, _⟩
[GOAL]
case refine'_2.intro.intro
R : Type u_1
A : Type u_2
K : Type u_3
inst✝¹⁶ : CommRing R
inst✝¹⁵ : CommRing A
inst✝¹⁴ : Field K
inst✝¹³ : IsDomain A
inst✝¹² : Algebra A K
inst✝¹¹ : IsFractionRing A K
L : Type u_4
inst✝¹⁰ : Field L
C : Type u_5
inst✝⁹ : CommRing C
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra A L
inst✝⁶ : IsScalarTower A K L
inst✝⁵ : Algebra C L
inst✝⁴ : IsIntegralClosure C A L
inst✝³ : Algebra A C
inst✝² : IsScalarTower A C L
inst✝¹ : IsSeparable K L
inst✝ : NoZeroSMulDivisors A L
this✝ : IsDomain C
this : NoZeroSMulDivisors A C
z : L
m : { x // x ∈ A⁰ }
hm : IsIntegral A (m • z)
x : C
hx : ↑(algebraMap C L) x = m • z
⊢ z *
      ↑(algebraMap C L)
        ↑(x,
              { val := ↑(algebraMap A C) ↑m,
                property := (_ : ∃ a, a ∈ ↑A⁰ ∧ ↑(algebraMap A C) a = ↑(algebraMap A C) ↑m) }).snd =
    ↑(algebraMap C L)
      (x,
          { val := ↑(algebraMap A C) ↑m,
            property := (_ : ∃ a, a ∈ ↑A⁰ ∧ ↑(algebraMap A C) a = ↑(algebraMap A C) ↑m) }).fst
[PROOFSTEP]
rw [Subtype.coe_mk, ← IsScalarTower.algebraMap_apply, hx, mul_comm, Submonoid.smul_def, smul_def]
[GOAL]
case refine'_3
R : Type u_1
A : Type u_2
K : Type u_3
inst✝¹⁶ : CommRing R
inst✝¹⁵ : CommRing A
inst✝¹⁴ : Field K
inst✝¹³ : IsDomain A
inst✝¹² : Algebra A K
inst✝¹¹ : IsFractionRing A K
L : Type u_4
inst✝¹⁰ : Field L
C : Type u_5
inst✝⁹ : CommRing C
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra A L
inst✝⁶ : IsScalarTower A K L
inst✝⁵ : Algebra C L
inst✝⁴ : IsIntegralClosure C A L
inst✝³ : Algebra A C
inst✝² : IsScalarTower A C L
inst✝¹ : IsSeparable K L
inst✝ : NoZeroSMulDivisors A L
this✝ : IsDomain C
this : NoZeroSMulDivisors A C
x y : C
h : ↑(algebraMap C L) x = ↑(algebraMap C L) y
⊢ ↑1 * x = ↑1 * y
[PROOFSTEP]
simp only [IsIntegralClosure.algebraMap_injective C A L h]
[GOAL]
case refine'_4
R : Type u_1
A : Type u_2
K : Type u_3
inst✝¹⁶ : CommRing R
inst✝¹⁵ : CommRing A
inst✝¹⁴ : Field K
inst✝¹³ : IsDomain A
inst✝¹² : Algebra A K
inst✝¹¹ : IsFractionRing A K
L : Type u_4
inst✝¹⁰ : Field L
C : Type u_5
inst✝⁹ : CommRing C
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra A L
inst✝⁶ : IsScalarTower A K L
inst✝⁵ : Algebra C L
inst✝⁴ : IsIntegralClosure C A L
inst✝³ : Algebra A C
inst✝² : IsScalarTower A C L
inst✝¹ : IsSeparable K L
inst✝ : NoZeroSMulDivisors A L
this✝ : IsDomain C
this : NoZeroSMulDivisors A C
x y : C
⊢ (∃ c, ↑c * x = ↑c * y) → ↑(algebraMap C L) x = ↑(algebraMap C L) y
[PROOFSTEP]
rintro ⟨⟨_, m, hm, rfl⟩, h⟩
[GOAL]
case refine'_4.intro.mk.intro.intro
R : Type u_1
A : Type u_2
K : Type u_3
inst✝¹⁶ : CommRing R
inst✝¹⁵ : CommRing A
inst✝¹⁴ : Field K
inst✝¹³ : IsDomain A
inst✝¹² : Algebra A K
inst✝¹¹ : IsFractionRing A K
L : Type u_4
inst✝¹⁰ : Field L
C : Type u_5
inst✝⁹ : CommRing C
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra A L
inst✝⁶ : IsScalarTower A K L
inst✝⁵ : Algebra C L
inst✝⁴ : IsIntegralClosure C A L
inst✝³ : Algebra A C
inst✝² : IsScalarTower A C L
inst✝¹ : IsSeparable K L
inst✝ : NoZeroSMulDivisors A L
this✝ : IsDomain C
this : NoZeroSMulDivisors A C
x y : C
m : A
hm : m ∈ ↑A⁰
h :
  ↑{ val := ↑(algebraMap A C) m, property := (_ : ∃ a, a ∈ ↑A⁰ ∧ ↑(algebraMap A C) a = ↑(algebraMap A C) m) } * x =
    ↑{ val := ↑(algebraMap A C) m, property := (_ : ∃ a, a ∈ ↑A⁰ ∧ ↑(algebraMap A C) a = ↑(algebraMap A C) m) } * y
⊢ ↑(algebraMap C L) x = ↑(algebraMap C L) y
[PROOFSTEP]
refine' congr_arg (algebraMap C L) ((mul_right_inj' _).mp h)
[GOAL]
case refine'_4.intro.mk.intro.intro
R : Type u_1
A : Type u_2
K : Type u_3
inst✝¹⁶ : CommRing R
inst✝¹⁵ : CommRing A
inst✝¹⁴ : Field K
inst✝¹³ : IsDomain A
inst✝¹² : Algebra A K
inst✝¹¹ : IsFractionRing A K
L : Type u_4
inst✝¹⁰ : Field L
C : Type u_5
inst✝⁹ : CommRing C
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra A L
inst✝⁶ : IsScalarTower A K L
inst✝⁵ : Algebra C L
inst✝⁴ : IsIntegralClosure C A L
inst✝³ : Algebra A C
inst✝² : IsScalarTower A C L
inst✝¹ : IsSeparable K L
inst✝ : NoZeroSMulDivisors A L
this✝ : IsDomain C
this : NoZeroSMulDivisors A C
x y : C
m : A
hm : m ∈ ↑A⁰
h :
  ↑{ val := ↑(algebraMap A C) m, property := (_ : ∃ a, a ∈ ↑A⁰ ∧ ↑(algebraMap A C) a = ↑(algebraMap A C) m) } * x =
    ↑{ val := ↑(algebraMap A C) m, property := (_ : ∃ a, a ∈ ↑A⁰ ∧ ↑(algebraMap A C) a = ↑(algebraMap A C) m) } * y
⊢ ↑{ val := ↑(algebraMap A C) m, property := (_ : ∃ a, a ∈ ↑A⁰ ∧ ↑(algebraMap A C) a = ↑(algebraMap A C) m) } ≠ 0
[PROOFSTEP]
rw [Subtype.coe_mk, map_ne_zero_iff _ (NoZeroSMulDivisors.algebraMap_injective A C)]
[GOAL]
case refine'_4.intro.mk.intro.intro
R : Type u_1
A : Type u_2
K : Type u_3
inst✝¹⁶ : CommRing R
inst✝¹⁵ : CommRing A
inst✝¹⁴ : Field K
inst✝¹³ : IsDomain A
inst✝¹² : Algebra A K
inst✝¹¹ : IsFractionRing A K
L : Type u_4
inst✝¹⁰ : Field L
C : Type u_5
inst✝⁹ : CommRing C
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra A L
inst✝⁶ : IsScalarTower A K L
inst✝⁵ : Algebra C L
inst✝⁴ : IsIntegralClosure C A L
inst✝³ : Algebra A C
inst✝² : IsScalarTower A C L
inst✝¹ : IsSeparable K L
inst✝ : NoZeroSMulDivisors A L
this✝ : IsDomain C
this : NoZeroSMulDivisors A C
x y : C
m : A
hm : m ∈ ↑A⁰
h :
  ↑{ val := ↑(algebraMap A C) m, property := (_ : ∃ a, a ∈ ↑A⁰ ∧ ↑(algebraMap A C) a = ↑(algebraMap A C) m) } * x =
    ↑{ val := ↑(algebraMap A C) m, property := (_ : ∃ a, a ∈ ↑A⁰ ∧ ↑(algebraMap A C) a = ↑(algebraMap A C) m) } * y
⊢ m ≠ 0
[PROOFSTEP]
exact mem_nonZeroDivisors_iff_ne_zero.mp hm
[GOAL]
R : Type u_1
A : Type u_2
K : Type u_3
inst✝¹⁹ : CommRing R
inst✝¹⁸ : CommRing A
inst✝¹⁷ : Field K
inst✝¹⁶ : IsDomain A
inst✝¹⁵ : Algebra A K
inst✝¹⁴ : IsFractionRing A K
L : Type u_4
inst✝¹³ : Field L
C : Type u_5
inst✝¹² : CommRing C
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A L
inst✝⁹ : IsScalarTower A K L
inst✝⁸ : Algebra C L
inst✝⁷ : IsIntegralClosure C A L
inst✝⁶ : Algebra A C
inst✝⁵ : IsScalarTower A C L
inst✝⁴ : FiniteDimensional K L
inst✝³ : IsSeparable K L
ι : Type u_6
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
b : Basis ι K L
hb_int : ∀ (i : ι), IsIntegral A (↑b i)
inst✝ : IsIntegrallyClosed A
⊢ LinearMap.range (↑A (Algebra.linearMap C L)) ≤
    Submodule.span A (Set.range ↑(BilinForm.dualBasis (traceForm K L) (_ : BilinForm.Nondegenerate (traceForm K L)) b))
[PROOFSTEP]
let db := (traceForm K L).dualBasis (traceForm_nondegenerate K L) b
[GOAL]
R : Type u_1
A : Type u_2
K : Type u_3
inst✝¹⁹ : CommRing R
inst✝¹⁸ : CommRing A
inst✝¹⁷ : Field K
inst✝¹⁶ : IsDomain A
inst✝¹⁵ : Algebra A K
inst✝¹⁴ : IsFractionRing A K
L : Type u_4
inst✝¹³ : Field L
C : Type u_5
inst✝¹² : CommRing C
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A L
inst✝⁹ : IsScalarTower A K L
inst✝⁸ : Algebra C L
inst✝⁷ : IsIntegralClosure C A L
inst✝⁶ : Algebra A C
inst✝⁵ : IsScalarTower A C L
inst✝⁴ : FiniteDimensional K L
inst✝³ : IsSeparable K L
ι : Type u_6
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
b : Basis ι K L
hb_int : ∀ (i : ι), IsIntegral A (↑b i)
inst✝ : IsIntegrallyClosed A
db : Basis ι K L := BilinForm.dualBasis (traceForm K L) (_ : BilinForm.Nondegenerate (traceForm K L)) b
⊢ LinearMap.range (↑A (Algebra.linearMap C L)) ≤
    Submodule.span A (Set.range ↑(BilinForm.dualBasis (traceForm K L) (_ : BilinForm.Nondegenerate (traceForm K L)) b))
[PROOFSTEP]
rintro _ ⟨x, rfl⟩
[GOAL]
case intro
R : Type u_1
A : Type u_2
K : Type u_3
inst✝¹⁹ : CommRing R
inst✝¹⁸ : CommRing A
inst✝¹⁷ : Field K
inst✝¹⁶ : IsDomain A
inst✝¹⁵ : Algebra A K
inst✝¹⁴ : IsFractionRing A K
L : Type u_4
inst✝¹³ : Field L
C : Type u_5
inst✝¹² : CommRing C
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A L
inst✝⁹ : IsScalarTower A K L
inst✝⁸ : Algebra C L
inst✝⁷ : IsIntegralClosure C A L
inst✝⁶ : Algebra A C
inst✝⁵ : IsScalarTower A C L
inst✝⁴ : FiniteDimensional K L
inst✝³ : IsSeparable K L
ι : Type u_6
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
b : Basis ι K L
hb_int : ∀ (i : ι), IsIntegral A (↑b i)
inst✝ : IsIntegrallyClosed A
db : Basis ι K L := BilinForm.dualBasis (traceForm K L) (_ : BilinForm.Nondegenerate (traceForm K L)) b
x : C
⊢ ↑(↑A (Algebra.linearMap C L)) x ∈
    Submodule.span A (Set.range ↑(BilinForm.dualBasis (traceForm K L) (_ : BilinForm.Nondegenerate (traceForm K L)) b))
[PROOFSTEP]
simp only [LinearMap.coe_restrictScalars, Algebra.linearMap_apply]
[GOAL]
case intro
R : Type u_1
A : Type u_2
K : Type u_3
inst✝¹⁹ : CommRing R
inst✝¹⁸ : CommRing A
inst✝¹⁷ : Field K
inst✝¹⁶ : IsDomain A
inst✝¹⁵ : Algebra A K
inst✝¹⁴ : IsFractionRing A K
L : Type u_4
inst✝¹³ : Field L
C : Type u_5
inst✝¹² : CommRing C
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A L
inst✝⁹ : IsScalarTower A K L
inst✝⁸ : Algebra C L
inst✝⁷ : IsIntegralClosure C A L
inst✝⁶ : Algebra A C
inst✝⁵ : IsScalarTower A C L
inst✝⁴ : FiniteDimensional K L
inst✝³ : IsSeparable K L
ι : Type u_6
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
b : Basis ι K L
hb_int : ∀ (i : ι), IsIntegral A (↑b i)
inst✝ : IsIntegrallyClosed A
db : Basis ι K L := BilinForm.dualBasis (traceForm K L) (_ : BilinForm.Nondegenerate (traceForm K L)) b
x : C
⊢ ↑(algebraMap C L) x ∈
    Submodule.span A (Set.range ↑(BilinForm.dualBasis (traceForm K L) (_ : BilinForm.Nondegenerate (traceForm K L)) b))
[PROOFSTEP]
have hx : IsIntegral A (algebraMap C L x) := (IsIntegralClosure.isIntegral A L x).algebraMap
[GOAL]
case intro
R : Type u_1
A : Type u_2
K : Type u_3
inst✝¹⁹ : CommRing R
inst✝¹⁸ : CommRing A
inst✝¹⁷ : Field K
inst✝¹⁶ : IsDomain A
inst✝¹⁵ : Algebra A K
inst✝¹⁴ : IsFractionRing A K
L : Type u_4
inst✝¹³ : Field L
C : Type u_5
inst✝¹² : CommRing C
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A L
inst✝⁹ : IsScalarTower A K L
inst✝⁸ : Algebra C L
inst✝⁷ : IsIntegralClosure C A L
inst✝⁶ : Algebra A C
inst✝⁵ : IsScalarTower A C L
inst✝⁴ : FiniteDimensional K L
inst✝³ : IsSeparable K L
ι : Type u_6
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
b : Basis ι K L
hb_int : ∀ (i : ι), IsIntegral A (↑b i)
inst✝ : IsIntegrallyClosed A
db : Basis ι K L := BilinForm.dualBasis (traceForm K L) (_ : BilinForm.Nondegenerate (traceForm K L)) b
x : C
hx : IsIntegral A (↑(algebraMap C L) x)
⊢ ↑(algebraMap C L) x ∈
    Submodule.span A (Set.range ↑(BilinForm.dualBasis (traceForm K L) (_ : BilinForm.Nondegenerate (traceForm K L)) b))
[PROOFSTEP]
rsuffices ⟨c, x_eq⟩ : ∃ c : ι → A, algebraMap C L x = ∑ i, c i • db i
[GOAL]
case intro.intro
R : Type u_1
A : Type u_2
K : Type u_3
inst✝¹⁹ : CommRing R
inst✝¹⁸ : CommRing A
inst✝¹⁷ : Field K
inst✝¹⁶ : IsDomain A
inst✝¹⁵ : Algebra A K
inst✝¹⁴ : IsFractionRing A K
L : Type u_4
inst✝¹³ : Field L
C : Type u_5
inst✝¹² : CommRing C
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A L
inst✝⁹ : IsScalarTower A K L
inst✝⁸ : Algebra C L
inst✝⁷ : IsIntegralClosure C A L
inst✝⁶ : Algebra A C
inst✝⁵ : IsScalarTower A C L
inst✝⁴ : FiniteDimensional K L
inst✝³ : IsSeparable K L
ι : Type u_6
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
b : Basis ι K L
hb_int : ∀ (i : ι), IsIntegral A (↑b i)
inst✝ : IsIntegrallyClosed A
db : Basis ι K L := BilinForm.dualBasis (traceForm K L) (_ : BilinForm.Nondegenerate (traceForm K L)) b
x : C
hx : IsIntegral A (↑(algebraMap C L) x)
c : ι → A
x_eq : ↑(algebraMap C L) x = ∑ i : ι, c i • ↑db i
⊢ ↑(algebraMap C L) x ∈
    Submodule.span A (Set.range ↑(BilinForm.dualBasis (traceForm K L) (_ : BilinForm.Nondegenerate (traceForm K L)) b))
[PROOFSTEP]
rw [x_eq]
[GOAL]
case intro.intro
R : Type u_1
A : Type u_2
K : Type u_3
inst✝¹⁹ : CommRing R
inst✝¹⁸ : CommRing A
inst✝¹⁷ : Field K
inst✝¹⁶ : IsDomain A
inst✝¹⁵ : Algebra A K
inst✝¹⁴ : IsFractionRing A K
L : Type u_4
inst✝¹³ : Field L
C : Type u_5
inst✝¹² : CommRing C
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A L
inst✝⁹ : IsScalarTower A K L
inst✝⁸ : Algebra C L
inst✝⁷ : IsIntegralClosure C A L
inst✝⁶ : Algebra A C
inst✝⁵ : IsScalarTower A C L
inst✝⁴ : FiniteDimensional K L
inst✝³ : IsSeparable K L
ι : Type u_6
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
b : Basis ι K L
hb_int : ∀ (i : ι), IsIntegral A (↑b i)
inst✝ : IsIntegrallyClosed A
db : Basis ι K L := BilinForm.dualBasis (traceForm K L) (_ : BilinForm.Nondegenerate (traceForm K L)) b
x : C
hx : IsIntegral A (↑(algebraMap C L) x)
c : ι → A
x_eq : ↑(algebraMap C L) x = ∑ i : ι, c i • ↑db i
⊢ ∑ i : ι, c i • ↑db i ∈
    Submodule.span A (Set.range ↑(BilinForm.dualBasis (traceForm K L) (_ : BilinForm.Nondegenerate (traceForm K L)) b))
[PROOFSTEP]
refine' Submodule.sum_mem _ fun i _ => Submodule.smul_mem _ _ (Submodule.subset_span _)
[GOAL]
case intro.intro
R : Type u_1
A : Type u_2
K : Type u_3
inst✝¹⁹ : CommRing R
inst✝¹⁸ : CommRing A
inst✝¹⁷ : Field K
inst✝¹⁶ : IsDomain A
inst✝¹⁵ : Algebra A K
inst✝¹⁴ : IsFractionRing A K
L : Type u_4
inst✝¹³ : Field L
C : Type u_5
inst✝¹² : CommRing C
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A L
inst✝⁹ : IsScalarTower A K L
inst✝⁸ : Algebra C L
inst✝⁷ : IsIntegralClosure C A L
inst✝⁶ : Algebra A C
inst✝⁵ : IsScalarTower A C L
inst✝⁴ : FiniteDimensional K L
inst✝³ : IsSeparable K L
ι : Type u_6
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
b : Basis ι K L
hb_int : ∀ (i : ι), IsIntegral A (↑b i)
inst✝ : IsIntegrallyClosed A
db : Basis ι K L := BilinForm.dualBasis (traceForm K L) (_ : BilinForm.Nondegenerate (traceForm K L)) b
x : C
hx : IsIntegral A (↑(algebraMap C L) x)
c : ι → A
x_eq : ↑(algebraMap C L) x = ∑ i : ι, c i • ↑db i
i : ι
x✝ : i ∈ Finset.univ
⊢ ↑db i ∈ Set.range ↑(BilinForm.dualBasis (traceForm K L) (_ : BilinForm.Nondegenerate (traceForm K L)) b)
[PROOFSTEP]
rw [Set.mem_range]
[GOAL]
case intro.intro
R : Type u_1
A : Type u_2
K : Type u_3
inst✝¹⁹ : CommRing R
inst✝¹⁸ : CommRing A
inst✝¹⁷ : Field K
inst✝¹⁶ : IsDomain A
inst✝¹⁵ : Algebra A K
inst✝¹⁴ : IsFractionRing A K
L : Type u_4
inst✝¹³ : Field L
C : Type u_5
inst✝¹² : CommRing C
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A L
inst✝⁹ : IsScalarTower A K L
inst✝⁸ : Algebra C L
inst✝⁷ : IsIntegralClosure C A L
inst✝⁶ : Algebra A C
inst✝⁵ : IsScalarTower A C L
inst✝⁴ : FiniteDimensional K L
inst✝³ : IsSeparable K L
ι : Type u_6
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
b : Basis ι K L
hb_int : ∀ (i : ι), IsIntegral A (↑b i)
inst✝ : IsIntegrallyClosed A
db : Basis ι K L := BilinForm.dualBasis (traceForm K L) (_ : BilinForm.Nondegenerate (traceForm K L)) b
x : C
hx : IsIntegral A (↑(algebraMap C L) x)
c : ι → A
x_eq : ↑(algebraMap C L) x = ∑ i : ι, c i • ↑db i
i : ι
x✝ : i ∈ Finset.univ
⊢ ∃ y, ↑(BilinForm.dualBasis (traceForm K L) (_ : BilinForm.Nondegenerate (traceForm K L)) b) y = ↑db i
[PROOFSTEP]
exact ⟨i, rfl⟩
[GOAL]
R : Type u_1
A : Type u_2
K : Type u_3
inst✝¹⁹ : CommRing R
inst✝¹⁸ : CommRing A
inst✝¹⁷ : Field K
inst✝¹⁶ : IsDomain A
inst✝¹⁵ : Algebra A K
inst✝¹⁴ : IsFractionRing A K
L : Type u_4
inst✝¹³ : Field L
C : Type u_5
inst✝¹² : CommRing C
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A L
inst✝⁹ : IsScalarTower A K L
inst✝⁸ : Algebra C L
inst✝⁷ : IsIntegralClosure C A L
inst✝⁶ : Algebra A C
inst✝⁵ : IsScalarTower A C L
inst✝⁴ : FiniteDimensional K L
inst✝³ : IsSeparable K L
ι : Type u_6
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
b : Basis ι K L
hb_int : ∀ (i : ι), IsIntegral A (↑b i)
inst✝ : IsIntegrallyClosed A
db : Basis ι K L := BilinForm.dualBasis (traceForm K L) (_ : BilinForm.Nondegenerate (traceForm K L)) b
x : C
hx : IsIntegral A (↑(algebraMap C L) x)
⊢ ∃ c, ↑(algebraMap C L) x = ∑ i : ι, c i • ↑db i
[PROOFSTEP]
suffices ∃ c : ι → K, (∀ i, IsIntegral A (c i)) ∧ algebraMap C L x = ∑ i, c i • db i
  by
  obtain ⟨c, hc, hx⟩ := this
  have hc' : ∀ i, IsLocalization.IsInteger A (c i) := fun i => IsIntegrallyClosed.isIntegral_iff.mp (hc i)
  use fun i => Classical.choose (hc' i)
  refine' hx.trans (Finset.sum_congr rfl fun i _ => _)
  conv_lhs => rw [← Classical.choose_spec (hc' i)]
  rw [← IsScalarTower.algebraMap_smul K (Classical.choose (hc' i)) (db i)]
[GOAL]
R : Type u_1
A : Type u_2
K : Type u_3
inst✝¹⁹ : CommRing R
inst✝¹⁸ : CommRing A
inst✝¹⁷ : Field K
inst✝¹⁶ : IsDomain A
inst✝¹⁵ : Algebra A K
inst✝¹⁴ : IsFractionRing A K
L : Type u_4
inst✝¹³ : Field L
C : Type u_5
inst✝¹² : CommRing C
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A L
inst✝⁹ : IsScalarTower A K L
inst✝⁸ : Algebra C L
inst✝⁷ : IsIntegralClosure C A L
inst✝⁶ : Algebra A C
inst✝⁵ : IsScalarTower A C L
inst✝⁴ : FiniteDimensional K L
inst✝³ : IsSeparable K L
ι : Type u_6
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
b : Basis ι K L
hb_int : ∀ (i : ι), IsIntegral A (↑b i)
inst✝ : IsIntegrallyClosed A
db : Basis ι K L := BilinForm.dualBasis (traceForm K L) (_ : BilinForm.Nondegenerate (traceForm K L)) b
x : C
hx : IsIntegral A (↑(algebraMap C L) x)
this : ∃ c, (∀ (i : ι), IsIntegral A (c i)) ∧ ↑(algebraMap C L) x = ∑ i : ι, c i • ↑db i
⊢ ∃ c, ↑(algebraMap C L) x = ∑ i : ι, c i • ↑db i
[PROOFSTEP]
obtain ⟨c, hc, hx⟩ := this
[GOAL]
case intro.intro
R : Type u_1
A : Type u_2
K : Type u_3
inst✝¹⁹ : CommRing R
inst✝¹⁸ : CommRing A
inst✝¹⁷ : Field K
inst✝¹⁶ : IsDomain A
inst✝¹⁵ : Algebra A K
inst✝¹⁴ : IsFractionRing A K
L : Type u_4
inst✝¹³ : Field L
C : Type u_5
inst✝¹² : CommRing C
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A L
inst✝⁹ : IsScalarTower A K L
inst✝⁸ : Algebra C L
inst✝⁷ : IsIntegralClosure C A L
inst✝⁶ : Algebra A C
inst✝⁵ : IsScalarTower A C L
inst✝⁴ : FiniteDimensional K L
inst✝³ : IsSeparable K L
ι : Type u_6
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
b : Basis ι K L
hb_int : ∀ (i : ι), IsIntegral A (↑b i)
inst✝ : IsIntegrallyClosed A
db : Basis ι K L := BilinForm.dualBasis (traceForm K L) (_ : BilinForm.Nondegenerate (traceForm K L)) b
x : C
hx✝ : IsIntegral A (↑(algebraMap C L) x)
c : ι → K
hc : ∀ (i : ι), IsIntegral A (c i)
hx : ↑(algebraMap C L) x = ∑ i : ι, c i • ↑db i
⊢ ∃ c, ↑(algebraMap C L) x = ∑ i : ι, c i • ↑db i
[PROOFSTEP]
have hc' : ∀ i, IsLocalization.IsInteger A (c i) := fun i => IsIntegrallyClosed.isIntegral_iff.mp (hc i)
[GOAL]
case intro.intro
R : Type u_1
A : Type u_2
K : Type u_3
inst✝¹⁹ : CommRing R
inst✝¹⁸ : CommRing A
inst✝¹⁷ : Field K
inst✝¹⁶ : IsDomain A
inst✝¹⁵ : Algebra A K
inst✝¹⁴ : IsFractionRing A K
L : Type u_4
inst✝¹³ : Field L
C : Type u_5
inst✝¹² : CommRing C
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A L
inst✝⁹ : IsScalarTower A K L
inst✝⁸ : Algebra C L
inst✝⁷ : IsIntegralClosure C A L
inst✝⁶ : Algebra A C
inst✝⁵ : IsScalarTower A C L
inst✝⁴ : FiniteDimensional K L
inst✝³ : IsSeparable K L
ι : Type u_6
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
b : Basis ι K L
hb_int : ∀ (i : ι), IsIntegral A (↑b i)
inst✝ : IsIntegrallyClosed A
db : Basis ι K L := BilinForm.dualBasis (traceForm K L) (_ : BilinForm.Nondegenerate (traceForm K L)) b
x : C
hx✝ : IsIntegral A (↑(algebraMap C L) x)
c : ι → K
hc : ∀ (i : ι), IsIntegral A (c i)
hx : ↑(algebraMap C L) x = ∑ i : ι, c i • ↑db i
hc' : ∀ (i : ι), IsLocalization.IsInteger A (c i)
⊢ ∃ c, ↑(algebraMap C L) x = ∑ i : ι, c i • ↑db i
[PROOFSTEP]
use fun i => Classical.choose (hc' i)
[GOAL]
case h
R : Type u_1
A : Type u_2
K : Type u_3
inst✝¹⁹ : CommRing R
inst✝¹⁸ : CommRing A
inst✝¹⁷ : Field K
inst✝¹⁶ : IsDomain A
inst✝¹⁵ : Algebra A K
inst✝¹⁴ : IsFractionRing A K
L : Type u_4
inst✝¹³ : Field L
C : Type u_5
inst✝¹² : CommRing C
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A L
inst✝⁹ : IsScalarTower A K L
inst✝⁸ : Algebra C L
inst✝⁷ : IsIntegralClosure C A L
inst✝⁶ : Algebra A C
inst✝⁵ : IsScalarTower A C L
inst✝⁴ : FiniteDimensional K L
inst✝³ : IsSeparable K L
ι : Type u_6
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
b : Basis ι K L
hb_int : ∀ (i : ι), IsIntegral A (↑b i)
inst✝ : IsIntegrallyClosed A
db : Basis ι K L := BilinForm.dualBasis (traceForm K L) (_ : BilinForm.Nondegenerate (traceForm K L)) b
x : C
hx✝ : IsIntegral A (↑(algebraMap C L) x)
c : ι → K
hc : ∀ (i : ι), IsIntegral A (c i)
hx : ↑(algebraMap C L) x = ∑ i : ι, c i • ↑db i
hc' : ∀ (i : ι), IsLocalization.IsInteger A (c i)
⊢ ↑(algebraMap C L) x = ∑ i : ι, Classical.choose (_ : IsLocalization.IsInteger A (c i)) • ↑db i
[PROOFSTEP]
refine' hx.trans (Finset.sum_congr rfl fun i _ => _)
[GOAL]
case h
R : Type u_1
A : Type u_2
K : Type u_3
inst✝¹⁹ : CommRing R
inst✝¹⁸ : CommRing A
inst✝¹⁷ : Field K
inst✝¹⁶ : IsDomain A
inst✝¹⁵ : Algebra A K
inst✝¹⁴ : IsFractionRing A K
L : Type u_4
inst✝¹³ : Field L
C : Type u_5
inst✝¹² : CommRing C
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A L
inst✝⁹ : IsScalarTower A K L
inst✝⁸ : Algebra C L
inst✝⁷ : IsIntegralClosure C A L
inst✝⁶ : Algebra A C
inst✝⁵ : IsScalarTower A C L
inst✝⁴ : FiniteDimensional K L
inst✝³ : IsSeparable K L
ι : Type u_6
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
b : Basis ι K L
hb_int : ∀ (i : ι), IsIntegral A (↑b i)
inst✝ : IsIntegrallyClosed A
db : Basis ι K L := BilinForm.dualBasis (traceForm K L) (_ : BilinForm.Nondegenerate (traceForm K L)) b
x : C
hx✝ : IsIntegral A (↑(algebraMap C L) x)
c : ι → K
hc : ∀ (i : ι), IsIntegral A (c i)
hx : ↑(algebraMap C L) x = ∑ i : ι, c i • ↑db i
hc' : ∀ (i : ι), IsLocalization.IsInteger A (c i)
i : ι
x✝ : i ∈ Finset.univ
⊢ c i • ↑db i = Classical.choose (_ : IsLocalization.IsInteger A (c i)) • ↑db i
[PROOFSTEP]
conv_lhs => rw [← Classical.choose_spec (hc' i)]
[GOAL]
R : Type u_1
A : Type u_2
K : Type u_3
inst✝¹⁹ : CommRing R
inst✝¹⁸ : CommRing A
inst✝¹⁷ : Field K
inst✝¹⁶ : IsDomain A
inst✝¹⁵ : Algebra A K
inst✝¹⁴ : IsFractionRing A K
L : Type u_4
inst✝¹³ : Field L
C : Type u_5
inst✝¹² : CommRing C
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A L
inst✝⁹ : IsScalarTower A K L
inst✝⁸ : Algebra C L
inst✝⁷ : IsIntegralClosure C A L
inst✝⁶ : Algebra A C
inst✝⁵ : IsScalarTower A C L
inst✝⁴ : FiniteDimensional K L
inst✝³ : IsSeparable K L
ι : Type u_6
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
b : Basis ι K L
hb_int : ∀ (i : ι), IsIntegral A (↑b i)
inst✝ : IsIntegrallyClosed A
db : Basis ι K L := BilinForm.dualBasis (traceForm K L) (_ : BilinForm.Nondegenerate (traceForm K L)) b
x : C
hx✝ : IsIntegral A (↑(algebraMap C L) x)
c : ι → K
hc : ∀ (i : ι), IsIntegral A (c i)
hx : ↑(algebraMap C L) x = ∑ i : ι, c i • ↑db i
hc' : ∀ (i : ι), IsLocalization.IsInteger A (c i)
i : ι
x✝ : i ∈ Finset.univ
| c i • ↑db i
[PROOFSTEP]
rw [← Classical.choose_spec (hc' i)]
[GOAL]
R : Type u_1
A : Type u_2
K : Type u_3
inst✝¹⁹ : CommRing R
inst✝¹⁸ : CommRing A
inst✝¹⁷ : Field K
inst✝¹⁶ : IsDomain A
inst✝¹⁵ : Algebra A K
inst✝¹⁴ : IsFractionRing A K
L : Type u_4
inst✝¹³ : Field L
C : Type u_5
inst✝¹² : CommRing C
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A L
inst✝⁹ : IsScalarTower A K L
inst✝⁸ : Algebra C L
inst✝⁷ : IsIntegralClosure C A L
inst✝⁶ : Algebra A C
inst✝⁵ : IsScalarTower A C L
inst✝⁴ : FiniteDimensional K L
inst✝³ : IsSeparable K L
ι : Type u_6
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
b : Basis ι K L
hb_int : ∀ (i : ι), IsIntegral A (↑b i)
inst✝ : IsIntegrallyClosed A
db : Basis ι K L := BilinForm.dualBasis (traceForm K L) (_ : BilinForm.Nondegenerate (traceForm K L)) b
x : C
hx✝ : IsIntegral A (↑(algebraMap C L) x)
c : ι → K
hc : ∀ (i : ι), IsIntegral A (c i)
hx : ↑(algebraMap C L) x = ∑ i : ι, c i • ↑db i
hc' : ∀ (i : ι), IsLocalization.IsInteger A (c i)
i : ι
x✝ : i ∈ Finset.univ
| c i • ↑db i
[PROOFSTEP]
rw [← Classical.choose_spec (hc' i)]
[GOAL]
R : Type u_1
A : Type u_2
K : Type u_3
inst✝¹⁹ : CommRing R
inst✝¹⁸ : CommRing A
inst✝¹⁷ : Field K
inst✝¹⁶ : IsDomain A
inst✝¹⁵ : Algebra A K
inst✝¹⁴ : IsFractionRing A K
L : Type u_4
inst✝¹³ : Field L
C : Type u_5
inst✝¹² : CommRing C
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A L
inst✝⁹ : IsScalarTower A K L
inst✝⁸ : Algebra C L
inst✝⁷ : IsIntegralClosure C A L
inst✝⁶ : Algebra A C
inst✝⁵ : IsScalarTower A C L
inst✝⁴ : FiniteDimensional K L
inst✝³ : IsSeparable K L
ι : Type u_6
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
b : Basis ι K L
hb_int : ∀ (i : ι), IsIntegral A (↑b i)
inst✝ : IsIntegrallyClosed A
db : Basis ι K L := BilinForm.dualBasis (traceForm K L) (_ : BilinForm.Nondegenerate (traceForm K L)) b
x : C
hx✝ : IsIntegral A (↑(algebraMap C L) x)
c : ι → K
hc : ∀ (i : ι), IsIntegral A (c i)
hx : ↑(algebraMap C L) x = ∑ i : ι, c i • ↑db i
hc' : ∀ (i : ι), IsLocalization.IsInteger A (c i)
i : ι
x✝ : i ∈ Finset.univ
| c i • ↑db i
[PROOFSTEP]
rw [← Classical.choose_spec (hc' i)]
[GOAL]
case h
R : Type u_1
A : Type u_2
K : Type u_3
inst✝¹⁹ : CommRing R
inst✝¹⁸ : CommRing A
inst✝¹⁷ : Field K
inst✝¹⁶ : IsDomain A
inst✝¹⁵ : Algebra A K
inst✝¹⁴ : IsFractionRing A K
L : Type u_4
inst✝¹³ : Field L
C : Type u_5
inst✝¹² : CommRing C
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A L
inst✝⁹ : IsScalarTower A K L
inst✝⁸ : Algebra C L
inst✝⁷ : IsIntegralClosure C A L
inst✝⁶ : Algebra A C
inst✝⁵ : IsScalarTower A C L
inst✝⁴ : FiniteDimensional K L
inst✝³ : IsSeparable K L
ι : Type u_6
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
b : Basis ι K L
hb_int : ∀ (i : ι), IsIntegral A (↑b i)
inst✝ : IsIntegrallyClosed A
db : Basis ι K L := BilinForm.dualBasis (traceForm K L) (_ : BilinForm.Nondegenerate (traceForm K L)) b
x : C
hx✝ : IsIntegral A (↑(algebraMap C L) x)
c : ι → K
hc : ∀ (i : ι), IsIntegral A (c i)
hx : ↑(algebraMap C L) x = ∑ i : ι, c i • ↑db i
hc' : ∀ (i : ι), IsLocalization.IsInteger A (c i)
i : ι
x✝ : i ∈ Finset.univ
⊢ ↑(algebraMap A K) (Classical.choose (_ : IsLocalization.IsInteger A (c i))) • ↑db i =
    Classical.choose (_ : IsLocalization.IsInteger A (c i)) • ↑db i
[PROOFSTEP]
rw [← IsScalarTower.algebraMap_smul K (Classical.choose (hc' i)) (db i)]
[GOAL]
R : Type u_1
A : Type u_2
K : Type u_3
inst✝¹⁹ : CommRing R
inst✝¹⁸ : CommRing A
inst✝¹⁷ : Field K
inst✝¹⁶ : IsDomain A
inst✝¹⁵ : Algebra A K
inst✝¹⁴ : IsFractionRing A K
L : Type u_4
inst✝¹³ : Field L
C : Type u_5
inst✝¹² : CommRing C
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A L
inst✝⁹ : IsScalarTower A K L
inst✝⁸ : Algebra C L
inst✝⁷ : IsIntegralClosure C A L
inst✝⁶ : Algebra A C
inst✝⁵ : IsScalarTower A C L
inst✝⁴ : FiniteDimensional K L
inst✝³ : IsSeparable K L
ι : Type u_6
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
b : Basis ι K L
hb_int : ∀ (i : ι), IsIntegral A (↑b i)
inst✝ : IsIntegrallyClosed A
db : Basis ι K L := BilinForm.dualBasis (traceForm K L) (_ : BilinForm.Nondegenerate (traceForm K L)) b
x : C
hx : IsIntegral A (↑(algebraMap C L) x)
⊢ ∃ c, (∀ (i : ι), IsIntegral A (c i)) ∧ ↑(algebraMap C L) x = ∑ i : ι, c i • ↑db i
[PROOFSTEP]
refine' ⟨fun i => db.repr (algebraMap C L x) i, fun i => _, (db.sum_repr _).symm⟩
[GOAL]
R : Type u_1
A : Type u_2
K : Type u_3
inst✝¹⁹ : CommRing R
inst✝¹⁸ : CommRing A
inst✝¹⁷ : Field K
inst✝¹⁶ : IsDomain A
inst✝¹⁵ : Algebra A K
inst✝¹⁴ : IsFractionRing A K
L : Type u_4
inst✝¹³ : Field L
C : Type u_5
inst✝¹² : CommRing C
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A L
inst✝⁹ : IsScalarTower A K L
inst✝⁸ : Algebra C L
inst✝⁷ : IsIntegralClosure C A L
inst✝⁶ : Algebra A C
inst✝⁵ : IsScalarTower A C L
inst✝⁴ : FiniteDimensional K L
inst✝³ : IsSeparable K L
ι : Type u_6
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
b : Basis ι K L
hb_int : ∀ (i : ι), IsIntegral A (↑b i)
inst✝ : IsIntegrallyClosed A
db : Basis ι K L := BilinForm.dualBasis (traceForm K L) (_ : BilinForm.Nondegenerate (traceForm K L)) b
x : C
hx : IsIntegral A (↑(algebraMap C L) x)
i : ι
⊢ IsIntegral A ((fun i => ↑(↑db.repr (↑(algebraMap C L) x)) i) i)
[PROOFSTEP]
simp_rw [BilinForm.dualBasis_repr_apply]
[GOAL]
R : Type u_1
A : Type u_2
K : Type u_3
inst✝¹⁹ : CommRing R
inst✝¹⁸ : CommRing A
inst✝¹⁷ : Field K
inst✝¹⁶ : IsDomain A
inst✝¹⁵ : Algebra A K
inst✝¹⁴ : IsFractionRing A K
L : Type u_4
inst✝¹³ : Field L
C : Type u_5
inst✝¹² : CommRing C
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A L
inst✝⁹ : IsScalarTower A K L
inst✝⁸ : Algebra C L
inst✝⁷ : IsIntegralClosure C A L
inst✝⁶ : Algebra A C
inst✝⁵ : IsScalarTower A C L
inst✝⁴ : FiniteDimensional K L
inst✝³ : IsSeparable K L
ι : Type u_6
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
b : Basis ι K L
hb_int : ∀ (i : ι), IsIntegral A (↑b i)
inst✝ : IsIntegrallyClosed A
db : Basis ι K L := BilinForm.dualBasis (traceForm K L) (_ : BilinForm.Nondegenerate (traceForm K L)) b
x : C
hx : IsIntegral A (↑(algebraMap C L) x)
i : ι
⊢ IsIntegral A (BilinForm.bilin (traceForm K L) (↑(algebraMap C L) x) (↑b i))
[PROOFSTEP]
exact isIntegral_trace (isIntegral_mul hx (hb_int i))
[GOAL]
R : Type u_1
A : Type u_2
K : Type u_3
inst✝¹⁹ : CommRing R
inst✝¹⁸ : CommRing A
inst✝¹⁷ : Field K
inst✝¹⁶ : IsDomain A
inst✝¹⁵ : Algebra A K
inst✝¹⁴ : IsFractionRing A K
L : Type u_4
inst✝¹³ : Field L
C : Type u_5
inst✝¹² : CommRing C
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A L
inst✝⁹ : IsScalarTower A K L
inst✝⁸ : Algebra C L
inst✝⁷ : IsIntegralClosure C A L
inst✝⁶ : Algebra A C
inst✝⁵ : IsScalarTower A C L
inst✝⁴ : FiniteDimensional K L
inst✝³ : IsSeparable K L
ι : Type u_6
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
b : Basis ι K L
hb_int : ∀ (i : ι), IsIntegral A (↑b i)
inst✝ : IsIntegrallyClosed A
⊢ ↑Subalgebra.toSubmodule (integralClosure A L) ≤
    Submodule.span A (Set.range ↑(BilinForm.dualBasis (traceForm K L) (_ : BilinForm.Nondegenerate (traceForm K L)) b))
[PROOFSTEP]
refine' le_trans _ (IsIntegralClosure.range_le_span_dualBasis (integralClosure A L) b hb_int)
[GOAL]
R : Type u_1
A : Type u_2
K : Type u_3
inst✝¹⁹ : CommRing R
inst✝¹⁸ : CommRing A
inst✝¹⁷ : Field K
inst✝¹⁶ : IsDomain A
inst✝¹⁵ : Algebra A K
inst✝¹⁴ : IsFractionRing A K
L : Type u_4
inst✝¹³ : Field L
C : Type u_5
inst✝¹² : CommRing C
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A L
inst✝⁹ : IsScalarTower A K L
inst✝⁸ : Algebra C L
inst✝⁷ : IsIntegralClosure C A L
inst✝⁶ : Algebra A C
inst✝⁵ : IsScalarTower A C L
inst✝⁴ : FiniteDimensional K L
inst✝³ : IsSeparable K L
ι : Type u_6
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
b : Basis ι K L
hb_int : ∀ (i : ι), IsIntegral A (↑b i)
inst✝ : IsIntegrallyClosed A
⊢ ↑Subalgebra.toSubmodule (integralClosure A L) ≤
    LinearMap.range (↑A (Algebra.linearMap { x // x ∈ integralClosure A L } L))
[PROOFSTEP]
intro x hx
[GOAL]
R : Type u_1
A : Type u_2
K : Type u_3
inst✝¹⁹ : CommRing R
inst✝¹⁸ : CommRing A
inst✝¹⁷ : Field K
inst✝¹⁶ : IsDomain A
inst✝¹⁵ : Algebra A K
inst✝¹⁴ : IsFractionRing A K
L : Type u_4
inst✝¹³ : Field L
C : Type u_5
inst✝¹² : CommRing C
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A L
inst✝⁹ : IsScalarTower A K L
inst✝⁸ : Algebra C L
inst✝⁷ : IsIntegralClosure C A L
inst✝⁶ : Algebra A C
inst✝⁵ : IsScalarTower A C L
inst✝⁴ : FiniteDimensional K L
inst✝³ : IsSeparable K L
ι : Type u_6
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
b : Basis ι K L
hb_int : ∀ (i : ι), IsIntegral A (↑b i)
inst✝ : IsIntegrallyClosed A
x : L
hx : x ∈ ↑Subalgebra.toSubmodule (integralClosure A L)
⊢ x ∈ LinearMap.range (↑A (Algebra.linearMap { x // x ∈ integralClosure A L } L))
[PROOFSTEP]
exact ⟨⟨x, hx⟩, rfl⟩
[GOAL]
R : Type u_1
A : Type u_2
K : Type u_3
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing A
inst✝¹³ : Field K
inst✝¹² : IsDomain A
inst✝¹¹ : Algebra A K
inst✝¹⁰ : IsFractionRing A K
L : Type u_4
inst✝⁹ : Field L
C : Type u_5
inst✝⁸ : CommRing C
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra A L
inst✝⁵ : IsScalarTower A K L
inst✝⁴ : Algebra C L
inst✝³ : IsIntegralClosure C A L
inst✝² : Algebra A C
inst✝¹ : IsScalarTower A C L
inst✝ : FiniteDimensional K L
s : Finset L
⊢ ∃ y x, ∀ (x : L), x ∈ s → IsIntegral A (y • x)
[PROOFSTEP]
haveI := Classical.decEq L
[GOAL]
R : Type u_1
A : Type u_2
K : Type u_3
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing A
inst✝¹³ : Field K
inst✝¹² : IsDomain A
inst✝¹¹ : Algebra A K
inst✝¹⁰ : IsFractionRing A K
L : Type u_4
inst✝⁹ : Field L
C : Type u_5
inst✝⁸ : CommRing C
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra A L
inst✝⁵ : IsScalarTower A K L
inst✝⁴ : Algebra C L
inst✝³ : IsIntegralClosure C A L
inst✝² : Algebra A C
inst✝¹ : IsScalarTower A C L
inst✝ : FiniteDimensional K L
s : Finset L
this : DecidableEq L
⊢ ∃ y x, ∀ (x : L), x ∈ s → IsIntegral A (y • x)
[PROOFSTEP]
refine' s.induction _ _
[GOAL]
case refine'_1
R : Type u_1
A : Type u_2
K : Type u_3
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing A
inst✝¹³ : Field K
inst✝¹² : IsDomain A
inst✝¹¹ : Algebra A K
inst✝¹⁰ : IsFractionRing A K
L : Type u_4
inst✝⁹ : Field L
C : Type u_5
inst✝⁸ : CommRing C
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra A L
inst✝⁵ : IsScalarTower A K L
inst✝⁴ : Algebra C L
inst✝³ : IsIntegralClosure C A L
inst✝² : Algebra A C
inst✝¹ : IsScalarTower A C L
inst✝ : FiniteDimensional K L
s : Finset L
this : DecidableEq L
⊢ ∃ y x, ∀ (x : L), x ∈ ∅ → IsIntegral A (y • x)
[PROOFSTEP]
use 1, one_ne_zero
[GOAL]
case h
R : Type u_1
A : Type u_2
K : Type u_3
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing A
inst✝¹³ : Field K
inst✝¹² : IsDomain A
inst✝¹¹ : Algebra A K
inst✝¹⁰ : IsFractionRing A K
L : Type u_4
inst✝⁹ : Field L
C : Type u_5
inst✝⁸ : CommRing C
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra A L
inst✝⁵ : IsScalarTower A K L
inst✝⁴ : Algebra C L
inst✝³ : IsIntegralClosure C A L
inst✝² : Algebra A C
inst✝¹ : IsScalarTower A C L
inst✝ : FiniteDimensional K L
s : Finset L
this : DecidableEq L
⊢ ∀ (x : L), x ∈ ∅ → IsIntegral A (1 • x)
[PROOFSTEP]
rintro x ⟨⟩
[GOAL]
case refine'_2
R : Type u_1
A : Type u_2
K : Type u_3
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing A
inst✝¹³ : Field K
inst✝¹² : IsDomain A
inst✝¹¹ : Algebra A K
inst✝¹⁰ : IsFractionRing A K
L : Type u_4
inst✝⁹ : Field L
C : Type u_5
inst✝⁸ : CommRing C
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra A L
inst✝⁵ : IsScalarTower A K L
inst✝⁴ : Algebra C L
inst✝³ : IsIntegralClosure C A L
inst✝² : Algebra A C
inst✝¹ : IsScalarTower A C L
inst✝ : FiniteDimensional K L
s : Finset L
this : DecidableEq L
⊢ ∀ ⦃a : L⦄ {s : Finset L},
    ¬a ∈ s → (∃ y x, ∀ (x : L), x ∈ s → IsIntegral A (y • x)) → ∃ y x, ∀ (x : L), x ∈ insert a s → IsIntegral A (y • x)
[PROOFSTEP]
rintro x s hx ⟨y, hy, hs⟩
[GOAL]
case refine'_2.intro.intro
R : Type u_1
A : Type u_2
K : Type u_3
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing A
inst✝¹³ : Field K
inst✝¹² : IsDomain A
inst✝¹¹ : Algebra A K
inst✝¹⁰ : IsFractionRing A K
L : Type u_4
inst✝⁹ : Field L
C : Type u_5
inst✝⁸ : CommRing C
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra A L
inst✝⁵ : IsScalarTower A K L
inst✝⁴ : Algebra C L
inst✝³ : IsIntegralClosure C A L
inst✝² : Algebra A C
inst✝¹ : IsScalarTower A C L
inst✝ : FiniteDimensional K L
s✝ : Finset L
this : DecidableEq L
x : L
s : Finset L
hx : ¬x ∈ s
y : A
hy : y ≠ 0
hs : ∀ (x : L), x ∈ s → IsIntegral A (y • x)
⊢ ∃ y x_1, ∀ (x_2 : L), x_2 ∈ insert x s → IsIntegral A (y • x_2)
[PROOFSTEP]
have :=
  exists_integral_multiple ((IsFractionRing.isAlgebraic_iff A K L).mpr (isAlgebraic_of_finite _ _ x))
    ((injective_iff_map_eq_zero (algebraMap A L)).mp ?_)
[GOAL]
case refine'_2.intro.intro.refine_2
R : Type u_1
A : Type u_2
K : Type u_3
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing A
inst✝¹³ : Field K
inst✝¹² : IsDomain A
inst✝¹¹ : Algebra A K
inst✝¹⁰ : IsFractionRing A K
L : Type u_4
inst✝⁹ : Field L
C : Type u_5
inst✝⁸ : CommRing C
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra A L
inst✝⁵ : IsScalarTower A K L
inst✝⁴ : Algebra C L
inst✝³ : IsIntegralClosure C A L
inst✝² : Algebra A C
inst✝¹ : IsScalarTower A C L
inst✝ : FiniteDimensional K L
s✝ : Finset L
this✝ : DecidableEq L
x : L
s : Finset L
hx : ¬x ∈ s
y : A
hy : y ≠ 0
hs : ∀ (x : L), x ∈ s → IsIntegral A (y • x)
this : ∃ x_1 y x_2, x * ↑(algebraMap A L) y = ↑x_1
⊢ ∃ y x_1, ∀ (x_2 : L), x_2 ∈ insert x s → IsIntegral A (y • x_2)
case refine'_2.intro.intro.refine_1
R : Type u_1
A : Type u_2
K : Type u_3
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing A
inst✝¹³ : Field K
inst✝¹² : IsDomain A
inst✝¹¹ : Algebra A K
inst✝¹⁰ : IsFractionRing A K
L : Type u_4
inst✝⁹ : Field L
C : Type u_5
inst✝⁸ : CommRing C
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra A L
inst✝⁵ : IsScalarTower A K L
inst✝⁴ : Algebra C L
inst✝³ : IsIntegralClosure C A L
inst✝² : Algebra A C
inst✝¹ : IsScalarTower A C L
inst✝ : FiniteDimensional K L
s✝ : Finset L
this : DecidableEq L
x : L
s : Finset L
hx : ¬x ∈ s
y : A
hy : y ≠ 0
hs : ∀ (x : L), x ∈ s → IsIntegral A (y • x)
⊢ Function.Injective ↑(algebraMap A L)
[PROOFSTEP]
rcases this with ⟨x', y', hy', hx'⟩
[GOAL]
case refine'_2.intro.intro.refine_2.intro.intro.intro
R : Type u_1
A : Type u_2
K : Type u_3
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing A
inst✝¹³ : Field K
inst✝¹² : IsDomain A
inst✝¹¹ : Algebra A K
inst✝¹⁰ : IsFractionRing A K
L : Type u_4
inst✝⁹ : Field L
C : Type u_5
inst✝⁸ : CommRing C
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra A L
inst✝⁵ : IsScalarTower A K L
inst✝⁴ : Algebra C L
inst✝³ : IsIntegralClosure C A L
inst✝² : Algebra A C
inst✝¹ : IsScalarTower A C L
inst✝ : FiniteDimensional K L
s✝ : Finset L
this : DecidableEq L
x : L
s : Finset L
hx : ¬x ∈ s
y : A
hy : y ≠ 0
hs : ∀ (x : L), x ∈ s → IsIntegral A (y • x)
x' : { x // x ∈ integralClosure A L }
y' : A
hy' : y' ≠ 0
hx' : x * ↑(algebraMap A L) y' = ↑x'
⊢ ∃ y x_1, ∀ (x_2 : L), x_2 ∈ insert x s → IsIntegral A (y • x_2)
case refine'_2.intro.intro.refine_1
R : Type u_1
A : Type u_2
K : Type u_3
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing A
inst✝¹³ : Field K
inst✝¹² : IsDomain A
inst✝¹¹ : Algebra A K
inst✝¹⁰ : IsFractionRing A K
L : Type u_4
inst✝⁹ : Field L
C : Type u_5
inst✝⁸ : CommRing C
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra A L
inst✝⁵ : IsScalarTower A K L
inst✝⁴ : Algebra C L
inst✝³ : IsIntegralClosure C A L
inst✝² : Algebra A C
inst✝¹ : IsScalarTower A C L
inst✝ : FiniteDimensional K L
s✝ : Finset L
this : DecidableEq L
x : L
s : Finset L
hx : ¬x ∈ s
y : A
hy : y ≠ 0
hs : ∀ (x : L), x ∈ s → IsIntegral A (y • x)
⊢ Function.Injective ↑(algebraMap A L)
[PROOFSTEP]
refine' ⟨y * y', mul_ne_zero hy hy', fun x'' hx'' => _⟩
[GOAL]
case refine'_2.intro.intro.refine_2.intro.intro.intro
R : Type u_1
A : Type u_2
K : Type u_3
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing A
inst✝¹³ : Field K
inst✝¹² : IsDomain A
inst✝¹¹ : Algebra A K
inst✝¹⁰ : IsFractionRing A K
L : Type u_4
inst✝⁹ : Field L
C : Type u_5
inst✝⁸ : CommRing C
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra A L
inst✝⁵ : IsScalarTower A K L
inst✝⁴ : Algebra C L
inst✝³ : IsIntegralClosure C A L
inst✝² : Algebra A C
inst✝¹ : IsScalarTower A C L
inst✝ : FiniteDimensional K L
s✝ : Finset L
this : DecidableEq L
x : L
s : Finset L
hx : ¬x ∈ s
y : A
hy : y ≠ 0
hs : ∀ (x : L), x ∈ s → IsIntegral A (y • x)
x' : { x // x ∈ integralClosure A L }
y' : A
hy' : y' ≠ 0
hx' : x * ↑(algebraMap A L) y' = ↑x'
x'' : L
hx'' : x'' ∈ insert x s
⊢ IsIntegral A ((y * y') • x'')
case refine'_2.intro.intro.refine_1
R : Type u_1
A : Type u_2
K : Type u_3
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing A
inst✝¹³ : Field K
inst✝¹² : IsDomain A
inst✝¹¹ : Algebra A K
inst✝¹⁰ : IsFractionRing A K
L : Type u_4
inst✝⁹ : Field L
C : Type u_5
inst✝⁸ : CommRing C
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra A L
inst✝⁵ : IsScalarTower A K L
inst✝⁴ : Algebra C L
inst✝³ : IsIntegralClosure C A L
inst✝² : Algebra A C
inst✝¹ : IsScalarTower A C L
inst✝ : FiniteDimensional K L
s✝ : Finset L
this : DecidableEq L
x : L
s : Finset L
hx : ¬x ∈ s
y : A
hy : y ≠ 0
hs : ∀ (x : L), x ∈ s → IsIntegral A (y • x)
⊢ Function.Injective ↑(algebraMap A L)
[PROOFSTEP]
rcases Finset.mem_insert.mp hx'' with (rfl | hx'')
[GOAL]
case refine'_2.intro.intro.refine_2.intro.intro.intro.inl
R : Type u_1
A : Type u_2
K : Type u_3
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing A
inst✝¹³ : Field K
inst✝¹² : IsDomain A
inst✝¹¹ : Algebra A K
inst✝¹⁰ : IsFractionRing A K
L : Type u_4
inst✝⁹ : Field L
C : Type u_5
inst✝⁸ : CommRing C
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra A L
inst✝⁵ : IsScalarTower A K L
inst✝⁴ : Algebra C L
inst✝³ : IsIntegralClosure C A L
inst✝² : Algebra A C
inst✝¹ : IsScalarTower A C L
inst✝ : FiniteDimensional K L
s✝ : Finset L
this : DecidableEq L
s : Finset L
y : A
hy : y ≠ 0
hs : ∀ (x : L), x ∈ s → IsIntegral A (y • x)
x' : { x // x ∈ integralClosure A L }
y' : A
hy' : y' ≠ 0
x'' : L
hx : ¬x'' ∈ s
hx' : x'' * ↑(algebraMap A L) y' = ↑x'
hx'' : x'' ∈ insert x'' s
⊢ IsIntegral A ((y * y') • x'')
[PROOFSTEP]
rw [mul_smul, Algebra.smul_def, Algebra.smul_def, mul_comm _ x'', hx']
[GOAL]
case refine'_2.intro.intro.refine_2.intro.intro.intro.inl
R : Type u_1
A : Type u_2
K : Type u_3
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing A
inst✝¹³ : Field K
inst✝¹² : IsDomain A
inst✝¹¹ : Algebra A K
inst✝¹⁰ : IsFractionRing A K
L : Type u_4
inst✝⁹ : Field L
C : Type u_5
inst✝⁸ : CommRing C
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra A L
inst✝⁵ : IsScalarTower A K L
inst✝⁴ : Algebra C L
inst✝³ : IsIntegralClosure C A L
inst✝² : Algebra A C
inst✝¹ : IsScalarTower A C L
inst✝ : FiniteDimensional K L
s✝ : Finset L
this : DecidableEq L
s : Finset L
y : A
hy : y ≠ 0
hs : ∀ (x : L), x ∈ s → IsIntegral A (y • x)
x' : { x // x ∈ integralClosure A L }
y' : A
hy' : y' ≠ 0
x'' : L
hx : ¬x'' ∈ s
hx' : x'' * ↑(algebraMap A L) y' = ↑x'
hx'' : x'' ∈ insert x'' s
⊢ IsIntegral A (↑(algebraMap A L) y * ↑x')
[PROOFSTEP]
exact isIntegral_mul isIntegral_algebraMap x'.2
[GOAL]
case refine'_2.intro.intro.refine_2.intro.intro.intro.inr
R : Type u_1
A : Type u_2
K : Type u_3
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing A
inst✝¹³ : Field K
inst✝¹² : IsDomain A
inst✝¹¹ : Algebra A K
inst✝¹⁰ : IsFractionRing A K
L : Type u_4
inst✝⁹ : Field L
C : Type u_5
inst✝⁸ : CommRing C
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra A L
inst✝⁵ : IsScalarTower A K L
inst✝⁴ : Algebra C L
inst✝³ : IsIntegralClosure C A L
inst✝² : Algebra A C
inst✝¹ : IsScalarTower A C L
inst✝ : FiniteDimensional K L
s✝ : Finset L
this : DecidableEq L
x : L
s : Finset L
hx : ¬x ∈ s
y : A
hy : y ≠ 0
hs : ∀ (x : L), x ∈ s → IsIntegral A (y • x)
x' : { x // x ∈ integralClosure A L }
y' : A
hy' : y' ≠ 0
hx' : x * ↑(algebraMap A L) y' = ↑x'
x'' : L
hx''✝ : x'' ∈ insert x s
hx'' : x'' ∈ s
⊢ IsIntegral A ((y * y') • x'')
[PROOFSTEP]
rw [mul_comm, mul_smul, Algebra.smul_def]
[GOAL]
case refine'_2.intro.intro.refine_2.intro.intro.intro.inr
R : Type u_1
A : Type u_2
K : Type u_3
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing A
inst✝¹³ : Field K
inst✝¹² : IsDomain A
inst✝¹¹ : Algebra A K
inst✝¹⁰ : IsFractionRing A K
L : Type u_4
inst✝⁹ : Field L
C : Type u_5
inst✝⁸ : CommRing C
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra A L
inst✝⁵ : IsScalarTower A K L
inst✝⁴ : Algebra C L
inst✝³ : IsIntegralClosure C A L
inst✝² : Algebra A C
inst✝¹ : IsScalarTower A C L
inst✝ : FiniteDimensional K L
s✝ : Finset L
this : DecidableEq L
x : L
s : Finset L
hx : ¬x ∈ s
y : A
hy : y ≠ 0
hs : ∀ (x : L), x ∈ s → IsIntegral A (y • x)
x' : { x // x ∈ integralClosure A L }
y' : A
hy' : y' ≠ 0
hx' : x * ↑(algebraMap A L) y' = ↑x'
x'' : L
hx''✝ : x'' ∈ insert x s
hx'' : x'' ∈ s
⊢ IsIntegral A (↑(algebraMap A L) y' * y • x'')
[PROOFSTEP]
exact isIntegral_mul isIntegral_algebraMap (hs _ hx'')
[GOAL]
case refine'_2.intro.intro.refine_1
R : Type u_1
A : Type u_2
K : Type u_3
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing A
inst✝¹³ : Field K
inst✝¹² : IsDomain A
inst✝¹¹ : Algebra A K
inst✝¹⁰ : IsFractionRing A K
L : Type u_4
inst✝⁹ : Field L
C : Type u_5
inst✝⁸ : CommRing C
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra A L
inst✝⁵ : IsScalarTower A K L
inst✝⁴ : Algebra C L
inst✝³ : IsIntegralClosure C A L
inst✝² : Algebra A C
inst✝¹ : IsScalarTower A C L
inst✝ : FiniteDimensional K L
s✝ : Finset L
this : DecidableEq L
x : L
s : Finset L
hx : ¬x ∈ s
y : A
hy : y ≠ 0
hs : ∀ (x : L), x ∈ s → IsIntegral A (y • x)
⊢ Function.Injective ↑(algebraMap A L)
[PROOFSTEP]
rw [IsScalarTower.algebraMap_eq A K L]
[GOAL]
case refine'_2.intro.intro.refine_1
R : Type u_1
A : Type u_2
K : Type u_3
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing A
inst✝¹³ : Field K
inst✝¹² : IsDomain A
inst✝¹¹ : Algebra A K
inst✝¹⁰ : IsFractionRing A K
L : Type u_4
inst✝⁹ : Field L
C : Type u_5
inst✝⁸ : CommRing C
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra A L
inst✝⁵ : IsScalarTower A K L
inst✝⁴ : Algebra C L
inst✝³ : IsIntegralClosure C A L
inst✝² : Algebra A C
inst✝¹ : IsScalarTower A C L
inst✝ : FiniteDimensional K L
s✝ : Finset L
this : DecidableEq L
x : L
s : Finset L
hx : ¬x ∈ s
y : A
hy : y ≠ 0
hs : ∀ (x : L), x ∈ s → IsIntegral A (y • x)
⊢ Function.Injective ↑(RingHom.comp (algebraMap K L) (algebraMap A K))
[PROOFSTEP]
apply (algebraMap K L).injective.comp
[GOAL]
case refine'_2.intro.intro.refine_1
R : Type u_1
A : Type u_2
K : Type u_3
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing A
inst✝¹³ : Field K
inst✝¹² : IsDomain A
inst✝¹¹ : Algebra A K
inst✝¹⁰ : IsFractionRing A K
L : Type u_4
inst✝⁹ : Field L
C : Type u_5
inst✝⁸ : CommRing C
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra A L
inst✝⁵ : IsScalarTower A K L
inst✝⁴ : Algebra C L
inst✝³ : IsIntegralClosure C A L
inst✝² : Algebra A C
inst✝¹ : IsScalarTower A C L
inst✝ : FiniteDimensional K L
s✝ : Finset L
this : DecidableEq L
x : L
s : Finset L
hx : ¬x ∈ s
y : A
hy : y ≠ 0
hs : ∀ (x : L), x ∈ s → IsIntegral A (y • x)
⊢ Function.Injective fun x => ↑(algebraMap A K) x
[PROOFSTEP]
exact IsFractionRing.injective _ _
[GOAL]
R : Type u_1
A : Type u_2
K : Type u_3
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing A
inst✝¹³ : Field K
inst✝¹² : IsDomain A
inst✝¹¹ : Algebra A K
inst✝¹⁰ : IsFractionRing A K
L : Type u_4
inst✝⁹ : Field L
C : Type u_5
inst✝⁸ : CommRing C
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra A L
inst✝⁵ : IsScalarTower A K L
inst✝⁴ : Algebra C L
inst✝³ : IsIntegralClosure C A L
inst✝² : Algebra A C
inst✝¹ : IsScalarTower A C L
inst✝ : FiniteDimensional K L
⊢ ∃ s b, ∀ (x : { x // x ∈ s }), IsIntegral A (↑b x)
[PROOFSTEP]
letI := Classical.decEq L
[GOAL]
R : Type u_1
A : Type u_2
K : Type u_3
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing A
inst✝¹³ : Field K
inst✝¹² : IsDomain A
inst✝¹¹ : Algebra A K
inst✝¹⁰ : IsFractionRing A K
L : Type u_4
inst✝⁹ : Field L
C : Type u_5
inst✝⁸ : CommRing C
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra A L
inst✝⁵ : IsScalarTower A K L
inst✝⁴ : Algebra C L
inst✝³ : IsIntegralClosure C A L
inst✝² : Algebra A C
inst✝¹ : IsScalarTower A C L
inst✝ : FiniteDimensional K L
this : DecidableEq L := Classical.decEq L
⊢ ∃ s b, ∀ (x : { x // x ∈ s }), IsIntegral A (↑b x)
[PROOFSTEP]
letI : IsNoetherian K L := IsNoetherian.iff_fg.2 inferInstance
[GOAL]
R : Type u_1
A : Type u_2
K : Type u_3
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing A
inst✝¹³ : Field K
inst✝¹² : IsDomain A
inst✝¹¹ : Algebra A K
inst✝¹⁰ : IsFractionRing A K
L : Type u_4
inst✝⁹ : Field L
C : Type u_5
inst✝⁸ : CommRing C
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra A L
inst✝⁵ : IsScalarTower A K L
inst✝⁴ : Algebra C L
inst✝³ : IsIntegralClosure C A L
inst✝² : Algebra A C
inst✝¹ : IsScalarTower A C L
inst✝ : FiniteDimensional K L
this✝ : DecidableEq L := Classical.decEq L
this : IsNoetherian K L := Iff.mpr IsNoetherian.iff_fg inferInstance
⊢ ∃ s b, ∀ (x : { x // x ∈ s }), IsIntegral A (↑b x)
[PROOFSTEP]
let s' := IsNoetherian.finsetBasisIndex K L
[GOAL]
R : Type u_1
A : Type u_2
K : Type u_3
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing A
inst✝¹³ : Field K
inst✝¹² : IsDomain A
inst✝¹¹ : Algebra A K
inst✝¹⁰ : IsFractionRing A K
L : Type u_4
inst✝⁹ : Field L
C : Type u_5
inst✝⁸ : CommRing C
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra A L
inst✝⁵ : IsScalarTower A K L
inst✝⁴ : Algebra C L
inst✝³ : IsIntegralClosure C A L
inst✝² : Algebra A C
inst✝¹ : IsScalarTower A C L
inst✝ : FiniteDimensional K L
this✝ : DecidableEq L := Classical.decEq L
this : IsNoetherian K L := Iff.mpr IsNoetherian.iff_fg inferInstance
s' : Finset L := IsNoetherian.finsetBasisIndex K L
⊢ ∃ s b, ∀ (x : { x // x ∈ s }), IsIntegral A (↑b x)
[PROOFSTEP]
let bs' := IsNoetherian.finsetBasis K L
[GOAL]
R : Type u_1
A : Type u_2
K : Type u_3
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing A
inst✝¹³ : Field K
inst✝¹² : IsDomain A
inst✝¹¹ : Algebra A K
inst✝¹⁰ : IsFractionRing A K
L : Type u_4
inst✝⁹ : Field L
C : Type u_5
inst✝⁸ : CommRing C
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra A L
inst✝⁵ : IsScalarTower A K L
inst✝⁴ : Algebra C L
inst✝³ : IsIntegralClosure C A L
inst✝² : Algebra A C
inst✝¹ : IsScalarTower A C L
inst✝ : FiniteDimensional K L
this✝ : DecidableEq L := Classical.decEq L
this : IsNoetherian K L := Iff.mpr IsNoetherian.iff_fg inferInstance
s' : Finset L := IsNoetherian.finsetBasisIndex K L
bs' : Basis { x // x ∈ IsNoetherian.finsetBasisIndex K L } K L := IsNoetherian.finsetBasis K L
⊢ ∃ s b, ∀ (x : { x // x ∈ s }), IsIntegral A (↑b x)
[PROOFSTEP]
obtain ⟨y, hy, his'⟩ := exists_integral_multiples A K (Finset.univ.image bs')
[GOAL]
case intro.intro
R : Type u_1
A : Type u_2
K : Type u_3
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing A
inst✝¹³ : Field K
inst✝¹² : IsDomain A
inst✝¹¹ : Algebra A K
inst✝¹⁰ : IsFractionRing A K
L : Type u_4
inst✝⁹ : Field L
C : Type u_5
inst✝⁸ : CommRing C
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra A L
inst✝⁵ : IsScalarTower A K L
inst✝⁴ : Algebra C L
inst✝³ : IsIntegralClosure C A L
inst✝² : Algebra A C
inst✝¹ : IsScalarTower A C L
inst✝ : FiniteDimensional K L
this✝ : DecidableEq L := Classical.decEq L
this : IsNoetherian K L := Iff.mpr IsNoetherian.iff_fg inferInstance
s' : Finset L := IsNoetherian.finsetBasisIndex K L
bs' : Basis { x // x ∈ IsNoetherian.finsetBasisIndex K L } K L := IsNoetherian.finsetBasis K L
y : A
hy : y ≠ 0
his' : ∀ (x : L), x ∈ Finset.image (↑bs') Finset.univ → IsIntegral A (y • x)
⊢ ∃ s b, ∀ (x : { x // x ∈ s }), IsIntegral A (↑b x)
[PROOFSTEP]
have hy' : algebraMap A L y ≠ 0 :=
  by
  refine' mt ((injective_iff_map_eq_zero (algebraMap A L)).mp _ _) hy
  rw [IsScalarTower.algebraMap_eq A K L]
  exact (algebraMap K L).injective.comp (IsFractionRing.injective A K)
[GOAL]
R : Type u_1
A : Type u_2
K : Type u_3
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing A
inst✝¹³ : Field K
inst✝¹² : IsDomain A
inst✝¹¹ : Algebra A K
inst✝¹⁰ : IsFractionRing A K
L : Type u_4
inst✝⁹ : Field L
C : Type u_5
inst✝⁸ : CommRing C
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra A L
inst✝⁵ : IsScalarTower A K L
inst✝⁴ : Algebra C L
inst✝³ : IsIntegralClosure C A L
inst✝² : Algebra A C
inst✝¹ : IsScalarTower A C L
inst✝ : FiniteDimensional K L
this✝ : DecidableEq L := Classical.decEq L
this : IsNoetherian K L := Iff.mpr IsNoetherian.iff_fg inferInstance
s' : Finset L := IsNoetherian.finsetBasisIndex K L
bs' : Basis { x // x ∈ IsNoetherian.finsetBasisIndex K L } K L := IsNoetherian.finsetBasis K L
y : A
hy : y ≠ 0
his' : ∀ (x : L), x ∈ Finset.image (↑bs') Finset.univ → IsIntegral A (y • x)
⊢ ↑(algebraMap A L) y ≠ 0
[PROOFSTEP]
refine' mt ((injective_iff_map_eq_zero (algebraMap A L)).mp _ _) hy
[GOAL]
R : Type u_1
A : Type u_2
K : Type u_3
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing A
inst✝¹³ : Field K
inst✝¹² : IsDomain A
inst✝¹¹ : Algebra A K
inst✝¹⁰ : IsFractionRing A K
L : Type u_4
inst✝⁹ : Field L
C : Type u_5
inst✝⁸ : CommRing C
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra A L
inst✝⁵ : IsScalarTower A K L
inst✝⁴ : Algebra C L
inst✝³ : IsIntegralClosure C A L
inst✝² : Algebra A C
inst✝¹ : IsScalarTower A C L
inst✝ : FiniteDimensional K L
this✝ : DecidableEq L := Classical.decEq L
this : IsNoetherian K L := Iff.mpr IsNoetherian.iff_fg inferInstance
s' : Finset L := IsNoetherian.finsetBasisIndex K L
bs' : Basis { x // x ∈ IsNoetherian.finsetBasisIndex K L } K L := IsNoetherian.finsetBasis K L
y : A
hy : y ≠ 0
his' : ∀ (x : L), x ∈ Finset.image (↑bs') Finset.univ → IsIntegral A (y • x)
⊢ Function.Injective ↑(algebraMap A L)
[PROOFSTEP]
rw [IsScalarTower.algebraMap_eq A K L]
[GOAL]
R : Type u_1
A : Type u_2
K : Type u_3
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing A
inst✝¹³ : Field K
inst✝¹² : IsDomain A
inst✝¹¹ : Algebra A K
inst✝¹⁰ : IsFractionRing A K
L : Type u_4
inst✝⁹ : Field L
C : Type u_5
inst✝⁸ : CommRing C
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra A L
inst✝⁵ : IsScalarTower A K L
inst✝⁴ : Algebra C L
inst✝³ : IsIntegralClosure C A L
inst✝² : Algebra A C
inst✝¹ : IsScalarTower A C L
inst✝ : FiniteDimensional K L
this✝ : DecidableEq L := Classical.decEq L
this : IsNoetherian K L := Iff.mpr IsNoetherian.iff_fg inferInstance
s' : Finset L := IsNoetherian.finsetBasisIndex K L
bs' : Basis { x // x ∈ IsNoetherian.finsetBasisIndex K L } K L := IsNoetherian.finsetBasis K L
y : A
hy : y ≠ 0
his' : ∀ (x : L), x ∈ Finset.image (↑bs') Finset.univ → IsIntegral A (y • x)
⊢ Function.Injective ↑(RingHom.comp (algebraMap K L) (algebraMap A K))
[PROOFSTEP]
exact (algebraMap K L).injective.comp (IsFractionRing.injective A K)
[GOAL]
case intro.intro
R : Type u_1
A : Type u_2
K : Type u_3
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing A
inst✝¹³ : Field K
inst✝¹² : IsDomain A
inst✝¹¹ : Algebra A K
inst✝¹⁰ : IsFractionRing A K
L : Type u_4
inst✝⁹ : Field L
C : Type u_5
inst✝⁸ : CommRing C
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra A L
inst✝⁵ : IsScalarTower A K L
inst✝⁴ : Algebra C L
inst✝³ : IsIntegralClosure C A L
inst✝² : Algebra A C
inst✝¹ : IsScalarTower A C L
inst✝ : FiniteDimensional K L
this✝ : DecidableEq L := Classical.decEq L
this : IsNoetherian K L := Iff.mpr IsNoetherian.iff_fg inferInstance
s' : Finset L := IsNoetherian.finsetBasisIndex K L
bs' : Basis { x // x ∈ IsNoetherian.finsetBasisIndex K L } K L := IsNoetherian.finsetBasis K L
y : A
hy : y ≠ 0
his' : ∀ (x : L), x ∈ Finset.image (↑bs') Finset.univ → IsIntegral A (y • x)
hy' : ↑(algebraMap A L) y ≠ 0
⊢ ∃ s b, ∀ (x : { x // x ∈ s }), IsIntegral A (↑b x)
[PROOFSTEP]
refine
  ⟨s',
    bs'.map
      {
        Algebra.lmul _ _ (algebraMap A L
            y) with
        toFun := fun x => algebraMap A L y * x
        invFun := fun x => (algebraMap A L y)⁻¹ * x
        left_inv := ?_
        right_inv := ?_ },
    ?_⟩
[GOAL]
case intro.intro.refine_1
R : Type u_1
A : Type u_2
K : Type u_3
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing A
inst✝¹³ : Field K
inst✝¹² : IsDomain A
inst✝¹¹ : Algebra A K
inst✝¹⁰ : IsFractionRing A K
L : Type u_4
inst✝⁹ : Field L
C : Type u_5
inst✝⁸ : CommRing C
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra A L
inst✝⁵ : IsScalarTower A K L
inst✝⁴ : Algebra C L
inst✝³ : IsIntegralClosure C A L
inst✝² : Algebra A C
inst✝¹ : IsScalarTower A C L
inst✝ : FiniteDimensional K L
this✝ : DecidableEq L := Classical.decEq L
this : IsNoetherian K L := Iff.mpr IsNoetherian.iff_fg inferInstance
s' : Finset L := IsNoetherian.finsetBasisIndex K L
bs' : Basis { x // x ∈ IsNoetherian.finsetBasisIndex K L } K L := IsNoetherian.finsetBasis K L
y : A
hy : y ≠ 0
his' : ∀ (x : L), x ∈ Finset.image (↑bs') Finset.univ → IsIntegral A (y • x)
hy' : ↑(algebraMap A L) y ≠ 0
src✝ : (fun x => Module.End K ((fun x => L) y)) (↑(algebraMap A L) y) :=
  ↑(lmul K ((fun x => L) y)) (↑(algebraMap A L) y)
⊢ Function.LeftInverse (fun x => (↑(algebraMap A L) y)⁻¹ * x)
    {
          toAddHom :=
            { toFun := fun x => ↑(algebraMap A L) y * x,
              map_add' :=
                (_ :
                  ∀ (x y_1 : (fun x => L) y),
                    AddHom.toFun src✝.toAddHom (x + y_1) =
                      AddHom.toFun src✝.toAddHom x + AddHom.toFun src✝.toAddHom y_1) },
          map_smul' :=
            (_ :
              ∀ (r : K) (x : (fun x => L) y),
                AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id K) r • AddHom.toFun src✝.toAddHom x) }.toAddHom.toFun
[PROOFSTEP]
intro x
[GOAL]
case intro.intro.refine_1
R : Type u_1
A : Type u_2
K : Type u_3
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing A
inst✝¹³ : Field K
inst✝¹² : IsDomain A
inst✝¹¹ : Algebra A K
inst✝¹⁰ : IsFractionRing A K
L : Type u_4
inst✝⁹ : Field L
C : Type u_5
inst✝⁸ : CommRing C
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra A L
inst✝⁵ : IsScalarTower A K L
inst✝⁴ : Algebra C L
inst✝³ : IsIntegralClosure C A L
inst✝² : Algebra A C
inst✝¹ : IsScalarTower A C L
inst✝ : FiniteDimensional K L
this✝ : DecidableEq L := Classical.decEq L
this : IsNoetherian K L := Iff.mpr IsNoetherian.iff_fg inferInstance
s' : Finset L := IsNoetherian.finsetBasisIndex K L
bs' : Basis { x // x ∈ IsNoetherian.finsetBasisIndex K L } K L := IsNoetherian.finsetBasis K L
y : A
hy : y ≠ 0
his' : ∀ (x : L), x ∈ Finset.image (↑bs') Finset.univ → IsIntegral A (y • x)
hy' : ↑(algebraMap A L) y ≠ 0
src✝ : (fun x => Module.End K ((fun x => L) y)) (↑(algebraMap A L) y) :=
  ↑(lmul K ((fun x => L) y)) (↑(algebraMap A L) y)
x : L
⊢ (fun x => (↑(algebraMap A L) y)⁻¹ * x)
      (AddHom.toFun
        {
            toAddHom :=
              { toFun := fun x => ↑(algebraMap A L) y * x,
                map_add' :=
                  (_ :
                    ∀ (x y_1 : (fun x => L) y),
                      AddHom.toFun src✝.toAddHom (x + y_1) =
                        AddHom.toFun src✝.toAddHom x + AddHom.toFun src✝.toAddHom y_1) },
            map_smul' :=
              (_ :
                ∀ (r : K) (x : (fun x => L) y),
                  AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id K) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
        x) =
    x
[PROOFSTEP]
simp only [inv_mul_cancel_left₀ hy']
[GOAL]
case intro.intro.refine_2
R : Type u_1
A : Type u_2
K : Type u_3
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing A
inst✝¹³ : Field K
inst✝¹² : IsDomain A
inst✝¹¹ : Algebra A K
inst✝¹⁰ : IsFractionRing A K
L : Type u_4
inst✝⁹ : Field L
C : Type u_5
inst✝⁸ : CommRing C
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra A L
inst✝⁵ : IsScalarTower A K L
inst✝⁴ : Algebra C L
inst✝³ : IsIntegralClosure C A L
inst✝² : Algebra A C
inst✝¹ : IsScalarTower A C L
inst✝ : FiniteDimensional K L
this✝ : DecidableEq L := Classical.decEq L
this : IsNoetherian K L := Iff.mpr IsNoetherian.iff_fg inferInstance
s' : Finset L := IsNoetherian.finsetBasisIndex K L
bs' : Basis { x // x ∈ IsNoetherian.finsetBasisIndex K L } K L := IsNoetherian.finsetBasis K L
y : A
hy : y ≠ 0
his' : ∀ (x : L), x ∈ Finset.image (↑bs') Finset.univ → IsIntegral A (y • x)
hy' : ↑(algebraMap A L) y ≠ 0
src✝ : (fun x => Module.End K ((fun x => L) y)) (↑(algebraMap A L) y) :=
  ↑(lmul K ((fun x => L) y)) (↑(algebraMap A L) y)
⊢ Function.RightInverse (fun x => (↑(algebraMap A L) y)⁻¹ * x)
    {
          toAddHom :=
            { toFun := fun x => ↑(algebraMap A L) y * x,
              map_add' :=
                (_ :
                  ∀ (x y_1 : (fun x => L) y),
                    AddHom.toFun src✝.toAddHom (x + y_1) =
                      AddHom.toFun src✝.toAddHom x + AddHom.toFun src✝.toAddHom y_1) },
          map_smul' :=
            (_ :
              ∀ (r : K) (x : (fun x => L) y),
                AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id K) r • AddHom.toFun src✝.toAddHom x) }.toAddHom.toFun
[PROOFSTEP]
intro x
[GOAL]
case intro.intro.refine_2
R : Type u_1
A : Type u_2
K : Type u_3
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing A
inst✝¹³ : Field K
inst✝¹² : IsDomain A
inst✝¹¹ : Algebra A K
inst✝¹⁰ : IsFractionRing A K
L : Type u_4
inst✝⁹ : Field L
C : Type u_5
inst✝⁸ : CommRing C
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra A L
inst✝⁵ : IsScalarTower A K L
inst✝⁴ : Algebra C L
inst✝³ : IsIntegralClosure C A L
inst✝² : Algebra A C
inst✝¹ : IsScalarTower A C L
inst✝ : FiniteDimensional K L
this✝ : DecidableEq L := Classical.decEq L
this : IsNoetherian K L := Iff.mpr IsNoetherian.iff_fg inferInstance
s' : Finset L := IsNoetherian.finsetBasisIndex K L
bs' : Basis { x // x ∈ IsNoetherian.finsetBasisIndex K L } K L := IsNoetherian.finsetBasis K L
y : A
hy : y ≠ 0
his' : ∀ (x : L), x ∈ Finset.image (↑bs') Finset.univ → IsIntegral A (y • x)
hy' : ↑(algebraMap A L) y ≠ 0
src✝ : (fun x => Module.End K ((fun x => L) y)) (↑(algebraMap A L) y) :=
  ↑(lmul K ((fun x => L) y)) (↑(algebraMap A L) y)
x : L
⊢ AddHom.toFun
      {
          toAddHom :=
            { toFun := fun x => ↑(algebraMap A L) y * x,
              map_add' :=
                (_ :
                  ∀ (x y_1 : (fun x => L) y),
                    AddHom.toFun src✝.toAddHom (x + y_1) =
                      AddHom.toFun src✝.toAddHom x + AddHom.toFun src✝.toAddHom y_1) },
          map_smul' :=
            (_ :
              ∀ (r : K) (x : (fun x => L) y),
                AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id K) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
      ((fun x => (↑(algebraMap A L) y)⁻¹ * x) x) =
    x
[PROOFSTEP]
simp only [mul_inv_cancel_left₀ hy']
[GOAL]
case intro.intro.refine_3
R : Type u_1
A : Type u_2
K : Type u_3
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing A
inst✝¹³ : Field K
inst✝¹² : IsDomain A
inst✝¹¹ : Algebra A K
inst✝¹⁰ : IsFractionRing A K
L : Type u_4
inst✝⁹ : Field L
C : Type u_5
inst✝⁸ : CommRing C
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra A L
inst✝⁵ : IsScalarTower A K L
inst✝⁴ : Algebra C L
inst✝³ : IsIntegralClosure C A L
inst✝² : Algebra A C
inst✝¹ : IsScalarTower A C L
inst✝ : FiniteDimensional K L
this✝ : DecidableEq L := Classical.decEq L
this : IsNoetherian K L := Iff.mpr IsNoetherian.iff_fg inferInstance
s' : Finset L := IsNoetherian.finsetBasisIndex K L
bs' : Basis { x // x ∈ IsNoetherian.finsetBasisIndex K L } K L := IsNoetherian.finsetBasis K L
y : A
hy : y ≠ 0
his' : ∀ (x : L), x ∈ Finset.image (↑bs') Finset.univ → IsIntegral A (y • x)
hy' : ↑(algebraMap A L) y ≠ 0
⊢ ∀ (x : { x // x ∈ s' }),
    IsIntegral A
      (↑(Basis.map bs'
            (let src := ↑(lmul K ((fun x => L) y)) (↑(algebraMap A L) y);
            {
              toLinearMap :=
                {
                  toAddHom :=
                    { toFun := fun x => ↑(algebraMap A L) y * x,
                      map_add' :=
                        (_ :
                          ∀ (x y_1 : (fun x => L) y),
                            AddHom.toFun src.toAddHom (x + y_1) =
                              AddHom.toFun src.toAddHom x + AddHom.toFun src.toAddHom y_1) },
                  map_smul' :=
                    (_ :
                      ∀ (r : K) (x : (fun x => L) y),
                        AddHom.toFun src.toAddHom (r • x) = ↑(RingHom.id K) r • AddHom.toFun src.toAddHom x) },
              invFun := fun x => (↑(algebraMap A L) y)⁻¹ * x,
              left_inv := (_ : ∀ (x : L), (↑(algebraMap A L) y)⁻¹ * (↑(algebraMap A L) y * x) = x),
              right_inv := (_ : ∀ (x : L), ↑(algebraMap A L) y * ((↑(algebraMap A L) y)⁻¹ * x) = x) }))
        x)
[PROOFSTEP]
rintro ⟨x', hx'⟩
[GOAL]
case intro.intro.refine_3.mk
R : Type u_1
A : Type u_2
K : Type u_3
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing A
inst✝¹³ : Field K
inst✝¹² : IsDomain A
inst✝¹¹ : Algebra A K
inst✝¹⁰ : IsFractionRing A K
L : Type u_4
inst✝⁹ : Field L
C : Type u_5
inst✝⁸ : CommRing C
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra A L
inst✝⁵ : IsScalarTower A K L
inst✝⁴ : Algebra C L
inst✝³ : IsIntegralClosure C A L
inst✝² : Algebra A C
inst✝¹ : IsScalarTower A C L
inst✝ : FiniteDimensional K L
this✝ : DecidableEq L := Classical.decEq L
this : IsNoetherian K L := Iff.mpr IsNoetherian.iff_fg inferInstance
s' : Finset L := IsNoetherian.finsetBasisIndex K L
bs' : Basis { x // x ∈ IsNoetherian.finsetBasisIndex K L } K L := IsNoetherian.finsetBasis K L
y : A
hy : y ≠ 0
his' : ∀ (x : L), x ∈ Finset.image (↑bs') Finset.univ → IsIntegral A (y • x)
hy' : ↑(algebraMap A L) y ≠ 0
x' : L
hx' : x' ∈ s'
⊢ IsIntegral A
    (↑(Basis.map bs'
          (let src := ↑(lmul K ((fun x => L) y)) (↑(algebraMap A L) y);
          {
            toLinearMap :=
              {
                toAddHom :=
                  { toFun := fun x => ↑(algebraMap A L) y * x,
                    map_add' :=
                      (_ :
                        ∀ (x y_1 : (fun x => L) y),
                          AddHom.toFun src.toAddHom (x + y_1) =
                            AddHom.toFun src.toAddHom x + AddHom.toFun src.toAddHom y_1) },
                map_smul' :=
                  (_ :
                    ∀ (r : K) (x : (fun x => L) y),
                      AddHom.toFun src.toAddHom (r • x) = ↑(RingHom.id K) r • AddHom.toFun src.toAddHom x) },
            invFun := fun x => (↑(algebraMap A L) y)⁻¹ * x,
            left_inv := (_ : ∀ (x : L), (↑(algebraMap A L) y)⁻¹ * (↑(algebraMap A L) y * x) = x),
            right_inv := (_ : ∀ (x : L), ↑(algebraMap A L) y * ((↑(algebraMap A L) y)⁻¹ * x) = x) }))
      { val := x', property := hx' })
[PROOFSTEP]
simp only [Algebra.smul_def, Finset.mem_image, exists_prop, Finset.mem_univ, true_and_iff] at his'
[GOAL]
case intro.intro.refine_3.mk
R : Type u_1
A : Type u_2
K : Type u_3
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing A
inst✝¹³ : Field K
inst✝¹² : IsDomain A
inst✝¹¹ : Algebra A K
inst✝¹⁰ : IsFractionRing A K
L : Type u_4
inst✝⁹ : Field L
C : Type u_5
inst✝⁸ : CommRing C
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra A L
inst✝⁵ : IsScalarTower A K L
inst✝⁴ : Algebra C L
inst✝³ : IsIntegralClosure C A L
inst✝² : Algebra A C
inst✝¹ : IsScalarTower A C L
inst✝ : FiniteDimensional K L
this✝ : DecidableEq L := Classical.decEq L
this : IsNoetherian K L := Iff.mpr IsNoetherian.iff_fg inferInstance
s' : Finset L := IsNoetherian.finsetBasisIndex K L
bs' : Basis { x // x ∈ IsNoetherian.finsetBasisIndex K L } K L := IsNoetherian.finsetBasis K L
y : A
hy : y ≠ 0
hy' : ↑(algebraMap A L) y ≠ 0
x' : L
hx' : x' ∈ s'
his' : ∀ (x : L), (∃ a, ↑(IsNoetherian.finsetBasis K L) a = x) → IsIntegral A (↑(algebraMap A L) y * x)
⊢ IsIntegral A
    (↑(Basis.map bs'
          (let src := ↑(lmul K ((fun x => L) y)) (↑(algebraMap A L) y);
          {
            toLinearMap :=
              {
                toAddHom :=
                  { toFun := fun x => ↑(algebraMap A L) y * x,
                    map_add' :=
                      (_ :
                        ∀ (x y_1 : (fun x => L) y),
                          AddHom.toFun src.toAddHom (x + y_1) =
                            AddHom.toFun src.toAddHom x + AddHom.toFun src.toAddHom y_1) },
                map_smul' :=
                  (_ :
                    ∀ (r : K) (x : (fun x => L) y),
                      AddHom.toFun src.toAddHom (r • x) = ↑(RingHom.id K) r • AddHom.toFun src.toAddHom x) },
            invFun := fun x => (↑(algebraMap A L) y)⁻¹ * x,
            left_inv := (_ : ∀ (x : L), (↑(algebraMap A L) y)⁻¹ * (↑(algebraMap A L) y * x) = x),
            right_inv := (_ : ∀ (x : L), ↑(algebraMap A L) y * ((↑(algebraMap A L) y)⁻¹ * x) = x) }))
      { val := x', property := hx' })
[PROOFSTEP]
simp only [Basis.map_apply, LinearEquiv.coe_mk]
[GOAL]
case intro.intro.refine_3.mk
R : Type u_1
A : Type u_2
K : Type u_3
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing A
inst✝¹³ : Field K
inst✝¹² : IsDomain A
inst✝¹¹ : Algebra A K
inst✝¹⁰ : IsFractionRing A K
L : Type u_4
inst✝⁹ : Field L
C : Type u_5
inst✝⁸ : CommRing C
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra A L
inst✝⁵ : IsScalarTower A K L
inst✝⁴ : Algebra C L
inst✝³ : IsIntegralClosure C A L
inst✝² : Algebra A C
inst✝¹ : IsScalarTower A C L
inst✝ : FiniteDimensional K L
this✝ : DecidableEq L := Classical.decEq L
this : IsNoetherian K L := Iff.mpr IsNoetherian.iff_fg inferInstance
s' : Finset L := IsNoetherian.finsetBasisIndex K L
bs' : Basis { x // x ∈ IsNoetherian.finsetBasisIndex K L } K L := IsNoetherian.finsetBasis K L
y : A
hy : y ≠ 0
hy' : ↑(algebraMap A L) y ≠ 0
x' : L
hx' : x' ∈ s'
his' : ∀ (x : L), (∃ a, ↑(IsNoetherian.finsetBasis K L) a = x) → IsIntegral A (↑(algebraMap A L) y * x)
⊢ IsIntegral A (↑(algebraMap A L) y * ↑(IsNoetherian.finsetBasis K L) { val := x', property := hx' })
[PROOFSTEP]
exact his' _ ⟨_, rfl⟩
[GOAL]
R : Type u_1
A : Type u_2
K : Type u_3
inst✝¹⁸ : CommRing R
inst✝¹⁷ : CommRing A
inst✝¹⁶ : Field K
inst✝¹⁵ : IsDomain A
inst✝¹⁴ : Algebra A K
inst✝¹³ : IsFractionRing A K
L : Type u_4
inst✝¹² : Field L
C : Type u_5
inst✝¹¹ : CommRing C
inst✝¹⁰ : Algebra K L
inst✝⁹ : Algebra A L
inst✝⁸ : IsScalarTower A K L
inst✝⁷ : Algebra C L
inst✝⁶ : IsIntegralClosure C A L
inst✝⁵ : Algebra A C
inst✝⁴ : IsScalarTower A C L
inst✝³ : FiniteDimensional K L
inst✝² : IsSeparable K L
inst✝¹ : IsIntegrallyClosed A
inst✝ : IsNoetherianRing A
⊢ IsNoetherian A C
[PROOFSTEP]
haveI := Classical.decEq L
[GOAL]
R : Type u_1
A : Type u_2
K : Type u_3
inst✝¹⁸ : CommRing R
inst✝¹⁷ : CommRing A
inst✝¹⁶ : Field K
inst✝¹⁵ : IsDomain A
inst✝¹⁴ : Algebra A K
inst✝¹³ : IsFractionRing A K
L : Type u_4
inst✝¹² : Field L
C : Type u_5
inst✝¹¹ : CommRing C
inst✝¹⁰ : Algebra K L
inst✝⁹ : Algebra A L
inst✝⁸ : IsScalarTower A K L
inst✝⁷ : Algebra C L
inst✝⁶ : IsIntegralClosure C A L
inst✝⁵ : Algebra A C
inst✝⁴ : IsScalarTower A C L
inst✝³ : FiniteDimensional K L
inst✝² : IsSeparable K L
inst✝¹ : IsIntegrallyClosed A
inst✝ : IsNoetherianRing A
this : DecidableEq L
⊢ IsNoetherian A C
[PROOFSTEP]
obtain ⟨s, b, hb_int⟩ := FiniteDimensional.exists_is_basis_integral A K L
[GOAL]
case intro.intro
R : Type u_1
A : Type u_2
K : Type u_3
inst✝¹⁸ : CommRing R
inst✝¹⁷ : CommRing A
inst✝¹⁶ : Field K
inst✝¹⁵ : IsDomain A
inst✝¹⁴ : Algebra A K
inst✝¹³ : IsFractionRing A K
L : Type u_4
inst✝¹² : Field L
C : Type u_5
inst✝¹¹ : CommRing C
inst✝¹⁰ : Algebra K L
inst✝⁹ : Algebra A L
inst✝⁸ : IsScalarTower A K L
inst✝⁷ : Algebra C L
inst✝⁶ : IsIntegralClosure C A L
inst✝⁵ : Algebra A C
inst✝⁴ : IsScalarTower A C L
inst✝³ : FiniteDimensional K L
inst✝² : IsSeparable K L
inst✝¹ : IsIntegrallyClosed A
inst✝ : IsNoetherianRing A
this : DecidableEq L
s : Finset L
b : Basis { x // x ∈ s } K L
hb_int : ∀ (x : { x // x ∈ s }), IsIntegral A (↑b x)
⊢ IsNoetherian A C
[PROOFSTEP]
let b' := (traceForm K L).dualBasis (traceForm_nondegenerate K L) b
[GOAL]
case intro.intro
R : Type u_1
A : Type u_2
K : Type u_3
inst✝¹⁸ : CommRing R
inst✝¹⁷ : CommRing A
inst✝¹⁶ : Field K
inst✝¹⁵ : IsDomain A
inst✝¹⁴ : Algebra A K
inst✝¹³ : IsFractionRing A K
L : Type u_4
inst✝¹² : Field L
C : Type u_5
inst✝¹¹ : CommRing C
inst✝¹⁰ : Algebra K L
inst✝⁹ : Algebra A L
inst✝⁸ : IsScalarTower A K L
inst✝⁷ : Algebra C L
inst✝⁶ : IsIntegralClosure C A L
inst✝⁵ : Algebra A C
inst✝⁴ : IsScalarTower A C L
inst✝³ : FiniteDimensional K L
inst✝² : IsSeparable K L
inst✝¹ : IsIntegrallyClosed A
inst✝ : IsNoetherianRing A
this : DecidableEq L
s : Finset L
b : Basis { x // x ∈ s } K L
hb_int : ∀ (x : { x // x ∈ s }), IsIntegral A (↑b x)
b' : Basis { x // x ∈ s } K L := BilinForm.dualBasis (traceForm K L) (_ : BilinForm.Nondegenerate (traceForm K L)) b
⊢ IsNoetherian A C
[PROOFSTEP]
letI := isNoetherian_span_of_finite A (Set.finite_range b')
[GOAL]
case intro.intro
R : Type u_1
A : Type u_2
K : Type u_3
inst✝¹⁸ : CommRing R
inst✝¹⁷ : CommRing A
inst✝¹⁶ : Field K
inst✝¹⁵ : IsDomain A
inst✝¹⁴ : Algebra A K
inst✝¹³ : IsFractionRing A K
L : Type u_4
inst✝¹² : Field L
C : Type u_5
inst✝¹¹ : CommRing C
inst✝¹⁰ : Algebra K L
inst✝⁹ : Algebra A L
inst✝⁸ : IsScalarTower A K L
inst✝⁷ : Algebra C L
inst✝⁶ : IsIntegralClosure C A L
inst✝⁵ : Algebra A C
inst✝⁴ : IsScalarTower A C L
inst✝³ : FiniteDimensional K L
inst✝² : IsSeparable K L
inst✝¹ : IsIntegrallyClosed A
inst✝ : IsNoetherianRing A
this✝ : DecidableEq L
s : Finset L
b : Basis { x // x ∈ s } K L
hb_int : ∀ (x : { x // x ∈ s }), IsIntegral A (↑b x)
b' : Basis { x // x ∈ s } K L := BilinForm.dualBasis (traceForm K L) (_ : BilinForm.Nondegenerate (traceForm K L)) b
this : IsNoetherian A { x // x ∈ Submodule.span A (Set.range ↑b') } :=
  isNoetherian_span_of_finite A (Set.finite_range ↑b')
⊢ IsNoetherian A C
[PROOFSTEP]
let f : C →ₗ[A] Submodule.span A (Set.range b') :=
  (Submodule.ofLe (IsIntegralClosure.range_le_span_dualBasis C b hb_int)).comp
    ((Algebra.linearMap C L).restrictScalars A).rangeRestrict
[GOAL]
case intro.intro
R : Type u_1
A : Type u_2
K : Type u_3
inst✝¹⁸ : CommRing R
inst✝¹⁷ : CommRing A
inst✝¹⁶ : Field K
inst✝¹⁵ : IsDomain A
inst✝¹⁴ : Algebra A K
inst✝¹³ : IsFractionRing A K
L : Type u_4
inst✝¹² : Field L
C : Type u_5
inst✝¹¹ : CommRing C
inst✝¹⁰ : Algebra K L
inst✝⁹ : Algebra A L
inst✝⁸ : IsScalarTower A K L
inst✝⁷ : Algebra C L
inst✝⁶ : IsIntegralClosure C A L
inst✝⁵ : Algebra A C
inst✝⁴ : IsScalarTower A C L
inst✝³ : FiniteDimensional K L
inst✝² : IsSeparable K L
inst✝¹ : IsIntegrallyClosed A
inst✝ : IsNoetherianRing A
this✝ : DecidableEq L
s : Finset L
b : Basis { x // x ∈ s } K L
hb_int : ∀ (x : { x // x ∈ s }), IsIntegral A (↑b x)
b' : Basis { x // x ∈ s } K L := BilinForm.dualBasis (traceForm K L) (_ : BilinForm.Nondegenerate (traceForm K L)) b
this : IsNoetherian A { x // x ∈ Submodule.span A (Set.range ↑b') } :=
  isNoetherian_span_of_finite A (Set.finite_range ↑b')
f : C →ₗ[A] { x // x ∈ Submodule.span A (Set.range ↑b') } :=
  LinearMap.comp
    (Submodule.ofLe
      (_ :
        LinearMap.range (↑A (Algebra.linearMap C L)) ≤
          Submodule.span A
            (Set.range ↑(BilinForm.dualBasis (traceForm K L) (_ : BilinForm.Nondegenerate (traceForm K L)) b))))
    (LinearMap.rangeRestrict (↑A (Algebra.linearMap C L)))
⊢ IsNoetherian A C
[PROOFSTEP]
refine' isNoetherian_of_ker_bot f _
[GOAL]
case intro.intro
R : Type u_1
A : Type u_2
K : Type u_3
inst✝¹⁸ : CommRing R
inst✝¹⁷ : CommRing A
inst✝¹⁶ : Field K
inst✝¹⁵ : IsDomain A
inst✝¹⁴ : Algebra A K
inst✝¹³ : IsFractionRing A K
L : Type u_4
inst✝¹² : Field L
C : Type u_5
inst✝¹¹ : CommRing C
inst✝¹⁰ : Algebra K L
inst✝⁹ : Algebra A L
inst✝⁸ : IsScalarTower A K L
inst✝⁷ : Algebra C L
inst✝⁶ : IsIntegralClosure C A L
inst✝⁵ : Algebra A C
inst✝⁴ : IsScalarTower A C L
inst✝³ : FiniteDimensional K L
inst✝² : IsSeparable K L
inst✝¹ : IsIntegrallyClosed A
inst✝ : IsNoetherianRing A
this✝ : DecidableEq L
s : Finset L
b : Basis { x // x ∈ s } K L
hb_int : ∀ (x : { x // x ∈ s }), IsIntegral A (↑b x)
b' : Basis { x // x ∈ s } K L := BilinForm.dualBasis (traceForm K L) (_ : BilinForm.Nondegenerate (traceForm K L)) b
this : IsNoetherian A { x // x ∈ Submodule.span A (Set.range ↑b') } :=
  isNoetherian_span_of_finite A (Set.finite_range ↑b')
f : C →ₗ[A] { x // x ∈ Submodule.span A (Set.range ↑b') } :=
  LinearMap.comp
    (Submodule.ofLe
      (_ :
        LinearMap.range (↑A (Algebra.linearMap C L)) ≤
          Submodule.span A
            (Set.range ↑(BilinForm.dualBasis (traceForm K L) (_ : BilinForm.Nondegenerate (traceForm K L)) b))))
    (LinearMap.rangeRestrict (↑A (Algebra.linearMap C L)))
⊢ LinearMap.ker f = ⊥
[PROOFSTEP]
rw [LinearMap.ker_comp, Submodule.ker_ofLe, Submodule.comap_bot, LinearMap.ker_codRestrict]
[GOAL]
case intro.intro
R : Type u_1
A : Type u_2
K : Type u_3
inst✝¹⁸ : CommRing R
inst✝¹⁷ : CommRing A
inst✝¹⁶ : Field K
inst✝¹⁵ : IsDomain A
inst✝¹⁴ : Algebra A K
inst✝¹³ : IsFractionRing A K
L : Type u_4
inst✝¹² : Field L
C : Type u_5
inst✝¹¹ : CommRing C
inst✝¹⁰ : Algebra K L
inst✝⁹ : Algebra A L
inst✝⁸ : IsScalarTower A K L
inst✝⁷ : Algebra C L
inst✝⁶ : IsIntegralClosure C A L
inst✝⁵ : Algebra A C
inst✝⁴ : IsScalarTower A C L
inst✝³ : FiniteDimensional K L
inst✝² : IsSeparable K L
inst✝¹ : IsIntegrallyClosed A
inst✝ : IsNoetherianRing A
this✝ : DecidableEq L
s : Finset L
b : Basis { x // x ∈ s } K L
hb_int : ∀ (x : { x // x ∈ s }), IsIntegral A (↑b x)
b' : Basis { x // x ∈ s } K L := BilinForm.dualBasis (traceForm K L) (_ : BilinForm.Nondegenerate (traceForm K L)) b
this : IsNoetherian A { x // x ∈ Submodule.span A (Set.range ↑b') } :=
  isNoetherian_span_of_finite A (Set.finite_range ↑b')
f : C →ₗ[A] { x // x ∈ Submodule.span A (Set.range ↑b') } :=
  LinearMap.comp
    (Submodule.ofLe
      (_ :
        LinearMap.range (↑A (Algebra.linearMap C L)) ≤
          Submodule.span A
            (Set.range ↑(BilinForm.dualBasis (traceForm K L) (_ : BilinForm.Nondegenerate (traceForm K L)) b))))
    (LinearMap.rangeRestrict (↑A (Algebra.linearMap C L)))
⊢ LinearMap.ker (↑A (Algebra.linearMap C L)) = ⊥
[PROOFSTEP]
exact LinearMap.ker_eq_bot_of_injective (IsIntegralClosure.algebraMap_injective C A L)
[GOAL]
R : Type u_1
A : Type u_2
K : Type u_3
inst✝¹⁸ : CommRing R
inst✝¹⁷ : CommRing A
inst✝¹⁶ : Field K
inst✝¹⁵ : IsDomain A
inst✝¹⁴ : Algebra A K
inst✝¹³ : IsFractionRing A K
L : Type u_4
inst✝¹² : Field L
C : Type u_5
inst✝¹¹ : CommRing C
inst✝¹⁰ : Algebra K L
inst✝⁹ : Algebra A L
inst✝⁸ : IsScalarTower A K L
inst✝⁷ : Algebra C L
inst✝⁶ : IsIntegralClosure C A L
inst✝⁵ : Algebra A C
inst✝⁴ : IsScalarTower A C L
inst✝³ : FiniteDimensional K L
inst✝² : IsSeparable K L
inst✝¹ : NoZeroSMulDivisors A L
inst✝ : IsPrincipalIdealRing A
⊢ Module.Free A C
[PROOFSTEP]
haveI : NoZeroSMulDivisors A C := IsIntegralClosure.noZeroSMulDivisors A L
[GOAL]
R : Type u_1
A : Type u_2
K : Type u_3
inst✝¹⁸ : CommRing R
inst✝¹⁷ : CommRing A
inst✝¹⁶ : Field K
inst✝¹⁵ : IsDomain A
inst✝¹⁴ : Algebra A K
inst✝¹³ : IsFractionRing A K
L : Type u_4
inst✝¹² : Field L
C : Type u_5
inst✝¹¹ : CommRing C
inst✝¹⁰ : Algebra K L
inst✝⁹ : Algebra A L
inst✝⁸ : IsScalarTower A K L
inst✝⁷ : Algebra C L
inst✝⁶ : IsIntegralClosure C A L
inst✝⁵ : Algebra A C
inst✝⁴ : IsScalarTower A C L
inst✝³ : FiniteDimensional K L
inst✝² : IsSeparable K L
inst✝¹ : NoZeroSMulDivisors A L
inst✝ : IsPrincipalIdealRing A
this : NoZeroSMulDivisors A C
⊢ Module.Free A C
[PROOFSTEP]
haveI : IsNoetherian A C := IsIntegralClosure.isNoetherian A K L _
[GOAL]
R : Type u_1
A : Type u_2
K : Type u_3
inst✝¹⁸ : CommRing R
inst✝¹⁷ : CommRing A
inst✝¹⁶ : Field K
inst✝¹⁵ : IsDomain A
inst✝¹⁴ : Algebra A K
inst✝¹³ : IsFractionRing A K
L : Type u_4
inst✝¹² : Field L
C : Type u_5
inst✝¹¹ : CommRing C
inst✝¹⁰ : Algebra K L
inst✝⁹ : Algebra A L
inst✝⁸ : IsScalarTower A K L
inst✝⁷ : Algebra C L
inst✝⁶ : IsIntegralClosure C A L
inst✝⁵ : Algebra A C
inst✝⁴ : IsScalarTower A C L
inst✝³ : FiniteDimensional K L
inst✝² : IsSeparable K L
inst✝¹ : NoZeroSMulDivisors A L
inst✝ : IsPrincipalIdealRing A
this✝ : NoZeroSMulDivisors A C
this : IsNoetherian A C
⊢ Module.Free A C
[PROOFSTEP]
exact Module.free_of_finite_type_torsion_free'
[GOAL]
R : Type u_1
A : Type u_2
K : Type u_3
inst✝¹⁸ : CommRing R
inst✝¹⁷ : CommRing A
inst✝¹⁶ : Field K
inst✝¹⁵ : IsDomain A
inst✝¹⁴ : Algebra A K
inst✝¹³ : IsFractionRing A K
L : Type u_4
inst✝¹² : Field L
C : Type u_5
inst✝¹¹ : CommRing C
inst✝¹⁰ : Algebra K L
inst✝⁹ : Algebra A L
inst✝⁸ : IsScalarTower A K L
inst✝⁷ : Algebra C L
inst✝⁶ : IsIntegralClosure C A L
inst✝⁵ : Algebra A C
inst✝⁴ : IsScalarTower A C L
inst✝³ : FiniteDimensional K L
inst✝² : IsSeparable K L
inst✝¹ : IsPrincipalIdealRing A
inst✝ : NoZeroSMulDivisors A L
⊢ FiniteDimensional.finrank A C = FiniteDimensional.finrank K L
[PROOFSTEP]
haveI : Module.Free A C := IsIntegralClosure.module_free A K L C
[GOAL]
R : Type u_1
A : Type u_2
K : Type u_3
inst✝¹⁸ : CommRing R
inst✝¹⁷ : CommRing A
inst✝¹⁶ : Field K
inst✝¹⁵ : IsDomain A
inst✝¹⁴ : Algebra A K
inst✝¹³ : IsFractionRing A K
L : Type u_4
inst✝¹² : Field L
C : Type u_5
inst✝¹¹ : CommRing C
inst✝¹⁰ : Algebra K L
inst✝⁹ : Algebra A L
inst✝⁸ : IsScalarTower A K L
inst✝⁷ : Algebra C L
inst✝⁶ : IsIntegralClosure C A L
inst✝⁵ : Algebra A C
inst✝⁴ : IsScalarTower A C L
inst✝³ : FiniteDimensional K L
inst✝² : IsSeparable K L
inst✝¹ : IsPrincipalIdealRing A
inst✝ : NoZeroSMulDivisors A L
this : Module.Free A C
⊢ FiniteDimensional.finrank A C = FiniteDimensional.finrank K L
[PROOFSTEP]
haveI : IsNoetherian A C := IsIntegralClosure.isNoetherian A K L C
[GOAL]
R : Type u_1
A : Type u_2
K : Type u_3
inst✝¹⁸ : CommRing R
inst✝¹⁷ : CommRing A
inst✝¹⁶ : Field K
inst✝¹⁵ : IsDomain A
inst✝¹⁴ : Algebra A K
inst✝¹³ : IsFractionRing A K
L : Type u_4
inst✝¹² : Field L
C : Type u_5
inst✝¹¹ : CommRing C
inst✝¹⁰ : Algebra K L
inst✝⁹ : Algebra A L
inst✝⁸ : IsScalarTower A K L
inst✝⁷ : Algebra C L
inst✝⁶ : IsIntegralClosure C A L
inst✝⁵ : Algebra A C
inst✝⁴ : IsScalarTower A C L
inst✝³ : FiniteDimensional K L
inst✝² : IsSeparable K L
inst✝¹ : IsPrincipalIdealRing A
inst✝ : NoZeroSMulDivisors A L
this✝ : Module.Free A C
this : IsNoetherian A C
⊢ FiniteDimensional.finrank A C = FiniteDimensional.finrank K L
[PROOFSTEP]
haveI : IsLocalization (Algebra.algebraMapSubmonoid C A⁰) L := IsIntegralClosure.isLocalization A K L C
[GOAL]
R : Type u_1
A : Type u_2
K : Type u_3
inst✝¹⁸ : CommRing R
inst✝¹⁷ : CommRing A
inst✝¹⁶ : Field K
inst✝¹⁵ : IsDomain A
inst✝¹⁴ : Algebra A K
inst✝¹³ : IsFractionRing A K
L : Type u_4
inst✝¹² : Field L
C : Type u_5
inst✝¹¹ : CommRing C
inst✝¹⁰ : Algebra K L
inst✝⁹ : Algebra A L
inst✝⁸ : IsScalarTower A K L
inst✝⁷ : Algebra C L
inst✝⁶ : IsIntegralClosure C A L
inst✝⁵ : Algebra A C
inst✝⁴ : IsScalarTower A C L
inst✝³ : FiniteDimensional K L
inst✝² : IsSeparable K L
inst✝¹ : IsPrincipalIdealRing A
inst✝ : NoZeroSMulDivisors A L
this✝¹ : Module.Free A C
this✝ : IsNoetherian A C
this : IsLocalization (algebraMapSubmonoid C A⁰) L
⊢ FiniteDimensional.finrank A C = FiniteDimensional.finrank K L
[PROOFSTEP]
let b := Basis.localizationLocalization K A⁰ L (Module.Free.chooseBasis A C)
[GOAL]
R : Type u_1
A : Type u_2
K : Type u_3
inst✝¹⁸ : CommRing R
inst✝¹⁷ : CommRing A
inst✝¹⁶ : Field K
inst✝¹⁵ : IsDomain A
inst✝¹⁴ : Algebra A K
inst✝¹³ : IsFractionRing A K
L : Type u_4
inst✝¹² : Field L
C : Type u_5
inst✝¹¹ : CommRing C
inst✝¹⁰ : Algebra K L
inst✝⁹ : Algebra A L
inst✝⁸ : IsScalarTower A K L
inst✝⁷ : Algebra C L
inst✝⁶ : IsIntegralClosure C A L
inst✝⁵ : Algebra A C
inst✝⁴ : IsScalarTower A C L
inst✝³ : FiniteDimensional K L
inst✝² : IsSeparable K L
inst✝¹ : IsPrincipalIdealRing A
inst✝ : NoZeroSMulDivisors A L
this✝¹ : Module.Free A C
this✝ : IsNoetherian A C
this : IsLocalization (algebraMapSubmonoid C A⁰) L
b : Basis (Module.Free.ChooseBasisIndex A C) K L := Basis.localizationLocalization K A⁰ L (Module.Free.chooseBasis A C)
⊢ FiniteDimensional.finrank A C = FiniteDimensional.finrank K L
[PROOFSTEP]
rw [FiniteDimensional.finrank_eq_card_chooseBasisIndex, FiniteDimensional.finrank_eq_card_basis b]


[GOAL]
x y : ℍ
⊢ ↑(starRingEnd ℝ) (inner y x) = inner x y
[PROOFSTEP]
simp [inner_def, mul_comm]
[GOAL]
x y z : ℍ
⊢ inner (x + y) z = inner x z + inner y z
[PROOFSTEP]
simp only [inner_def, add_mul, add_re]
[GOAL]
x y : ℍ
r : ℝ
⊢ inner (r • x) y = ↑(starRingEnd ℝ) r * inner x y
[PROOFSTEP]
simp [inner_def]
[GOAL]
a : ℍ
⊢ ↑normSq a = ‖a‖ * ‖a‖
[PROOFSTEP]
rw [← inner_self, real_inner_self_eq_norm_mul_norm]
[GOAL]
⊢ ‖1‖ = 1
[PROOFSTEP]
rw [norm_eq_sqrt_real_inner, inner_self, normSq.map_one, Real.sqrt_one]
[GOAL]
a : ℝ
⊢ ‖↑a‖ = ‖a‖
[PROOFSTEP]
rw [norm_eq_sqrt_real_inner, inner_self, normSq_coe, Real.sqrt_sq_eq_abs, Real.norm_eq_abs]
[GOAL]
a : ℍ
⊢ ‖star a‖ = ‖a‖
[PROOFSTEP]
simp_rw [norm_eq_sqrt_real_inner, inner_self, normSq_star]
[GOAL]
a b : ℍ
⊢ ‖a * b‖ = ‖a‖ * ‖b‖
[PROOFSTEP]
simp only [norm_eq_sqrt_real_inner, inner_self, normSq.map_mul]
[GOAL]
a b : ℍ
⊢ Real.sqrt (↑normSq a * ↑normSq b) = Real.sqrt (↑normSq a) * Real.sqrt (↑normSq b)
[PROOFSTEP]
exact
  Real.sqrt_mul normSq_nonneg
    _
      -- porting note: added `noncomputable`
[GOAL]
z w : ℂ
⊢ ↑(z + w) = ↑z + ↑w
[PROOFSTEP]
ext
[GOAL]
case a
z w : ℂ
⊢ (↑(z + w)).re = (↑z + ↑w).re
[PROOFSTEP]
simp
[GOAL]
case a
z w : ℂ
⊢ (↑(z + w)).imI = (↑z + ↑w).imI
[PROOFSTEP]
simp
[GOAL]
case a
z w : ℂ
⊢ (↑(z + w)).imJ = (↑z + ↑w).imJ
[PROOFSTEP]
simp
[GOAL]
case a
z w : ℂ
⊢ (↑(z + w)).imK = (↑z + ↑w).imK
[PROOFSTEP]
simp
[GOAL]
z w : ℂ
⊢ ↑(z * w) = ↑z * ↑w
[PROOFSTEP]
ext
[GOAL]
case a
z w : ℂ
⊢ (↑(z * w)).re = (↑z * ↑w).re
[PROOFSTEP]
simp
[GOAL]
case a
z w : ℂ
⊢ (↑(z * w)).imI = (↑z * ↑w).imI
[PROOFSTEP]
simp
[GOAL]
case a
z w : ℂ
⊢ (↑(z * w)).imJ = (↑z * ↑w).imJ
[PROOFSTEP]
simp
[GOAL]
case a
z w : ℂ
⊢ (↑(z * w)).imK = (↑z * ↑w).imK
[PROOFSTEP]
simp
[GOAL]
r : ℝ
z : ℂ
⊢ ↑(r • z) = ↑r * ↑z
[PROOFSTEP]
ext
[GOAL]
case a
r : ℝ
z : ℂ
⊢ (↑(r • z)).re = (↑r * ↑z).re
[PROOFSTEP]
simp
[GOAL]
case a
r : ℝ
z : ℂ
⊢ (↑(r • z)).imI = (↑r * ↑z).imI
[PROOFSTEP]
simp
[GOAL]
case a
r : ℝ
z : ℂ
⊢ (↑(r • z)).imJ = (↑r * ↑z).imJ
[PROOFSTEP]
simp
[GOAL]
case a
r : ℝ
z : ℂ
⊢ (↑(r • z)).imK = (↑r * ↑z).imK
[PROOFSTEP]
simp
[GOAL]
x : ℍ
⊢ ‖↑(PiLp.equiv 2 fun x => ℝ).symm (↑(equivTuple ℝ) x)‖ = ‖x‖
[PROOFSTEP]
rw [norm_eq_sqrt_real_inner, norm_eq_sqrt_real_inner, inner_self, normSq_def', PiLp.inner_apply, Fin.sum_univ_four]
[GOAL]
x : ℍ
⊢ Real.sqrt
      (inner (↑(PiLp.equiv 2 fun x => ℝ).symm (↑(equivTuple ℝ) x) 0)
              (↑(PiLp.equiv 2 fun x => ℝ).symm (↑(equivTuple ℝ) x) 0) +
            inner (↑(PiLp.equiv 2 fun x => ℝ).symm (↑(equivTuple ℝ) x) 1)
              (↑(PiLp.equiv 2 fun x => ℝ).symm (↑(equivTuple ℝ) x) 1) +
          inner (↑(PiLp.equiv 2 fun x => ℝ).symm (↑(equivTuple ℝ) x) 2)
            (↑(PiLp.equiv 2 fun x => ℝ).symm (↑(equivTuple ℝ) x) 2) +
        inner (↑(PiLp.equiv 2 fun x => ℝ).symm (↑(equivTuple ℝ) x) 3)
          (↑(PiLp.equiv 2 fun x => ℝ).symm (↑(equivTuple ℝ) x) 3)) =
    Real.sqrt (x.re ^ 2 + x.imI ^ 2 + x.imJ ^ 2 + x.imK ^ 2)
[PROOFSTEP]
simp_rw [IsROrC.inner_apply, starRingEnd_apply, star_trivial, ← sq]
[GOAL]
x : ℍ
⊢ Real.sqrt
      (↑(PiLp.equiv 2 fun x => ℝ).symm (↑(equivTuple ℝ) x) 0 ^ 2 +
            ↑(PiLp.equiv 2 fun x => ℝ).symm (↑(equivTuple ℝ) x) 1 ^ 2 +
          ↑(PiLp.equiv 2 fun x => ℝ).symm (↑(equivTuple ℝ) x) 2 ^ 2 +
        ↑(PiLp.equiv 2 fun x => ℝ).symm (↑(equivTuple ℝ) x) 3 ^ 2) =
    Real.sqrt (x.re ^ 2 + x.imI ^ 2 + x.imJ ^ 2 + x.imK ^ 2)
[PROOFSTEP]
rfl
[GOAL]
⊢ Continuous ↑normSq
[PROOFSTEP]
simpa [← normSq_eq_norm_mul_self] using (continuous_norm.mul continuous_norm : Continuous fun q : ℍ => ‖q‖ * ‖q‖)
[GOAL]
⊢ Continuous fun q => im q
[PROOFSTEP]
simpa only [← sub_self_re] using continuous_id.sub (continuous_coe.comp continuous_re)
[GOAL]
this : UniformEmbedding ↑(LinearEquiv.toEquiv linearIsometryEquivTuple.toLinearEquiv).symm
⊢ CompleteSpace (EuclideanSpace ℝ (Fin 4))
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u_1
f : α → ℝ
r : ℝ
h : HasSum (fun a => ↑(f a)) ↑r
⊢ HasSum f r
[PROOFSTEP]
simpa only using h.map (show ℍ →ₗ[ℝ] ℝ from QuaternionAlgebra.reₗ _ _) continuous_re
[GOAL]
α : Type u_1
f : α → ℝ
r : ℝ
h : HasSum f r
⊢ HasSum (fun a => ↑(f a)) ↑r
[PROOFSTEP]
simpa only using h.map (algebraMap ℝ ℍ) (continuous_algebraMap _ _)
[GOAL]
α : Type u_1
f : α → ℝ
⊢ (Summable fun a => ↑(f a)) ↔ Summable f
[PROOFSTEP]
simpa only using
  Summable.map_iff_of_leftInverse (algebraMap ℝ ℍ) (show ℍ →ₗ[ℝ] ℝ from QuaternionAlgebra.reₗ _ _)
    (continuous_algebraMap _ _) continuous_re coe_re
[GOAL]
α : Type u_1
f : α → ℝ
⊢ ∑' (a : α), ↑(f a) = ↑(∑' (a : α), f a)
[PROOFSTEP]
by_cases hf : Summable f
[GOAL]
case pos
α : Type u_1
f : α → ℝ
hf : Summable f
⊢ ∑' (a : α), ↑(f a) = ↑(∑' (a : α), f a)
[PROOFSTEP]
exact (hasSum_coe.mpr hf.hasSum).tsum_eq
[GOAL]
case neg
α : Type u_1
f : α → ℝ
hf : ¬Summable f
⊢ ∑' (a : α), ↑(f a) = ↑(∑' (a : α), f a)
[PROOFSTEP]
simp [tsum_eq_zero_of_not_summable hf, tsum_eq_zero_of_not_summable (summable_coe.not.mpr hf)]