awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
α : E
| IsIntegral F α
have rw : IsIntegral F (A := E) ((algebraMap (↥F⟮α⟯) E : (a : ↥F⟮α⟯) → E) (gen F α) : E)
Tactic: rw [← AdjoinSimple.algebraMap_gen F α]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
α : E
⊢ IsIntegral F (A := ↥F⟮α⟯) (gen F α) ↔ IsIntegral F α
have conv_rhs : IsIntegral F (A := ↥F⟮α⟯) (gen F α) ↔ IsIntegral F (A := E) ((algebraMap (↥F⟮α⟯) E : (a : ↥F⟮α⟯) → E) (gen F α) : E)
Tactic: conv_rhs => rw [← AdjoinSimple.algebraMap_gen F α]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
α : E
⊢ IsIntegral F (A := ↥F⟮α⟯) (gen F α) ↔ IsIntegral F (A := E) ((algebraMap (↥F⟮α⟯) E : (a : ↥F⟮α⟯) → E) (gen F α) : E)
have rw : IsIntegral F (A := ↥F⟮α⟯) (gen F α) ↔ IsIntegral F (A := ↥F⟮α⟯) (gen F α)
Tactic: rw [isIntegral_algebraMap_iff (algebraMap F⟮α⟯ E).injective]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S : Set E
hS : ∀ x ∈ S, IsAlgebraic F x
⊢ Eq (α := IntermediateField F E) (adjoin F S) ⊤ ↔ Eq (α := Subalgebra F E) (Algebra.adjoin F S) ⊤
have rw : Eq (α := IntermediateField F E) (adjoin F S) ⊤ ↔ Eq (α := Subalgebra F E) (toSubalgebra (adjoin F S)) ⊤
Tactic: rw [← IntermediateField.adjoin_toSubalgebra_of_isAlgebraic hS,
      ← IntermediateField.toSubalgebra_inj,
      IntermediateField.top_toSubalgebra]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S : Set E
hS : ∀ x ∈ S, IsAlgebraic F x
rw : Eq (α := IntermediateField F E) (adjoin F S) ⊤ ↔ Eq (α := Subalgebra F E) (toSubalgebra (adjoin F S)) ⊤
⊢ Eq (α := IntermediateField F E) (adjoin F S) ⊤ ↔ Eq (α := Subalgebra F E) (Algebra.adjoin F S) ⊤
have rw₁ : Eq (α := Subalgebra F E) (toSubalgebra (adjoin F S)) (toSubalgebra ⊤) ↔
  Eq (α := Subalgebra F E) (toSubalgebra (adjoin F S)) ⊤
Tactic: rw [← IntermediateField.adjoin_toSubalgebra_of_isAlgebraic hS,
      ← IntermediateField.toSubalgebra_inj,
      IntermediateField.top_toSubalgebra]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S : Set E
hS : ∀ x ∈ S, IsAlgebraic F x
rw : Eq (α := IntermediateField F E) (adjoin F S) ⊤ ↔ Eq (α := Subalgebra F E) (toSubalgebra (adjoin F S)) ⊤
rw₁ :
  Eq (α := Subalgebra F E) (toSubalgebra (adjoin F S)) (toSubalgebra ⊤) ↔
    Eq (α := Subalgebra F E) (toSubalgebra (adjoin F S)) ⊤
⊢ Eq (α := IntermediateField F E) (adjoin F S) ⊤ ↔ Eq (α := Subalgebra F E) (Algebra.adjoin F S) ⊤
have rw₂ : Eq (α := Subalgebra F E) (toSubalgebra (adjoin F S)) ⊤ ↔ Eq (α := Subalgebra F E) (toSubalgebra (adjoin F S)) ⊤
Tactic: rw [← IntermediateField.adjoin_toSubalgebra_of_isAlgebraic hS,
      ← IntermediateField.toSubalgebra_inj,
      IntermediateField.top_toSubalgebra]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : EssFiniteType F E
