awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.Extension (goal)
Goal:
F : Type u_1
E : Type u_2
K : Type u_3
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra F K
S : Set E
L₁ L₂ : Lifts F E K
c : Set (Lifts F E K)
hc_1 : IsChain (fun (x1 x2 : Lifts F E K) ↦ x1 ≤ x2) c
t : (i : (↑(insert ⊥ c) : Type (max u_2 u_3))) → IntermediateField F E :=
  fun (i : (↑(insert ⊥ c) : Type (max u_2 u_3))) ↦ (↑i : Lifts F E K).carrier
hc : IsChain (fun (x1 x2 : Lifts F E K) ↦ x1 ≤ x2) (insert ⊥ c)
dir : Directed (fun (x1 x2 : IntermediateField F E) ↦ x1 ≤ x2) t
i j : (↑(insert ⊥ c) : Type (max u_2 u_3))
h :
  LE.le.{u_2} (α := Subalgebra F E) ((fun (x : (↑(insert ⊥ c) : Type (max u_2 u_3))) ↦ (t x).toSubalgebra) i)
    ((fun (x : (↑(insert ⊥ c) : Type (max u_2 u_3))) ↦ (t x).toSubalgebra) j)
x : ↥(↑i : Lifts F E K).carrier
hji : (↑j : Lifts F E K) ≤ (↑i : Lifts F E K)
⊢ Eq.{u_3 + 1} (α := K) (((↑i : Lifts F E K).emb : (a : ↥(↑i : Lifts F E K).carrier) → K) x : K)
    (((↑j : Lifts F E K).emb : (a : ↥(t j)) → K)
        ((inclusion h : (a : ↥(↑i : Lifts F E K).carrier) → ↥(t j)) x : ↥(t j)) :
      K)
have rw : Eq.{u_3 + 1} (α := K) (((↑i : Lifts F E K).emb : (a : ↥(↑i : Lifts F E K).carrier) → K) x : K)
  (((↑i : Lifts F E K).emb : (a : ↥(↑i : Lifts F E K).carrier) → K)
      ((inclusion sorry : (a : ↥(↑j : Lifts F E K).carrier) → ↥(↑i : Lifts F E K).carrier)
          ((inclusion h : (a : ↥(t i)) → ↥(t j)) x) :
        ↥(↑i : Lifts F E K).carrier) :
    K)
Tactic: rw [← hji.snd (inclusion h x), inclusion_inclusion, inclusion_self, AlgHom.id_apply x]
-- Lean 4 proof step from Mathlib.FieldTheory.Extension (goal)
Goal:
F : Type u_1
E : Type u_2
K : Type u_3
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra F K
S : Set E
L₁ L₂ : Lifts F E K
c : Set (Lifts F E K)
hc_1 : IsChain (fun (x1 x2 : Lifts F E K) ↦ x1 ≤ x2) c
t : (i : (↑(insert ⊥ c) : Type (max u_2 u_3))) → IntermediateField F E :=
  fun (i : (↑(insert ⊥ c) : Type (max u_2 u_3))) ↦ (↑i : Lifts F E K).carrier
hc : IsChain (fun (x1 x2 : Lifts F E K) ↦ x1 ≤ x2) (insert ⊥ c)
dir : Directed (fun (x1 x2 : IntermediateField F E) ↦ x1 ≤ x2) t
i j : (↑(insert ⊥ c) : Type (max u_2 u_3))
h :
  LE.le.{u_2} (α := Subalgebra F E) ((fun (x : (↑(insert ⊥ c) : Type (max u_2 u_3))) ↦ (t x).toSubalgebra) i)
    ((fun (x : (↑(insert ⊥ c) : Type (max u_2 u_3))) ↦ (t x).toSubalgebra) j)
x : ↥(↑i : Lifts F E K).carrier
hji : (↑j : Lifts F E K) ≤ (↑i : Lifts F E K)
rw :
  Eq.{u_3 + 1} (α := K) (((↑i : Lifts F E K).emb : (a : ↥(↑i : Lifts F E K).carrier) → K) x : K)
    (((↑i : Lifts F E K).emb : (a : ↥(↑i : Lifts F E K).carrier) → K)
        ((inclusion ⋯ : (a : ↥(↑j : Lifts F E K).carrier) → ↥(↑i : Lifts F E K).carrier)
            ((inclusion h : (a : ↥(t i)) → ↥(t j)) x) :
          ↥(↑i : Lifts F E K).carrier) :
      K)
⊢ Eq.{u_3 + 1} (α := K) (((↑i : Lifts F E K).emb : (a : ↥(↑i : Lifts F E K).carrier) → K) x : K)
    (((↑j : Lifts F E K).emb : (a : ↥(t j)) → K)
        ((inclusion h : (a : ↥(↑i : Lifts F E K).carrier) → ↥(t j)) x : ↥(t j)) :
      K)
