mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

Goal state before:
pp: F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
α : E
K : Type u
inst✝¹ : Field K
inst✝ : Algebra F K
h : IsIntegral F α
f : AdjoinRoot (minpoly F α) →+* ↥F⟮α⟯ := AdjoinRoot.lift (↑(Algebra.ofId F ↥F⟮α⟯)) (AdjoinSimple.gen F α) ⋯
⊢ Function.Bijective ⇑(AdjoinRoot.liftAlgHom (minpoly F α) (Algebra.ofId F ↥F⟮α⟯) (AdjoinSimple.gen F α) ⋯)

Tactic:
have := Fact.mk (minpoly.irreducible h)

Goal state after:
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
α : E
K : Type u
inst✝¹ : Field K
inst✝ : Algebra F K
h : IsIntegral F α
f : AdjoinRoot (minpoly F α) →+* ↥F⟮α⟯ := AdjoinRoot.lift (↑(Algebra.ofId F ↥F⟮α⟯)) (AdjoinSimple.gen F α) ⋯
this : Fact (Irreducible (minpoly F α))
⊢ Function.Bijective ⇑(AdjoinRoot.liftAlgHom (minpoly F α) (Algebra.ofId F ↥F⟮α⟯) (AdjoinSimple.gen F α) ⋯)
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

Goal state before:
pp: case left
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
α : E
K : Type u
inst✝¹ : Field K
inst✝ : Algebra F K
h : IsIntegral F α
f : AdjoinRoot (minpoly F α) →+* ↥F⟮α⟯ := ⋯
this : Fact (Irreducible (minpoly F α))
⊢ Function.Injective ⇑(AdjoinRoot.liftAlgHom (minpoly F α) (Algebra.ofId F ↥F⟮α⟯) (AdjoinSimple.gen F α) ⋯)

pp: case right
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
α : E
K : Type u
inst✝¹ : Field K
inst✝ : Algebra F K
h : IsIntegral F α
f : AdjoinRoot (minpoly F α) →+* ↥F⟮α⟯ := ⋯
this : Fact (Irreducible (minpoly F α))
⊢ Function.Surjective ⇑(AdjoinRoot.liftAlgHom (minpoly F α) (Algebra.ofId F ↥F⟮α⟯) (AdjoinSimple.gen F α) ⋯)

Tactic:
·

Goal state after:
case left
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
α : E
K : Type u
inst✝¹ : Field K
inst✝ : Algebra F K
h : IsIntegral F α
f : AdjoinRoot (minpoly F α) →+* ↥F⟮α⟯ := ⋯
this : Fact (Irreducible (minpoly F α))
⊢ Function.Injective ⇑(AdjoinRoot.liftAlgHom (minpoly F α) (Algebra.ofId F ↥F⟮α⟯) (AdjoinSimple.gen F α) ⋯)
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

Goal state before:
pp: case right
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
α : E
K : Type u
inst✝¹ : Field K
inst✝ : Algebra F K
h : IsIntegral F α
f : AdjoinRoot (minpoly F α) →+* ↥F⟮α⟯ := ⋯
this : Fact (Irreducible (minpoly F α))
⊢ Function.Surjective ⇑(AdjoinRoot.liftAlgHom (minpoly F α) (Algebra.ofId F ↥F⟮α⟯) (AdjoinSimple.gen F α) ⋯)

Tactic:
·

Goal state after:
case right
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
α : E
K : Type u
inst✝¹ : Field K
inst✝ : Algebra F K
h : IsIntegral F α
f : AdjoinRoot (minpoly F α) →+* ↥F⟮α⟯ := ⋯
this : Fact (Irreducible (minpoly F α))
⊢ Function.Surjective ⇑(AdjoinRoot.liftAlgHom (minpoly F α) (Algebra.ofId F ↥F⟮α⟯) (AdjoinSimple.gen F α) ⋯)
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

Goal state before:
pp: case right.refine_1
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
α : E
K : Type u
inst✝¹ : Field K
inst✝ : Algebra F K
h : IsIntegral F α
f : AdjoinRoot (minpoly F α) →+* ↥F⟮α⟯ := AdjoinRoot.lift (↑(Algebra.ofId F ↥F⟮α⟯)) (AdjoinSimple.gen F α) ⋯
this : Fact (Irreducible (minpoly F α))
x : E
hx : x ∈ Set.range ⇑(algebraMap F E)
⊢ x ∈ ↑(F⟮α⟯.toSubfield.subtype.comp f).fieldRange

