awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Defs (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
y : F
rw :
  Eq (α := E)
    ((algebraMap (↥⊥) E : (a : ↥⊥) → E)
        (((AlgEquiv.symm (botEquiv F E) : AlgEquiv.{u_1, u_1, u_2} F F ↥⊥) : (a : F) → ↥⊥) y : ↥⊥) :
      E)
    ((algebraMap F E : (a : F) → E)
        ((botEquiv F E : (a : ↥⊥) → F)
            (((AlgEquiv.symm (botEquiv F E) : AlgEquiv.{u_1, u_1, u_2} F F ↥⊥) : (a : F) → ↥⊥) y : ↥⊥) :
          F) :
      E)
rw₁ :
  Eq (α := E)
    ((algebraMap (↥⊥) E : (a : ↥⊥) → E)
        (((AlgEquiv.symm (botEquiv F E) : AlgEquiv.{u_1, u_1, u_2} F F ↥⊥) : (a : F) → ↥⊥) y : ↥⊥) :
      E)
    ((algebraMap F E : (a : F) → E) y : E)
⊢ Eq (α := E)
    ((algebraMap (↥⊥) E : (a : ↥⊥) → E)
        (((AlgEquiv.symm (botEquiv F E) : AlgEquiv.{u_1, u_1, u_2} F F ↥⊥) : (a : F) → ↥⊥) y : ↥⊥) :
      E)
    ((algebraMap F E : (a : F) → E)
        ((algebraMap (↥⊥) F : (a : ↥⊥) → F)
            (((AlgEquiv.symm (botEquiv F E) : AlgEquiv.{u_1, u_1, u_2} F F ↥⊥) : (a : F) → ↥⊥) y : ↥⊥) :
          F) :
      E)
have rw₂ : Eq (α := E) ((algebraMap (↥⊥) E : (a : ↥⊥) → E) ((algebraMap F ↥⊥ : (a : F) → ↥⊥) y : ↥⊥) : E)
  ((algebraMap F E : (a : F) → E) y : E)
Tactic: rw [coe_algebraMap_over_bot, (botEquiv F E).apply_symm_apply, botEquiv_symm,
        IsScalarTower.algebraMap_apply F (⊥ : IntermediateField F E) E]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Defs (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
y : F
rw :
  Eq (α := E)
    ((algebraMap (↥⊥) E : (a : ↥⊥) → E)
        (((AlgEquiv.symm (botEquiv F E) : AlgEquiv.{u_1, u_1, u_2} F F ↥⊥) : (a : F) → ↥⊥) y : ↥⊥) :
      E)
    ((algebraMap F E : (a : F) → E)
        ((botEquiv F E : (a : ↥⊥) → F)
            (((AlgEquiv.symm (botEquiv F E) : AlgEquiv.{u_1, u_1, u_2} F F ↥⊥) : (a : F) → ↥⊥) y : ↥⊥) :
          F) :
      E)
rw₁ :
  Eq (α := E)
    ((algebraMap (↥⊥) E : (a : ↥⊥) → E)
        (((AlgEquiv.symm (botEquiv F E) : AlgEquiv.{u_1, u_1, u_2} F F ↥⊥) : (a : F) → ↥⊥) y : ↥⊥) :
      E)
    ((algebraMap F E : (a : F) → E) y : E)
rw₂ :
  Eq (α := E) ((algebraMap (↥⊥) E : (a : ↥⊥) → E) ((algebraMap F ↥⊥ : (a : F) → ↥⊥) y : ↥⊥) : E)
    ((algebraMap F E : (a : F) → E) y : E)
⊢ Eq (α := E)
    ((algebraMap (↥⊥) E : (a : ↥⊥) → E)
        (((AlgEquiv.symm (botEquiv F E) : AlgEquiv.{u_1, u_1, u_2} F F ↥⊥) : (a : F) → ↥⊥) y : ↥⊥) :
      E)
    ((algebraMap F E : (a : F) → E)
        ((algebraMap (↥⊥) F : (a : ↥⊥) → F)
            (((AlgEquiv.symm (botEquiv F E) : AlgEquiv.{u_1, u_1, u_2} F F ↥⊥) : (a : F) → ↥⊥) y : ↥⊥) :
          F) :
      E)
have rw₃ : Eq (α := E) ((algebraMap (↥⊥) E : (a : ↥⊥) → E) ((algebraMap F ↥⊥ : (a : F) → ↥⊥) y : ↥⊥) : E)
  ((algebraMap (↥⊥) E : (a : ↥⊥) → E) ((algebraMap F ↥⊥ : (a : F) → ↥⊥) y : ↥⊥) : E)
Tactic: rw [coe_algebraMap_over_bot, (botEquiv F E).apply_symm_apply, botEquiv_symm,
        IsScalarTower.algebraMap_apply F (⊥ : IntermediateField F E) E]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Defs (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
ι : Sort u_4
inst_5 : Nonempty ι
f : E →ₐ[F] K
s : ι → IntermediateField F E
⊢ map f (iInf s) = ⨅ (i : ι), map f (s i)
have a : (↑(map f (iInf s)) : Set K) = (↑(⨅ (i : ι), map f (s i)) : Set K)
Tactic: apply SetLike.coe_injective
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Defs (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S T : Set E
⊢ Eq (α := IntermediateField F E) (restrictScalars F (L' := ↥(adjoin F S)) (adjoin (↥(adjoin F S)) T))
    (adjoin F (S ∪ T))
have rw : (↑(restrictScalars F (L' := ↥(adjoin F S)) (adjoin (↥(adjoin F S)) T)) : Set E) = (↑(adjoin F (S ∪ T)) : Set E)
Tactic: rw [SetLike.ext'_iff]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Defs (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S T : Set E
⊢ (↑(adjoin (↥(adjoin F S)) T) : Set E) = (↑(adjoin F (S ∪ T)) : Set E)
have a : (↑(adjoin (↥(adjoin F S)) T) : Set E) ⊆ (↑(adjoin F (S ∪ T)) : Set E)
Tactic: apply subset_antisymm
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Defs (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S T : Set E
a : (↑(adjoin (↥(adjoin F S)) T) : Set E) ⊆ (↑(adjoin F (S ∪ T)) : Set E)
⊢ (↑(adjoin (↥(adjoin F S)) T) : Set E) = (↑(adjoin F (S ∪ T)) : Set E)
have a₁ : (↑(adjoin F (S ∪ T)) : Set E) ⊆ (↑(adjoin (↥(adjoin F S)) T) : Set E)
Tactic: apply subset_antisymm
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Defs (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S T : Set E
⊢ (↑(adjoin (↥(adjoin F S)) T) : Set E) ⊆ (↑(adjoin F (S ∪ T)) : Set E)
have a : Set.range (ι := ↥(adjoin F S)) (⇑(algebraMap (↥(adjoin F S)) E) : (a : ↥(adjoin F S)) → E) ⊆
    (↑(adjoin F (S ∪ T)) : Set E) ∧
  T ⊆ (↑(adjoin F (S ∪ T)) : Set E)
Tactic: rw [adjoin_subset_adjoin_iff]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Defs (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S T : Set E
⊢ (↑(adjoin F (S ∪ T)) : Set E) ⊆ (↑(adjoin (↥(adjoin F S)) T) : Set E)
have a : Set.range.{u_2, u_1 + 1} (ι := F) (⇑(algebraMap F E) : (a : F) → E) ⊆ (↑(adjoin (↥(adjoin F S)) T) : Set E) ∧
  S ∪ T ⊆ (↑(adjoin (↥(adjoin F S)) T) : Set E)
Tactic: rw [adjoin_subset_adjoin_iff]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Defs (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S T : Set E
⊢ Set.range (ι := ↥(adjoin F S)) (⇑(algebraMap (↥(adjoin F S)) E) : (a : ↥(adjoin F S)) → E) ⊆
      (↑(adjoin F (S ∪ T)) : Set E) ∧
    T ⊆ (↑(adjoin F (S ∪ T)) : Set E)
have a : Set.range (ι := ↥(adjoin F S)) (⇑(algebraMap (↥(adjoin F S)) E) : (a : ↥(adjoin F S)) → E) ⊆
  (↑(adjoin F (S ∪ T)) : Set E)
Tactic: constructor
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Defs (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S T : Set E
a :
  Set.range (ι := ↥(adjoin F S)) (⇑(algebraMap (↥(adjoin F S)) E) : (a : ↥(adjoin F S)) → E) ⊆
    (↑(adjoin F (S ∪ T)) : Set E)
⊢ Set.range (ι := ↥(adjoin F S)) (⇑(algebraMap (↥(adjoin F S)) E) : (a : ↥(adjoin F S)) → E) ⊆
      (↑(adjoin F (S ∪ T)) : Set E) ∧
    T ⊆ (↑(adjoin F (S ∪ T)) : Set E)
have a₁ : T ⊆ (↑(adjoin F (S ∪ T)) : Set E)
Tactic: constructor
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Defs (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S T : Set E
⊢ Set.range.{u_2, u_1 + 1} (ι := F) (⇑(algebraMap F E) : (a : F) → E) ⊆ (↑(adjoin (↥(adjoin F S)) T) : Set E) ∧
    S ∪ T ⊆ (↑(adjoin (↥(adjoin F S)) T) : Set E)
have a : Set.range.{u_2, u_1 + 1} (ι := F) (⇑(algebraMap F E) : (a : F) → E) ⊆ (↑(adjoin (↥(adjoin F S)) T) : Set E)
Tactic: constructor
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Defs (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S T : Set E
a : Set.range.{u_2, u_1 + 1} (ι := F) (⇑(algebraMap F E) : (a : F) → E) ⊆ (↑(adjoin (↥(adjoin F S)) T) : Set E)
⊢ Set.range.{u_2, u_1 + 1} (ι := F) (⇑(algebraMap F E) : (a : F) → E) ⊆ (↑(adjoin (↥(adjoin F S)) T) : Set E) ∧
    S ∪ T ⊆ (↑(adjoin (↥(adjoin F S)) T) : Set E)
have a₁ : S ∪ T ⊆ (↑(adjoin (↥(adjoin F S)) T) : Set E)
Tactic: constructor
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Defs (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
x : E
⊢ LE.le (α := IntermediateField F E) (adjoin F (insert x S)) (adjoin F (insert x (↑(adjoin F S) : Set E)))
have grw : LE.le (α := IntermediateField F E) (adjoin F (insert x S)) (adjoin F (insert x S))
Tactic: grw [← subset_adjoin]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Defs (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S T : Set E
⊢ Eq (α := IntermediateField F E) (restrictScalars F (L' := ↥(adjoin F S)) (adjoin (↥(adjoin F S)) T))
    (restrictScalars F (L' := ↥(adjoin F T)) (adjoin (↥(adjoin F T)) S))
have rw : Eq (α := IntermediateField F E) (adjoin F (S ∪ T)) (restrictScalars F (L' := ↥(adjoin F T)) (adjoin (↥(adjoin F T)) S))
Tactic: rw [adjoin_adjoin_left, adjoin_adjoin_left, Set.union_comm]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Defs (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S T : Set E
rw :
  Eq (α := IntermediateField F E) (adjoin F (S ∪ T))
    (restrictScalars F (L' := ↥(adjoin F T)) (adjoin (↥(adjoin F T)) S))
⊢ Eq (α := IntermediateField F E) (restrictScalars F (L' := ↥(adjoin F S)) (adjoin (↥(adjoin F S)) T))
    (restrictScalars F (L' := ↥(adjoin F T)) (adjoin (↥(adjoin F T)) S))
have rw₁ : Eq (α := IntermediateField F E) (adjoin F (S ∪ T)) (adjoin F (T ∪ S))
Tactic: rw [adjoin_adjoin_left, adjoin_adjoin_left, Set.union_comm]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Defs (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S T : Set E
rw :
  Eq (α := IntermediateField F E) (adjoin F (S ∪ T))
    (restrictScalars F (L' := ↥(adjoin F T)) (adjoin (↥(adjoin F T)) S))
rw₁ : Eq (α := IntermediateField F E) (adjoin F (S ∪ T)) (adjoin F (T ∪ S))
⊢ Eq (α := IntermediateField F E) (restrictScalars F (L' := ↥(adjoin F S)) (adjoin (↥(adjoin F S)) T))
    (restrictScalars F (L' := ↥(adjoin F T)) (adjoin (↥(adjoin F T)) S))
have rw₂ : Eq (α := IntermediateField F E) (adjoin F (T ∪ S)) (adjoin F (T ∪ S))
Tactic: rw [adjoin_adjoin_left, adjoin_adjoin_left, Set.union_comm]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Defs (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
K : IntermediateField F E
⊢ lift (F := K) ⊤ = K
have rw : map K.val ⊤ = K
Tactic: rw [lift, ← AlgHom.fieldRange_eq_map, fieldRange_val]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Defs (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
K : IntermediateField F E
rw : map K.val ⊤ = K
⊢ lift (F := K) ⊤ = K
have rw₁ : K.val.fieldRange = K
Tactic: rw [lift, ← AlgHom.fieldRange_eq_map, fieldRange_val]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Defs (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
K : IntermediateField F E
rw : map K.val ⊤ = K
rw₁ : K.val.fieldRange = K
⊢ lift (F := K) ⊤ = K
have rw₂ : K = K
Tactic: rw [lift, ← AlgHom.fieldRange_eq_map, fieldRange_val]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Defs (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
K : IntermediateField F E
S : Set E
⊢ Eq (α := IntermediateField F E) (restrictScalars F (L' := ↥K) (adjoin (↥K) S)) (adjoin F ((↑K : Set E) ∪ S))
have rw : Eq (α := IntermediateField F E)
  (restrictScalars F (L' := ↥(adjoin F (↑K : Set E))) (adjoin (↥(adjoin F (↑K : Set E))) S))
  (adjoin F ((↑(adjoin F (↑K : Set E)) : Set E) ∪ S))
Tactic: rw [← adjoin_self _ K, adjoin_adjoin_left, adjoin_self _ K]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Defs (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
K : IntermediateField F E
S : Set E
rw :
  Eq (α := IntermediateField F E)
    (restrictScalars F (L' := ↥(adjoin F (↑K : Set E))) (adjoin (↥(adjoin F (↑K : Set E))) S))
    (adjoin F ((↑(adjoin F (↑K : Set E)) : Set E) ∪ S))
⊢ Eq (α := IntermediateField F E) (restrictScalars F (L' := ↥K) (adjoin (↥K) S)) (adjoin F ((↑K : Set E) ∪ S))
have rw₁ : Eq (α := IntermediateField F E) (adjoin F ((↑K : Set E) ∪ S)) (adjoin F ((↑(adjoin F (↑K : Set E)) : Set E) ∪ S))
Tactic: rw [← adjoin_self _ K, adjoin_adjoin_left, adjoin_self _ K]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Defs (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
K : IntermediateField F E
S : Set E
rw :
  Eq (α := IntermediateField F E)
    (restrictScalars F (L' := ↥(adjoin F (↑K : Set E))) (adjoin (↥(adjoin F (↑K : Set E))) S))
    (adjoin F ((↑(adjoin F (↑K : Set E)) : Set E) ∪ S))
rw₁ : Eq (α := IntermediateField F E) (adjoin F ((↑K : Set E) ∪ S)) (adjoin F ((↑(adjoin F (↑K : Set E)) : Set E) ∪ S))
⊢ Eq (α := IntermediateField F E) (restrictScalars F (L' := ↥K) (adjoin (↥K) S)) (adjoin F ((↑K : Set E) ∪ S))
have rw₂ : Eq (α := IntermediateField F E) (adjoin F ((↑K : Set E) ∪ S)) (adjoin F ((↑K : Set E) ∪ S))
Tactic: rw [← adjoin_self _ K, adjoin_adjoin_left, adjoin_self _ K]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Defs (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
K : IntermediateField F E
S : Set E
h : K ≤ adjoin F S
⊢ Eq (α := IntermediateField F E) (restrictScalars F (extendScalars h)) (restrictScalars F (L' := ↥K) (adjoin (↥K) S))
have rw : Eq (α := IntermediateField F E) (adjoin F S) (adjoin F ((↑K : Set E) ∪ S))
Tactic: rw [extendScalars_restrictScalars, restrictScalars_adjoin]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Defs (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
K : IntermediateField F E
S : Set E
⊢ restrictScalars F (L' := ↥K) (adjoin (↥K) S) = K ⊔ adjoin F S
have rw : adjoin F ((↑K : Set E) ∪ S) = K ⊔ adjoin F S
Tactic: rw [restrictScalars_adjoin, adjoin_union, adjoin_self]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Defs (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
K : IntermediateField F E
S : Set E
rw : adjoin F ((↑K : Set E) ∪ S) = K ⊔ adjoin F S
⊢ restrictScalars F (L' := ↥K) (adjoin (↥K) S) = K ⊔ adjoin F S
have rw₁ : adjoin F (↑K : Set E) ⊔ adjoin F S = K ⊔ adjoin F S
Tactic: rw [restrictScalars_adjoin, adjoin_union, adjoin_self]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Defs (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
K : IntermediateField F E
S : Set E
rw : adjoin F ((↑K : Set E) ∪ S) = K ⊔ adjoin F S
rw₁ : adjoin F (↑K : Set E) ⊔ adjoin F S = K ⊔ adjoin F S
⊢ restrictScalars F (L' := ↥K) (adjoin (↥K) S) = K ⊔ adjoin F S
have rw₂ : K ⊔ adjoin F S = K ⊔ adjoin F S
Tactic: rw [restrictScalars_adjoin, adjoin_union, adjoin_self]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Defs (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
ι : Sort u_3
f : ι → IntermediateField F E
⊢ Eq.{u_2 + 1} (α := IntermediateField F E) (⨆ (i : ι), f i) (adjoin F (⋃ (i : ι), (↑(f i) : Set E)))
have simp_rw : Eq.{u_2 + 1} (α := IntermediateField F E) (⨆ (i : ι), f i) (⨆ (i : ι), adjoin F (↑(f i) : Set E))
Tactic: simp_rw [adjoin_iUnion, adjoin_self]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Defs (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
L : Type u_3
L' : Type u_4
inst_3 : Field L
inst_4 : Field L'
inst_5 : Algebra F L
inst_6 : Algebra L E
inst_7 : Algebra F L'
inst_8 : Algebra L' E
inst_9 : IsScalarTower F L E
inst_10 : IsScalarTower F L' E
i : L ≃ₐ[F] L'
hi :
  Eq (α := (a : L) → E) (⇑(algebraMap L E) : (a : L) → E)
    (Function.comp.{u_3 + 1, u_4 + 1, u_2 + 1} (β := L') (⇑(algebraMap L' E) : (a : L') → E) (⇑i : (a : L) → L'))
S : Set E
K K' : IntermediateField F E
h : K.toSubfield = K'.toSubfield
⊢ K = K'
have h₁ : ∀ (x : E), x ∈ K ↔ x ∈ K'
Tactic: ext x
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Defs (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
L : Type u_3
L' : Type u_4
inst_3 : Field L
inst_4 : Field L'
inst_5 : Algebra F L
inst_6 : Algebra L E
inst_7 : Algebra F L'
inst_8 : Algebra L' E
inst_9 : IsScalarTower F L E
inst_10 : IsScalarTower F L' E
i : L ≃ₐ[F] L'
hi :
  Eq (α := (a : L) → E) (⇑(algebraMap L E) : (a : L) → E)
    (Function.comp.{u_3 + 1, u_4 + 1, u_2 + 1} (β := L') (⇑(algebraMap L' E) : (a : L') → E) (⇑i : (a : L) → L'))
S : Set E
K K' : IntermediateField F E
h : K.toSubfield = K'.toSubfield
x : E
⊢ x ∈ K ↔ x ∈ K'
have h₁ : x ∈ K.toSubfield ↔ x ∈ K'.toSubfield
Tactic: change x ∈ K.toSubfield ↔ x ∈ K'.toSubfield
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Defs (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
L : Type u_3
L' : Type u_4
inst_3 : Field L
inst_4 : Field L'
inst_5 : Algebra F L
inst_6 : Algebra L E
inst_7 : Algebra F L'
inst_8 : Algebra L' E
inst_9 : IsScalarTower F L E
inst_10 : IsScalarTower F L' E
i : L ≃ₐ[F] L'
hi :
  Eq (α := (a : L) → E) (⇑(algebraMap L E) : (a : L) → E)
    (Function.comp.{u_3 + 1, u_4 + 1, u_2 + 1} (β := L') (⇑(algebraMap L' E) : (a : L') → E) (⇑i : (a : L) → L'))
S : Set E
K K' : IntermediateField F E
h : K.toSubfield = K'.toSubfield
x : E
⊢ x ∈ K.toSubfield ↔ x ∈ K'.toSubfield
have h₁ : x ∈ K'.toSubfield ↔ x ∈ K'.toSubfield
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Defs (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
L : Type u_3
L' : Type u_4
inst_3 : Field L
inst_4 : Field L'
inst_5 : Algebra F L
inst_6 : Algebra L E
inst_7 : Algebra F L'
inst_8 : Algebra L' E
inst_9 : IsScalarTower F L E
inst_10 : IsScalarTower F L' E
i : L ≃ₐ[F] L'
hi :
  Eq (α := (a : L) → E) (⇑(algebraMap L E) : (a : L) → E)
    (Function.comp.{u_3 + 1, u_4 + 1, u_2 + 1} (β := L') (⇑(algebraMap L' E) : (a : L') → E) (⇑i : (a : L) → L'))
S : Set E
⊢ Eq (α := IntermediateField F E) (restrictScalars F (adjoin L S)) (restrictScalars F (adjoin L' S))
have apply_fun : Eq (α := Subfield E) (toSubfield (restrictScalars F (adjoin L S))) (toSubfield (restrictScalars F (adjoin L' S)))
Tactic: apply_fun toSubfield using (fun K K' h ↦ by
    ext x; change x ∈ K.toSubfield ↔ x ∈ K'.toSubfield; rw [h])
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Defs (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
p : (x : E) → Membership.mem (γ := IntermediateField F E) (adjoin F s) x → Prop
mem : ∀ (x : E) (hx : x ∈ s), p x ⋯
algebraMap : ∀ (x : F), p ((Algebra.algebraMap F E : (a : F) → E) x) ⋯
add :
  ∀ (x y : E) (hx : Membership.mem (γ := IntermediateField F E) (adjoin F s) x)
    (hy : Membership.mem (γ := IntermediateField F E) (adjoin F s) y), p x hx → p y hy → p (x + y) ⋯
inv : ∀ (x : E) (hx : Membership.mem (γ := IntermediateField F E) (adjoin F s) x), p x hx → p x⁻¹ ⋯
mul :
  ∀ (x y : E) (hx : Membership.mem (γ := IntermediateField F E) (adjoin F s) x)
    (hy : Membership.mem (γ := IntermediateField F E) (adjoin F s) y), p x hx → p y hy → p (x * y) ⋯
x : E
h : Membership.mem (γ := IntermediateField F E) (adjoin F s) x
⊢ p 1 ⋯
have simp_rw : p ((Algebra.algebraMap F E : (a : F) → E) 1) sorry
Tactic: simp_rw [← (Algebra.algebraMap F E).map_one]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Defs (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
p : (x : E) → Membership.mem (γ := IntermediateField F E) (adjoin F s) x → Prop
mem : ∀ (x : E) (hx : x ∈ s), p x ⋯
algebraMap : ∀ (x : F), p ((Algebra.algebraMap F E : (a : F) → E) x) ⋯
add :
  ∀ (x y : E) (hx : Membership.mem (γ := IntermediateField F E) (adjoin F s) x)
    (hy : Membership.mem (γ := IntermediateField F E) (adjoin F s) y), p x hx → p y hy → p (x + y) ⋯
inv : ∀ (x : E) (hx : Membership.mem (γ := IntermediateField F E) (adjoin F s) x), p x hx → p x⁻¹ ⋯
mul :
  ∀ (x y : E) (hx : Membership.mem (γ := IntermediateField F E) (adjoin F s) x)
    (hy : Membership.mem (γ := IntermediateField F E) (adjoin F s) y), p x hx → p y hy → p (x * y) ⋯
x_1 : E
h_1 : Membership.mem (γ := IntermediateField F E) (adjoin F s) x_1
x : E
h_2 :
  Membership.mem (γ := Subfield E)
    (Subfield.closure (Set.range.{u_2, u_1 + 1} (ι := F) (⇑(Algebra.algebraMap F E) : (a : F) → E) ∪ s)) x
h : p x h_2
⊢ p (-x) ⋯
have simp_rw : p (HMul.hMul (α := E) ((Algebra.algebraMap F E : (a : F) → E) (-1) : E) x) sorry
Tactic: simp_rw [← neg_one_smul F x, Algebra.smul_def]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Defs (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 : Semiring K
inst_4 : Algebra F K
s : Set E
φ₁ φ₂ : AlgHom.{u_1, u_2, u_3} F (↥(adjoin F s)) K
h :
  ∀ (x : E) (hx : x ∈ s),
    Eq.{u_3 + 1} (α := K)
      ((φ₁ : (a : ↥(adjoin F s)) → K)
          (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (adjoin F s) x) x ⋯) :
        K)
      ((φ₂ : (a : ↥(adjoin F s)) → K)
          (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (adjoin F s) x) x ⋯) :
        K)
x_1 : ↥(adjoin F s)
x : E
hx : Membership.mem (γ := IntermediateField F E) (adjoin F s) x
x_2 x_3 : E
h_1 : Membership.mem (γ := IntermediateField F E) (adjoin F s) x_2
h_2 : Membership.mem (γ := IntermediateField F E) (adjoin F s) x_3
h₁ :
  Eq.{u_3 + 1} (α := K)
    ((φ₁ : (a : ↥(adjoin F s)) → K)
        (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (adjoin F s) x) x_2 h_1) :
      K)
    ((φ₂ : (a : ↥(adjoin F s)) → K)
        (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (adjoin F s) x) x_2 h_1) :
      K)
h₂ :
  Eq.{u_3 + 1} (α := K)
    ((φ₁ : (a : ↥(adjoin F s)) → K)
        (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (adjoin F s) x) x_3 h_2) :
      K)
    ((φ₂ : (a : ↥(adjoin F s)) → K)
        (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (adjoin F s) x) x_3 h_2) :
      K)
⊢ Eq.{u_3 + 1} (α := K)
    ((φ₁ : (a : ↥(adjoin F s)) → K)
        (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (adjoin F s) x) (x_2 + x_3) ⋯) :
      K)
    ((φ₂ : (a : ↥(adjoin F s)) → K)
        (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (adjoin F s) x) (x_2 + x_3) ⋯) :
      K)
have h₃ : (φ₁ : (a : ↥(adjoin F s)) → K)
    (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (adjoin F s) x) (x_2 + x_3) sorry) =
  HAdd.hAdd (α := K) (β := K)
    ((φ₁ : (a : ↥(adjoin F s)) → K)
        (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (adjoin F s) x) x_2 h_1) :
      K)
    ((φ₁ : (a : ↥(adjoin F s)) → K)
        (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (adjoin F s) x) x_3 h_2) :
      K)
Tactic: convert! congr_arg₂ (· + ·) h₁ h₂