have rw₁ : Eq.{u_3 + 1} (α := K) (((↑i : Lifts F E K).emb : (a : ↥(↑i : Lifts F E K).carrier) → K) x : K)
  (((↑i : Lifts F E K).emb : (a : ↥(↑i : Lifts F E K).carrier) → K)
      ((inclusion sorry : (a : ↥(t i)) → ↥(↑i : Lifts F E K).carrier) x : ↥(↑i : Lifts F E K).carrier) :
    K)
Tactic: rw [← hji.snd (inclusion h x), inclusion_inclusion, inclusion_self, AlgHom.id_apply x]
-- Lean 4 proof step from Mathlib.FieldTheory.Extension (goal)
Goal:
F : Type u_1
E : Type u_2
K : Type u_3
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra F K
S : Set E
L₁ L₂ : Lifts F E K
c : Set (Lifts F E K)
hc_1 : IsChain (fun (x1 x2 : Lifts F E K) ↦ x1 ≤ x2) c
t : (i : (↑(insert ⊥ c) : Type (max u_2 u_3))) → IntermediateField F E :=
  fun (i : (↑(insert ⊥ c) : Type (max u_2 u_3))) ↦ (↑i : Lifts F E K).carrier
hc : IsChain (fun (x1 x2 : Lifts F E K) ↦ x1 ≤ x2) (insert ⊥ c)
dir : Directed (fun (x1 x2 : IntermediateField F E) ↦ x1 ≤ x2) t
i j : (↑(insert ⊥ c) : Type (max u_2 u_3))
h :
  LE.le.{u_2} (α := Subalgebra F E) ((fun (x : (↑(insert ⊥ c) : Type (max u_2 u_3))) ↦ (t x).toSubalgebra) i)
    ((fun (x : (↑(insert ⊥ c) : Type (max u_2 u_3))) ↦ (t x).toSubalgebra) j)
x : ↥(↑i : Lifts F E K).carrier
hji : (↑j : Lifts F E K) ≤ (↑i : Lifts F E K)
rw :
  Eq.{u_3 + 1} (α := K) (((↑i : Lifts F E K).emb : (a : ↥(↑i : Lifts F E K).carrier) → K) x : K)
    (((↑i : Lifts F E K).emb : (a : ↥(↑i : Lifts F E K).carrier) → K)
        ((inclusion ⋯ : (a : ↥(↑j : Lifts F E K).carrier) → ↥(↑i : Lifts F E K).carrier)
            ((inclusion h : (a : ↥(t i)) → ↥(t j)) x) :
          ↥(↑i : Lifts F E K).carrier) :
      K)
rw₁ :
  Eq.{u_3 + 1} (α := K) (((↑i : Lifts F E K).emb : (a : ↥(↑i : Lifts F E K).carrier) → K) x : K)
    (((↑i : Lifts F E K).emb : (a : ↥(↑i : Lifts F E K).carrier) → K)
        ((inclusion ⋯ : (a : ↥(t i)) → ↥(↑i : Lifts F E K).carrier) x : ↥(↑i : Lifts F E K).carrier) :
      K)
⊢ Eq.{u_3 + 1} (α := K) (((↑i : Lifts F E K).emb : (a : ↥(↑i : Lifts F E K).carrier) → K) x : K)
    (((↑j : Lifts F E K).emb : (a : ↥(t j)) → K)
        ((inclusion h : (a : ↥(↑i : Lifts F E K).carrier) → ↥(t j)) x : ↥(t j)) :
      K)
have rw₂ : Eq.{u_3 + 1} (α := K) (((↑i : Lifts F E K).emb : (a : ↥(↑i : Lifts F E K).carrier) → K) x : K)
  (((↑i : Lifts F E K).emb : (a : ↥(↑i : Lifts F E K).carrier) → K)
      ((AlgHom.id F ↥(t i) : (a : ↥(t i)) → ↥(↑i : Lifts F E K).carrier) x : ↥(↑i : Lifts F E K).carrier) :
    K)
Tactic: rw [← hji.snd (inclusion h x), inclusion_inclusion, inclusion_self, AlgHom.id_apply x]
-- Lean 4 proof step from Mathlib.FieldTheory.Extension (goal)
Goal:
F : Type u_1
E : Type u_2
K : Type u_3
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra F K
S : Set E
L₁ L₂ : Lifts F E K
c : Set (Lifts F E K)
hc_1 : IsChain (fun (x1 x2 : Lifts F E K) ↦ x1 ≤ x2) c
t : (i : (↑(insert ⊥ c) : Type (max u_2 u_3))) → IntermediateField F E :=
  fun (i : (↑(insert ⊥ c) : Type (max u_2 u_3))) ↦ (↑i : Lifts F E K).carrier