pp: case right.refine_2
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
α : E
K : Type u
inst✝¹ : Field K
inst✝ : Algebra F K
h : IsIntegral F α
f : AdjoinRoot (minpoly F α) →+* ↥F⟮α⟯ := AdjoinRoot.lift (↑(Algebra.ofId F ↥F⟮α⟯)) (AdjoinSimple.gen F α) ⋯
this : Fact (Irreducible (minpoly F α))
⊢ {α} ⊆ ↑(F⟮α⟯.toSubfield.subtype.comp f).fieldRange

Tactic:
·

Goal state after:
case right.refine_1
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
α : E
K : Type u
inst✝¹ : Field K
inst✝ : Algebra F K
h : IsIntegral F α
f : AdjoinRoot (minpoly F α) →+* ↥F⟮α⟯ := AdjoinRoot.lift (↑(Algebra.ofId F ↥F⟮α⟯)) (AdjoinSimple.gen F α) ⋯
this : Fact (Irreducible (minpoly F α))
x : E
hx : x ∈ Set.range ⇑(algebraMap F E)
⊢ x ∈ ↑(F⟮α⟯.toSubfield.subtype.comp f).fieldRange
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

Goal state before:
pp: case right.refine_2
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
α : E
K : Type u
inst✝¹ : Field K
inst✝ : Algebra F K
h : IsIntegral F α
f : AdjoinRoot (minpoly F α) →+* ↥F⟮α⟯ := AdjoinRoot.lift (↑(Algebra.ofId F ↥F⟮α⟯)) (AdjoinSimple.gen F α) ⋯
this : Fact (Irreducible (minpoly F α))
⊢ {α} ⊆ ↑(F⟮α⟯.toSubfield.subtype.comp f).fieldRange

Tactic:
·

Goal state after:
case right.refine_2
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
α : E
K : Type u
inst✝¹ : Field K
inst✝ : Algebra F K
h : IsIntegral F α
f : AdjoinRoot (minpoly F α) →+* ↥F⟮α⟯ := AdjoinRoot.lift (↑(Algebra.ofId F ↥F⟮α⟯)) (AdjoinSimple.gen F α) ⋯
this : Fact (Irreducible (minpoly F α))
⊢ {α} ⊆ ↑(F⟮α⟯.toSubfield.subtype.comp f).fieldRange
Module: Mathlib.FieldTheory.Extension

Goal state before:
pp: case refine_2
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
S : Set E
L : IntermediateField F E
f : ↥L →ₐ[F] K
hK : ∀ s ∈ S, IsIntegral (↥L) s ∧ (Polynomial.map f.toRingHom (minpoly (↥L) s)).Splits
φ : Lifts F E K
hfφ : { carrier := L, emb := f } ≤ φ
hφ : IsMax φ
s : E
h : s ∈ S
this✝² : Algebra ↥{ carrier := L, emb := f }.carrier ↥φ.carrier := (inclusion ⋯).toAlgebra
this✝¹ : SMul ↥L ↥φ.carrier := this✝².toSMul
this✝ : IsScalarTower (↥L) (↥φ.carrier) E
this : ∃ y, φ ≤ y ∧ s ∈ y.carrier
⊢ s ∈ ↑(extendScalars ⋯)

pp: case refine_1
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
S : Set E
L : IntermediateField F E
f : ↥L →ₐ[F] K
hK : ∀ s ∈ S, IsIntegral (↥L) s ∧ (Polynomial.map f.toRingHom (minpoly (↥L) s)).Splits
φ : Lifts F E K
hfφ : { carrier := L, emb := f } ≤ φ
hφ : IsMax φ
s : E
h : s ∈ S
this✝¹ : Algebra ↥{ carrier := L, emb := f }.carrier ↥φ.carrier := (inclusion ⋯).toAlgebra
this✝ : SMul ↥L ↥φ.carrier := this✝¹.toSMul
this : IsScalarTower (↥L) (↥φ.carrier) E
⊢ (Polynomial.map (φ.emb.comp (algebraMap ↥L ↥φ.carrier)) (minpoly (↥L) s)).Splits

Tactic:
·