inst_4 : Algebra.IsAlgebraic F E
⊢ Module.Finite F E
have obtain : ∀ (s : Finset E) (hs : Eq (α := IntermediateField F E) (adjoin F (↑s : Set E)) ⊤), Module.Finite F E
Tactic: obtain ⟨s, hs⟩ := fg_top F E
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : EssFiniteType F E
inst_4 : Algebra.IsAlgebraic F E
s : Finset E
hs : Eq (α := IntermediateField F E) (adjoin F (↑s : Set E)) ⊤
⊢ FiniteType F E
have h : Eq (α := Subalgebra F E) (Algebra.adjoin F (↑s : Set E)) ⊤
Tactic: use s
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : EssFiniteType F E
inst_4 : Algebra.IsAlgebraic F E
s : Finset E
hs : Eq (α := IntermediateField F E) (adjoin F (↑s : Set E)) ⊤
⊢ Eq (α := Subalgebra F E) (Algebra.adjoin F (↑s : Set E)) ⊤
have h : Eq (α := Subalgebra F E) (toSubalgebra (adjoin F (↑s : Set E))) ⊤
Tactic: rw [← adjoin_toSubalgebra_of_isAlgebraic fun x hx ↦ Algebra.IsAlgebraic.isAlgebraic x]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra (hypothesis)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : EssFiniteType F E
inst_4 : Algebra.IsAlgebraic F E
s : Finset E
hs : Eq (α := IntermediateField F E) (adjoin F (↑s : Set E)) ⊤
⊢ Module.Finite F E
have this : FiniteType F E
Tactic: have : Algebra.FiniteType F E := by
    use s
    rw [← adjoin_toSubalgebra_of_isAlgebraic fun x hx ↦ Algebra.IsAlgebraic.isAlgebraic x]
    simpa [← toSubalgebra_inj] using hs
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra (hypothesis)
Goal:
K : Type u_3
L : Type u_4
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
E1 E2 : IntermediateField K L
inst_3 : Algebra.IsAlgebraic.{u_3, u_4} K ↥E2
⊢ (E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra
have this : Eq (α := Subalgebra (↥E1) L) (toSubalgebra (adjoin ↥E1 (↑E2 : Set L))) (Algebra.adjoin ↥E1 (↑E2 : Set L))
Tactic: have : (adjoin E1 (E2 : Set L)).toSubalgebra = _ := adjoin_toSubalgebra_of_isAlgebraic fun x h ↦
    IsAlgebraic.tower_top _ (isAlgebraic_iff.mp (Algebra.IsAlgebraic.isAlgebraic (⟨x, h⟩ : E2)))
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra (hypothesis)
Goal:
K : Type u_3
L : Type u_4
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
E1 E2 : IntermediateField K L
inst_3 : Algebra.IsAlgebraic.{u_3, u_4} K ↥E2
this : Eq (α := Subalgebra (↥E1) L) (toSubalgebra (adjoin ↥E1 (↑E2 : Set L))) (Algebra.adjoin ↥E1 (↑E2 : Set L))
⊢ (E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra
have this₁ : Eq (α := Subalgebra K L) (Subalgebra.restrictScalars K (S := ↥E1) (toSubalgebra (adjoin ↥E1 (↑E2 : Set L))))
  (Subalgebra.restrictScalars K (S := ↥E1) (Algebra.adjoin ↥E1 (↑E2 : Set L)))
Tactic: apply_fun Subalgebra.restrictScalars K at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra (hypothesis)
Goal:
K : Type u_3
L : Type u_4
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
E1 E2 : IntermediateField K L
inst_3 : Algebra.IsAlgebraic.{u_3, u_4} K ↥E2
this :
  Eq (α := Subalgebra K L) (Subalgebra.restrictScalars K (S := ↥E1) (toSubalgebra (adjoin ↥E1 (↑E2 : Set L))))
    (Subalgebra.restrictScalars K (S := ↥E1) (Algebra.adjoin ↥E1 (↑E2 : Set L)))
⊢ (E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra
have this₁ : Eq (α := Subalgebra K L) (toSubalgebra (adjoin K ((↑E1 : Set L) ∪ (↑E2 : Set L))))
  (Subalgebra.restrictScalars K (S := ↥E1) (Algebra.adjoin ↥E1 (↑E2 : Set L)))
Tactic: rw [← restrictScalars_toSubalgebra, restrictScalars_adjoin] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra (hypothesis)
Goal:
K : Type u_3
L : Type u_4
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
E1 E2 : IntermediateField K L
inst_3 : Algebra.IsAlgebraic.{u_3, u_4} K ↥E2
this :
  Eq (α := Subalgebra K L) (toSubalgebra (adjoin K ((↑E1 : Set L) ∪ (↑E2 : Set L))))
    (Subalgebra.restrictScalars K (S := ↥E1.toSubalgebra) (Algebra.adjoin ↥E1.toSubalgebra (↑E2 : Set L)))
⊢ (E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra
have this₁ : Eq (α := Subalgebra K L) (toSubalgebra (adjoin K ((↑E1 : Set L) ∪ (↑E2 : Set L))))
  (Algebra.adjoin K ((↑E1.toSubalgebra : Set L) ∪ (↑E2 : Set L)))
Tactic: rw [Algebra.restrictScalars_adjoin] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra (hypothesis)
Goal:
K : Type u_3
L : Type u_4
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
E1 E2 : IntermediateField K L
inst_3 : Algebra.IsAlgebraic.{u_3, u_4} K ↥E1
⊢ (E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra
have this : (E2 ⊔ E1).toSubalgebra = E2.toSubalgebra ⊔ E1.toSubalgebra
Tactic: have := sup_toSubalgebra_of_isAlgebraic_right E2 E1
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra (goal)
Goal:
K : Type u_3
L : Type u_4
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
E1 E2 : IntermediateField K L
inst_3 : Algebra.IsAlgebraic.{u_3, u_4} K ↥E1
this : (E2 ⊔ E1).toSubalgebra = E2.toSubalgebra ⊔ E1.toSubalgebra
⊢ (E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra
have rwa : (E2 ⊔ E1).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra
Tactic: rwa [sup_comm (a := E1), sup_comm (a := E1.toSubalgebra)]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
K : Type u_3
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
L : IntermediateField F K
halg : Algebra.IsAlgebraic F E ∨ Algebra.IsAlgebraic.{u_1, u_3} F ↥L
i : E →ₐ[F] K := IsScalarTower.toAlgHom F E K
E' : IntermediateField F K := i.fieldRange
i' : AlgEquiv.{u_1, u_2, u_3} F E ↥E' := AlgEquiv.ofInjectiveField i
⊢ Eq (α := (a : E) → K) (⇑(algebraMap E K) : (a : E) → K)
    (Function.comp (β := ↥E') (⇑(algebraMap (↥E') K) : (a : ↥E') → K) (⇑i' : (a : E) → ↥E'))
have h : ∀ (x : E),
  Eq (α := K) ((algebraMap E K : (a : E) → K) x : K)
    (Function.comp (β := ↥E') (⇑(algebraMap (↥E') K) : (a : ↥E') → K) (⇑i' : (a : E) → ↥E') x : K)
Tactic: ext x
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra (hypothesis)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
K : Type u_3
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
L : IntermediateField F K
halg : Algebra.IsAlgebraic F E ∨ Algebra.IsAlgebraic.{u_1, u_3} F ↥L
i : E →ₐ[F] K := IsScalarTower.toAlgHom F E K
E' : IntermediateField F K := i.fieldRange
i' : AlgEquiv.{u_1, u_2, u_3} F E ↥E' := AlgEquiv.ofInjectiveField i
⊢ Eq (α := Subalgebra E K) (toSubalgebra (adjoin E (↑L : Set K))) (Algebra.adjoin E (↑L : Set K))
have hi : Eq (α := (a : E) → K) (⇑(algebraMap E K) : (a : E) → K)
  (Function.comp (β := ↥E') (⇑(algebraMap (↥E') K) : (a : ↥E') → K) (⇑i' : (a : E) → ↥E'))
Tactic: have hi : algebraMap E K = (algebraMap E' K) ∘ i' := by ext x; rfl
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
K : Type u_3
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
L : IntermediateField F K
halg : Algebra.IsAlgebraic F E ∨ Algebra.IsAlgebraic.{u_1, u_3} F ↥L
i : E →ₐ[F] K := IsScalarTower.toAlgHom F E K
E' : IntermediateField F K := i.fieldRange
i' : AlgEquiv.{u_1, u_2, u_3} F E ↥E' := AlgEquiv.ofInjectiveField i
hi :
  Eq (α := (a : E) → K) (⇑(algebraMap E K) : (a : E) → K)
    (Function.comp (β := ↥E') (⇑(algebraMap (↥E') K) : (a : ↥E') → K) (⇑i' : (a : E) → ↥E'))
⊢ Eq (α := Subalgebra E K) (toSubalgebra (adjoin E (↑L : Set K))) (Algebra.adjoin E (↑L : Set K))
have apply_fun : Eq (α := Subalgebra F K) (Subalgebra.restrictScalars F (toSubalgebra (adjoin E (↑L : Set K))))
  (Subalgebra.restrictScalars F (Algebra.adjoin E (↑L : Set K)))
Tactic: apply_fun _ using Subalgebra.restrictScalars_injective F
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
K : Type u_3
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
L : IntermediateField F K
halg : Algebra.IsAlgebraic F E ∨ Algebra.IsAlgebraic.{u_1, u_3} F ↥L
i : E →ₐ[F] K := IsScalarTower.toAlgHom F E K
E' : IntermediateField F K := i.fieldRange
i' : AlgEquiv.{u_1, u_2, u_3} F E ↥E' := AlgEquiv.ofInjectiveField i
hi :
  Eq (α := (a : E) → K) (⇑(algebraMap E K) : (a : E) → K)
    (Function.comp (β := ↥E') (⇑(algebraMap (↥E') K) : (a : ↥E') → K) (⇑i' : (a : E) → ↥E'))
⊢ Eq (α := Subalgebra F K) (Subalgebra.restrictScalars F (toSubalgebra (adjoin E (↑L : Set K))))
    (Subalgebra.restrictScalars F (Algebra.adjoin E (↑L : Set K)))
have rw : Eq (α := Subalgebra F K) (toSubalgebra (adjoin F ((↑E' : Set K) ∪ (↑L : Set K))))
  (Subalgebra.restrictScalars F (S := ↥E') (Algebra.adjoin ↥E' (↑L : Set K)))
Tactic: rw [← restrictScalars_toSubalgebra, restrictScalars_adjoin_of_algEquiv i' hi,
    Algebra.restrictScalars_adjoin_of_algEquiv i' hi, restrictScalars_adjoin]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S : IntermediateField F E
h : S.FG
⊢ S.FG
have obtain : ∀ (t : Finset E) (ht : Algebra.adjoin F (↑t : Set E) = S.toSubalgebra), S.FG
Tactic: obtain ⟨t, ht⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra (goal)
Goal:
F : Type u_1
A : Type u_2
K : Type u_3
L : Type u_4
inst : Field F
inst_1 : CommRing A
inst_2 : Algebra F A
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra A K
inst_6 : IsFractionRing A K
inst_7 : Field L
inst_8 : Algebra F L
g : A →ₐ[F] L
f : K →ₐ[F] L
h :
  Eq (α := A →+* L) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f : K →+* L) (algebraMap A K)) (↑g : A →+* L)
⊢ f.fieldRange = IntermediateField.adjoin F (↑g.range : Set L)
have a : f.fieldRange.toSubfield = IntermediateField.toSubfield (IntermediateField.adjoin F (↑g.range : Set L))
Tactic: apply IntermediateField.toSubfield_injective
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra (goal)
Goal:
F : Type u_1
A : Type u_2
K : Type u_3
L : Type u_4
inst : Field F
inst_1 : CommRing A
inst_2 : Algebra F A
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra A K
inst_6 : IsFractionRing A K
inst_7 : Field L
inst_8 : Algebra F L
g : A →ₐ[F] L
f : K →ₐ[F] L
h :
  Eq (α := A →+* L) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f : K →+* L) (algebraMap A K)) (↑g : A →+* L)
⊢ f.fieldRange.toSubfield = IntermediateField.toSubfield (IntermediateField.adjoin F (↑g.range : Set L))
have a : Eq (α := Subfield L) (RingHom.fieldRange (↑f : K →+* L))
  (Subfield.closure (Set.range.{u_4, u_1 + 1} (ι := F) (⇑(algebraMap F L) : (a : F) → L) ∪ (↑g.range : Set L)))
Tactic: simp_rw [AlgHom.fieldRange_toSubfield, IntermediateField.adjoin_toSubfield]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra (goal)
Goal:
F : Type u_1
A : Type u_2
K : Type u_3
L : Type u_4
inst : Field F
inst_1 : CommRing A
inst_2 : Algebra F A
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra A K
inst_6 : IsFractionRing A K
inst_7 : Field L
inst_8 : Algebra F L
g : A →ₐ[F] L
f : K →ₐ[F] L
h :
  Eq (α := A →+* L) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f : K →+* L) (algebraMap A K)) (↑g : A →+* L)
⊢ Eq (α := Subfield L) (RingHom.fieldRange (↑f : K →+* L))
    (Subfield.closure (Set.range.{u_4, u_1 + 1} (ι := F) (⇑(algebraMap F L) : (a : F) → L) ∪ (↑g.range : Set L)))
have h₁ : Set.range.{u_4, u_1 + 1} (ι := F) (⇑(algebraMap F L) : (a : F) → L) ∪ (↑g.range : Set L) =
  (↑(RingHom.range (↑g : A →+* L)) : Set L)
Tactic: convert! ringHom_fieldRange_eq_of_comp_eq h using 2
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra (goal)
Goal:
F : Type u_1
A : Type u_2
K : Type u_3
L : Type u_4
inst : Field F
inst_1 : CommRing A
inst_2 : Algebra F A
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra A K
inst_6 : IsFractionRing A K
inst_7 : Field L
inst_8 : Algebra F L
g : A →ₐ[F] L
f : K →ₐ[F] L
h :
  Eq (α := A →+* L) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f : K →+* L) (algebraMap A K)) (↑g : A →+* L)
s : Set L
hs : g.range = Algebra.adjoin F s
⊢ f.fieldRange = IntermediateField.adjoin F s
have a : f.fieldRange.toSubfield = IntermediateField.toSubfield (IntermediateField.adjoin F s)
Tactic: apply IntermediateField.toSubfield_injective
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra (goal)
Goal:
F : Type u_1
A : Type u_2
K : Type u_3
L : Type u_4
inst : Field F
inst_1 : CommRing A
inst_2 : Algebra F A
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra A K
inst_6 : IsFractionRing A K
inst_7 : Field L
inst_8 : Algebra F L
g : A →ₐ[F] L
f : K →ₐ[F] L
h :
  Eq (α := A →+* L) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f : K →+* L) (algebraMap A K)) (↑g : A →+* L)
s : Set L
hs : g.range = Algebra.adjoin F s
⊢ f.fieldRange.toSubfield = IntermediateField.toSubfield (IntermediateField.adjoin F s)
have a : Eq (α := Subfield L) (RingHom.fieldRange (↑f : K →+* L))
  (Subfield.closure (Set.range.{u_4, u_1 + 1} (ι := F) (⇑(algebraMap F L) : (a : F) → L) ∪ s))
Tactic: simp_rw [AlgHom.fieldRange_toSubfield, IntermediateField.adjoin_toSubfield]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra (goal)
Goal:
F : Type u_1
A : Type u_2
K : Type u_3
L : Type u_4
inst : Field F
inst_1 : CommRing A
inst_2 : Algebra F A
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra A K
inst_6 : IsFractionRing A K
inst_7 : Field L
inst_8 : Algebra F L
g : A →ₐ[F] L
f : K →ₐ[F] L
h :
  Eq (α := A →+* L) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f : K →+* L) (algebraMap A K)) (↑g : A →+* L)
s : Set L
hs : g.range = Algebra.adjoin F s
⊢ Eq (α := Subfield L) (RingHom.fieldRange (↑f : K →+* L))
    (Subfield.closure (Set.range.{u_4, u_1 + 1} (ι := F) (⇑(algebraMap F L) : (a : F) → L) ∪ s))
have a : Eq (α := Subring L) (RingHom.range (↑g : A →+* L))
  (Subring.closure (Set.range.{u_4, u_1 + 1} (ι := F) (⇑(algebraMap F L) : (a : F) → L) ∪ s))
Tactic: refine ringHom_fieldRange_eq_of_comp_eq_of_range_eq h ?_
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra (goal)
Goal:
F : Type u_1
A : Type u_2
K : Type u_3
L : Type u_4
inst : Field F
inst_1 : CommRing A
inst_2 : Algebra F A
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra A K
inst_6 : IsFractionRing A K
inst_7 : Field L
inst_8 : Algebra F L
g : A →ₐ[F] L
f : K →ₐ[F] L
h :
  Eq (α := A →+* L) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f : K →+* L) (algebraMap A K)) (↑g : A →+* L)
s : Set L
hs : g.range = Algebra.adjoin F s
⊢ Eq (α := Subring L) (RingHom.range (↑g : A →+* L))
    (Subring.closure (Set.range.{u_4, u_1 + 1} (ι := F) (⇑(algebraMap F L) : (a : F) → L) ∪ s))
have a : RingHom.range (↑g : A →+* L) = g.range.toSubring
Tactic: rw [← Algebra.adjoin_eq_ring_closure, ← hs]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra (goal)
Goal:
F : Type u_1
A : Type u_2
K : Type u_3
L : Type u_4
inst : Field F
inst_1 : CommRing A
inst_2 : Algebra F A
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra A K
inst_6 : IsFractionRing A K
inst_7 : Field L
inst_8 : Algebra F L
g : A →ₐ[F] L
inst_9 : IsScalarTower F A K
hg : Function.Injective.{u_2 + 1, u_4 + 1} (α := A) (β := L) (⇑g : (a : A) → L)
⊢ Eq (α := A →+* L) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑(liftAlgHom hg) : K →+* L) (algebraMap A K))
    (↑g : A →+* L)
have a : ∀ (x : A),
  Eq.{u_4 + 1} (α := L)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑(liftAlgHom hg) : K →+* L) (algebraMap A K) : (a : A) → L)
        x :
      L)
    (((↑g : A →+* L) : (a : A) → L) x : L)