hc : IsChain (fun (x1 x2 : Lifts F E K) ↦ x1 ≤ x2) (insert ⊥ c)
dir : Directed (fun (x1 x2 : IntermediateField F E) ↦ x1 ≤ x2) t
i j : (↑(insert ⊥ c) : Type (max u_2 u_3))
h :
  LE.le.{u_2} (α := Subalgebra F E) ((fun (x : (↑(insert ⊥ c) : Type (max u_2 u_3))) ↦ (t x).toSubalgebra) i)
    ((fun (x : (↑(insert ⊥ c) : Type (max u_2 u_3))) ↦ (t x).toSubalgebra) j)
x : ↥(↑i : Lifts F E K).carrier
hji : (↑j : Lifts F E K) ≤ (↑i : Lifts F E K)
rw :
  Eq.{u_3 + 1} (α := K) (((↑i : Lifts F E K).emb : (a : ↥(↑i : Lifts F E K).carrier) → K) x : K)
    (((↑i : Lifts F E K).emb : (a : ↥(↑i : Lifts F E K).carrier) → K)
        ((inclusion ⋯ : (a : ↥(↑j : Lifts F E K).carrier) → ↥(↑i : Lifts F E K).carrier)
            ((inclusion h : (a : ↥(t i)) → ↥(t j)) x) :
          ↥(↑i : Lifts F E K).carrier) :
      K)
rw₁ :
  Eq.{u_3 + 1} (α := K) (((↑i : Lifts F E K).emb : (a : ↥(↑i : Lifts F E K).carrier) → K) x : K)
    (((↑i : Lifts F E K).emb : (a : ↥(↑i : Lifts F E K).carrier) → K)
        ((inclusion ⋯ : (a : ↥(t i)) → ↥(↑i : Lifts F E K).carrier) x : ↥(↑i : Lifts F E K).carrier) :
      K)
rw₂ :
  Eq.{u_3 + 1} (α := K) (((↑i : Lifts F E K).emb : (a : ↥(↑i : Lifts F E K).carrier) → K) x : K)
    (((↑i : Lifts F E K).emb : (a : ↥(↑i : Lifts F E K).carrier) → K)
        ((AlgHom.id F ↥(t i) : (a : ↥(t i)) → ↥(↑i : Lifts F E K).carrier) x : ↥(↑i : Lifts F E K).carrier) :
      K)
⊢ Eq.{u_3 + 1} (α := K) (((↑i : Lifts F E K).emb : (a : ↥(↑i : Lifts F E K).carrier) → K) x : K)
    (((↑j : Lifts F E K).emb : (a : ↥(t j)) → K)
        ((inclusion h : (a : ↥(↑i : Lifts F E K).carrier) → ↥(t j)) x : ↥(t j)) :
      K)
have rw₃ : Eq.{u_3 + 1} (α := K) (((↑i : Lifts F E K).emb : (a : ↥(↑i : Lifts F E K).carrier) → K) x : K)
  (((↑i : Lifts F E K).emb : (a : ↥(↑i : Lifts F E K).carrier) → K) x : K)
Tactic: rw [← hji.snd (inclusion h x), inclusion_inclusion, inclusion_self, AlgHom.id_apply x]
-- Lean 4 proof step from Mathlib.FieldTheory.Extension (goal)
Goal:
F : Type u_1
E : Type u_2
K : Type u_3
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra F K
c : Set (Lifts F E K)
hc : IsChain (fun (x1 x2 : Lifts F E K) ↦ x1 ≤ x2) c
σ : Lifts F E K
hσ_1 : σ ∈ c
hσ : σ ∈ insert ⊥ c
t : (i : (↑(insert ⊥ c) : Type (max u_2 u_3))) → IntermediateField F E :=
  fun (i : (↑(insert ⊥ c) : Type (max u_2 u_3))) ↦ (↑i : Lifts F E K).carrier
x : ↥σ.carrier
⊢ Eq.{u_3 + 1} (α := K)
    (((union c hc).emb : (a : ↥(union c hc).carrier) → K)
        (((inclusion ⋯ : ↥σ.carrier →ₐ[F] ↥(union c hc).carrier) : (a : ↥σ.carrier) → ↥(union c hc).carrier) x :
          ↥(union c hc).carrier) :
      K)
    ((σ.emb : (a : ↥σ.carrier) → K) x : K)
