[GOAL]
K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field L'
inst✝¹ : Algebra K L
inst✝ : Algebra K L'
S : IntermediateField K L
⊢ Function.Injective fun S => S.carrier
[PROOFSTEP]
rintro ⟨⟨⟩⟩ ⟨⟨⟩⟩
[GOAL]
case mk.mk.mk.mk
K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field L'
inst✝¹ : Algebra K L
inst✝ : Algebra K L'
S : IntermediateField K L
toSubsemiring✝¹ : Subsemiring L
algebraMap_mem'✝¹ : ∀ (r : K), ↑(algebraMap K L) r ∈ toSubsemiring✝¹.carrier
inv_mem'✝¹ :
  ∀ (x : L),
    x ∈
        { toSubsemiring := toSubsemiring✝¹,
                  algebraMap_mem' := algebraMap_mem'✝¹ }.toSubsemiring.toSubmonoid.toSubsemigroup.carrier →
      x⁻¹ ∈
        { toSubsemiring := toSubsemiring✝¹,
                  algebraMap_mem' := algebraMap_mem'✝¹ }.toSubsemiring.toSubmonoid.toSubsemigroup.carrier
toSubsemiring✝ : Subsemiring L
algebraMap_mem'✝ : ∀ (r : K), ↑(algebraMap K L) r ∈ toSubsemiring✝.carrier
inv_mem'✝ :
  ∀ (x : L),
    x ∈
        { toSubsemiring := toSubsemiring✝,
                  algebraMap_mem' := algebraMap_mem'✝ }.toSubsemiring.toSubmonoid.toSubsemigroup.carrier →
      x⁻¹ ∈
        { toSubsemiring := toSubsemiring✝,
                  algebraMap_mem' := algebraMap_mem'✝ }.toSubsemiring.toSubmonoid.toSubsemigroup.carrier
⊢ (fun S => S.carrier)
        { toSubalgebra := { toSubsemiring := toSubsemiring✝¹, algebraMap_mem' := algebraMap_mem'✝¹ },
          inv_mem' := inv_mem'✝¹ } =
      (fun S => S.carrier)
        { toSubalgebra := { toSubsemiring := toSubsemiring✝, algebraMap_mem' := algebraMap_mem'✝ },
          inv_mem' := inv_mem'✝ } →
    { toSubalgebra := { toSubsemiring := toSubsemiring✝¹, algebraMap_mem' := algebraMap_mem'✝¹ },
        inv_mem' := inv_mem'✝¹ } =
      { toSubalgebra := { toSubsemiring := toSubsemiring✝, algebraMap_mem' := algebraMap_mem'✝ },
        inv_mem' := inv_mem'✝ }
