[GOAL]
A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
pnz : p ≠ 0
hp : ↑(Polynomial.aeval x) p = 0
⊢ ↑(Polynomial.aeval x) (p * ↑C (leadingCoeff p)⁻¹) = 0
[PROOFSTEP]
simp [hp]
[GOAL]
A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
pmonic : Monic p
hp : ↑(Polynomial.aeval x) p = 0
pmin : ∀ (q : A[X]), Monic q → ↑(Polynomial.aeval x) q = 0 → degree p ≤ degree q
⊢ p = minpoly A x
[PROOFSTEP]
have hx : IsIntegral A x := ⟨p, pmonic, hp⟩
[GOAL]
A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
pmonic : Monic p
hp : ↑(Polynomial.aeval x) p = 0
pmin : ∀ (q : A[X]), Monic q → ↑(Polynomial.aeval x) q = 0 → degree p ≤ degree q
hx : IsIntegral A x
⊢ p = minpoly A x
[PROOFSTEP]
symm
[GOAL]
A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
pmonic : Monic p
hp : ↑(Polynomial.aeval x) p = 0
pmin : ∀ (q : A[X]), Monic q → ↑(Polynomial.aeval x) q = 0 → degree p ≤ degree q
hx : IsIntegral A x
⊢ minpoly A x = p
[PROOFSTEP]
apply eq_of_sub_eq_zero
[GOAL]
case h
A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
pmonic : Monic p
hp : ↑(Polynomial.aeval x) p = 0
pmin : ∀ (q : A[X]), Monic q → ↑(Polynomial.aeval x) q = 0 → degree p ≤ degree q
hx : IsIntegral A x
⊢ minpoly A x - p = 0
[PROOFSTEP]
by_contra hnz
[GOAL]
case h
A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
pmonic : Monic p
hp : ↑(Polynomial.aeval x) p = 0
pmin : ∀ (q : A[X]), Monic q → ↑(Polynomial.aeval x) q = 0 → degree p ≤ degree q
hx : IsIntegral A x
hnz : ¬minpoly A x - p = 0
⊢ False
[PROOFSTEP]
have hd := degree_le_of_ne_zero A x hnz (by simp [hp])
[GOAL]
A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
pmonic : Monic p
hp : ↑(Polynomial.aeval x) p = 0
pmin : ∀ (q : A[X]), Monic q → ↑(Polynomial.aeval x) q = 0 → degree p ≤ degree q
hx : IsIntegral A x
hnz : ¬minpoly A x - p = 0
⊢ ↑(Polynomial.aeval x) (minpoly A x - p) = 0
[PROOFSTEP]
simp [hp]
[GOAL]
case h
A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
pmonic : Monic p
hp : ↑(Polynomial.aeval x) p = 0
pmin : ∀ (q : A[X]), Monic q → ↑(Polynomial.aeval x) q = 0 → degree p ≤ degree q
hx : IsIntegral A x
hnz : ¬minpoly A x - p = 0
hd : degree (minpoly A x) ≤ degree (minpoly A x - p)
⊢ False
[PROOFSTEP]
contrapose! hd
[GOAL]
case h
A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
pmonic : Monic p
hp : ↑(Polynomial.aeval x) p = 0
pmin : ∀ (q : A[X]), Monic q → ↑(Polynomial.aeval x) q = 0 → degree p ≤ degree q
hx : IsIntegral A x
hnz : ¬minpoly A x - p = 0
hd : ¬False
⊢ degree (minpoly A x - p) < degree (minpoly A x)
[PROOFSTEP]
apply degree_sub_lt _ (minpoly.ne_zero hx)
[GOAL]
case h
A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
pmonic : Monic p
hp : ↑(Polynomial.aeval x) p = 0
pmin : ∀ (q : A[X]), Monic q → ↑(Polynomial.aeval x) q = 0 → degree p ≤ degree q
hx : IsIntegral A x
hnz : ¬minpoly A x - p = 0
hd : ¬False
⊢ leadingCoeff (minpoly A x) = leadingCoeff p
[PROOFSTEP]
rw [(monic hx).leadingCoeff, pmonic.leadingCoeff]
[GOAL]
A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
pmonic : Monic p
hp : ↑(Polynomial.aeval x) p = 0
pmin : ∀ (q : A[X]), Monic q → ↑(Polynomial.aeval x) q = 0 → degree p ≤ degree q
hx : IsIntegral A x
hnz : ¬minpoly A x - p = 0
hd : ¬False
⊢ degree (minpoly A x) = degree p
[PROOFSTEP]
exact le_antisymm (min A x pmonic hp) (pmin (minpoly A x) (monic hx) (aeval A x))
[GOAL]
A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
hp : ↑(Polynomial.aeval x) p = 0
⊢ minpoly A x ∣ p
[PROOFSTEP]
by_cases hp0 : p = 0
[GOAL]
case pos
A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
hp : ↑(Polynomial.aeval x) p = 0
hp0 : p = 0
⊢ minpoly A x ∣ p
[PROOFSTEP]
simp only [hp0, dvd_zero]
[GOAL]
case neg
A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
hp : ↑(Polynomial.aeval x) p = 0
hp0 : ¬p = 0
⊢ minpoly A x ∣ p
[PROOFSTEP]
have hx : IsIntegral A x := by
  rw [← isAlgebraic_iff_isIntegral]
  exact ⟨p, hp0, hp⟩