Goal state after:
case refine_2
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
S : Set E
L : IntermediateField F E
f : ↥L →ₐ[F] K
hK : ∀ s ∈ S, IsIntegral (↥L) s ∧ (Polynomial.map f.toRingHom (minpoly (↥L) s)).Splits
φ : Lifts F E K
hfφ : { carrier := L, emb := f } ≤ φ
hφ : IsMax φ
s : E
h : s ∈ S
this✝² : Algebra ↥{ carrier := L, emb := f }.carrier ↥φ.carrier := (inclusion ⋯).toAlgebra
this✝¹ : SMul ↥L ↥φ.carrier := this✝².toSMul
this✝ : IsScalarTower (↥L) (↥φ.carrier) E
this : ∃ y, φ ≤ y ∧ s ∈ y.carrier
⊢ s ∈ ↑(extendScalars ⋯)
Module: Mathlib.FieldTheory.Extension

Goal state before:
pp: case refine_1
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
S : Set E
L : IntermediateField F E
f : ↥L →ₐ[F] K
hK : ∀ s ∈ S, IsIntegral (↥L) s ∧ (Polynomial.map f.toRingHom (minpoly (↥L) s)).Splits
φ : Lifts F E K
hfφ : { carrier := L, emb := f } ≤ φ
hφ : IsMax φ
s : E
h : s ∈ S
this✝¹ : Algebra ↥{ carrier := L, emb := f }.carrier ↥φ.carrier := (inclusion ⋯).toAlgebra
this✝ : SMul ↥L ↥φ.carrier := this✝¹.toSMul
this : IsScalarTower (↥L) (↥φ.carrier) E
⊢ (Polynomial.map (φ.emb.comp (algebraMap ↥L ↥φ.carrier)) (minpoly (↥L) s)).Splits

Tactic:
·

Goal state after:
case refine_1
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
S : Set E
L : IntermediateField F E
f : ↥L →ₐ[F] K
hK : ∀ s ∈ S, IsIntegral (↥L) s ∧ (Polynomial.map f.toRingHom (minpoly (↥L) s)).Splits
φ : Lifts F E K
hfφ : { carrier := L, emb := f } ≤ φ
hφ : IsMax φ
s : E
h : s ∈ S
this✝¹ : Algebra ↥{ carrier := L, emb := f }.carrier ↥φ.carrier := (inclusion ⋯).toAlgebra
this✝ : SMul ↥L ↥φ.carrier := this✝¹.toSMul
this : IsScalarTower (↥L) (↥φ.carrier) E
⊢ (Polynomial.map (φ.emb.comp (algebraMap ↥L ↥φ.carrier)) (minpoly (↥L) s)).Splits
Module: Mathlib.FieldTheory.Extension