[PROOFSTEP]
simp
[GOAL]
K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field L'
inst✝¹ : Algebra K L
inst✝ : Algebra K L'
S : IntermediateField K L
x : L
hx : x ∈ S
⊢ -x ∈ S
[PROOFSTEP]
show -x ∈ S.toSubalgebra
[GOAL]
K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field L'
inst✝¹ : Algebra K L
inst✝ : Algebra K L'
S : IntermediateField K L
x : L
hx : x ∈ S
⊢ -x ∈ S.toSubalgebra
[PROOFSTEP]
simpa
[GOAL]
K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field L'
inst✝¹ : Algebra K L
inst✝ : Algebra K L'
S : IntermediateField K L
n : ℕ
⊢ ↑n ∈ S
[PROOFSTEP]
simpa using coe_int_mem S n
[GOAL]
K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field L'
inst✝¹ : Algebra K L
inst✝ : Algebra K L'
S✝ : IntermediateField K L
S : Subalgebra K L
inv_mem : ∀ (x : L), x ∈ S → x⁻¹ ∈ S
⊢ (Subalgebra.toIntermediateField S inv_mem).toSubalgebra = S
[PROOFSTEP]
ext
[GOAL]
case h
K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field L'
inst✝¹ : Algebra K L
inst✝ : Algebra K L'
S✝ : IntermediateField K L
S : Subalgebra K L
inv_mem : ∀ (x : L), x ∈ S → x⁻¹ ∈ S
x✝ : L
⊢ x✝ ∈ (Subalgebra.toIntermediateField S inv_mem).toSubalgebra ↔ x✝ ∈ S
[PROOFSTEP]
rfl
[GOAL]
K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field L'
inst✝¹ : Algebra K L
inst✝ : Algebra K L'
S✝ S : IntermediateField K L
⊢ Subalgebra.toIntermediateField S.toSubalgebra (_ : ∀ (x : L), x ∈ S → x⁻¹ ∈ S) = S
[PROOFSTEP]
ext
[GOAL]
case h
K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field L'
inst✝¹ : Algebra K L
inst✝ : Algebra K L'
S✝ S : IntermediateField K L
x✝ : L
⊢ x✝ ∈ Subalgebra.toIntermediateField S.toSubalgebra (_ : ∀ (x : L), x ∈ S → x⁻¹ ∈ S) ↔ x✝ ∈ S
[PROOFSTEP]
rfl
[GOAL]
K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field L'
inst✝¹ : Algebra K L
inst✝ : Algebra K L'
S✝ : IntermediateField K L
S : Subalgebra K L
hS : IsField { x // x ∈ S }
x : L
hx : x ∈ S
⊢ x⁻¹ ∈ S
[PROOFSTEP]
by_cases hx0 : x = 0
[GOAL]
case pos
K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field L'
inst✝¹ : Algebra K L
inst✝ : Algebra K L'
S✝ : IntermediateField K L
S : Subalgebra K L
hS : IsField { x // x ∈ S }
x : L
hx : x ∈ S
hx0 : x = 0
⊢ x⁻¹ ∈ S
[PROOFSTEP]
rw [hx0, inv_zero]
[GOAL]
case pos
K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field L'
inst✝¹ : Algebra K L
inst✝ : Algebra K L'
S✝ : IntermediateField K L
S : Subalgebra K L
hS : IsField { x // x ∈ S }
x : L
hx : x ∈ S
hx0 : x = 0
⊢ 0 ∈ S
[PROOFSTEP]
exact S.zero_mem
[GOAL]
case neg
K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field L'
inst✝¹ : Algebra K L
inst✝ : Algebra K L'
S✝ : IntermediateField K L
S : Subalgebra K L
hS : IsField { x // x ∈ S }
x : L
hx : x ∈ S
hx0 : ¬x = 0
⊢ x⁻¹ ∈ S
[PROOFSTEP]
letI hS' := hS.toField
[GOAL]
case neg
K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field L'
inst✝¹ : Algebra K L
inst✝ : Algebra K L'
S✝ : IntermediateField K L
S : Subalgebra K L
hS : IsField { x // x ∈ S }
x : L
hx : x ∈ S
hx0 : ¬x = 0
hS' : Field { x // x ∈ S } := IsField.toField hS
⊢ x⁻¹ ∈ S
[PROOFSTEP]
obtain ⟨y, hy⟩ := hS.mul_inv_cancel (show (⟨x, hx⟩ : S) ≠ 0 from Subtype.ne_of_val_ne hx0)
[GOAL]
case neg.intro
K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field L'
inst✝¹ : Algebra K L
inst✝ : Algebra K L'
S✝ : IntermediateField K L
S : Subalgebra K L
hS : IsField { x // x ∈ S }
x : L
hx : x ∈ S
hx0 : ¬x = 0
hS' : Field { x // x ∈ S } := IsField.toField hS
y : { x // x ∈ S }
hy : { val := x, property := hx } * y = 1
⊢ x⁻¹ ∈ S
[PROOFSTEP]
rw [Subtype.ext_iff, S.coe_mul, S.coe_one, Subtype.coe_mk, mul_eq_one_iff_inv_eq₀ hx0] at hy 
[GOAL]
case neg.intro
K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field L'
inst✝¹ : Algebra K L
inst✝ : Algebra K L'
S✝ : IntermediateField K L
S : Subalgebra K L
hS : IsField { x // x ∈ S }
x : L
hx : x ∈ S
hx0 : ¬x = 0
hS' : Field { x // x ∈ S } := IsField.toField hS
y : { x // x ∈ S }
hy : x⁻¹ = ↑y
⊢ x⁻¹ ∈ S
[PROOFSTEP]
exact hy.symm ▸ y.2
[GOAL]
K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field L'
inst✝¹ : Algebra K L
inst✝ : Algebra K L'
S✝ : IntermediateField K L
S : Subalgebra K L
hS : IsField { x // x ∈ S }
⊢ (Subalgebra.toIntermediateField' S hS).toSubalgebra = S
[PROOFSTEP]
ext
[GOAL]
case h
K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field L'
inst✝¹ : Algebra K L
inst✝ : Algebra K L'
S✝ : IntermediateField K L
S : Subalgebra K L
hS : IsField { x // x ∈ S }
x✝ : L
⊢ x✝ ∈ (Subalgebra.toIntermediateField' S hS).toSubalgebra ↔ x✝ ∈ S
[PROOFSTEP]
rfl
[GOAL]
K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field L'
inst✝¹ : Algebra K L
inst✝ : Algebra K L'
S✝ S : IntermediateField K L
⊢ Subalgebra.toIntermediateField' S.toSubalgebra (_ : IsField { x // x ∈ S }) = S
[PROOFSTEP]
ext
[GOAL]
case h
K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field L'
inst✝¹ : Algebra K L
inst✝ : Algebra K L'
S✝ S : IntermediateField K L
x✝ : L
⊢ x✝ ∈ Subalgebra.toIntermediateField' S.toSubalgebra (_ : IsField { x // x ∈ S }) ↔ x✝ ∈ S
[PROOFSTEP]
rfl
[GOAL]
K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Field L'
inst✝² : Algebra K L
inst✝¹ : Algebra K L'
S : IntermediateField K L
ι : Type u_4
inst✝ : Fintype ι
f : ι → { x // x ∈ S }
⊢ ↑(∑ i : ι, f i) = ∑ i : ι, ↑(f i)
[PROOFSTEP]
classical
induction' (Finset.univ : Finset ι) using Finset.induction_on with i s hi H
· simp
· rw [Finset.sum_insert hi, AddMemClass.coe_add, H, Finset.sum_insert hi]
[GOAL]
K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Field L'
inst✝² : Algebra K L
inst✝¹ : Algebra K L'
S : IntermediateField K L
ι : Type u_4
inst✝ : Fintype ι
f : ι → { x // x ∈ S }
⊢ ↑(∑ i : ι, f i) = ∑ i : ι, ↑(f i)
[PROOFSTEP]
induction' (Finset.univ : Finset ι) using Finset.induction_on with i s hi H
[GOAL]
case empty
K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Field L'
inst✝² : Algebra K L
inst✝¹ : Algebra K L'
S : IntermediateField K L
ι : Type u_4
inst✝ : Fintype ι
f : ι → { x // x ∈ S }
⊢ ↑(∑ i in ∅, f i) = ∑ i in ∅, ↑(f i)
[PROOFSTEP]
simp
[GOAL]
case insert
K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Field L'
inst✝² : Algebra K L
inst✝¹ : Algebra K L'
S : IntermediateField K L
ι : Type u_4
inst✝ : Fintype ι
f : ι → { x // x ∈ S }
i : ι
s : Finset ι
hi : ¬i ∈ s
H : ↑(∑ i in s, f i) = ∑ i in s, ↑(f i)
⊢ ↑(∑ i in insert i s, f i) = ∑ i in insert i s, ↑(f i)
[PROOFSTEP]
rw [Finset.sum_insert hi, AddMemClass.coe_add, H, Finset.sum_insert hi]
[GOAL]
K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Field L'
inst✝² : Algebra K L
inst✝¹ : Algebra K L'
S : IntermediateField K L
ι : Type u_4
inst✝ : Fintype ι
f : ι → { x // x ∈ S }
⊢ ↑(∏ i : ι, f i) = ∏ i : ι, ↑(f i)
[PROOFSTEP]
classical
induction' (Finset.univ : Finset ι) using Finset.induction_on with i s hi H
· simp
· rw [Finset.prod_insert hi, MulMemClass.coe_mul, H, Finset.prod_insert hi]
[GOAL]
K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Field L'
inst✝² : Algebra K L
inst✝¹ : Algebra K L'
S : IntermediateField K L
ι : Type u_4
inst✝ : Fintype ι
f : ι → { x // x ∈ S }
⊢ ↑(∏ i : ι, f i) = ∏ i : ι, ↑(f i)
[PROOFSTEP]
induction' (Finset.univ : Finset ι) using Finset.induction_on with i s hi H
[GOAL]
case empty
K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Field L'
inst✝² : Algebra K L
inst✝¹ : Algebra K L'
S : IntermediateField K L
ι : Type u_4
inst✝ : Fintype ι
f : ι → { x // x ∈ S }
⊢ ↑(∏ i in ∅, f i) = ∏ i in ∅, ↑(f i)
[PROOFSTEP]
simp
[GOAL]
case insert
K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Field L'
inst✝² : Algebra K L
inst✝¹ : Algebra K L'
S : IntermediateField K L
ι : Type u_4
inst✝ : Fintype ι
f : ι → { x // x ∈ S }
i : ι
s : Finset ι
hi : ¬i ∈ s
H : ↑(∏ i in s, f i) = ∏ i in s, ↑(f i)
⊢ ↑(∏ i in insert i s, f i) = ∏ i in insert i s, ↑(f i)
[PROOFSTEP]
rw [Finset.prod_insert hi, MulMemClass.coe_mul, H, Finset.prod_insert hi]
[GOAL]
K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field L'
inst✝¹ : Algebra K L
inst✝ : Algebra K L'
S✝ : IntermediateField K L
f : L →ₐ[K] L'
S : IntermediateField K L
src✝ : Subalgebra K L' := Subalgebra.map f S.toSubalgebra
⊢ ∀ (x : L'),
    x ∈
        { toSubsemiring := src✝.toSubsemiring,
                  algebraMap_mem' :=
                    (_ :
                      ∀ (r : K),
                        ↑(algebraMap K L') r ∈ src✝.carrier) }.toSubsemiring.toSubmonoid.toSubsemigroup.carrier →
      x⁻¹ ∈
        { toSubsemiring := src✝.toSubsemiring,
                  algebraMap_mem' :=
                    (_ :
                      ∀ (r : K), ↑(algebraMap K L') r ∈ src✝.carrier) }.toSubsemiring.toSubmonoid.toSubsemigroup.carrier
[PROOFSTEP]
rintro _ ⟨x, hx, rfl⟩
[GOAL]
case intro.intro
K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field L'
inst✝¹ : Algebra K L
inst✝ : Algebra K L'
S✝ : IntermediateField K L
f : L →ₐ[K] L'
S : IntermediateField K L
src✝ : Subalgebra K L' := Subalgebra.map f S.toSubalgebra
x : L
hx : x ∈ ↑S.toSubsemiring
⊢ (↑↑f x)⁻¹ ∈
    { toSubsemiring := src✝.toSubsemiring,
              algebraMap_mem' :=
                (_ : ∀ (r : K), ↑(algebraMap K L') r ∈ src✝.carrier) }.toSubsemiring.toSubmonoid.toSubsemigroup.carrier
[PROOFSTEP]
exact ⟨x⁻¹, S.inv_mem hx, map_inv₀ f x⟩
[GOAL]
K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Field L'
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra K L'
S : IntermediateField K L
R : Type u_4
inst✝³ : CommRing R
inst✝² : Algebra R K
inst✝¹ : Algebra R L
inst✝ : IsScalarTower R K L
x : { x // x ∈ S }
P : R[X]
⊢ ↑(aeval ↑x) P = ↑(↑(aeval x) P)
[PROOFSTEP]
refine' Polynomial.induction_on' P (fun f g hf hg => _) fun n r => _
[GOAL]
case refine'_1
K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Field L'
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra K L'
S : IntermediateField K L
R : Type u_4
inst✝³ : CommRing R
inst✝² : Algebra R K
inst✝¹ : Algebra R L
inst✝ : IsScalarTower R K L
x : { x // x ∈ S }
P f g : R[X]
hf : ↑(aeval ↑x) f = ↑(↑(aeval x) f)
hg : ↑(aeval ↑x) g = ↑(↑(aeval x) g)
⊢ ↑(aeval ↑x) (f + g) = ↑(↑(aeval x) (f + g))
[PROOFSTEP]
rw [aeval_add, aeval_add, AddMemClass.coe_add, hf, hg]
[GOAL]
case refine'_2
K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Field L'
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra K L'
S : IntermediateField K L
R : Type u_4
inst✝³ : CommRing R
inst✝² : Algebra R K
inst✝¹ : Algebra R L
inst✝ : IsScalarTower R K L
x : { x // x ∈ S }
P : R[X]
n : ℕ
r : R
⊢ ↑(aeval ↑x) (↑(monomial n) r) = ↑(↑(aeval x) (↑(monomial n) r))
[PROOFSTEP]
simp only [MulMemClass.coe_mul, aeval_monomial, SubmonoidClass.coe_pow, mul_eq_mul_right_iff]
[GOAL]
case refine'_2
K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Field L'
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra K L'
S : IntermediateField K L
R : Type u_4
inst✝³ : CommRing R
inst✝² : Algebra R K
inst✝¹ : Algebra R L
inst✝ : IsScalarTower R K L
x : { x // x ∈ S }
P : R[X]
n : ℕ
r : R
⊢ ↑(algebraMap R L) r = ↑(↑(algebraMap R { x // x ∈ S }) r) ∨ ↑x ^ n = 0
[PROOFSTEP]
left
[GOAL]
case refine'_2.h
K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Field L'
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra K L'
S : IntermediateField K L
R : Type u_4
inst✝³ : CommRing R
inst✝² : Algebra R K
inst✝¹ : Algebra R L
inst✝ : IsScalarTower R K L
x : { x // x ∈ S }
P : R[X]
n : ℕ
r : R
⊢ ↑(algebraMap R L) r = ↑(↑(algebraMap R { x // x ∈ S }) r)
[PROOFSTEP]
rfl
[GOAL]
K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Field L'
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra K L'
S : IntermediateField K L
R : Type u_4
inst✝³ : CommRing R
inst✝² : Algebra R K
inst✝¹ : Algebra R L
inst✝ : IsScalarTower R K L
x : { x // x ∈ S }
⊢ IsIntegral R ↑x ↔ IsIntegral R x
[PROOFSTEP]
refine' ⟨fun h => _, fun h => _⟩
[GOAL]
case refine'_1
K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Field L'
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra K L'
S : IntermediateField K L
R : Type u_4
inst✝³ : CommRing R
inst✝² : Algebra R K
inst✝¹ : Algebra R L
inst✝ : IsScalarTower R K L
x : { x // x ∈ S }
h : IsIntegral R ↑x
⊢ IsIntegral R x
[PROOFSTEP]
obtain ⟨P, hPmo, hProot⟩ := h
[GOAL]
case refine'_1.intro.intro
K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Field L'
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra K L'
S : IntermediateField K L
R : Type u_4
inst✝³ : CommRing R
inst✝² : Algebra R K
inst✝¹ : Algebra R L
inst✝ : IsScalarTower R K L
x : { x // x ∈ S }
P : R[X]
hPmo : Monic P
hProot : eval₂ (algebraMap R L) (↑x) P = 0
⊢ IsIntegral R x
[PROOFSTEP]
refine' ⟨P, hPmo, (injective_iff_map_eq_zero _).1 (algebraMap (↥S) L).injective _ _⟩
[GOAL]
case refine'_1.intro.intro
K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Field L'
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra K L'
S : IntermediateField K L
R : Type u_4
inst✝³ : CommRing R
inst✝² : Algebra R K
inst✝¹ : Algebra R L
inst✝ : IsScalarTower R K L
x : { x // x ∈ S }
P : R[X]
hPmo : Monic P
hProot : eval₂ (algebraMap R L) (↑x) P = 0
⊢ ↑(algebraMap { x // x ∈ S } L) (eval₂ (algebraMap R { x // x ∈ S }) x P) = 0
[PROOFSTEP]
letI : IsScalarTower R S L := IsScalarTower.of_algebraMap_eq (congr_fun rfl)
[GOAL]
case refine'_1.intro.intro
K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Field L'
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra K L'
S : IntermediateField K L
R : Type u_4
inst✝³ : CommRing R
inst✝² : Algebra R K
inst✝¹ : Algebra R L
inst✝ : IsScalarTower R K L
x : { x // x ∈ S }
P : R[X]
hPmo : Monic P
hProot : eval₂ (algebraMap R L) (↑x) P = 0
this : IsScalarTower R { x // x ∈ S } L := IsScalarTower.of_algebraMap_eq (congr_fun rfl)
⊢ ↑(algebraMap { x // x ∈ S } L) (eval₂ (algebraMap R { x // x ∈ S }) x P) = 0
[PROOFSTEP]
rw [eval₂_eq_eval_map, ← eval₂_at_apply, eval₂_eq_eval_map, Polynomial.map_map, ←
  --Porting note: very strange that I have to `rw` twice with `eval₂_eq_eval_map`.
        -- The first `rw` does nothingIsScalarTower.algebraMap_eq, ← eval₂_eq_eval_map, ← eval₂_eq_eval_map]
[GOAL]
case refine'_1.intro.intro
K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Field L'
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra K L'
S : IntermediateField K L
R : Type u_4
inst✝³ : CommRing R
inst✝² : Algebra R K
inst✝¹ : Algebra R L
inst✝ : IsScalarTower R K L
x : { x // x ∈ S }
P : R[X]
hPmo : Monic P
hProot : eval₂ (algebraMap R L) (↑x) P = 0
this : IsScalarTower R { x // x ∈ S } L := IsScalarTower.of_algebraMap_eq (congr_fun rfl)
⊢ eval₂ (algebraMap R L) (↑(algebraMap { x // x ∈ S } L) x) P = 0
[PROOFSTEP]
exact hProot
[GOAL]
case refine'_2
K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Field L'
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra K L'
S : IntermediateField K L
R : Type u_4
inst✝³ : CommRing R
inst✝² : Algebra R K
inst✝¹ : Algebra R L
inst✝ : IsScalarTower R K L
x : { x // x ∈ S }
h : IsIntegral R x
⊢ IsIntegral R ↑x
[PROOFSTEP]
obtain ⟨P, hPmo, hProot⟩ := h
[GOAL]
case refine'_2.intro.intro
K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Field L'
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra K L'
S : IntermediateField K L
R : Type u_4
inst✝³ : CommRing R
inst✝² : Algebra R K
inst✝¹ : Algebra R L
inst✝ : IsScalarTower R K L
x : { x // x ∈ S }
P : R[X]
hPmo : Monic P
hProot : eval₂ (algebraMap R { x // x ∈ S }) x P = 0
⊢ IsIntegral R ↑x
[PROOFSTEP]
refine' ⟨P, hPmo, _⟩
[GOAL]
case refine'_2.intro.intro
K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Field L'
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra K L'
S : IntermediateField K L
R : Type u_4
inst✝³ : CommRing R
inst✝² : Algebra R K
inst✝¹ : Algebra R L
inst✝ : IsScalarTower R K L
x : { x // x ∈ S }
P : R[X]
hPmo : Monic P
hProot : eval₂ (algebraMap R { x // x ∈ S }) x P = 0
⊢ eval₂ (algebraMap R L) (↑x) P = 0
[PROOFSTEP]
rw [← aeval_def, aeval_coe, aeval_def, hProot, ZeroMemClass.coe_zero]
[GOAL]
K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field L'
inst✝¹ : Algebra K L
inst✝ : Algebra K L'
S✝ S S' : IntermediateField K L
h : S.toSubalgebra = S'.toSubalgebra
⊢ S = S'
[PROOFSTEP]
ext
[GOAL]
case h
K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field L'
inst✝¹ : Algebra K L
inst✝ : Algebra K L'
S✝ S S' : IntermediateField K L
h : S.toSubalgebra = S'.toSubalgebra
x✝ : L
⊢ x✝ ∈ S ↔ x✝ ∈ S'
[PROOFSTEP]
rw [← mem_toSubalgebra, ← mem_toSubalgebra, h]
[GOAL]
K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field L'
inst✝¹ : Algebra K L
inst✝ : Algebra K L'
S : IntermediateField K L
x : L
hx : x ∈ RingHom.fieldRange (algebraMap K L)
⊢ x ∈ Set.range ↑(algebraMap K L)
[PROOFSTEP]
rwa [Set.mem_range, ← RingHom.mem_fieldRange]
[GOAL]
K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Field L'
inst✝³ : Algebra K L
inst✝² : Algebra K L'
S : IntermediateField K L
inst✝¹ : Algebra L' L
inst✝ : IsScalarTower K L' L
U V : IntermediateField L' L
H : restrictScalars K U = restrictScalars K V
x : L
⊢ x ∈ U ↔ x ∈ V
[PROOFSTEP]
rw [← mem_restrictScalars K, H, mem_restrictScalars]
[GOAL]
K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field L'
inst✝¹ : Algebra K L
inst✝ : Algebra K L'
S F : IntermediateField K L
E : IntermediateField { x // x ∈ F } L
⊢ Algebra K { x // x ∈ E }
[PROOFSTEP]
infer_instance
[GOAL]
K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field L'
inst✝¹ : Algebra K L
inst✝ : Algebra K L'
S F E : IntermediateField K L
⊢ F.toSubalgebra = E.toSubalgebra ↔ F = E
[PROOFSTEP]
rw [SetLike.ext_iff, SetLike.ext'_iff, Set.ext_iff]
[GOAL]
K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field L'
inst✝¹ : Algebra K L
inst✝ : Algebra K L'
S F E : IntermediateField K L
⊢ (∀ (x : L), x ∈ F.toSubalgebra ↔ x ∈ E.toSubalgebra) ↔ ∀ (x : L), x ∈ ↑F ↔ x ∈ ↑E
[PROOFSTEP]
rfl
[GOAL]
K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Field L'
inst✝² : Algebra K L
inst✝¹ : Algebra K L'
S F E : IntermediateField K L
inst✝ : FiniteDimensional K L
h_le : F ≤ E
h_finrank : finrank { x // x ∈ F } L ≤ finrank { x // x ∈ E } L
⊢ F = E
[PROOFSTEP]
apply eq_of_le_of_finrank_le h_le
[GOAL]
K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Field L'
inst✝² : Algebra K L
inst✝¹ : Algebra K L'
S F E : IntermediateField K L
inst✝ : FiniteDimensional K L
h_le : F ≤ E
h_finrank : finrank { x // x ∈ F } L ≤ finrank { x // x ∈ E } L
⊢ finrank K { x // x ∈ E } ≤ finrank K { x // x ∈ F }
[PROOFSTEP]
have h1 := finrank_mul_finrank K F L
[GOAL]
K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Field L'
inst✝² : Algebra K L
inst✝¹ : Algebra K L'
S F E : IntermediateField K L
inst✝ : FiniteDimensional K L
h_le : F ≤ E
h_finrank : finrank { x // x ∈ F } L ≤ finrank { x // x ∈ E } L
h1 : finrank K { x // x ∈ F } * finrank { x // x ∈ F } L = finrank K L
⊢ finrank K { x // x ∈ E } ≤ finrank K { x // x ∈ F }
[PROOFSTEP]
have h2 := finrank_mul_finrank K E L
[GOAL]
K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Field L'
inst✝² : Algebra K L
inst✝¹ : Algebra K L'
S F E : IntermediateField K L
inst✝ : FiniteDimensional K L
h_le : F ≤ E
h_finrank : finrank { x // x ∈ F } L ≤ finrank { x // x ∈ E } L
h1 : finrank K { x // x ∈ F } * finrank { x // x ∈ F } L = finrank K L
h2 : finrank K { x // x ∈ E } * finrank { x // x ∈ E } L = finrank K L
⊢ finrank K { x // x ∈ E } ≤ finrank K { x // x ∈ F }
[PROOFSTEP]
have h3 : 0 < finrank E L := finrank_pos
[GOAL]
K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Field L'
inst✝² : Algebra K L
inst✝¹ : Algebra K L'
S F E : IntermediateField K L
inst✝ : FiniteDimensional K L
h_le : F ≤ E
h_finrank : finrank { x // x ∈ F } L ≤ finrank { x // x ∈ E } L
h1 : finrank K { x // x ∈ F } * finrank { x // x ∈ F } L = finrank K L
h2 : finrank K { x // x ∈ E } * finrank { x // x ∈ E } L = finrank K L
h3 : 0 < finrank { x // x ∈ E } L
⊢ finrank K { x // x ∈ E } ≤ finrank K { x // x ∈ F }
[PROOFSTEP]
nlinarith
[GOAL]
K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field L'
inst✝¹ : Algebra K L
inst✝ : Algebra K L'
S : IntermediateField K L
x : { x // x ∈ S }
⊢ IsIntegral K x ↔ IsIntegral K ↑x
[PROOFSTEP]
rw [← isAlgebraic_iff_isIntegral, isAlgebraic_iff, isAlgebraic_iff_isIntegral]
[GOAL]
K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field L'
inst✝¹ : Algebra K L
inst✝ : Algebra K L'
S : IntermediateField K L
x : { x // x ∈ S }
⊢ minpoly K x = minpoly K ↑x
[PROOFSTEP]
by_cases hx : IsIntegral K x
[GOAL]
case pos
K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field L'
inst✝¹ : Algebra K L
inst✝ : Algebra K L'
S : IntermediateField K L
x : { x // x ∈ S }
hx : IsIntegral K x
⊢ minpoly K x = minpoly K ↑x
[PROOFSTEP]
exact minpoly.eq_of_algebraMap_eq (algebraMap S L).injective hx rfl
[GOAL]
case neg
K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field L'
inst✝¹ : Algebra K L
inst✝ : Algebra K L'
S : IntermediateField K L
x : { x // x ∈ S }
hx : ¬IsIntegral K x
⊢ minpoly K x = minpoly K ↑x
[PROOFSTEP]
exact (minpoly.eq_zero hx).trans (minpoly.eq_zero (mt isIntegral_iff.mpr hx)).symm