[GOAL]
A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
hp : ↑(Polynomial.aeval x) p = 0
hp0 : ¬p = 0
⊢ IsIntegral A x
[PROOFSTEP]
rw [← isAlgebraic_iff_isIntegral]
[GOAL]
A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
hp : ↑(Polynomial.aeval x) p = 0
hp0 : ¬p = 0
⊢ IsAlgebraic A x
[PROOFSTEP]
exact ⟨p, hp0, hp⟩
[GOAL]
case neg
A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
hp : ↑(Polynomial.aeval x) p = 0
hp0 : ¬p = 0
hx : IsIntegral A x
⊢ minpoly A x ∣ p
[PROOFSTEP]
rw [← dvd_iff_modByMonic_eq_zero (monic hx)]
[GOAL]
case neg
A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
hp : ↑(Polynomial.aeval x) p = 0
hp0 : ¬p = 0
hx : IsIntegral A x
⊢ p %ₘ minpoly A x = 0
[PROOFSTEP]
by_contra hnz
[GOAL]
case neg
A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
hp : ↑(Polynomial.aeval x) p = 0
hp0 : ¬p = 0
hx : IsIntegral A x
hnz : ¬p %ₘ minpoly A x = 0
⊢ False
[PROOFSTEP]
have hd := degree_le_of_ne_zero A x hnz ((aeval_modByMonic_eq_self_of_root (monic hx) (aeval _ _)).trans hp)
[GOAL]
case neg
A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
hp : ↑(Polynomial.aeval x) p = 0
hp0 : ¬p = 0
hx : IsIntegral A x
hnz : ¬p %ₘ minpoly A x = 0
hd : degree (minpoly A x) ≤ degree (p %ₘ minpoly A x)
⊢ False
[PROOFSTEP]
contrapose! hd
[GOAL]
case neg
A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
hp : ↑(Polynomial.aeval x) p = 0
hp0 : ¬p = 0
hx : IsIntegral A x
hnz : ¬p %ₘ minpoly A x = 0
hd : ¬False
⊢ degree (p %ₘ minpoly A x) < degree (minpoly A x)
[PROOFSTEP]
exact degree_modByMonic_lt _ (monic hx)
[GOAL]
A✝ : Type u_1
B : Type u_2
inst✝⁹ : Field A✝
inst✝⁸ : Ring B
inst✝⁷ : Algebra A✝ B
x✝ : B
A : Type u_3
K : Type u_4
R : Type u_5
inst✝⁶ : CommRing A
inst✝⁵ : Field K
inst✝⁴ : CommRing R
inst✝³ : Algebra A K
inst✝² : Algebra A R
inst✝¹ : Algebra K R
inst✝ : IsScalarTower A K R
x : R
⊢ minpoly K x ∣ map (algebraMap A K) (minpoly A x)
[PROOFSTEP]
refine' minpoly.dvd K x _
[GOAL]
A✝ : Type u_1
B : Type u_2
inst✝⁹ : Field A✝
inst✝⁸ : Ring B
inst✝⁷ : Algebra A✝ B
x✝ : B
A : Type u_3
K : Type u_4
R : Type u_5
inst✝⁶ : CommRing A
inst✝⁵ : Field K
inst✝⁴ : CommRing R
inst✝³ : Algebra A K
inst✝² : Algebra A R
inst✝¹ : Algebra K R
inst✝ : IsScalarTower A K R
x : R
⊢ ↑(Polynomial.aeval x) (map (algebraMap A K) (minpoly A x)) = 0
[PROOFSTEP]
rw [aeval_map_algebraMap, minpoly.aeval]
[GOAL]
A : Type u_1
B : Type u_2
inst✝¹³ : Field A
inst✝¹² : Ring B
inst✝¹¹ : Algebra A B
x : B
R : Type u_3
S : Type u_4
K : Type u_5
L : Type u_6
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Field K
inst✝⁷ : CommRing L
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R K
inst✝⁴ : Algebra S L
inst✝³ : Algebra K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsScalarTower R S L
s : S
⊢ minpoly K (↑(algebraMap S L) s) ∣ map (algebraMap R K) (minpoly R s)
[PROOFSTEP]
apply minpoly.dvd K (algebraMap S L s)
[GOAL]
A : Type u_1
B : Type u_2
inst✝¹³ : Field A
inst✝¹² : Ring B
inst✝¹¹ : Algebra A B
x : B
R : Type u_3
S : Type u_4
K : Type u_5
L : Type u_6
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Field K
inst✝⁷ : CommRing L
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R K
inst✝⁴ : Algebra S L
inst✝³ : Algebra K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsScalarTower R S L
s : S
⊢ ↑(Polynomial.aeval (↑(algebraMap S L) s)) (map (algebraMap R K) (minpoly R s)) = 0
[PROOFSTEP]
rw [← map_aeval_eq_aeval_map, minpoly.aeval, map_zero]
[GOAL]
case h
A : Type u_1
B : Type u_2
inst✝¹³ : Field A
inst✝¹² : Ring B
inst✝¹¹ : Algebra A B
x : B
R : Type u_3
S : Type u_4
K : Type u_5
L : Type u_6
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Field K
inst✝⁷ : CommRing L
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R K
inst✝⁴ : Algebra S L
inst✝³ : Algebra K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsScalarTower R S L
s : S
⊢ RingHom.comp (algebraMap K ((fun x => L) s)) (algebraMap R K) = RingHom.comp (algebraMap S L) (algebraMap R S)
[PROOFSTEP]
rw [← IsScalarTower.algebraMap_eq, ← IsScalarTower.algebraMap_eq]
[GOAL]
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
p : A[X]
hp1 : Irreducible p
hp2 : ↑(Polynomial.aeval x) p = 0
⊢ p * ↑C (leadingCoeff p)⁻¹ = minpoly A x
[PROOFSTEP]
have : p.leadingCoeff ≠ 0 := leadingCoeff_ne_zero.mpr hp1.ne_zero
[GOAL]
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
p : A[X]
hp1 : Irreducible p
hp2 : ↑(Polynomial.aeval x) p = 0
this : leadingCoeff p ≠ 0
⊢ p * ↑C (leadingCoeff p)⁻¹ = minpoly A x
[PROOFSTEP]
apply eq_of_irreducible_of_monic
[GOAL]
case hp1
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
p : A[X]
hp1 : Irreducible p
hp2 : ↑(Polynomial.aeval x) p = 0
this : leadingCoeff p ≠ 0
⊢ Irreducible (p * ↑C (leadingCoeff p)⁻¹)
[PROOFSTEP]
exact
  Associated.irreducible
    ⟨⟨C p.leadingCoeff⁻¹, C p.leadingCoeff, by rwa [← C_mul, inv_mul_cancel, C_1], by
        rwa [← C_mul, mul_inv_cancel, C_1]⟩,
      rfl⟩
    hp1