Tactic: ext
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra (goal)
Goal:
F : Type u_1
A : Type u_2
K : Type u_3
L : Type u_4
inst : Field F
inst_1 : CommRing A
inst_2 : Algebra F A
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra A K
inst_6 : IsFractionRing A K
inst_7 : Field L
inst_8 : Algebra F L
g : A →ₐ[F] L
inst_9 : IsScalarTower F A K
hg : Function.Injective.{u_2 + 1, u_4 + 1} (α := A) (β := L) (⇑g : (a : A) → L)
s : Set L
hs : g.range = Algebra.adjoin F s
⊢ Eq (α := A →+* L) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑(liftAlgHom hg) : K →+* L) (algebraMap A K))
    (↑g : A →+* L)
have a : ∀ (x : A),
  Eq.{u_4 + 1} (α := L)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑(liftAlgHom hg) : K →+* L) (algebraMap A K) : (a : A) → L)
        x :
      L)
    (((↑g : A →+* L) : (a : A) → L) x : L)
Tactic: ext
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
Goal:
K : Type u_1
L : Type u_2
E : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Field E
inst_3 : Algebra K L
inst_4 : Algebra K E
inst_5 : Algebra L E
inst_6 : IsScalarTower K L E
E' : IntermediateField L E
H : FG (restrictScalars K E')
⊢ E'.FG
have obtain : ∀ (s : Finset E) (hs : Eq (α := IntermediateField K E) (adjoin K (↑s : Set E)) (restrictScalars K E')), E'.FG
Tactic: obtain ⟨s, hs⟩ := H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
Goal:
K : Type u_1
L : Type u_2
E : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Field E
inst_3 : Algebra K L
inst_4 : Algebra K E
inst_5 : Algebra L E
inst_6 : IsScalarTower K L E
E' : IntermediateField L E
s : Finset E
hs : Eq (α := IntermediateField K E) (adjoin K (↑s : Set E)) (restrictScalars K E')
⊢ E'.FG
have refine_1 : adjoin L (↑s : Set E) ≤ E'
Tactic: refine ⟨s, le_antisymm ?_ ?_⟩
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
Goal:
K : Type u_1
L : Type u_2
E : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Field E
inst_3 : Algebra K L
inst_4 : Algebra K E
inst_5 : Algebra L E
inst_6 : IsScalarTower K L E
E' : IntermediateField L E
s : Finset E
hs : Eq (α := IntermediateField K E) (adjoin K (↑s : Set E)) (restrictScalars K E')
refine_1 : adjoin L (↑s : Set E) ≤ E'
⊢ E'.FG
have refine_2 : E' ≤ adjoin L (↑s : Set E)
Tactic: refine ⟨s, le_antisymm ?_ ?_⟩
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
Goal:
K : Type u_1
L : Type u_2
E : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Field E
inst_3 : Algebra K L
inst_4 : Algebra K E
inst_5 : Algebra L E
inst_6 : IsScalarTower K L E
E' : IntermediateField L E
s : Finset E
hs : Eq (α := IntermediateField K E) (adjoin K (↑s : Set E)) (restrictScalars K E')
⊢ adjoin L (↑s : Set E) ≤ E'
have refine_1 : (↑s : Set E) ⊆ (↑E' : Set E)
Tactic: rw [adjoin_le_iff]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
Goal:
K : Type u_1
L : Type u_2
E : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Field E
inst_3 : Algebra K L
inst_4 : Algebra K E
inst_5 : Algebra L E
inst_6 : IsScalarTower K L E
E' : IntermediateField L E
s : Finset E
hs : Eq (α := IntermediateField K E) (adjoin K (↑s : Set E)) (restrictScalars K E')
⊢ E' ≤ adjoin L (↑s : Set E)
have refine_2 : (↑s : Set E) ⊆ (↑(restrictScalars K (adjoin L (↑s : Set E))) : Set E)
Tactic: rw [← restrictScalars_le_iff K, ← hs, adjoin_le_iff]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
ι : Type u_3
i : ι → E
x : E
⊢ Membership.mem (γ := IntermediateField F E) (adjoin F (Set.range i)) x ↔
    ∃ (r : MvPolynomial ι F) (s : MvPolynomial ι F),
      x =
        HDiv.hDiv (α := E) (β := E) ((MvPolynomial.aeval i : (a : MvPolynomial ι F) → E) r : E)
          ((MvPolynomial.aeval i : (a : MvPolynomial ι F) → E) s : E)
have simp_rw : (∃ (r : E),
    Membership.mem (γ := Subalgebra F E) (Algebra.adjoin F (Set.range i)) r ∧
      ∃ (s : E), Membership.mem (γ := Subalgebra F E) (Algebra.adjoin F (Set.range i)) s ∧ x = r / s) ↔
  ∃ (r : MvPolynomial ι F) (s : MvPolynomial ι F),
    x =
      HDiv.hDiv (α := E) (β := E) ((MvPolynomial.aeval i : (a : MvPolynomial ι F) → E) r : E)
        ((MvPolynomial.aeval i : (a : MvPolynomial ι F) → E) s : E)
Tactic: simp_rw [mem_adjoin_iff_div, Algebra.adjoin_range_eq_range_aeval,
    AlgHom.mem_range, exists_exists_eq_and]