have dsimp : Eq.{u_3 + 1} (α := K)
  ((Subalgebra.iSupLift (fun (x : (↑(insert ⊥ c) : Type (max u_2 u_3))) ↦ (↑x : Lifts F E K).carrier.toSubalgebra) sorry
          (fun (x : (↑(insert ⊥ c) : Type (max u_2 u_3))) ↦ (↑x : Lifts F E K).emb) sorry
          (⨆ (x : (↑(insert ⊥ c) : Type (max u_2 u_3))), (↑x : Lifts F E K).carrier.toSubalgebra) sorry :
        (a : ↥(⨆ (x : (↑(insert ⊥ c) : Type (max u_2 u_3))), (↑x : Lifts F E K).carrier.toSubalgebra)) → K)
      (((↑(Subalgebra.equivOfEq
                  (toSubalgebra (⨆ (i : (↑(insert ⊥ c) : Type (max u_2 u_3))), (↑i : Lifts F E K).carrier))
                  (⨆ (i : (↑(insert ⊥ c) : Type (max u_2 u_3))), (↑i : Lifts F E K).carrier.toSubalgebra) sorry) :
              ↥(⨆ (i : (↑(insert ⊥ c) : Type (max u_2 u_3))), (↑i : Lifts F E K).carrier).toSubalgebra →ₐ[F]
                ↥(⨆ (i : (↑(insert ⊥ c) : Type (max u_2 u_3))), (↑i : Lifts F E K).carrier.toSubalgebra)) :
            (a : ↥(⨆ (i : (↑(insert ⊥ c) : Type (max u_2 u_3))), (↑i : Lifts F E K).carrier)) →
              ↥(⨆ (x : (↑(insert ⊥ c) : Type (max u_2 u_3))), (↑x : Lifts F E K).carrier.toSubalgebra))
          (((inclusion sorry :
                ↥σ.carrier →ₐ[F] ↥(⨆ (i : (↑(insert ⊥ c) : Type (max u_2 u_3))), (↑i : Lifts F E K).carrier)) :
              (a : ↥σ.carrier) → ↥(⨆ (i : (↑(insert ⊥ c) : Type (max u_2 u_3))), (↑i : Lifts F E K).carrier))
            x) :
        ↥(⨆ (x : (↑(insert ⊥ c) : Type (max u_2 u_3))), (↑x : Lifts F E K).carrier.toSubalgebra)) :
    K)
  ((σ.emb : (a : ↥σ.carrier) → K) x : K)
Tactic: dsimp only [union, AlgHom.comp_apply]
-- Lean 4 proof step from Mathlib.FieldTheory.Extension (goal)
Goal:
F : Type u_1
E : Type u_2
K : Type u_3
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra F K
c : Set (Lifts F E K)
hc : IsChain (fun (x1 x2 : Lifts F E K) ↦ x1 ≤ x2) c
alg : Algebra.IsAlgebraic F E
inst_5 : Nonempty (↑c : Type (max u_2 u_3))
hext : ∀ σ ∈ c, σ.IsExtendible
S : Finset E
Ω : Type (max u_2 u_3) := AlgHom.{u_1, u_2, u_3} F (↥(adjoin F (↑S : Set E))) K
⊢ ∃ (ω : Ω),
    ∀ (π : (↑c : Type (max u_2 u_3))),
      ∃ θ ≥ (↑π : Lifts F E K),
        { carrier := adjoin F (↑S : Set E), emb := ω : Lifts F E K } ≤ θ ∧
          θ.carrier = (↑π : Lifts F E K).carrier ⊔ adjoin F (↑S : Set E)
have by_contra! : ∀
  (this :
    ∀ (ω : Ω),
      ∃ (π : (↑c : Type (max u_2 u_3))),
        ∀ (θ : Lifts F E K) (_ : θ ≥ (↑π : Lifts F E K))
          (_ : { carrier := adjoin F (↑S : Set E), emb := ω : Lifts F E K } ≤ θ),
          θ.carrier ≠ (↑π : Lifts F E K).carrier ⊔ adjoin F (↑S : Set E)),
  False
Tactic: by_contra!
-- Lean 4 proof step from Mathlib.FieldTheory.Extension (goal)
Goal:
F : Type u_1
E : Type u_2
K : Type u_3
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra F K
c : Set (Lifts F E K)
hc : IsChain (fun (x1 x2 : Lifts F E K) ↦ x1 ≤ x2) c
alg : Algebra.IsAlgebraic F E
inst_5 : Nonempty (↑c : Type (max u_2 u_3))
hext : ∀ σ ∈ c, σ.IsExtendible
S : Finset E
Ω : Type (max u_2 u_3) := AlgHom.{u_1, u_2, u_3} F (↥(adjoin F (↑S : Set E))) K
this :
  ∀ (ω : Ω),
    ∃ (π : (↑c : Type (max u_2 u_3))),
      ∀ (θ : Lifts F E K) (_ : θ ≥ (↑π : Lifts F E K))
        (_ : { carrier := adjoin F (↑S : Set E), emb := ω : Lifts F E K } ≤ θ),
        θ.carrier ≠ (↑π : Lifts F E K).carrier ⊔ adjoin F (↑S : Set E)
⊢ False
have choose : ∀ (π : (ω : Ω) → (↑c : Type (max u_2 u_3)))
  (hπ :
    ∀ (ω : Ω) (θ : Lifts F E K) (_ : θ ≥ (↑(π ω) : Lifts F E K))
      (_ : { carrier := adjoin F (↑S : Set E), emb := ω : Lifts F E K } ≤ θ),
      θ.carrier ≠ (↑(π ω) : Lifts F E K).carrier ⊔ adjoin F (↑S : Set E)),
  False
