awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
Goal:
F : Type u
inst : Field F
E : Type v
inst_1 : Field E
inst_2 : Algebra F E
s : Set E
⊢ max
      (max (Cardinal.lift.{u, v} #(↑(Set.range.{v, u + 1} (ι := F) (⇑(algebraMap F E) : (a : F) → E)) : Type v))
        (Cardinal.lift.{u, v} #(↑s : Type v)))
      ℵ₀ ≤
    max (max (Cardinal.lift.{v, u} #F) (Cardinal.lift.{u, v} #(↑s : Type v))) ℵ₀
have grw : max (max (Cardinal.lift.{v, u} #F) (Cardinal.lift.{u, v} #(↑s : Type v))) ℵ₀ ≤
  max (max (Cardinal.lift.{v, u} #F) (Cardinal.lift.{u, v} #(↑s : Type v))) ℵ₀
Tactic: grw [mk_range_le_lift]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x y : L
hx : IsIntegral K x
hy : IsIntegral K y
⊢ Algebra.IsAlgebraic.{u_1, u_2} K ↥K⟮x, y⟯
have hS : ∀ (x_1 : L), Membership.mem (γ := Set L) {x, y} x_1 → IsIntegral K x_1
Tactic: apply IntermediateField.isAlgebraic_adjoin
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (hypothesis)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x y : L
hx : IsIntegral K x
hy : IsIntegral K y
⊢ FiniteDimensional.{u_1, u_2} K ↥K⟮x, y⟯
have this : FiniteDimensional.{u_1, u_2} K ↥K⟮x⟯
Tactic: have := adjoin.finiteDimensional hx
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (hypothesis)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x y : L
hx : IsIntegral K x
hy : IsIntegral K y
this : FiniteDimensional.{u_1, u_2} K ↥K⟮x⟯
⊢ FiniteDimensional.{u_1, u_2} K ↥K⟮x, y⟯
have this₁ : FiniteDimensional.{u_1, u_2} K ↥K⟮y⟯
Tactic: have := adjoin.finiteDimensional hy
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x y : L
hx : IsIntegral K x
hy : IsIntegral K y
this_1 : FiniteDimensional.{u_1, u_2} K ↥K⟮x⟯
this : FiniteDimensional.{u_1, u_2} K ↥K⟮y⟯
⊢ FiniteDimensional.{u_1, u_2} K ↥K⟮x, y⟯
have rw : FiniteDimensional.{u_1, u_2} K ↥(K⟮x⟯ ⊔ K⟮y⟯)
Tactic: rw [← Set.singleton_union, adjoin_union]
-- 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
⊢ Membership.mem (γ := IntermediateField F E) (adjoin F S) x ↔
    ∃ (r : E),
      Membership.mem (γ := Subalgebra F E) (Algebra.adjoin F S) r ∧
        ∃ (s : E), Membership.mem (γ := Subalgebra F E) (Algebra.adjoin F S) s ∧ x = r / s
have simp_rw : Membership.mem (γ := IntermediateField F E)
    {
      toSubsemiring :=
        Subring.toSubsemiring
          (Subfield.toSubring
            (Subfield.closure (Set.range.{u_2, u_1 + 1} (ι := F) (⇑(algebraMap F E) : (a : F) → E) ∪ S))),
      algebraMap_mem' := sorry, inv_mem' := sorry }
    x ↔
  ∃ (r : E),
    Membership.mem (γ := Subalgebra F E) (Algebra.adjoin F S) r ∧
      ∃ (s : E), Membership.mem (γ := Subalgebra F E) (Algebra.adjoin F S) s ∧ x = r / s
Tactic: simp_rw [adjoin, mem_mk, Subring.mem_toSubsemiring, Subfield.mem_toSubring,
    Subfield.mem_closure_iff, ← Algebra.adjoin_eq_ring_closure, Subalgebra.mem_toSubring, eq_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 : Set E
x : E
simp_rw :
  Membership.mem (γ := IntermediateField F E)
      {
        toSubsemiring :=
          Subring.toSubsemiring
            (Subfield.toSubring
              (Subfield.closure (Set.range.{u_2, u_1 + 1} (ι := F) (⇑(algebraMap F E) : (a : F) → E) ∪ S))),
        algebraMap_mem' := ⋯, inv_mem' := ⋯ }
      x ↔
    ∃ (r : E),
      Membership.mem (γ := Subalgebra F E) (Algebra.adjoin F S) r ∧
        ∃ (s : E), Membership.mem (γ := Subalgebra F E) (Algebra.adjoin F S) s ∧ x = r / s
⊢ Membership.mem (γ := IntermediateField F E) (adjoin F S) x ↔
    ∃ (r : E),
      Membership.mem (γ := Subalgebra F E) (Algebra.adjoin F S) r ∧
        ∃ (s : E), Membership.mem (γ := Subalgebra F E) (Algebra.adjoin F S) s ∧ x = r / s
have simp_rw₁ : Membership.mem (γ := Subsemiring E)
    (Subring.toSubsemiring
        (Subfield.toSubring
          (Subfield.closure (Set.range.{u_2, u_1 + 1} (ι := F) (⇑(algebraMap F E) : (a : F) → E) ∪ S))) :
      Subsemiring E)
    x ↔
  ∃ (r : E),
    Membership.mem (γ := Subalgebra F E) (Algebra.adjoin F S) r ∧
      ∃ (s : E), Membership.mem (γ := Subalgebra F E) (Algebra.adjoin F S) s ∧ x = r / s
Tactic: simp_rw [adjoin, mem_mk, Subring.mem_toSubsemiring, Subfield.mem_toSubring,
    Subfield.mem_closure_iff, ← Algebra.adjoin_eq_ring_closure, Subalgebra.mem_toSubring, eq_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 : Set E
x : E
simp_rw :
  Membership.mem (γ := IntermediateField F E)
      {
        toSubsemiring :=
          Subring.toSubsemiring
            (Subfield.toSubring
              (Subfield.closure (Set.range.{u_2, u_1 + 1} (ι := F) (⇑(algebraMap F E) : (a : F) → E) ∪ S))),
        algebraMap_mem' := ⋯, inv_mem' := ⋯ }
      x ↔
    ∃ (r : E),
      Membership.mem (γ := Subalgebra F E) (Algebra.adjoin F S) r ∧
        ∃ (s : E), Membership.mem (γ := Subalgebra F E) (Algebra.adjoin F S) s ∧ x = r / s
simp_rw₁ :
  Membership.mem (γ := Subsemiring E)
      (Subring.toSubsemiring
          (Subfield.toSubring
            (Subfield.closure (Set.range.{u_2, u_1 + 1} (ι := F) (⇑(algebraMap F E) : (a : F) → E) ∪ S))) :
        Subsemiring E)
      x ↔
    ∃ (r : E),
      Membership.mem (γ := Subalgebra F E) (Algebra.adjoin F S) r ∧
        ∃ (s : E), Membership.mem (γ := Subalgebra F E) (Algebra.adjoin F S) s ∧ x = r / s
⊢ Membership.mem (γ := IntermediateField F E) (adjoin F S) x ↔
    ∃ (r : E),
      Membership.mem (γ := Subalgebra F E) (Algebra.adjoin F S) r ∧
        ∃ (s : E), Membership.mem (γ := Subalgebra F E) (Algebra.adjoin F S) s ∧ x = r / s
have simp_rw₂ : Membership.mem (γ := Subring E)
    (Subfield.toSubring (Subfield.closure (Set.range.{u_2, u_1 + 1} (ι := F) (⇑(algebraMap F E) : (a : F) → E) ∪ S)))
    x ↔
  ∃ (r : E),
    Membership.mem (γ := Subalgebra F E) (Algebra.adjoin F S) r ∧
      ∃ (s : E), Membership.mem (γ := Subalgebra F E) (Algebra.adjoin F S) s ∧ x = r / s
Tactic: simp_rw [adjoin, mem_mk, Subring.mem_toSubsemiring, Subfield.mem_toSubring,
    Subfield.mem_closure_iff, ← Algebra.adjoin_eq_ring_closure, Subalgebra.mem_toSubring, eq_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 : Set E
x : E
simp_rw :
  Membership.mem (γ := IntermediateField F E)
      {
        toSubsemiring :=
          Subring.toSubsemiring
            (Subfield.toSubring
              (Subfield.closure (Set.range.{u_2, u_1 + 1} (ι := F) (⇑(algebraMap F E) : (a : F) → E) ∪ S))),
        algebraMap_mem' := ⋯, inv_mem' := ⋯ }
      x ↔
    ∃ (r : E),
      Membership.mem (γ := Subalgebra F E) (Algebra.adjoin F S) r ∧
        ∃ (s : E), Membership.mem (γ := Subalgebra F E) (Algebra.adjoin F S) s ∧ x = r / s
simp_rw₁ :
  Membership.mem (γ := Subsemiring E)
      (Subring.toSubsemiring
          (Subfield.toSubring
            (Subfield.closure (Set.range.{u_2, u_1 + 1} (ι := F) (⇑(algebraMap F E) : (a : F) → E) ∪ S))) :
        Subsemiring E)
      x ↔
    ∃ (r : E),
      Membership.mem (γ := Subalgebra F E) (Algebra.adjoin F S) r ∧
        ∃ (s : E), Membership.mem (γ := Subalgebra F E) (Algebra.adjoin F S) s ∧ x = r / s
simp_rw₂ :
  Membership.mem (γ := Subring E)
      (Subfield.toSubring (Subfield.closure (Set.range.{u_2, u_1 + 1} (ι := F) (⇑(algebraMap F E) : (a : F) → E) ∪ S)))
      x ↔
    ∃ (r : E),
      Membership.mem (γ := Subalgebra F E) (Algebra.adjoin F S) r ∧
        ∃ (s : E), Membership.mem (γ := Subalgebra F E) (Algebra.adjoin F S) s ∧ x = r / s
⊢ Membership.mem (γ := IntermediateField F E) (adjoin F S) x ↔
    ∃ (r : E),
      Membership.mem (γ := Subalgebra F E) (Algebra.adjoin F S) r ∧
        ∃ (s : E), Membership.mem (γ := Subalgebra F E) (Algebra.adjoin F S) s ∧ x = r / s
have simp_rw₃ : Membership.mem (γ := Subfield E)
    (Subfield.closure (Set.range.{u_2, u_1 + 1} (ι := F) (⇑(algebraMap F E) : (a : F) → E) ∪ S)) x ↔
  ∃ (r : E),
    Membership.mem (γ := Subalgebra F E) (Algebra.adjoin F S) r ∧
      ∃ (s : E), Membership.mem (γ := Subalgebra F E) (Algebra.adjoin F S) s ∧ x = r / s
Tactic: simp_rw [adjoin, mem_mk, Subring.mem_toSubsemiring, Subfield.mem_toSubring,
    Subfield.mem_closure_iff, ← Algebra.adjoin_eq_ring_closure, Subalgebra.mem_toSubring, eq_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 : Set E
x : E
simp_rw :
  Membership.mem (γ := IntermediateField F E)
      {
        toSubsemiring :=
          Subring.toSubsemiring
            (Subfield.toSubring
              (Subfield.closure (Set.range.{u_2, u_1 + 1} (ι := F) (⇑(algebraMap F E) : (a : F) → E) ∪ S))),
        algebraMap_mem' := ⋯, inv_mem' := ⋯ }
      x ↔
    ∃ (r : E),
      Membership.mem (γ := Subalgebra F E) (Algebra.adjoin F S) r ∧
        ∃ (s : E), Membership.mem (γ := Subalgebra F E) (Algebra.adjoin F S) s ∧ x = r / s
simp_rw₁ :
  Membership.mem (γ := Subsemiring E)
      (Subring.toSubsemiring
          (Subfield.toSubring
            (Subfield.closure (Set.range.{u_2, u_1 + 1} (ι := F) (⇑(algebraMap F E) : (a : F) → E) ∪ S))) :
        Subsemiring E)
      x ↔
    ∃ (r : E),
      Membership.mem (γ := Subalgebra F E) (Algebra.adjoin F S) r ∧
        ∃ (s : E), Membership.mem (γ := Subalgebra F E) (Algebra.adjoin F S) s ∧ x = r / s
simp_rw₂ :
  Membership.mem (γ := Subring E)
      (Subfield.toSubring (Subfield.closure (Set.range.{u_2, u_1 + 1} (ι := F) (⇑(algebraMap F E) : (a : F) → E) ∪ S)))
      x ↔
    ∃ (r : E),
      Membership.mem (γ := Subalgebra F E) (Algebra.adjoin F S) r ∧
        ∃ (s : E), Membership.mem (γ := Subalgebra F E) (Algebra.adjoin F S) s ∧ x = r / s
simp_rw₃ :
  Membership.mem (γ := Subfield E)
      (Subfield.closure (Set.range.{u_2, u_1 + 1} (ι := F) (⇑(algebraMap F E) : (a : F) → E) ∪ S)) x ↔
    ∃ (r : E),
      Membership.mem (γ := Subalgebra F E) (Algebra.adjoin F S) r ∧
        ∃ (s : E), Membership.mem (γ := Subalgebra F E) (Algebra.adjoin F S) s ∧ x = r / s
⊢ Membership.mem (γ := IntermediateField F E) (adjoin F S) x ↔
    ∃ (r : E),
      Membership.mem (γ := Subalgebra F E) (Algebra.adjoin F S) r ∧
        ∃ (s : E), Membership.mem (γ := Subalgebra F E) (Algebra.adjoin F S) s ∧ x = r / s
have simp_rw₄ : (∃ (y : E),
    Membership.mem (γ := Subring E)
        (Subring.closure (Set.range.{u_2, u_1 + 1} (ι := F) (⇑(algebraMap F E) : (a : F) → E) ∪ S)) y ∧
      ∃ (z : E),
        Membership.mem (γ := Subring E)
            (Subring.closure (Set.range.{u_2, u_1 + 1} (ι := F) (⇑(algebraMap F E) : (a : F) → E) ∪ S)) z ∧
          y / z = x) ↔
  ∃ (r : E),
    Membership.mem (γ := Subalgebra F E) (Algebra.adjoin F S) r ∧
      ∃ (s : E), Membership.mem (γ := Subalgebra F E) (Algebra.adjoin F S) s ∧ x = r / s
Tactic: simp_rw [adjoin, mem_mk, Subring.mem_toSubsemiring, Subfield.mem_toSubring,
    Subfield.mem_closure_iff, ← Algebra.adjoin_eq_ring_closure, Subalgebra.mem_toSubring, eq_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 : Set E
x : E
simp_rw :
  Membership.mem (γ := IntermediateField F E)
      {
        toSubsemiring :=
          Subring.toSubsemiring
            (Subfield.toSubring
              (Subfield.closure (Set.range.{u_2, u_1 + 1} (ι := F) (⇑(algebraMap F E) : (a : F) → E) ∪ S))),
        algebraMap_mem' := ⋯, inv_mem' := ⋯ }
      x ↔
    ∃ (r : E),
      Membership.mem (γ := Subalgebra F E) (Algebra.adjoin F S) r ∧
        ∃ (s : E), Membership.mem (γ := Subalgebra F E) (Algebra.adjoin F S) s ∧ x = r / s
simp_rw₁ :
  Membership.mem (γ := Subsemiring E)
      (Subring.toSubsemiring
          (Subfield.toSubring
            (Subfield.closure (Set.range.{u_2, u_1 + 1} (ι := F) (⇑(algebraMap F E) : (a : F) → E) ∪ S))) :
        Subsemiring E)
      x ↔
    ∃ (r : E),
      Membership.mem (γ := Subalgebra F E) (Algebra.adjoin F S) r ∧
        ∃ (s : E), Membership.mem (γ := Subalgebra F E) (Algebra.adjoin F S) s ∧ x = r / s
simp_rw₂ :
  Membership.mem (γ := Subring E)
      (Subfield.toSubring (Subfield.closure (Set.range.{u_2, u_1 + 1} (ι := F) (⇑(algebraMap F E) : (a : F) → E) ∪ S)))
      x ↔
    ∃ (r : E),
      Membership.mem (γ := Subalgebra F E) (Algebra.adjoin F S) r ∧
        ∃ (s : E), Membership.mem (γ := Subalgebra F E) (Algebra.adjoin F S) s ∧ x = r / s
simp_rw₃ :
  Membership.mem (γ := Subfield E)
      (Subfield.closure (Set.range.{u_2, u_1 + 1} (ι := F) (⇑(algebraMap F E) : (a : F) → E) ∪ S)) x ↔
    ∃ (r : E),
      Membership.mem (γ := Subalgebra F E) (Algebra.adjoin F S) r ∧
        ∃ (s : E), Membership.mem (γ := Subalgebra F E) (Algebra.adjoin F S) s ∧ x = r / s
simp_rw₄ :
  (∃ (y : E),
      Membership.mem (γ := Subring E)
          (Subring.closure (Set.range.{u_2, u_1 + 1} (ι := F) (⇑(algebraMap F E) : (a : F) → E) ∪ S)) y ∧
        ∃ (z : E),
          Membership.mem (γ := Subring E)
              (Subring.closure (Set.range.{u_2, u_1 + 1} (ι := F) (⇑(algebraMap F E) : (a : F) → E) ∪ S)) z ∧
            y / z = x) ↔
    ∃ (r : E),
      Membership.mem (γ := Subalgebra F E) (Algebra.adjoin F S) r ∧
        ∃ (s : E), Membership.mem (γ := Subalgebra F E) (Algebra.adjoin F S) s ∧ x = r / s
⊢ Membership.mem (γ := IntermediateField F E) (adjoin F S) x ↔
    ∃ (r : E),
      Membership.mem (γ := Subalgebra F E) (Algebra.adjoin F S) r ∧
        ∃ (s : E), Membership.mem (γ := Subalgebra F E) (Algebra.adjoin F S) s ∧ x = r / s
have simp_rw₅ : (∃ (y : E),
    Membership.mem (γ := Subring E) (Subalgebra.toSubring (Algebra.adjoin F S)) y ∧
      ∃ (z : E), Membership.mem (γ := Subring E) (Subalgebra.toSubring (Algebra.adjoin F S)) z ∧ y / z = x) ↔
  ∃ (r : E),
    Membership.mem (γ := Subalgebra F E) (Algebra.adjoin F S) r ∧
      ∃ (s : E), Membership.mem (γ := Subalgebra F E) (Algebra.adjoin F S) s ∧ x = r / s
Tactic: simp_rw [adjoin, mem_mk, Subring.mem_toSubsemiring, Subfield.mem_toSubring,
    Subfield.mem_closure_iff, ← Algebra.adjoin_eq_ring_closure, Subalgebra.mem_toSubring, eq_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 : IntermediateField F E
⊢ (S ⊔ T).toSubfield = S.toSubfield ⊔ T.toSubfield
have rw : (S ⊔ T).toSubfield = Subfield.closure ((↑S.toSubfield : Set E) ∪ (↑T.toSubfield : Set E))
Tactic: rw [← S.toSubfield.closure_eq, ← T.toSubfield.closure_eq, ← Subfield.closure_union]
-- 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 : IntermediateField F E
⊢ (S ⊔ T).toSubfield = Subfield.closure ((↑S.toSubfield : Set E) ∪ (↑T.toSubfield : Set E))
have simp_rw : Eq (α := Subfield E)
  (Subfield.closure
    (Set.range.{u_2, u_1 + 1} (ι := F) (⇑(algebraMap F E) : (a : F) → E) ∪ ((↑S : Set E) ∪ (↑T : Set E))))
  (Subfield.closure ((↑S : Set E) ∪ (↑T : Set E)))
Tactic: simp_rw [sup_def, adjoin_toSubfield, coe_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
S T : IntermediateField F E
⊢ Eq (α := Subfield E)
    (Subfield.closure
      (Set.range.{u_2, u_1 + 1} (ι := F) (⇑(algebraMap F E) : (a : F) → E) ∪ ((↑S : Set E) ∪ (↑T : Set E))))
    (Subfield.closure ((↑S : Set E) ∪ (↑T : Set E)))
have e_s : Set.range.{u_2, u_1 + 1} (ι := F) (⇑(algebraMap F E) : (a : F) → E) ∪ ((↑S : Set E) ∪ (↑T : Set E)) =
  (↑S : Set E) ∪ (↑T : Set E)
Tactic: congr 1
-- 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 : IntermediateField F E
⊢ Set.range.{u_2, u_1 + 1} (ι := F) (⇑(algebraMap F E) : (a : F) → E) ∪ ((↑S : Set E) ∪ (↑T : Set E)) =
    (↑S : Set E) ∪ (↑T : Set E)
have e_s : Set.range.{u_2, u_1 + 1} (ι := F) (⇑(algebraMap F E) : (a : F) → E) ⊆ (↑S : Set E) ∪ (↑T : Set E)
Tactic: rw [Set.union_eq_right]
-- 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 (IntermediateField F E)
hS : S.Nonempty
⊢ toSubfield '' S = Subfield.closure '' SetLike.coe '' S
have rw : toSubfield '' S = (fun (x : IntermediateField F E) ↦ Subfield.closure (↑x : Set E)) '' S
Tactic: rw [Set.image_image]
-- 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 (IntermediateField F E)
hS : S.Nonempty
⊢ toSubfield '' S = (fun (x : IntermediateField F E) ↦ Subfield.closure (↑x : Set E)) '' S
have h : ∀ x ∈ S, x.toSubfield = Subfield.closure (↑x : Set E)
Tactic: congr! with x
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Defs (hypothesis)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S : Set (IntermediateField F E)
hS : S.Nonempty
⊢ (sSup S).toSubfield = sSup (toSubfield '' S)
have h : toSubfield '' S = Subfield.closure '' SetLike.coe '' S
Tactic: have h : toSubfield '' S = Subfield.closure '' SetLike.coe '' S := by
    rw [Set.image_image]
    congr! with x
    exact x.toSubfield.closure_eq.symm
-- 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 (IntermediateField F E)
hS : S.Nonempty
h : toSubfield '' S = Subfield.closure '' SetLike.coe '' S
⊢ (sSup S).toSubfield = sSup (toSubfield '' S)
have rw : Eq (α := Subfield E)
  (Subfield.closure (Set.range.{u_2, u_1 + 1} (ι := F) (⇑(algebraMap F E) : (a : F) → E) ∪ ⋃₀ (SetLike.coe '' S)))
  (Subfield.closure (⋃₀ (SetLike.coe '' S)))
Tactic: rw [h, sSup_image, ← Subfield.closure_sUnion, sSup_def, adjoin_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
S : Set (IntermediateField F E)
hS : S.Nonempty
h : toSubfield '' S = Subfield.closure '' SetLike.coe '' S
⊢ Eq (α := Subfield E)
    (Subfield.closure (Set.range.{u_2, u_1 + 1} (ι := F) (⇑(algebraMap F E) : (a : F) → E) ∪ ⋃₀ (SetLike.coe '' S)))
    (Subfield.closure (⋃₀ (SetLike.coe '' S)))
have e_s : Set.range.{u_2, u_1 + 1} (ι := F) (⇑(algebraMap F E) : (a : F) → E) ∪ ⋃₀ (SetLike.coe '' S) = ⋃₀ (SetLike.coe '' S)
Tactic: congr 1
-- 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 (IntermediateField F E)
hS : S.Nonempty
h : toSubfield '' S = Subfield.closure '' SetLike.coe '' S
⊢ Set.range.{u_2, u_1 + 1} (ι := F) (⇑(algebraMap F E) : (a : F) → E) ∪ ⋃₀ (SetLike.coe '' S) = ⋃₀ (SetLike.coe '' S)
have e_s : Set.range.{u_2, u_1 + 1} (ι := F) (⇑(algebraMap F E) : (a : F) → E) ⊆ ⋃₀ (SetLike.coe '' S)
Tactic: rw [Set.union_eq_right]
-- 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 (IntermediateField F E)
hS : S.Nonempty
h : toSubfield '' S = Subfield.closure '' SetLike.coe '' S
x : F
⊢ Membership.mem (α := E) (⋃₀ (SetLike.coe '' S)) ((algebraMap F E : (a : F) → E) x : E)
have e_s : ∀ (y : IntermediateField F E) (hy : y ∈ S),
  Membership.mem (α := E) (⋃₀ (SetLike.coe '' S)) ((algebraMap F E : (a : F) → E) x : E)
Tactic: obtain ⟨y, hy⟩ := hS
Cleared hypotheses: hS
-- 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 (IntermediateField F E)
h : toSubfield '' S = Subfield.closure '' SetLike.coe '' S
x : F
y : IntermediateField F E
hy : y ∈ S
⊢ Membership.mem (α := E) (⋃₀ (SetLike.coe '' S)) ((algebraMap F E : (a : F) → E) x : E)
have e_s : ∃ a ∈ S, Membership.mem (α := E) a ((algebraMap F E : (a : F) → E) x : E)
Tactic: simp only [Set.mem_sUnion, Set.mem_image, exists_exists_and_eq_and, SetLike.mem_coe]
-- 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
x : ↥⊥
⊢ Eq (α := E) ((algebraMap (↥⊥) E : (a : ↥⊥) → E) x : E)
    ((algebraMap F E : (a : F) → E) ((algebraMap (↥⊥) F : (a : ↥⊥) → F) x : F) : E)
have obtain : ∀ (y : F),
  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)
Tactic: obtain ⟨y, rfl⟩ := (botEquiv F E).symm.surjective x
Cleared hypotheses: 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
y : F
⊢ 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)
      (((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)
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)
⊢ 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)
      (((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)
Tactic: rw [coe_algebraMap_over_bot, (botEquiv F E).apply_symm_apply, botEquiv_symm,
        IsScalarTower.algebraMap_apply F (⊥ : IntermediateField F E) E]