awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableClosure (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.EssFiniteType F E
d : (s : Finset E) → ℕ := fun (s : Finset E) ↦ finInsepDegree (↥(adjoin F (↑s : Set E))) E
Hexists :
  Set.Nonempty.{v} (α := Finset E)
    {s : Finset E | IsTranscendenceBasis.{v, u, v} (ι := ↥s) F (Subtype.val (p := fun (x : E) ↦ x ∈ s))}
s : Finset E :=
  Function.argminOn d
    {s : Finset E | IsTranscendenceBasis.{v, u, v} (ι := ↥s) F (Subtype.val (p := fun (x : E) ↦ x ∈ s))} Hexists
hs :
  Membership.mem (γ := Set (Finset E))
    {s : Finset E | IsTranscendenceBasis.{v, u, v} (ι := ↥s) F (Subtype.val (p := fun (x : E) ↦ x ∈ s))}
    (Function.argminOn d
      {s : Finset E | IsTranscendenceBasis.{v, u, v} (ι := ↥s) F (Subtype.val (p := fun (x : E) ↦ x ∈ s))} Hexists)
t : Finset E
ht :
  IsTranscendenceBasis.{v, u, v} (ι := { x : E // x ∈ (↑t : Set E) }) F
    (Subtype.val (p := fun (x : E) ↦ x ∈ (↑t : Set E)))
H :
  LT.lt.{v} (α := IntermediateField F E)
    ((fun (t : Set E) ↦
        (restrictScalars F (L' := ↥(adjoin F t)) (separableClosure (↥(adjoin F t)) E) : IntermediateField F E))
      (↑s : Set E))
    ((fun (t : Set E) ↦
        (restrictScalars F (L' := ↥(adjoin F t)) (separableClosure (↥(adjoin F t)) E) : IntermediateField F E))
      (↑t : Set E))
h :
  ∀ (x : E),
    (↑s : Set E) =
      Set.range (ι :=
        ↥(Function.argminOn d
            {s : Finset E | IsTranscendenceBasis.{v, u, v} (ι := ↥s) F (Subtype.val (p := fun (x : E) ↦ x ∈ s))}
            Hexists))
        (Subtype.val (p := fun (x : E) ↦
          x ∈
            Function.argminOn d
              {s : Finset E | IsTranscendenceBasis.{v, u, v} (ι := ↥s) F (Subtype.val (p := fun (x : E) ↦ x ∈ s))}
              Hexists))
⊢ Algebra.IsAlgebraic (↥(adjoin F (↑s : Set E))) E
have h₁ : ↥(adjoin F (↑s : Set E)) =
    ↥(adjoin F
        (Set.range (ι :=
          ↥(Function.argminOn d
              {s : Finset E | IsTranscendenceBasis.{v, u, v} (ι := ↥s) F (Subtype.val (p := fun (x : E) ↦ x ∈ s))}
              Hexists))
          (Subtype.val (p := fun (x : E) ↦
            x ∈
              Function.argminOn d
                {s : Finset E | IsTranscendenceBasis.{v, u, v} (ι := ↥s) F (Subtype.val (p := fun (x : E) ↦ x ∈ s))}
                Hexists)))) →
  (↑s : Set E) =
    Set.range (ι :=
      ↥(Function.argminOn d
          {s : Finset E | IsTranscendenceBasis.{v, u, v} (ι := ↥s) F (Subtype.val (p := fun (x : E) ↦ x ∈ s))} Hexists))
      (Subtype.val (p := fun (x : E) ↦
        x ∈
          Function.argminOn d
            {s : Finset E | IsTranscendenceBasis.{v, u, v} (ι := ↥s) F (Subtype.val (p := fun (x : E) ↦ x ∈ s))}
            Hexists))
Tactic: convert! hs.isAlgebraic_field
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableClosure (hypothesis)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.EssFiniteType F E
d : (s : Finset E) → ℕ := fun (s : Finset E) ↦ finInsepDegree (↥(adjoin F (↑s : Set E))) E
Hexists :
  Set.Nonempty.{v} (α := Finset E)
    {s : Finset E | IsTranscendenceBasis.{v, u, v} (ι := ↥s) F (Subtype.val (p := fun (x : E) ↦ x ∈ s))}
s : Finset E :=
  Function.argminOn d
    {s : Finset E | IsTranscendenceBasis.{v, u, v} (ι := ↥s) F (Subtype.val (p := fun (x : E) ↦ x ∈ s))} Hexists
hs :
  Membership.mem (γ := Set (Finset E))
    {s : Finset E | IsTranscendenceBasis.{v, u, v} (ι := ↥s) F (Subtype.val (p := fun (x : E) ↦ x ∈ s))}
    (Function.argminOn d
      {s : Finset E | IsTranscendenceBasis.{v, u, v} (ι := ↥s) F (Subtype.val (p := fun (x : E) ↦ x ∈ s))} Hexists)
t : Finset E
ht :
  IsTranscendenceBasis.{v, u, v} (ι := { x : E // x ∈ (↑t : Set E) }) F
    (Subtype.val (p := fun (x : E) ↦ x ∈ (↑t : Set E)))
H :
  LT.lt.{v} (α := IntermediateField F E)
    ((fun (t : Set E) ↦
        (restrictScalars F (L' := ↥(adjoin F t)) (separableClosure (↥(adjoin F t)) E) : IntermediateField F E))
      (↑s : Set E))
    ((fun (t : Set E) ↦
        (restrictScalars F (L' := ↥(adjoin F t)) (separableClosure (↥(adjoin F t)) E) : IntermediateField F E))
      (↑t : Set E))
⊢ False
have this : Module.Finite (↥(adjoin F (↑s : Set E))) E
Tactic: have : Module.Finite (adjoin F (s : Set E)) E := by
    apply +allowSynthFailures Algebra.finite_of_essFiniteType_of_isAlgebraic
    · exact .of_comp F _ _
    · convert! hs.isAlgebraic_field <;> simp [s]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableClosure (hypothesis)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.EssFiniteType F E
d : (s : Finset E) → ℕ := fun (s : Finset E) ↦ finInsepDegree (↥(adjoin F (↑s : Set E))) E
Hexists :
  Set.Nonempty.{v} (α := Finset E)
    {s : Finset E | IsTranscendenceBasis.{v, u, v} (ι := ↥s) F (Subtype.val (p := fun (x : E) ↦ x ∈ s))}
s : Finset E :=
  Function.argminOn d
    {s : Finset E | IsTranscendenceBasis.{v, u, v} (ι := ↥s) F (Subtype.val (p := fun (x : E) ↦ x ∈ s))} Hexists
hs :
  Membership.mem (γ := Set (Finset E))
    {s : Finset E | IsTranscendenceBasis.{v, u, v} (ι := ↥s) F (Subtype.val (p := fun (x : E) ↦ x ∈ s))}
    (Function.argminOn d
      {s : Finset E | IsTranscendenceBasis.{v, u, v} (ι := ↥s) F (Subtype.val (p := fun (x : E) ↦ x ∈ s))} Hexists)
t : Finset E
ht :
  IsTranscendenceBasis.{v, u, v} (ι := { x : E // x ∈ (↑t : Set E) }) F
    (Subtype.val (p := fun (x : E) ↦ x ∈ (↑t : Set E)))
H :
  LT.lt.{v} (α := IntermediateField F E)
    ((fun (t : Set E) ↦
        (restrictScalars F (L' := ↥(adjoin F t)) (separableClosure (↥(adjoin F t)) E) : IntermediateField F E))
      (↑s : Set E))
    ((fun (t : Set E) ↦
        (restrictScalars F (L' := ↥(adjoin F t)) (separableClosure (↥(adjoin F t)) E) : IntermediateField F E))
      (↑t : Set E))
this : Module.Finite (↥(adjoin F (↑s : Set E))) E
⊢ False
have this₁ : Module.Finite (↥(restrictScalars F (L' := ↥(adjoin F (↑s : Set E))) (separableClosure (↥(adjoin F (↑s : Set E))) E))) E
Tactic: have : Module.Finite ((separableClosure (adjoin F (s : Set E)) E).restrictScalars F) E :=
    inferInstanceAs <| Module.Finite (separableClosure (adjoin F (s : Set E)) E) E
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableClosure (hypothesis)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
⊢ sepDegree F ↥⊥ = 1
have this : Cardinal.lift.{u, v} (sepDegree F ↥⊥) = Cardinal.lift.{v, u} (sepDegree F F)
Tactic: have := lift_sepDegree_eq_of_equiv _ _ _ (botEquiv F E)
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableClosure (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
this : Cardinal.lift.{u, v} (sepDegree F ↥⊥) = Cardinal.lift.{v, u} (sepDegree F F)
⊢ sepDegree F ↥⊥ = 1
have rwa : ∀ (this : Cardinal.lift.{u, v} (sepDegree F ↥⊥) = Cardinal.lift.{v, u} 1), sepDegree F ↥⊥ = 1
Tactic: rwa [sepDegree_self, Cardinal.lift_one, ← Cardinal.lift_one.{v, u}, Cardinal.lift_inj] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableClosure (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
this : Cardinal.lift.{u, v} (sepDegree F ↥⊥) = Cardinal.lift.{v, u} (sepDegree F F)
rwa : ∀ (this : Cardinal.lift.{u, v} (sepDegree F ↥⊥) = Cardinal.lift.{v, u} 1), sepDegree F ↥⊥ = 1
⊢ sepDegree F ↥⊥ = 1
have rwa₁ : ∀ (this : Cardinal.lift.{u, v} (sepDegree F ↥⊥) = 1), sepDegree F ↥⊥ = 1
Tactic: rwa [sepDegree_self, Cardinal.lift_one, ← Cardinal.lift_one.{v, u}, Cardinal.lift_inj] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableClosure (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
this : Cardinal.lift.{u, v} (sepDegree F ↥⊥) = Cardinal.lift.{v, u} (sepDegree F F)
rwa : ∀ (this : Cardinal.lift.{u, v} (sepDegree F ↥⊥) = Cardinal.lift.{v, u} 1), sepDegree F ↥⊥ = 1
rwa₁ : ∀ (this : Cardinal.lift.{u, v} (sepDegree F ↥⊥) = 1), sepDegree F ↥⊥ = 1
⊢ sepDegree F ↥⊥ = 1
have rwa₂ : ∀ (this : Cardinal.lift.{u, v} (sepDegree F ↥⊥) = Cardinal.lift.{u, v} 1), sepDegree F ↥⊥ = 1
Tactic: rwa [sepDegree_self, Cardinal.lift_one, ← Cardinal.lift_one.{v, u}, Cardinal.lift_inj] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableClosure (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
this : Cardinal.lift.{u, v} (sepDegree F ↥⊥) = Cardinal.lift.{v, u} (sepDegree F F)
rwa : ∀ (this : Cardinal.lift.{u, v} (sepDegree F ↥⊥) = Cardinal.lift.{v, u} 1), sepDegree F ↥⊥ = 1
rwa₁ : ∀ (this : Cardinal.lift.{u, v} (sepDegree F ↥⊥) = 1), sepDegree F ↥⊥ = 1
rwa₂ : ∀ (this : Cardinal.lift.{u, v} (sepDegree F ↥⊥) = Cardinal.lift.{u, v} 1), sepDegree F ↥⊥ = 1
⊢ sepDegree F ↥⊥ = 1
have rwa₃ : ∀ (this : sepDegree F ↥⊥ = 1), sepDegree F ↥⊥ = 1
Tactic: rwa [sepDegree_self, Cardinal.lift_one, ← Cardinal.lift_one.{v, u}, Cardinal.lift_inj] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableClosure (hypothesis)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
⊢ insepDegree F ↥⊥ = 1
have this : Cardinal.lift.{u, v} (insepDegree F ↥⊥) = Cardinal.lift.{v, u} (insepDegree F F)
Tactic: have := lift_insepDegree_eq_of_equiv _ _ _ (botEquiv F E)
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableClosure (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
this : Cardinal.lift.{u, v} (insepDegree F ↥⊥) = Cardinal.lift.{v, u} (insepDegree F F)
⊢ insepDegree F ↥⊥ = 1
have rwa : ∀ (this : Cardinal.lift.{u, v} (insepDegree F ↥⊥) = Cardinal.lift.{v, u} 1), insepDegree F ↥⊥ = 1
Tactic: rwa [insepDegree_self, Cardinal.lift_one, ← Cardinal.lift_one.{v, u}, Cardinal.lift_inj] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableClosure (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
this : Cardinal.lift.{u, v} (insepDegree F ↥⊥) = Cardinal.lift.{v, u} (insepDegree F F)
rwa : ∀ (this : Cardinal.lift.{u, v} (insepDegree F ↥⊥) = Cardinal.lift.{v, u} 1), insepDegree F ↥⊥ = 1
⊢ insepDegree F ↥⊥ = 1
have rwa₁ : ∀ (this : Cardinal.lift.{u, v} (insepDegree F ↥⊥) = 1), insepDegree F ↥⊥ = 1
Tactic: rwa [insepDegree_self, Cardinal.lift_one, ← Cardinal.lift_one.{v, u}, Cardinal.lift_inj] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableClosure (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
this : Cardinal.lift.{u, v} (insepDegree F ↥⊥) = Cardinal.lift.{v, u} (insepDegree F F)
rwa : ∀ (this : Cardinal.lift.{u, v} (insepDegree F ↥⊥) = Cardinal.lift.{v, u} 1), insepDegree F ↥⊥ = 1
rwa₁ : ∀ (this : Cardinal.lift.{u, v} (insepDegree F ↥⊥) = 1), insepDegree F ↥⊥ = 1
⊢ insepDegree F ↥⊥ = 1
have rwa₂ : ∀ (this : Cardinal.lift.{u, v} (insepDegree F ↥⊥) = Cardinal.lift.{u, v} 1), insepDegree F ↥⊥ = 1
Tactic: rwa [insepDegree_self, Cardinal.lift_one, ← Cardinal.lift_one.{v, u}, Cardinal.lift_inj] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableClosure (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
this : Cardinal.lift.{u, v} (insepDegree F ↥⊥) = Cardinal.lift.{v, u} (insepDegree F F)
rwa : ∀ (this : Cardinal.lift.{u, v} (insepDegree F ↥⊥) = Cardinal.lift.{v, u} 1), insepDegree F ↥⊥ = 1
rwa₁ : ∀ (this : Cardinal.lift.{u, v} (insepDegree F ↥⊥) = 1), insepDegree F ↥⊥ = 1
rwa₂ : ∀ (this : Cardinal.lift.{u, v} (insepDegree F ↥⊥) = Cardinal.lift.{u, v} 1), insepDegree F ↥⊥ = 1
⊢ insepDegree F ↥⊥ = 1
have rwa₃ : ∀ (this : insepDegree F ↥⊥ = 1), insepDegree F ↥⊥ = 1
Tactic: rwa [insepDegree_self, Cardinal.lift_one, ← Cardinal.lift_one.{v, u}, Cardinal.lift_inj] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableClosure (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
⊢ finInsepDegree.{u, v} F ↥⊥ = 1
have rw : finInsepDegree F F = 1
Tactic: rw [finInsepDegree_eq_of_equiv _ _ _ (botEquiv F E), finInsepDegree_self]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableClosure (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
rw : finInsepDegree F F = 1
⊢ finInsepDegree.{u, v} F ↥⊥ = 1
have rw₁ : Eq (α := ℕ) 1 1
Tactic: rw [finInsepDegree_eq_of_equiv _ _ _ (botEquiv F E), finInsepDegree_self]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableClosure (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
⊢ finInsepDegree.{u, w} F ↥⊤ = finInsepDegree F K
have rw : (Cardinal.toNat : (a : Cardinal.{w}) → ℕ) (insepDegree F ↥⊤) = finInsepDegree F K
Tactic: rw [finInsepDegree_def', insepDegree_top, ← finInsepDegree_def']
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableClosure (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
rw : (Cardinal.toNat : (a : Cardinal.{w}) → ℕ) (insepDegree F ↥⊤) = finInsepDegree F K
⊢ finInsepDegree.{u, w} F ↥⊤ = finInsepDegree F K
have rw₁ : (Cardinal.toNat : (a : Cardinal.{w}) → ℕ) (insepDegree F K) = finInsepDegree F K
Tactic: rw [finInsepDegree_def', insepDegree_top, ← finInsepDegree_def']
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableClosure (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
rw : (Cardinal.toNat : (a : Cardinal.{w}) → ℕ) (insepDegree F ↥⊤) = finInsepDegree F K
rw₁ : (Cardinal.toNat : (a : Cardinal.{w}) → ℕ) (insepDegree F K) = finInsepDegree F K
⊢ finInsepDegree.{u, w} F ↥⊤ = finInsepDegree F K
have rw₂ : finInsepDegree F K = finInsepDegree F K
Tactic: rw [finInsepDegree_def', insepDegree_top, ← finInsepDegree_def']
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableClosure (hypothesis)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type v
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
this : Algebra ↥(separableClosure F K) ↥(restrictScalars F (separableClosure E K)) :=
  RingHom.toAlgebra (AlgHom.toRingHom (inclusion ⋯))
⊢ insepDegree E K ≤ insepDegree F K
have this₁ : IsScalarTower (↥(separableClosure F K)) (↥(restrictScalars F (separableClosure E K))) K
Tactic: have : IsScalarTower (separableClosure F K) ((separableClosure E K).restrictScalars F) K :=
    .of_algebraMap_eq' rfl
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableClosure (hypothesis)
Goal:
F : Type u
inst : Field F
K : Type v
inst_1 : Field K
inst_2 : Algebra F K
E₁ E₂ : IntermediateField F K
H : E₁ ≤ E₂
this : Algebra ↥E₁ ↥E₂ := (inclusion H).toAlgebra
⊢ insepDegree (↥E₂) K ≤ insepDegree (↥E₁) K
have this₁ : IsScalarTower (↥E₁) (↥E₂) K
Tactic: have : IsScalarTower E₁ E₂ K := .of_algebraMap_eq' rfl
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableClosure (hypothesis)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type v
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
inst_7 : Module.Finite F K
this : Algebra ↥(separableClosure F K) ↥(restrictScalars F (separableClosure E K)) :=
  RingHom.toAlgebra (AlgHom.toRingHom (inclusion ⋯))
⊢ finInsepDegree E K ≤ finInsepDegree F K
have this₁ : IsScalarTower (↥(separableClosure F K)) (↥(restrictScalars F (separableClosure E K))) K
Tactic: have : IsScalarTower (separableClosure F K) ((separableClosure E K).restrictScalars F) K :=
    .of_algebraMap_eq' rfl
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableClosure (hypothesis)
Goal:
F : Type u
inst : Field F
K : Type v
inst_1 : Field K
inst_2 : Algebra F K
E₁ E₂ : IntermediateField F K
H : E₁ ≤ E₂
inst_3 : Module.Finite (↥E₁) K
this : Algebra ↥E₁ ↥E₂ := (inclusion H).toAlgebra
⊢ finInsepDegree (↥E₂) K ≤ finInsepDegree (↥E₁) K
have this₁ : IsScalarTower (↥E₁) (↥E₂) K
Tactic: have : IsScalarTower E₁ E₂ K := .of_algebraMap_eq' rfl
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableClosure (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.IsSeparable F E
⊢ sepDegree F E = Module.rank F E
have rw : Module.rank F ↥(separableClosure F E) = Module.rank F E
Tactic: rw [sepDegree, (separableClosure.eq_top_iff F E).2 ‹_›, IntermediateField.rank_top']
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableClosure (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.IsSeparable F E
rw : Module.rank F ↥(separableClosure F E) = Module.rank F E
⊢ sepDegree F E = Module.rank F E
have rw₁ : Module.rank F ↥⊤ = Module.rank F E
Tactic: rw [sepDegree, (separableClosure.eq_top_iff F E).2 ‹_›, IntermediateField.rank_top']
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableClosure (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.IsSeparable F E
rw : Module.rank F ↥(separableClosure F E) = Module.rank F E
rw₁ : Module.rank F ↥⊤ = Module.rank F E
⊢ sepDegree F E = Module.rank F E
have rw₂ : Module.rank F E = Module.rank F E
Tactic: rw [sepDegree, (separableClosure.eq_top_iff F E).2 ‹_›, IntermediateField.rank_top']
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableClosure (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.IsSeparable F E
⊢ insepDegree F E = 1
have rw : Module.rank (↥(separableClosure F E)) E = 1
Tactic: rw [insepDegree, (separableClosure.eq_top_iff F E).2 ‹_›, IntermediateField.rank_top]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableClosure (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.IsSeparable F E
rw : Module.rank (↥(separableClosure F E)) E = 1
⊢ insepDegree F E = 1
have rw₁ : Module.rank (↥⊤) E = 1
Tactic: rw [insepDegree, (separableClosure.eq_top_iff F E).2 ‹_›, IntermediateField.rank_top]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableClosure (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.IsSeparable F E
rw : Module.rank (↥(separableClosure F E)) E = 1
rw₁ : Module.rank (↥⊤) E = 1
⊢ insepDegree F E = 1
have rw₂ : Eq.{v + 2} (α := Cardinal.{v}) 1 1
Tactic: rw [insepDegree, (separableClosure.eq_top_iff F E).2 ‹_›, IntermediateField.rank_top]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
i : E ≃ₐ[F] K
x : Algebra E K := (↑i : E →ₐ[F] K).toAlgebra
⊢ Algebra.IsAlgebraic E K
have isAlgebraic : ∀ (x_1 : K), IsAlgebraic E x_1
Tactic: constructor
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (hypothesis)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
i : E ≃ₐ[F] K
x_1 : Algebra E K := (↑i : E →ₐ[F] K).toAlgebra
x : K
⊢ IsAlgebraic E x
have h : IsAlgebraic.{v, w} E (A := K) ((algebraMap E K : (a : E) → K) (((↑i.symm : K →ₐ[F] E) : (a : K) → E) x : E) : K)
Tactic: have h := isAlgebraic_algebraMap (R := E) (A := K) (i.symm.toAlgHom x)
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (hypothesis)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
i : E ≃ₐ[F] K
x_1 : Algebra E K := (↑i : E →ₐ[F] K).toAlgebra
x : K
h : IsAlgebraic.{v, w} E (A := K) ((algebraMap E K : (a : E) → K) (((↑i.symm : K →ₐ[F] E) : (a : K) → E) x : E) : K)
⊢ IsAlgebraic E x
have h₁ : IsAlgebraic.{v, w} E (A := K) (((↑i : E →ₐ[F] K) : (a : E) → K) (((↑i.symm : K →ₐ[F] E) : (a : K) → E) x : E) : K)
Tactic: rw [show ∀ y : E, (algebraMap E K) y = i.toAlgHom y from fun y ↦ rfl] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (hypothesis)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
i : E ≃ₐ[F] K
x : Algebra E K := (↑i : E →ₐ[F] K).toAlgebra
⊢ AlgEquiv.{u, w, v} F (AlgebraicClosure K) (AlgebraicClosure E)
have this : Algebra.IsAlgebraic E K
Tactic: have : Algebra.IsAlgebraic E K := by
    constructor
    intro x
    have h := isAlgebraic_algebraMap (R := E) (A := K) (i.symm.toAlgHom x)
    rw [show ∀ y : E, (algebraMap E K) y = i.toAlgHom y from fun y ↦ rfl] at h
    simpa only [AlgEquiv.coe_algHom, AlgEquiv.apply_symm_apply] using h
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
i : E ≃ₐ[F] K
x : Algebra E K := (↑i : E →ₐ[F] K).toAlgebra
this : Algebra.IsAlgebraic E K
⊢ AlgEquiv.{u, w, v} F (AlgebraicClosure K) (AlgebraicClosure E)
have apply : AlgEquiv.{v, w, v} E (AlgebraicClosure K) (AlgebraicClosure E)
Tactic: apply AlgEquiv.restrictScalars (R := F) (S := E)
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
inst : Field F
⊢ finSepDegree F F = 1
have rw : Subsingleton.{u + 1} (Emb F F) ∧ Nonempty.{u + 1} (Emb F F)
Tactic: rw [finSepDegree, Nat.card_eq_one_iff_unique]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
inst : Field F
⊢ Subsingleton.{u + 1} (Emb F F) ∧ Nonempty.{u + 1} (Emb F F)
have left : Subsingleton.{u + 1} (Emb F F)
Tactic: constructor
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
inst : Field F
left : Subsingleton.{u + 1} (Emb F F)
⊢ Subsingleton.{u + 1} (Emb F F) ∧ Nonempty.{u + 1} (Emb F F)
have right : Nonempty.{u + 1} (Emb F F)
Tactic: constructor
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
⊢ finSepDegree.{u, v} F ↥⊥ = 1
have rw : finSepDegree F F = 1
Tactic: rw [finSepDegree_eq_of_equiv _ _ _ (botEquiv F E), finSepDegree_self]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
rw : finSepDegree F F = 1
⊢ finSepDegree.{u, v} F ↥⊥ = 1
have rw₁ : Eq (α := ℕ) 1 1
Tactic: rw [finSepDegree_eq_of_equiv _ _ _ (botEquiv F E), finSepDegree_self]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
H : Algebra.Transcendental F E
⊢ Infinite.{v + 1} (Emb F E)
have obtain : ∀ (ι : Type v) (x : ι → E) (hx : IsTranscendenceBasis F x), Infinite.{v + 1} (Emb F E)
Tactic: obtain ⟨ι, x, hx⟩ := exists_isTranscendenceBasis' F E
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (hypothesis)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
H : Algebra.Transcendental F E
ι : Type v
x : ι → E
hx : IsTranscendenceBasis F x
⊢ Infinite.{v + 1} (Emb F E)
have this : Algebra.IsAlgebraic (↥(adjoin F (Set.range x))) E
Tactic: have := hx.isAlgebraic_field
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
H : Algebra.Transcendental F E
ι : Type v
x : ι → E
hx : IsTranscendenceBasis F x
this : Algebra.IsAlgebraic (↥(adjoin F (Set.range x))) E
⊢ Infinite.{v + 1} (Emb F E)
have rw : Infinite.{v + 1} (Emb F ↥(adjoin F (Set.range x)) × Emb (↥(adjoin F (Set.range x))) E)
Tactic: rw [← (embProdEmbOfIsAlgebraic F (adjoin F (Set.range x)) E).infinite_iff]