Tactic: choose π hπ using this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.FieldTheory.Extension (hypothesis)
Goal:
F : Type u_1
E : Type u_2
K : Type u_3
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra F K
c : Set (Lifts F E K)
hc : IsChain (fun (x1 x2 : Lifts F E K) ↦ x1 ≤ x2) c
alg : Algebra.IsAlgebraic F E
inst_5 : Nonempty (↑c : Type (max u_2 u_3))
hext : ∀ σ ∈ c, σ.IsExtendible
S : Finset E
Ω : Type (max u_2 u_3) := AlgHom.{u_1, u_2, u_3} F (↥(adjoin F (↑S : Set E))) K
π : (ω : Ω) → (↑c : Type (max u_2 u_3))
hπ :
  ∀ (ω : Ω) (θ : Lifts F E K) (_ : θ ≥ (↑(π ω) : Lifts F E K))
    (_ : { carrier := adjoin F (↑S : Set E), emb := ω : Lifts F E K } ≤ θ),
    θ.carrier ≠ (↑(π ω) : Lifts F E K).carrier ⊔ adjoin F (↑S : Set E)
⊢ False
have this : FiniteDimensional.{u_1, u_2} F ↥(adjoin F (↑S : Set E))
Tactic: have := finiteDimensional_adjoin (S := (S : Set E)) fun _ _ ↦ (alg.isIntegral).1 _
-- Lean 4 proof step from Mathlib.FieldTheory.Extension (goal)
Goal:
F : Type u_1
E : Type u_2
K : Type u_3
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra F K
c : Set (Lifts F E K)
hc : IsChain (fun (x1 x2 : Lifts F E K) ↦ x1 ≤ x2) c
alg : Algebra.IsAlgebraic F E
inst_5 : Nonempty (↑c : Type (max u_2 u_3))
hext : ∀ σ ∈ c, σ.IsExtendible
S : Finset E
Ω : Type (max u_2 u_3) := AlgHom.{u_1, u_2, u_3} F (↥(adjoin F (↑S : Set E))) K
π : (ω : Ω) → (↑c : Type (max u_2 u_3))
hπ :
  ∀ (ω : Ω) (θ : Lifts F E K) (_ : θ ≥ (↑(π ω) : Lifts F E K))
    (_ : { carrier := adjoin F (↑S : Set E), emb := ω : Lifts F E K } ≤ θ),
    θ.carrier ≠ (↑(π ω) : Lifts F E K).carrier ⊔ adjoin F (↑S : Set E)