Goal state before:
pp: case refine_2
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁸ : Field F
inst✝⁷ : Field E
inst✝⁶ : Field K
inst✝⁵ : Algebra F E
inst✝⁴ : Algebra F K
S : Set E
L : Type u_4
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra L E
inst✝ : IsScalarTower F L E
f : L →ₐ[F] K
hK : ∀ s ∈ S, IsIntegral L s ∧ (Polynomial.map f.toRingHom (minpoly L s)).Splits
L' : IntermediateField F E := (IsScalarTower.toAlgHom F L E).fieldRange
f' : ↥L' →ₐ[F] K := f.comp ↑(AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)).symm
this : ∃ φ, AlgHom.domRestrict (↥L') φ = f'
⊢ ∃ φ, AlgHom.domRestrict L φ = f

pp: case refine_1
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁸ : Field F
inst✝⁷ : Field E
inst✝⁶ : Field K
inst✝⁵ : Algebra F E
inst✝⁴ : Algebra F K
S : Set E
L : Type u_4
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra L E
inst✝ : IsScalarTower F L E
f : L →ₐ[F] K
hK : ∀ s ∈ S, IsIntegral L s ∧ (Polynomial.map f.toRingHom (minpoly L s)).Splits
L' : IntermediateField F E := (IsScalarTower.toAlgHom F L E).fieldRange
f' : ↥L' →ₐ[F] K := f.comp ↑(AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)).symm
s : E
hs : s ∈ S
⊢ IsIntegral (↥L') s ∧ (Polynomial.map f'.toRingHom (minpoly (↥L') s)).Splits

Tactic:
·

Goal state after:
case refine_2
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁸ : Field F
inst✝⁷ : Field E
inst✝⁶ : Field K
inst✝⁵ : Algebra F E
inst✝⁴ : Algebra F K
S : Set E
L : Type u_4
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra L E
inst✝ : IsScalarTower F L E
f : L →ₐ[F] K
hK : ∀ s ∈ S, IsIntegral L s ∧ (Polynomial.map f.toRingHom (minpoly L s)).Splits
L' : IntermediateField F E := (IsScalarTower.toAlgHom F L E).fieldRange
f' : ↥L' →ₐ[F] K := f.comp ↑(AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)).symm
this : ∃ φ, AlgHom.domRestrict (↥L') φ = f'
⊢ ∃ φ, AlgHom.domRestrict L φ = f
Module: Mathlib.FieldTheory.Extension

Goal state before:
pp: case refine_2.refine_1
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁸ : Field F
inst✝⁷ : Field E
inst✝⁶ : Field K
inst✝⁵ : Algebra F E
inst✝⁴ : Algebra F K
S : Set E
L : Type u_4
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra L E
inst✝ : IsScalarTower F L E
f : L →ₐ[F] K
hK : ∀ s ∈ S, IsIntegral L s ∧ (Polynomial.map f.toRingHom (minpoly L s)).Splits
L' : IntermediateField F E := (IsScalarTower.toAlgHom F L E).fieldRange
f' : ↥L' →ₐ[F] K := f.comp ↑(AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)).symm
φ : ↥(adjoin (↥L') S) →ₐ[F] K
hφ : AlgHom.domRestrict (↥L') φ = f'
⊢ restrictScalars F (adjoin L S) ≤ restrictScalars F (adjoin (↥L') S)

pp: case refine_2.refine_2
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁸ : Field F
inst✝⁷ : Field E
inst✝⁶ : Field K
inst✝⁵ : Algebra F E
inst✝⁴ : Algebra F K
S : Set E
L : Type u_4
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra L E
inst✝ : IsScalarTower F L E
f : L →ₐ[F] K
hK : ∀ s ∈ S, IsIntegral L s ∧ (Polynomial.map f.toRingHom (minpoly L s)).Splits
L' : IntermediateField F E := (IsScalarTower.toAlgHom F L E).fieldRange
f' : ↥L' →ₐ[F] K := f.comp ↑(AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)).symm
φ : ↥(adjoin (↥L') S) →ₐ[F] K
hφ : AlgHom.domRestrict (↥L') φ = f'
⊢ AlgHom.domRestrict L (φ.comp (inclusion ?refine_2.refine_1)) = f

Tactic:
·

Goal state after:
case refine_2.refine_1
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁸ : Field F
inst✝⁷ : Field E
inst✝⁶ : Field K
inst✝⁵ : Algebra F E
inst✝⁴ : Algebra F K
S : Set E
L : Type u_4
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra L E
inst✝ : IsScalarTower F L E
f : L →ₐ[F] K
hK : ∀ s ∈ S, IsIntegral L s ∧ (Polynomial.map f.toRingHom (minpoly L s)).Splits
L' : IntermediateField F E := (IsScalarTower.toAlgHom F L E).fieldRange
f' : ↥L' →ₐ[F] K := f.comp ↑(AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)).symm
φ : ↥(adjoin (↥L') S) →ₐ[F] K
hφ : AlgHom.domRestrict (↥L') φ = f'
⊢ restrictScalars F (adjoin L S) ≤ restrictScalars F (adjoin (↥L') S)
Module: Mathlib.FieldTheory.Extension

Goal state before:
pp: case refine_2.refine_2
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁸ : Field F
inst✝⁷ : Field E
inst✝⁶ : Field K
inst✝⁵ : Algebra F E
inst✝⁴ : Algebra F K
S : Set E
L : Type u_4
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra L E
inst✝ : IsScalarTower F L E
f : L →ₐ[F] K
hK : ∀ s ∈ S, IsIntegral L s ∧ (Polynomial.map f.toRingHom (minpoly L s)).Splits
L' : IntermediateField F E := (IsScalarTower.toAlgHom F L E).fieldRange
f' : ↥L' →ₐ[F] K := f.comp ↑(AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)).symm
φ : ↥(adjoin (↥L') S) →ₐ[F] K
hφ : AlgHom.domRestrict (↥L') φ = f'
⊢ AlgHom.domRestrict L (φ.comp (inclusion ⋯)) = f

Tactic:
·

Goal state after:
case refine_2.refine_2
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁸ : Field F
inst✝⁷ : Field E
inst✝⁶ : Field K
inst✝⁵ : Algebra F E
inst✝⁴ : Algebra F K
S : Set E
L : Type u_4
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra L E
inst✝ : IsScalarTower F L E
f : L →ₐ[F] K
hK : ∀ s ∈ S, IsIntegral L s ∧ (Polynomial.map f.toRingHom (minpoly L s)).Splits
L' : IntermediateField F E := (IsScalarTower.toAlgHom F L E).fieldRange
f' : ↥L' →ₐ[F] K := f.comp ↑(AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)).symm
φ : ↥(adjoin (↥L') S) →ₐ[F] K
hφ : AlgHom.domRestrict (↥L') φ = f'
⊢ AlgHom.domRestrict L (φ.comp (inclusion ⋯)) = f
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

Goal state before:
pp: F : Type u_1
inst✝⁶ : Field F
E : Type u_2
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
α : E
K : Type u
inst✝³ : Field K
inst✝² : Algebra F K
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
⊢ ∀ (x : ↥⊥), IsAlgebraic K x

Tactic:
by
    intro ⟨x, hx⟩
    obtain ⟨c, rfl⟩ := hx
    exact isAlgebraic_algebraMap c

Goal state after:
Module: Mathlib.FieldTheory.Extension

Goal state before:
pp: case refine_1
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
S : Set E
hK : ∀ s ∈ S, IsIntegral F s ∧ (Polynomial.map (algebraMap F K) (minpoly F s)).Splits
L : IntermediateField F E
f : ↥L →ₐ[F] K
hL : L ≤ adjoin F S
φ : Lifts F E K
hfφ : { carrier := L, emb := f } ≤ φ
hφ : IsMax φ
s : E
hs : s ∈ S
⊢ s ∈ ↑φ.carrier

pp: case refine_2
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
S : Set E
hK : ∀ s ∈ S, IsIntegral F s ∧ (Polynomial.map (algebraMap F K) (minpoly F s)).Splits
L : IntermediateField F E
f : ↥L →ₐ[F] K
hL : L ≤ adjoin F S
φ : Lifts F E K
hfφ : { carrier := L, emb := f } ≤ φ
hφ : IsMax φ
⊢ (φ.emb.comp (inclusion ⋯)).comp (inclusion hL) = f

Tactic:
·

Goal state after:
case refine_1
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
S : Set E
hK : ∀ s ∈ S, IsIntegral F s ∧ (Polynomial.map (algebraMap F K) (minpoly F s)).Splits
L : IntermediateField F E
f : ↥L →ₐ[F] K
hL : L ≤ adjoin F S
φ : Lifts F E K
hfφ : { carrier := L, emb := f } ≤ φ
hφ : IsMax φ
s : E
hs : s ∈ S
⊢ s ∈ ↑φ.carrier
Module: Mathlib.LinearAlgebra.Eigenspace.Pi

Goal state before:
pp: case insert.refine_1
ι : Type u_1
R : Type u_2
M : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
f : ι → End R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
h : ∀ (l : ι) (χ : ι → R), MapsTo (⇑(f l)) (⨅ i, ↑((f i).maxGenEigenspace (χ i))) (⨅ i, ↑((f i).maxGenEigenspace (χ i)))
χ₁ χ₂ : ι → R
s : Finset (ι → R)
_n : χ₂ ∉ s
ih : Disjoint (⨅ i, (f i).maxGenEigenspace (χ₁ i)) (s.sup fun χ ↦ ⨅ i, (f i).maxGenEigenspace (χ i))
hχ₁₂✝ : χ₁ ∉ insert χ₂ s
hχ₁₂ : χ₁ ≠ χ₂
hχ₁ : χ₁ ∉ s
y : M
hy : y ∈ ⨅ i, (f i).maxGenEigenspace (χ₂ i)
z : M
hz : z ∈ s.sup fun χ ↦ ⨅ i, (f i).maxGenEigenspace (χ i)
hx : y + z ∈ ⨅ i, (f i).maxGenEigenspace (χ₁ i)
l : ι
g : End R M := f l - (algebraMap R (End R M)) (χ₂ l)
k : ℕ
hk : (g ^ k) y = 0
aux :
  ∀ (f : End R M) (φ : R) (k : ℕ) (p : Submodule R M),
    MapsTo ⇑f ↑p ↑p → MapsTo ⇑((f - (algebraMap R (End R M)) φ) ^ k) ↑p ↑p
⊢ ((f l - (algebraMap R (End R M)) (χ₂ l)) ^ k) (y + z) ∈ ↑(⨅ i, (f i).maxGenEigenspace (χ₁ i))

pp: case insert.refine_2
ι : Type u_1
R : Type u_2
M : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
f : ι → End R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
h : ∀ (l : ι) (χ : ι → R), MapsTo (⇑(f l)) (⨅ i, ↑((f i).maxGenEigenspace (χ i))) (⨅ i, ↑((f i).maxGenEigenspace (χ i)))
χ₁ χ₂ : ι → R
s : Finset (ι → R)
_n : χ₂ ∉ s
ih : Disjoint (⨅ i, (f i).maxGenEigenspace (χ₁ i)) (s.sup fun χ ↦ ⨅ i, (f i).maxGenEigenspace (χ i))
hχ₁₂✝ : χ₁ ∉ insert χ₂ s
hχ₁₂ : χ₁ ≠ χ₂
hχ₁ : χ₁ ∉ s
y : M
hy : y ∈ ⨅ i, (f i).maxGenEigenspace (χ₂ i)
z : M
hz : z ∈ s.sup fun χ ↦ ⨅ i, (f i).maxGenEigenspace (χ i)
hx : y + z ∈ ⨅ i, (f i).maxGenEigenspace (χ₁ i)
l : ι
g : End R M := f l - (algebraMap R (End R M)) (χ₂ l)
k : ℕ
hk : (g ^ k) y = 0
aux :
  ∀ (f : End R M) (φ : R) (k : ℕ) (p : Submodule R M),
    MapsTo ⇑f ↑p ↑p → MapsTo ⇑((f - (algebraMap R (End R M)) φ) ^ k) ↑p ↑p
⊢ ((f l - (algebraMap R (End R M)) (χ₂ l)) ^ k) (y + z) ∈ ↑(s.sup fun χ ↦ ⨅ i, (f i).maxGenEigenspace (χ i))

Tactic:
·

Goal state after:
case insert.refine_1
ι : Type u_1
R : Type u_2
M : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
f : ι → End R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
h : ∀ (l : ι) (χ : ι → R), MapsTo (⇑(f l)) (⨅ i, ↑((f i).maxGenEigenspace (χ i))) (⨅ i, ↑((f i).maxGenEigenspace (χ i)))
χ₁ χ₂ : ι → R
s : Finset (ι → R)
_n : χ₂ ∉ s
ih : Disjoint (⨅ i, (f i).maxGenEigenspace (χ₁ i)) (s.sup fun χ ↦ ⨅ i, (f i).maxGenEigenspace (χ i))
hχ₁₂✝ : χ₁ ∉ insert χ₂ s
hχ₁₂ : χ₁ ≠ χ₂
hχ₁ : χ₁ ∉ s
y : M
hy : y ∈ ⨅ i, (f i).maxGenEigenspace (χ₂ i)
z : M
hz : z ∈ s.sup fun χ ↦ ⨅ i, (f i).maxGenEigenspace (χ i)
hx : y + z ∈ ⨅ i, (f i).maxGenEigenspace (χ₁ i)
l : ι
g : End R M := f l - (algebraMap R (End R M)) (χ₂ l)
k : ℕ
hk : (g ^ k) y = 0
aux :
  ∀ (f : End R M) (φ : R) (k : ℕ) (p : Submodule R M),
    MapsTo ⇑f ↑p ↑p → MapsTo ⇑((f - (algebraMap R (End R M)) φ) ^ k) ↑p ↑p
⊢ ((f l - (algebraMap R (End R M)) (χ₂ l)) ^ k) (y + z) ∈ ↑(⨅ i, (f i).maxGenEigenspace (χ₁ i))
Module: Mathlib.FieldTheory.Extension

Goal state before:
pp: case refine_2
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
S : Set E
hK : ∀ s ∈ S, IsIntegral F s ∧ (Polynomial.map (algebraMap F K) (minpoly F s)).Splits
L : IntermediateField F E
f : ↥L →ₐ[F] K
hL : L ≤ adjoin F S
φ : Lifts F E K
hfφ : { carrier := L, emb := f } ≤ φ
hφ : IsMax φ
⊢ (φ.emb.comp (inclusion ⋯)).comp (inclusion hL) = f

Tactic:
·

Goal state after:
case refine_2
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
S : Set E
hK : ∀ s ∈ S, IsIntegral F s ∧ (Polynomial.map (algebraMap F K) (minpoly F s)).Splits
L : IntermediateField F E
f : ↥L →ₐ[F] K
hL : L ≤ adjoin F S
φ : Lifts F E K
hfφ : { carrier := L, emb := f } ≤ φ
hφ : IsMax φ
⊢ (φ.emb.comp (inclusion ⋯)).comp (inclusion hL) = f
Module: Mathlib.LinearAlgebra.Eigenspace.Pi

Goal state before:
pp: case insert.refine_2
ι : Type u_1
R : Type u_2
M : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
f : ι → End R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
h : ∀ (l : ι) (χ : ι → R), MapsTo (⇑(f l)) (⨅ i, ↑((f i).maxGenEigenspace (χ i))) (⨅ i, ↑((f i).maxGenEigenspace (χ i)))
χ₁ χ₂ : ι → R
s : Finset (ι → R)
_n : χ₂ ∉ s
ih : Disjoint (⨅ i, (f i).maxGenEigenspace (χ₁ i)) (s.sup fun χ ↦ ⨅ i, (f i).maxGenEigenspace (χ i))
hχ₁₂✝ : χ₁ ∉ insert χ₂ s
hχ₁₂ : χ₁ ≠ χ₂
hχ₁ : χ₁ ∉ s
y : M
hy : y ∈ ⨅ i, (f i).maxGenEigenspace (χ₂ i)
z : M
hz : z ∈ s.sup fun χ ↦ ⨅ i, (f i).maxGenEigenspace (χ i)
hx : y + z ∈ ⨅ i, (f i).maxGenEigenspace (χ₁ i)
l : ι
g : End R M := f l - (algebraMap R (End R M)) (χ₂ l)
k : ℕ
hk : (g ^ k) y = 0
aux :
  ∀ (f : End R M) (φ : R) (k : ℕ) (p : Submodule R M),
    MapsTo ⇑f ↑p ↑p → MapsTo ⇑((f - (algebraMap R (End R M)) φ) ^ k) ↑p ↑p
⊢ ((f l - (algebraMap R (End R M)) (χ₂ l)) ^ k) (y + z) ∈ ↑(s.sup fun χ ↦ ⨅ i, (f i).maxGenEigenspace (χ i))

Tactic:
·

Goal state after:
case insert.refine_2
ι : Type u_1
R : Type u_2
M : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
f : ι → End R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
h : ∀ (l : ι) (χ : ι → R), MapsTo (⇑(f l)) (⨅ i, ↑((f i).maxGenEigenspace (χ i))) (⨅ i, ↑((f i).maxGenEigenspace (χ i)))
χ₁ χ₂ : ι → R
s : Finset (ι → R)
_n : χ₂ ∉ s
ih : Disjoint (⨅ i, (f i).maxGenEigenspace (χ₁ i)) (s.sup fun χ ↦ ⨅ i, (f i).maxGenEigenspace (χ i))
hχ₁₂✝ : χ₁ ∉ insert χ₂ s
hχ₁₂ : χ₁ ≠ χ₂
hχ₁ : χ₁ ∉ s
y : M
hy : y ∈ ⨅ i, (f i).maxGenEigenspace (χ₂ i)
z : M
hz : z ∈ s.sup fun χ ↦ ⨅ i, (f i).maxGenEigenspace (χ i)
hx : y + z ∈ ⨅ i, (f i).maxGenEigenspace (χ₁ i)
l : ι
g : End R M := f l - (algebraMap R (End R M)) (χ₂ l)
k : ℕ
hk : (g ^ k) y = 0
aux :
  ∀ (f : End R M) (φ : R) (k : ℕ) (p : Submodule R M),
    MapsTo ⇑f ↑p ↑p → MapsTo ⇑((f - (algebraMap R (End R M)) φ) ^ k) ↑p ↑p
⊢ ((f l - (algebraMap R (End R M)) (χ₂ l)) ^ k) (y + z) ∈ ↑(s.sup fun χ ↦ ⨅ i, (f i).maxGenEigenspace (χ i))