[GOAL]
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
p : A[X]
hp1 : Irreducible p
hp2 : ↑(Polynomial.aeval x) p = 0
this : leadingCoeff p ≠ 0
⊢ ↑C (leadingCoeff p)⁻¹ * ↑C (leadingCoeff p) = 1
[PROOFSTEP]
rwa [← C_mul, inv_mul_cancel, C_1]
[GOAL]
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
p : A[X]
hp1 : Irreducible p
hp2 : ↑(Polynomial.aeval x) p = 0
this : leadingCoeff p ≠ 0
⊢ ↑C (leadingCoeff p) * ↑C (leadingCoeff p)⁻¹ = 1
[PROOFSTEP]
rwa [← C_mul, mul_inv_cancel, C_1]
[GOAL]
case hp2
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
p : A[X]
hp1 : Irreducible p
hp2 : ↑(Polynomial.aeval x) p = 0
this : leadingCoeff p ≠ 0
⊢ ↑(Polynomial.aeval x) (p * ↑C (leadingCoeff p)⁻¹) = 0
[PROOFSTEP]
rw [aeval_mul, hp2, zero_mul]
[GOAL]
case hp3
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
p : A[X]
hp1 : Irreducible p
hp2 : ↑(Polynomial.aeval x) p = 0
this : leadingCoeff p ≠ 0
⊢ Monic (p * ↑C (leadingCoeff p)⁻¹)
[PROOFSTEP]
rwa [Polynomial.Monic, leadingCoeff_mul, leadingCoeff_C, mul_inv_cancel]
[GOAL]
A : Type u_1
B : Type u_2
inst✝⁹ : Field A
inst✝⁸ : Ring B
inst✝⁷ : Algebra A B
x✝ : B
K : Type u_3
S : Type u_4
T : Type u_5
inst✝⁶ : Field K
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra K S
inst✝² : Algebra K T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower K S T
hST : Injective ↑(algebraMap S T)
x : S
y : T
hx : IsIntegral K x
h : y = ↑(algebraMap S T) x
⊢ ↑(Polynomial.aeval y) (minpoly K x) = 0
[PROOFSTEP]
rw [h, aeval_algebraMap_apply, minpoly.aeval, RingHom.map_zero]
[GOAL]
A : Type u_1
B✝ : Type u_2
inst✝⁴ : Field A
inst✝³ : Ring B✝
inst✝² : Algebra A B✝
x✝ : B✝
B : Type u_3
inst✝¹ : CommRing B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
a : A
⊢ minpoly A (x + ↑(algebraMap A B) a) = Polynomial.comp (minpoly A x) (X - ↑C a)
[PROOFSTEP]
refine' (minpoly.unique _ _ ((minpoly.monic hx).comp_X_sub_C _) _ fun q qmo hq => _).symm
[GOAL]
case refine'_1
A : Type u_1
B✝ : Type u_2
inst✝⁴ : Field A
inst✝³ : Ring B✝
inst✝² : Algebra A B✝
x✝ : B✝
B : Type u_3
inst✝¹ : CommRing B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
a : A
⊢ ↑(Polynomial.aeval (x + ↑(algebraMap A B) a)) (Polynomial.comp (minpoly A x) (X - ↑C a)) = 0
[PROOFSTEP]
simp [aeval_comp]
[GOAL]
case refine'_2
A : Type u_1
B✝ : Type u_2
inst✝⁴ : Field A
inst✝³ : Ring B✝
inst✝² : Algebra A B✝
x✝ : B✝
B : Type u_3
inst✝¹ : CommRing B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
a : A
q : A[X]
qmo : Monic q
hq : ↑(Polynomial.aeval (x + ↑(algebraMap A B) a)) q = 0
⊢ degree (Polynomial.comp (minpoly A x) (X - ↑C a)) ≤ degree q
[PROOFSTEP]
have : (Polynomial.aeval x) (q.comp (X + C a)) = 0 := by simpa [aeval_comp] using hq
[GOAL]
A : Type u_1
B✝ : Type u_2
inst✝⁴ : Field A
inst✝³ : Ring B✝
inst✝² : Algebra A B✝
x✝ : B✝
B : Type u_3
inst✝¹ : CommRing B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
a : A
q : A[X]
qmo : Monic q
hq : ↑(Polynomial.aeval (x + ↑(algebraMap A B) a)) q = 0
⊢ ↑(Polynomial.aeval x) (Polynomial.comp q (X + ↑C a)) = 0
[PROOFSTEP]
simpa [aeval_comp] using hq
[GOAL]
case refine'_2
A : Type u_1
B✝ : Type u_2
inst✝⁴ : Field A
inst✝³ : Ring B✝
inst✝² : Algebra A B✝
x✝ : B✝
B : Type u_3
inst✝¹ : CommRing B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
a : A
q : A[X]
qmo : Monic q
hq : ↑(Polynomial.aeval (x + ↑(algebraMap A B) a)) q = 0
this : ↑(Polynomial.aeval x) (Polynomial.comp q (X + ↑C a)) = 0
⊢ degree (Polynomial.comp (minpoly A x) (X - ↑C a)) ≤ degree q
[PROOFSTEP]
have H := minpoly.min A x (qmo.comp_X_add_C _) this
[GOAL]
case refine'_2
A : Type u_1
B✝ : Type u_2
inst✝⁴ : Field A
inst✝³ : Ring B✝
inst✝² : Algebra A B✝
x✝ : B✝
B : Type u_3
inst✝¹ : CommRing B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
a : A
q : A[X]
qmo : Monic q
hq : ↑(Polynomial.aeval (x + ↑(algebraMap A B) a)) q = 0
this : ↑(Polynomial.aeval x) (Polynomial.comp q (X + ↑C a)) = 0
H : degree (minpoly A x) ≤ degree (Polynomial.comp q (X + ↑C a))
⊢ degree (Polynomial.comp (minpoly A x) (X - ↑C a)) ≤ degree q
[PROOFSTEP]
rw [degree_eq_natDegree qmo.ne_zero, degree_eq_natDegree ((minpoly.monic hx).comp_X_sub_C _).ne_zero, natDegree_comp,
  natDegree_X_sub_C, mul_one]