this : FiniteDimensional.{u_1, u_2} F ↥(adjoin F (↑S : Set E))
⊢ False
have have : ∀ (π₀ : { a : Lifts F E K // a ∈ c }) (hπ₀ : ∀ (i : Ω), (↑(π i) : Lifts F E K) ≤ (↑π₀ : Lifts F E K)), False
Tactic: have ⟨π₀, hπ₀⟩ := hc.directed.finite_le π
-- Lean 4 proof step from Mathlib.FieldTheory.Extension (goal)
Goal:
F : Type u_1
E : Type u_2
K : Type u_3
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra F K
c : Set (Lifts F E K)
hc : IsChain (fun (x1 x2 : Lifts F E K) ↦ x1 ≤ x2) c
alg : Algebra.IsAlgebraic F E
inst_5 : Nonempty (↑c : Type (max u_2 u_3))
hext : ∀ σ ∈ c, σ.IsExtendible
S : Finset E
Ω : Type (max u_2 u_3) := AlgHom.{u_1, u_2, u_3} F (↥(adjoin F (↑S : Set E))) K
π : (ω : Ω) → (↑c : Type (max u_2 u_3))
hπ :
  ∀ (ω : Ω) (θ : Lifts F E K) (_ : θ ≥ (↑(π ω) : Lifts F E K))
    (_ : { carrier := adjoin F (↑S : Set E), emb := ω : Lifts F E K } ≤ θ),
    θ.carrier ≠ (↑(π ω) : Lifts F E K).carrier ⊔ adjoin F (↑S : Set E)
this : FiniteDimensional.{u_1, u_2} F ↥(adjoin F (↑S : Set E))
π₀ : { a : Lifts F E K // a ∈ c }
hπ₀ : ∀ (i : Ω), (↑(π i) : Lifts F E K) ≤ (↑π₀ : Lifts F E K)
⊢ False
have have : ∀ (θ : Lifts F E K) (hθπ : θ ≥ (↑π₀ : Lifts F E K)) (hθ : (↑S : Set E) ⊆ (↑θ.carrier : Set E)), False
Tactic: have ⟨θ, hθπ, hθ⟩ := hext _ π₀.2 S
-- Lean 4 proof step from Mathlib.FieldTheory.Extension (hypothesis)
Goal:
F : Type u_1
E : Type u_2
K : Type u_3
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra F K
c : Set (Lifts F E K)
hc : IsChain (fun (x1 x2 : Lifts F E K) ↦ x1 ≤ x2) c
alg : Algebra.IsAlgebraic F E
inst_5 : Nonempty (↑c : Type (max u_2 u_3))
hext : ∀ σ ∈ c, σ.IsExtendible
S : Finset E
Ω : Type (max u_2 u_3) := AlgHom.{u_1, u_2, u_3} F (↥(adjoin F (↑S : Set E))) K
π : (ω : Ω) → (↑c : Type (max u_2 u_3))
hπ :
  ∀ (ω : Ω) (θ : Lifts F E K) (_ : θ ≥ (↑(π ω) : Lifts F E K))
    (_ : { carrier := adjoin F (↑S : Set E), emb := ω : Lifts F E K } ≤ θ),
    θ.carrier ≠ (↑(π ω) : Lifts F E K).carrier ⊔ adjoin F (↑S : Set E)
this : FiniteDimensional.{u_1, u_2} F ↥(adjoin F (↑S : Set E))
π₀ : { a : Lifts F E K // a ∈ c }
hπ₀ : ∀ (i : Ω), (↑(π i) : Lifts F E K) ≤ (↑π₀ : Lifts F E K)
θ : Lifts F E K
hθπ : θ ≥ (↑π₀ : Lifts F E K)
hθ : (↑S : Set E) ⊆ (↑θ.carrier : Set E)
⊢ False
have hθ₁ : adjoin F (↑S : Set E) ≤ θ.carrier
Tactic: rw [← adjoin_le_iff] at hθ
Cleared hypotheses: hθ
-- Lean 4 proof step from Mathlib.FieldTheory.Extension (hypothesis)
Goal:
F : Type u_1
E : Type u_2
K : Type u_3
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra F K
c : Set (Lifts F E K)
hc : IsChain (fun (x1 x2 : Lifts F E K) ↦ x1 ≤ x2) c
alg : Algebra.IsAlgebraic F E
inst_5 : Nonempty (↑c : Type (max u_2 u_3))
hext : ∀ σ ∈ c, σ.IsExtendible
S : Finset E
Ω : Type (max u_2 u_3) := AlgHom.{u_1, u_2, u_3} F (↥(adjoin F (↑S : Set E))) K
π : (ω : Ω) → (↑c : Type (max u_2 u_3))
hπ :
  ∀ (ω : Ω) (θ : Lifts F E K) (_ : θ ≥ (↑(π ω) : Lifts F E K))
    (_ : { carrier := adjoin F (↑S : Set E), emb := ω : Lifts F E K } ≤ θ),
    θ.carrier ≠ (↑(π ω) : Lifts F E K).carrier ⊔ adjoin F (↑S : Set E)
this : FiniteDimensional.{u_1, u_2} F ↥(adjoin F (↑S : Set E))
π₀ : { a : Lifts F E K // a ∈ c }
hπ₀ : ∀ (i : Ω), (↑(π i) : Lifts F E K) ≤ (↑π₀ : Lifts F E K)
θ : Lifts F E K
hθπ : θ ≥ (↑π₀ : Lifts F E K)
hθ : adjoin F (↑S : Set E) ≤ θ.carrier
θ₀ : AlgHom.{u_1, u_2, u_3} F (↥(adjoin F (↑S : Set E))) K := θ.emb.comp (inclusion hθ)
⊢ False
have this₁ : (↑(π θ₀) : Lifts F E K) ≤ θ
Tactic: have := (hπ₀ θ₀).trans hθπ
-- Lean 4 proof step from Mathlib.FieldTheory.Extension (goal)
Goal:
F : Type u_1
E : Type u_2
K : Type u_3
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra F K
c : Set (Lifts F E K)
hc : IsChain (fun (x1 x2 : Lifts F E K) ↦ x1 ≤ x2) c
alg : Algebra.IsAlgebraic F E
inst_5 : Nonempty (↑c : Type (max u_2 u_3))
hext : ∀ σ ∈ c, σ.IsExtendible
S : Finset E
Ω : Type (max u_2 u_3) := AlgHom.{u_1, u_2, u_3} F (↥(adjoin F (↑S : Set E))) K
⊢ ∃ τ ≥ union c hc, (↑S : Set E) ⊆ (↑τ.carrier : Set E)
have have : ∀ (ω : Ω)
  (hω :
    ∀ (π : (↑c : Type (max u_2 u_3))),
      ∃ θ ≥ (↑π : Lifts F E K),
        { carrier := adjoin F (↑S : Set E), emb := ω : Lifts F E K } ≤ θ ∧
          θ.carrier = (↑π : Lifts F E K).carrier ⊔ adjoin F (↑S : Set E)),
  ∃ τ ≥ union c hc, (↑S : Set E) ⊆ (↑τ.carrier : Set E)
Tactic: have ⟨ω, hω⟩ : ∃ ω : Ω, ∀ π : c, ∃ θ ≥ π.1, ⟨_, ω⟩ ≤ θ ∧ θ.carrier = π.1.1 ⊔ adjoin F S := by
    by_contra!; choose π hπ using this
    have := finiteDimensional_adjoin (S := (S : Set E)) fun _ _ ↦ (alg.isIntegral).1 _
    have ⟨π₀, hπ₀⟩ := hc.directed.finite_le π
    have ⟨θ, hθπ, hθ⟩ := hext _ π₀.2 S
    rw [← adjoin_le_iff] at hθ
    let θ₀ := θ.emb.comp (inclusion hθ)
    have := (hπ₀ θ₀).trans hθπ
    exact hπ θ₀ ⟨_, θ.emb.comp <| inclusion <| sup_le this.1 hθ⟩
      ⟨le_sup_left, this.2⟩ ⟨le_sup_right, fun _ ↦ rfl⟩ rfl
-- Lean 4 proof step from Mathlib.FieldTheory.Extension (goal)
Goal:
F : Type u_1
E : Type u_2
K : Type u_3
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra F K
c : Set (Lifts F E K)
hc : IsChain (fun (x1 x2 : Lifts F E K) ↦ x1 ≤ x2) c
alg : Algebra.IsAlgebraic F E
inst_5 : Nonempty (↑c : Type (max u_2 u_3))
hext : ∀ σ ∈ c, σ.IsExtendible
S : Finset E
Ω : Type (max u_2 u_3) := AlgHom.{u_1, u_2, u_3} F (↥(adjoin F (↑S : Set E))) K
ω : Ω
hω :
  ∀ (π : (↑c : Type (max u_2 u_3))),
    ∃ θ ≥ (↑π : Lifts F E K),
      { carrier := adjoin F (↑S : Set E), emb := ω : Lifts F E K } ≤ θ ∧
        θ.carrier = (↑π : Lifts F E K).carrier ⊔ adjoin F (↑S : Set E)
⊢ ∃ τ ≥ union c hc, (↑S : Set E) ⊆ (↑τ.carrier : Set E)
have choose : ∀ (θ : (π : (↑c : Type (max u_2 u_3))) → Lifts F E K) (ge : ∀ (π : (↑c : Type (max u_2 u_3))), θ π ≥ (↑π : Lifts F E K))
  (hθ : ∀ (π : (↑c : Type (max u_2 u_3))), { carrier := adjoin F (↑S : Set E), emb := ω : Lifts F E K } ≤ θ π)
  (eq : ∀ (π : (↑c : Type (max u_2 u_3))), (θ π).carrier = (↑π : Lifts F E K).carrier ⊔ adjoin F (↑S : Set E)),
  ∃ τ ≥ union c hc, (↑S : Set E) ⊆ (↑τ.carrier : Set E)
Tactic: choose θ ge hθ eq using hω
Cleared hypotheses: hω
-- Lean 4 proof step from Mathlib.FieldTheory.Extension (hypothesis)
Goal:
F : Type u_1
E : Type u_2
K : Type u_3
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra F K
c : Set (Lifts F E K)
hc : IsChain (fun (x1 x2 : Lifts F E K) ↦ x1 ≤ x2) c
alg : Algebra.IsAlgebraic F E
inst_5 : Nonempty (↑c : Type (max u_2 u_3))
hext : ∀ σ ∈ c, σ.IsExtendible
S : Finset E
Ω : Type (max u_2 u_3) := AlgHom.{u_1, u_2, u_3} F (↥(adjoin F (↑S : Set E))) K
ω : Ω
θ : (π : (↑c : Type (max u_2 u_3))) → Lifts F E K
ge : ∀ (π : (↑c : Type (max u_2 u_3))), θ π ≥ (↑π : Lifts F E K)
hθ : ∀ (π : (↑c : Type (max u_2 u_3))), { carrier := adjoin F (↑S : Set E), emb := ω : Lifts F E K } ≤ θ π
eq : ∀ (π : (↑c : Type (max u_2 u_3))), (θ π).carrier = (↑π : Lifts F E K).carrier ⊔ adjoin F (↑S : Set E)
⊢ IsChain (fun (x1 x2 : Lifts F E K) ↦ x1 ≤ x2) (Set.range θ)
have eq₁ : ∀ (π : (↑c : Type (max u_2 u_3))), (θ π).carrier = adjoin F ((↑(↑π : Lifts F E K).carrier : Set E) ∪ (↑S : Set E))
Tactic: simp_rw [← restrictScalars_adjoin_eq_sup, restrictScalars_adjoin] at eq
Cleared hypotheses: eq
-- Lean 4 proof step from Mathlib.FieldTheory.Extension (goal)
Goal:
F : Type u_1
E : Type u_2
K : Type u_3
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra F K
c : Set (Lifts F E K)
hc : IsChain (fun (x1 x2 : Lifts F E K) ↦ x1 ≤ x2) c
alg : Algebra.IsAlgebraic F E
inst_5 : Nonempty (↑c : Type (max u_2 u_3))
hext : ∀ σ ∈ c, σ.IsExtendible
S : Finset E
Ω : Type (max u_2 u_3) := AlgHom.{u_1, u_2, u_3} F (↥(adjoin F (↑S : Set E))) K
ω : Ω
θ : (π : (↑c : Type (max u_2 u_3))) → Lifts F E K
ge : ∀ (π : (↑c : Type (max u_2 u_3))), θ π ≥ (↑π : Lifts F E K)
hθ : ∀ (π : (↑c : Type (max u_2 u_3))), { carrier := adjoin F (↑S : Set E), emb := ω : Lifts F E K } ≤ θ π
eq : ∀ (π : (↑c : Type (max u_2 u_3))), (θ π).carrier = adjoin F ((↑(↑π : Lifts F E K).carrier : Set E) ∪ (↑S : Set E))
π₁ π₂ : (↑c : Type (max u_2 u_3))
⊢ (fun (x1 x2 : Lifts F E K) ↦ x1 ≤ x2) (θ π₁) (θ π₂) ∨ (fun (x1 x2 : Lifts F E K) ↦ x1 ≤ x2) (θ π₂) (θ π₁)
have inr : ∀
  (this :
    ∀ (π₁ π₂ : (↑c : Type (max u_2 u_3))) (h : π₁ ≤ π₂),
      (fun (x1 x2 : Lifts F E K) ↦ x1 ≤ x2) (θ π₁) (θ π₂) ∨ (fun (x1 x2 : Lifts F E K) ↦ x1 ≤ x2) (θ π₂) (θ π₁))
  (h : ¬π₁ ≤ π₂),
  (fun (x1 x2 : Lifts F E K) ↦ x1 ≤ x2) (θ π₁) (θ π₂) ∨ (fun (x1 x2 : Lifts F E K) ↦ x1 ≤ x2) (θ π₂) (θ π₁)
Tactic: wlog h : π₁ ≤ π₂ generalizing π₁ π₂
-- Lean 4 proof step from Mathlib.FieldTheory.Extension (goal)
Goal:
F : Type u_1
E : Type u_2
K : Type u_3
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra F K
c : Set (Lifts F E K)
hc : IsChain (fun (x1 x2 : Lifts F E K) ↦ x1 ≤ x2) c
alg : Algebra.IsAlgebraic F E
inst_5 : Nonempty (↑c : Type (max u_2 u_3))
hext : ∀ σ ∈ c, σ.IsExtendible
S : Finset E
Ω : Type (max u_2 u_3) := AlgHom.{u_1, u_2, u_3} F (↥(adjoin F (↑S : Set E))) K
ω : Ω
θ : (π : (↑c : Type (max u_2 u_3))) → Lifts F E K
ge : ∀ (π : (↑c : Type (max u_2 u_3))), θ π ≥ (↑π : Lifts F E K)
hθ : ∀ (π : (↑c : Type (max u_2 u_3))), { carrier := adjoin F (↑S : Set E), emb := ω : Lifts F E K } ≤ θ π
eq : ∀ (π : (↑c : Type (max u_2 u_3))), (θ π).carrier = adjoin F ((↑(↑π : Lifts F E K).carrier : Set E) ∪ (↑S : Set E))
π₁ π₂ : (↑c : Type (max u_2 u_3))
inr :
  ∀
    (this :
      ∀ (π₁ π₂ : (↑c : Type (max u_2 u_3))) (h : π₁ ≤ π₂),
        (fun (x1 x2 : Lifts F E K) ↦ x1 ≤ x2) (θ π₁) (θ π₂) ∨ (fun (x1 x2 : Lifts F E K) ↦ x1 ≤ x2) (θ π₂) (θ π₁))
    (h : ¬π₁ ≤ π₂),
    (fun (x1 x2 : Lifts F E K) ↦ x1 ≤ x2) (θ π₁) (θ π₂) ∨ (fun (x1 x2 : Lifts F E K) ↦ x1 ≤ x2) (θ π₂) (θ π₁)
⊢ (fun (x1 x2 : Lifts F E K) ↦ x1 ≤ x2) (θ π₁) (θ π₂) ∨ (fun (x1 x2 : Lifts F E K) ↦ x1 ≤ x2) (θ π₂) (θ π₁)
have wlog : ∀ (π₁ π₂ : (↑c : Type (max u_2 u_3))) (h : π₁ ≤ π₂),
  (fun (x1 x2 : Lifts F E K) ↦ x1 ≤ x2) (θ π₁) (θ π₂) ∨ (fun (x1 x2 : Lifts F E K) ↦ x1 ≤ x2) (θ π₂) (θ π₁)
Tactic: wlog h : π₁ ≤ π₂ generalizing π₁ π₂
Cleared hypotheses: π₁, π₂