[GOAL]
case refine'_2
A : Type u_1
B✝ : Type u_2
inst✝⁴ : Field A
inst✝³ : Ring B✝
inst✝² : Algebra A B✝
x✝ : B✝
B : Type u_3
inst✝¹ : CommRing B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
a : A
q : A[X]
qmo : Monic q
hq : ↑(Polynomial.aeval (x + ↑(algebraMap A B) a)) q = 0
this : ↑(Polynomial.aeval x) (Polynomial.comp q (X + ↑C a)) = 0
H : degree (minpoly A x) ≤ degree (Polynomial.comp q (X + ↑C a))
⊢ ↑(natDegree (minpoly A x)) ≤ ↑(natDegree q)
[PROOFSTEP]
rwa [degree_eq_natDegree (minpoly.ne_zero hx), degree_eq_natDegree (qmo.comp_X_add_C _).ne_zero, natDegree_comp,
  natDegree_X_add_C, mul_one] at H
[GOAL]
A : Type u_1
B✝ : Type u_2
inst✝⁴ : Field A
inst✝³ : Ring B✝
inst✝² : Algebra A B✝
x✝ : B✝
B : Type u_3
inst✝¹ : CommRing B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
a : A
⊢ minpoly A (x - ↑(algebraMap A B) a) = Polynomial.comp (minpoly A x) (X + ↑C a)
[PROOFSTEP]
simpa [sub_eq_add_neg] using add_algebraMap hx (-a)
[GOAL]
A : Type u_1
B : Type u_2
inst✝⁹ : Field A
inst✝⁸ : Ring B
inst✝⁷ : Algebra A B
x✝ : B
F : Type u_3
E : Type u_4
K : Type u_5
inst✝⁶ : Field F
inst✝⁵ : Ring E
inst✝⁴ : CommRing K
inst✝³ : IsDomain K
inst✝² : Algebra F E
inst✝¹ : Algebra F K
inst✝ : FiniteDimensional F E
φ : E →ₐ[F] K
x : ↑(range ↑(FiniteDimensional.finBasis F E))
⊢ ↑φ ↑x ∈ roots (map (algebraMap F K) (minpoly F ↑x))
[PROOFSTEP]
rw [mem_roots_map (minpoly.ne_zero_of_finite F x.val), ← aeval_def, aeval_algHom_apply, minpoly.aeval, map_zero]
[GOAL]
A : Type u_1
B : Type u_2
inst✝⁹ : Field A
inst✝⁸ : Ring B
inst✝⁷ : Algebra A B
x : B
F : Type u_3
E : Type u_4
K : Type u_5
inst✝⁶ : Field F
inst✝⁵ : Ring E
inst✝⁴ : CommRing K
inst✝³ : IsDomain K
inst✝² : Algebra F E
inst✝¹ : Algebra F K
inst✝ : FiniteDimensional F E
⊢ Injective (rootsOfMinPolyPiType F E K)
[PROOFSTEP]
intro f g h
[GOAL]
A : Type u_1
B : Type u_2
inst✝⁹ : Field A
inst✝⁸ : Ring B
inst✝⁷ : Algebra A B
x : B
F : Type u_3
E : Type u_4
K : Type u_5
inst✝⁶ : Field F
inst✝⁵ : Ring E
inst✝⁴ : CommRing K
inst✝³ : IsDomain K
inst✝² : Algebra F E
inst✝¹ : Algebra F K
inst✝ : FiniteDimensional F E
f g : E →ₐ[F] K
h : rootsOfMinPolyPiType F E K f = rootsOfMinPolyPiType F E K g
⊢ f = g
[PROOFSTEP]
suffices (f : E →ₗ[F] K) = g by rwa [FunLike.ext'_iff] at this ⊢
[GOAL]
A : Type u_1
B : Type u_2
inst✝⁹ : Field A
inst✝⁸ : Ring B
inst✝⁷ : Algebra A B
x : B
F : Type u_3
E : Type u_4
K : Type u_5
inst✝⁶ : Field F
inst✝⁵ : Ring E
inst✝⁴ : CommRing K
inst✝³ : IsDomain K
inst✝² : Algebra F E
inst✝¹ : Algebra F K
inst✝ : FiniteDimensional F E
f g : E →ₐ[F] K
h : rootsOfMinPolyPiType F E K f = rootsOfMinPolyPiType F E K g
this : ↑↑f = ↑↑g
⊢ f = g
[PROOFSTEP]
rwa [FunLike.ext'_iff] at this ⊢
[GOAL]
A : Type u_1
B : Type u_2
inst✝⁹ : Field A
inst✝⁸ : Ring B
inst✝⁷ : Algebra A B
x : B
F : Type u_3
E : Type u_4
K : Type u_5
inst✝⁶ : Field F
inst✝⁵ : Ring E
inst✝⁴ : CommRing K
inst✝³ : IsDomain K
inst✝² : Algebra F E
inst✝¹ : Algebra F K
inst✝ : FiniteDimensional F E
f g : E →ₐ[F] K
h : rootsOfMinPolyPiType F E K f = rootsOfMinPolyPiType F E K g
⊢ ↑↑f = ↑↑g
[PROOFSTEP]
rw [funext_iff] at h
[GOAL]
A : Type u_1
B : Type u_2
inst✝⁹ : Field A
inst✝⁸ : Ring B
inst✝⁷ : Algebra A B
x : B
F : Type u_3
E : Type u_4
K : Type u_5
inst✝⁶ : Field F
inst✝⁵ : Ring E
inst✝⁴ : CommRing K
inst✝³ : IsDomain K
inst✝² : Algebra F E
inst✝¹ : Algebra F K
inst✝ : FiniteDimensional F E
f g : E →ₐ[F] K
h : ∀ (a : ↑(range ↑(FiniteDimensional.finBasis F E))), rootsOfMinPolyPiType F E K f a = rootsOfMinPolyPiType F E K g a
⊢ ↑↑f = ↑↑g
[PROOFSTEP]
exact LinearMap.ext_on (FiniteDimensional.finBasis F E).span_eq fun e he => Subtype.ext_iff.mp (h ⟨e, he⟩)
[GOAL]
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
⊢ minpoly A 0 = X
[PROOFSTEP]
simpa only [add_zero, C_0, sub_eq_add_neg, neg_zero, RingHom.map_zero] using eq_X_sub_C B (0 : A)
[GOAL]
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
⊢ minpoly A 1 = X - 1
[PROOFSTEP]
simpa only [RingHom.map_one, C_1, sub_eq_add_neg] using eq_X_sub_C B (1 : A)
[GOAL]
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : IsDomain B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
⊢ Prime (minpoly A x)
[PROOFSTEP]
refine' ⟨minpoly.ne_zero hx, not_isUnit A x, _⟩
[GOAL]
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : IsDomain B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
⊢ ∀ (a b : A[X]), minpoly A x ∣ a * b → minpoly A x ∣ a ∨ minpoly A x ∣ b
[PROOFSTEP]
rintro p q ⟨d, h⟩
[GOAL]
case intro
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : IsDomain B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
p q d : A[X]
h : p * q = minpoly A x * d
⊢ minpoly A x ∣ p ∨ minpoly A x ∣ q
[PROOFSTEP]
have : Polynomial.aeval x (p * q) = 0 := by simp [h, aeval A x]
[GOAL]
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : IsDomain B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
p q d : A[X]
h : p * q = minpoly A x * d
⊢ ↑(Polynomial.aeval x) (p * q) = 0
[PROOFSTEP]
simp [h, aeval A x]
[GOAL]
case intro
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : IsDomain B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
p q d : A[X]
h : p * q = minpoly A x * d
this : ↑(Polynomial.aeval x) (p * q) = 0
⊢ minpoly A x ∣ p ∨ minpoly A x ∣ q
[PROOFSTEP]
replace : Polynomial.aeval x p = 0 ∨ Polynomial.aeval x q = 0 := by simpa
[GOAL]
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : IsDomain B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
p q d : A[X]
h : p * q = minpoly A x * d
this : ↑(Polynomial.aeval x) (p * q) = 0
⊢ ↑(Polynomial.aeval x) p = 0 ∨ ↑(Polynomial.aeval x) q = 0
[PROOFSTEP]
simpa
[GOAL]
case intro
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : IsDomain B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
p q d : A[X]
h : p * q = minpoly A x * d
this : ↑(Polynomial.aeval x) p = 0 ∨ ↑(Polynomial.aeval x) q = 0
⊢ minpoly A x ∣ p ∨ minpoly A x ∣ q
[PROOFSTEP]
exact Or.imp (dvd A x) (dvd A x) this
[GOAL]
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : IsDomain B
inst✝ : Algebra A B
x✝ x : B
hx : IsIntegral A x
y : A
h : IsRoot (minpoly A x) y
⊢ ↑(algebraMap A B) y = x
[PROOFSTEP]
have key : minpoly A x = X - C y :=
  eq_of_monic_of_associated (monic hx) (monic_X_sub_C y)
    (associated_of_dvd_dvd ((irreducible_X_sub_C y).dvd_symm (irreducible hx) (dvd_iff_isRoot.2 h))
      (dvd_iff_isRoot.2 h))
[GOAL]
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : IsDomain B
inst✝ : Algebra A B
x✝ x : B
hx : IsIntegral A x
y : A
h : IsRoot (minpoly A x) y
key : minpoly A x = X - ↑C y
⊢ ↑(algebraMap A B) y = x
[PROOFSTEP]
have := aeval A x
[GOAL]
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : IsDomain B
inst✝ : Algebra A B
x✝ x : B
hx : IsIntegral A x
y : A
h : IsRoot (minpoly A x) y
key : minpoly A x = X - ↑C y
this : ↑(Polynomial.aeval x) (minpoly A x) = 0
⊢ ↑(algebraMap A B) y = x
[PROOFSTEP]
rwa [key, AlgHom.map_sub, aeval_X, aeval_C, sub_eq_zero, eq_comm] at this
[GOAL]
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : IsDomain B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
⊢ coeff (minpoly A x) 0 = 0 ↔ x = 0
[PROOFSTEP]
constructor
[GOAL]
case mp
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : IsDomain B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
⊢ coeff (minpoly A x) 0 = 0 → x = 0
[PROOFSTEP]
intro h
[GOAL]
case mp
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : IsDomain B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
h : coeff (minpoly A x) 0 = 0
⊢ x = 0
[PROOFSTEP]
have zero_root := zero_isRoot_of_coeff_zero_eq_zero h
[GOAL]
case mp
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : IsDomain B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
h : coeff (minpoly A x) 0 = 0
zero_root : IsRoot (minpoly A x) 0
⊢ x = 0
[PROOFSTEP]
rw [← root hx zero_root]
[GOAL]
case mp
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : IsDomain B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
h : coeff (minpoly A x) 0 = 0
zero_root : IsRoot (minpoly A x) 0
⊢ ↑(algebraMap A B) 0 = 0
[PROOFSTEP]
exact RingHom.map_zero _
[GOAL]
case mpr
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : IsDomain B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
⊢ x = 0 → coeff (minpoly A x) 0 = 0
[PROOFSTEP]
rintro rfl
[GOAL]
case mpr
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : IsDomain B
inst✝ : Algebra A B
hx : IsIntegral A 0
⊢ coeff (minpoly A 0) 0 = 0
[PROOFSTEP]
simp
[GOAL]
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : IsDomain B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
h : x ≠ 0
⊢ coeff (minpoly A x) 0 ≠ 0
[PROOFSTEP]
contrapose! h
[GOAL]
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : IsDomain B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
h : coeff (minpoly A x) 0 = 0
⊢ x = 0
[PROOFSTEP]
simpa only [hx, coeff_zero_eq_zero] using 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
⊢ 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


[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
⊢ inv (inv r) = r
[PROOFSTEP]
ext x y
[GOAL]
case a.h.a
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
x : α
y : β
⊢ inv (inv r) x y ↔ r x y
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
⊢ codom (inv r) = dom r
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
x : α
⊢ x ∈ codom (inv r) ↔ x ∈ dom r
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
⊢ dom (inv r) = codom r
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
x : β
⊢ x ∈ dom (inv r) ↔ x ∈ codom r
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ : Rel α β
δ : Type u_4
r : Rel α β
s : Rel β γ
t : Rel γ δ
⊢ (r • s) • t = r • s • t
[PROOFSTEP]
unfold comp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ : Rel α β
δ : Type u_4
r : Rel α β
s : Rel β γ
t : Rel γ δ
⊢ (fun x z => ∃ y, (∃ y_1, r x y_1 ∧ s y_1 y) ∧ t y z) = fun x z => ∃ y, r x y ∧ ∃ y_1, s y y_1 ∧ t y_1 z
[PROOFSTEP]
ext (x w)
[GOAL]
case a.h.a
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ : Rel α β
δ : Type u_4
r : Rel α β
s : Rel β γ
t : Rel γ δ
x : α
w : δ
⊢ (∃ y, (∃ y_1, r x y_1 ∧ s y_1 y) ∧ t y w) ↔ ∃ y, r x y ∧ ∃ y_1, s y y_1 ∧ t y_1 w
[PROOFSTEP]
constructor
[GOAL]
case a.h.a.mp
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ : Rel α β
δ : Type u_4
r : Rel α β
s : Rel β γ
t : Rel γ δ
x : α
w : δ
⊢ (∃ y, (∃ y_1, r x y_1 ∧ s y_1 y) ∧ t y w) → ∃ y, r x y ∧ ∃ y_1, s y y_1 ∧ t y_1 w
[PROOFSTEP]
rintro ⟨z, ⟨y, rxy, syz⟩, tzw⟩
[GOAL]
case a.h.a.mp.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ : Rel α β
δ : Type u_4
r : Rel α β
s : Rel β γ
t : Rel γ δ
x : α
w : δ
z : γ
tzw : t z w
y : β
rxy : r x y
syz : s y z
⊢ ∃ y, r x y ∧ ∃ y_1, s y y_1 ∧ t y_1 w
[PROOFSTEP]
exact ⟨y, rxy, z, syz, tzw⟩
[GOAL]
case a.h.a.mpr
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ : Rel α β
δ : Type u_4
r : Rel α β
s : Rel β γ
t : Rel γ δ
x : α
w : δ
⊢ (∃ y, r x y ∧ ∃ y_1, s y y_1 ∧ t y_1 w) → ∃ y, (∃ y_1, r x y_1 ∧ s y_1 y) ∧ t y w
[PROOFSTEP]
rintro ⟨y, rxy, z, syz, tzw⟩
[GOAL]
case a.h.a.mpr.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ : Rel α β
δ : Type u_4
r : Rel α β
s : Rel β γ
t : Rel γ δ
x : α
w : δ
y : β
rxy : r x y
z : γ
syz : s y z
tzw : t z w
⊢ ∃ y, (∃ y_1, r x y_1 ∧ s y_1 y) ∧ t y w
[PROOFSTEP]
exact ⟨z, ⟨y, rxy, syz⟩, tzw⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ r : Rel α β
⊢ r • Eq = r
[PROOFSTEP]
unfold comp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ r : Rel α β
⊢ (fun x z => ∃ y, r x y ∧ y = z) = r
[PROOFSTEP]
ext y
[GOAL]
case a.h.a
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ r : Rel α β
y : α
x✝ : β
⊢ (∃ y_1, r y y_1 ∧ y_1 = x✝) ↔ r y x✝
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ r : Rel α β
⊢ Eq • r = r
[PROOFSTEP]
unfold comp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ r : Rel α β
⊢ (fun x z => ∃ y, x = y ∧ r y z) = r
[PROOFSTEP]
ext x
[GOAL]
case a.h.a
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ r : Rel α β
x : α
x✝ : β
⊢ (∃ y, x = y ∧ r y x✝) ↔ r x x✝
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
⊢ inv Eq = Eq
[PROOFSTEP]
ext x y
[GOAL]
case a.h.a
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
x y : α
⊢ inv Eq x y ↔ x = y
[PROOFSTEP]
constructor
[GOAL]
case a.h.a.mp
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
x y : α
⊢ inv Eq x y → x = y
[PROOFSTEP]
apply Eq.symm
[GOAL]
case a.h.a.mpr
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
x y : α
⊢ x = y → inv Eq x y
[PROOFSTEP]
apply Eq.symm
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ r : Rel α β
s : Rel β γ
⊢ inv (r • s) = inv s • inv r
[PROOFSTEP]
ext x z
[GOAL]
case a.h.a
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ r : Rel α β
s : Rel β γ
x : γ
z : α
⊢ inv (r • s) x z ↔ (inv s • inv r) x z
[PROOFSTEP]
simp [comp, inv, flip, and_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
s : Set α
⊢ image Eq s = s
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
s : Set α
x : α
⊢ x ∈ image Eq s ↔ x ∈ s
[PROOFSTEP]
simp [mem_image]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
s : Rel β γ
t : Set α
⊢ image (r • s) t = image s (image r t)
[PROOFSTEP]
ext z
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
s : Rel β γ
t : Set α
z : γ
⊢ z ∈ image (r • s) t ↔ z ∈ image s (image r t)
[PROOFSTEP]
simp only [mem_image]
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
s : Rel β γ
t : Set α
z : γ
⊢ (∃ x, x ∈ t ∧ (r • s) x z) ↔ ∃ x, (∃ x_1, x_1 ∈ t ∧ r x_1 x) ∧ s x z
[PROOFSTEP]
constructor
[GOAL]
case h.mp
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
s : Rel β γ
t : Set α
z : γ
⊢ (∃ x, x ∈ t ∧ (r • s) x z) → ∃ x, (∃ x_1, x_1 ∈ t ∧ r x_1 x) ∧ s x z
[PROOFSTEP]
rintro ⟨x, xt, y, rxy, syz⟩
[GOAL]
case h.mp.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
s : Rel β γ
t : Set α
z : γ
x : α
xt : x ∈ t
y : β
rxy : r x y
syz : s y z
⊢ ∃ x, (∃ x_1, x_1 ∈ t ∧ r x_1 x) ∧ s x z
[PROOFSTEP]
exact ⟨y, ⟨x, xt, rxy⟩, syz⟩
[GOAL]
case h.mpr
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
s : Rel β γ
t : Set α
z : γ
⊢ (∃ x, (∃ x_1, x_1 ∈ t ∧ r x_1 x) ∧ s x z) → ∃ x, x ∈ t ∧ (r • s) x z
[PROOFSTEP]
rintro ⟨y, ⟨x, xt, rxy⟩, syz⟩
[GOAL]
case h.mpr.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
s : Rel β γ
t : Set α
z : γ
y : β
syz : s y z
x : α
xt : x ∈ t
rxy : r x y
⊢ ∃ x, x ∈ t ∧ (r • s) x z
[PROOFSTEP]
exact ⟨x, xt, y, rxy, syz⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
⊢ image r Set.univ = codom r
[PROOFSTEP]
ext y
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
y : β
⊢ y ∈ image r Set.univ ↔ y ∈ codom r
[PROOFSTEP]
simp [mem_image, codom]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
s : Set α
⊢ preimage Eq s = s
[PROOFSTEP]
simp only [preimage, inv_id, image_id]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
s : Rel β γ
t : Set γ
⊢ preimage (r • s) t = preimage r (preimage s t)
[PROOFSTEP]
simp only [preimage, inv_comp, image_comp]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
⊢ preimage r Set.univ = dom r
[PROOFSTEP]
rw [preimage, image_univ, codom_inv]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
s t : Set β
⊢ ∀ (x : α), x ∈ core r (s ∩ t) ↔ x ∈ core r s ∩ core r t
[PROOFSTEP]
simp [mem_core, imp_and, forall_and]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
⊢ ∀ (x : α), x ∈ core r Set.univ ↔ x ∈ Set.univ
[PROOFSTEP]
simp [mem_core]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
s : Set α
⊢ core Eq s = s
[PROOFSTEP]
simp [core]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
s : Rel β γ
t : Set γ
⊢ core (r • s) t = core r (core s t)
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
s : Rel β γ
t : Set γ
x : α
⊢ x ∈ core (r • s) t ↔ x ∈ core r (core s t)
[PROOFSTEP]
simp [core, comp]
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
s : Rel β γ
t : Set γ
x : α
⊢ (∀ (y : γ) (x_1 : β), r x x_1 → s x_1 y → y ∈ t) ↔ ∀ (y : β), r x y → ∀ (y_1 : γ), s y y_1 → y_1 ∈ t
[PROOFSTEP]
constructor
[GOAL]
case h.mp
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
s : Rel β γ
t : Set γ
x : α
⊢ (∀ (y : γ) (x_1 : β), r x x_1 → s x_1 y → y ∈ t) → ∀ (y : β), r x y → ∀ (y_1 : γ), s y y_1 → y_1 ∈ t
[PROOFSTEP]
exact fun h y rxy z => h z y rxy
[GOAL]
case h.mpr
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
s : Rel β γ
t : Set γ
x : α
⊢ (∀ (y : β), r x y → ∀ (y_1 : γ), s y y_1 → y_1 ∈ t) → ∀ (y : γ) (x_1 : β), r x x_1 → s x_1 y → y ∈ t
[PROOFSTEP]
exact fun h z y rzy => h y rzy z
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
s : Set α
⊢ f '' s = Rel.image (Function.graph f) s
[PROOFSTEP]
simp [Set.image, Function.graph, Rel.image]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
s : Set β
⊢ f ⁻¹' s = Rel.preimage (Function.graph f) s
[PROOFSTEP]
simp [Set.preimage, Function.graph, Rel.preimage, Rel.inv, flip, Rel.image]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
s : Set β
⊢ f ⁻¹' s = Rel.core (Function.graph f) s
[PROOFSTEP]
simp [Set.preimage, Function.graph, Rel.core]