awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.Differential.Liouville (hypothesis)
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Differential F
inst_3 : Differential K
inst_4 : Algebra F K
inst_5 : DifferentialAlgebra F K
inst_6 : CharZero F
inst_7 : FiniteDimensional F K
inst_8 : IsGalois F K
a : F
ι : Type
inst_9 : Fintype ι
c : ι → F
hc : ∀ (x : ι), Eq (α := F) ((c x)′ : F) (0 : F)
u : ι → K
v : K
this : CharZero K
ffb : Eq.{u_2 + 1} (α := IntermediateField F K) (fixedField ⊤) ⊥
e : Gal(K/F)
h :
  Eq (α := K) ((e : (a : K) → K) (↑a : K) : K)
    ((e : (a : K) → K) (HAdd.hAdd (α := K) (β := K) (∑ x : ι, (↑(c x) : K) * logDeriv (u x) : K) (v′ : K)) : K)
⊢ (↑a : K) =
    HAdd.hAdd (α := K) (β := K)
      (∑ x : ι, HMul.hMul (α := K) (β := K) ((↑(c x) : K) : K) (logDeriv ((e : (a : K) → K) (u x)) : K) : K)
      (((e : (a : K) → K) v : K)′ : K)
have h₁ : (algebraMap F K : (a : F) → K) a =
  HAdd.hAdd (α := K) (β := K)
    (∑ x : ι,
        HMul.hMul (α := K) (β := K) ((algebraMap F K : (a : F) → K) (c x) : K)
          ((e : (a : K) → K) (logDeriv (u x)) : K) :
      K)
    ((e : (a : K) → K) (v′ : K) : K)
Tactic: simp only [AlgEquiv.commutes, map_add, map_sum, map_mul] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.FieldTheory.Differential.Liouville (goal)
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Differential F
inst_3 : Differential K
inst_4 : Algebra F K
inst_5 : DifferentialAlgebra F K
inst_6 : CharZero F
inst_7 : FiniteDimensional F K
inst_8 : IsGalois F K
a : F
ι : Type
inst_9 : Fintype ι
c : ι → F
hc : ∀ (x : ι), Eq (α := F) ((c x)′ : F) (0 : F)
u : ι → K
v : K
this : CharZero K
ffb : Eq.{u_2 + 1} (α := IntermediateField F K) (fixedField ⊤) ⊥
e : Gal(K/F)
h :
  (algebraMap F K : (a : F) → K) a =
    HAdd.hAdd (α := K) (β := K)
      (∑ x : ι,
          HMul.hMul (α := K) (β := K) ((algebraMap F K : (a : F) → K) (c x) : K)
            ((e : (a : K) → K) (logDeriv (u x)) : K) :
        K)
      ((e : (a : K) → K) (v′ : K) : K)
⊢ (↑a : K) =
    HAdd.hAdd (α := K) (β := K)
      (∑ x : ι, HMul.hMul (α := K) (β := K) ((↑(c x) : K) : K) (logDeriv ((e : (a : K) → K) (u x)) : K) : K)
      (((e : (a : K) → K) v : K)′ : K)
have h₁ : Eq.{u_2 + 1} (α := K) (∑ x : ι, HMul.hMul (α := K) (β := K) ((↑(c x) : K) : K) (logDeriv ((e : (a : K) → K) (u x)) : K))
  (∑ x : ι,
    HMul.hMul (α := K) (β := K) ((algebraMap F K : (a : F) → K) (c x) : K) ((e : (a : K) → K) (logDeriv (u x)) : K))
Tactic: convert! h using 2
-- Lean 4 proof step from Mathlib.FieldTheory.Differential.Liouville (goal)
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Differential F
inst_3 : Differential K
inst_4 : Algebra F K
inst_5 : DifferentialAlgebra F K
inst_6 : CharZero F
inst_7 : FiniteDimensional F K
inst_8 : IsGalois F K
a : F
ι : Type
inst_9 : Fintype ι
c : ι → F
hc : ∀ (x : ι), Eq (α := F) ((c x)′ : F) (0 : F)
u : ι → K
v : K
this : CharZero K
ffb : Eq.{u_2 + 1} (α := IntermediateField F K) (fixedField ⊤) ⊥
e : Gal(K/F)
h :
  (algebraMap F K : (a : F) → K) a =
    HAdd.hAdd (α := K) (β := K)
      (∑ x : ι,
          HMul.hMul (α := K) (β := K) ((algebraMap F K : (a : F) → K) (c x) : K)
            ((e : (a : K) → K) (logDeriv (u x)) : K) :
        K)
      ((e : (a : K) → K) (v′ : K) : K)
h₁ :
  Eq.{u_2 + 1} (α := K)
    (∑ x : ι, HMul.hMul (α := K) (β := K) ((↑(c x) : K) : K) (logDeriv ((e : (a : K) → K) (u x)) : K))
    (∑ x : ι,
      HMul.hMul (α := K) (β := K) ((algebraMap F K : (a : F) → K) (c x) : K) ((e : (a : K) → K) (logDeriv (u x)) : K))
⊢ (↑a : K) =
    HAdd.hAdd (α := K) (β := K)
      (∑ x : ι, HMul.hMul (α := K) (β := K) ((↑(c x) : K) : K) (logDeriv ((e : (a : K) → K) (u x)) : K) : K)
      (((e : (a : K) → K) v : K)′ : K)
have h₂ : Eq (α := K) (((e : (a : K) → K) v : K)′ : K) ((e : (a : K) → K) (v′ : K) : K)
Tactic: convert! h using 2
-- Lean 4 proof step from Mathlib.FieldTheory.Differential.Liouville (goal)
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Differential F
inst_3 : Differential K
inst_4 : Algebra F K
inst_5 : DifferentialAlgebra F K
inst_6 : CharZero F
inst_7 : FiniteDimensional F K
inst_8 : IsGalois F K
a : F
ι : Type
inst_9 : Fintype ι
c : ι → F
hc : ∀ (x : ι), Eq (α := F) ((c x)′ : F) (0 : F)
u : ι → K
v : K
this : CharZero K
ffb : Eq.{u_2 + 1} (α := IntermediateField F K) (fixedField ⊤) ⊥
e : Gal(K/F)
h :
  (algebraMap F K : (a : F) → K) a =
    HAdd.hAdd (α := K) (β := K)
      (∑ x : ι,
          HMul.hMul (α := K) (β := K) ((algebraMap F K : (a : F) → K) (c x) : K)
            ((e : (a : K) → K) (logDeriv (u x)) : K) :
        K)
      ((e : (a : K) → K) (v′ : K) : K)
⊢ Eq.{u_2 + 1} (α := K)
    (∑ x : ι, HMul.hMul (α := K) (β := K) ((↑(c x) : K) : K) (logDeriv ((e : (a : K) → K) (u x)) : K))
    (∑ x : ι,
      HMul.hMul (α := K) (β := K) ((algebraMap F K : (a : F) → K) (c x) : K) ((e : (a : K) → K) (logDeriv (u x)) : K))
have h₁ : ∀ (x : ι), Eq (α := K) (logDeriv ((e : (a : K) → K) (u x)) : K) ((e : (a : K) → K) (logDeriv (u x)) : K)
Tactic: rcongr x
-- Lean 4 proof step from Mathlib.FieldTheory.Differential.Liouville (goal)
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Differential F
inst_3 : Differential K
inst_4 : Algebra F K
inst_5 : DifferentialAlgebra F K
inst_6 : CharZero F
inst_7 : FiniteDimensional F K
inst_8 : IsGalois F K
a : F
ι : Type
inst_9 : Fintype ι
c : ι → F
hc : ∀ (x : ι), Eq (α := F) ((c x)′ : F) (0 : F)
u : ι → K
v : K
this : CharZero K
ffb : Eq.{u_2 + 1} (α := IntermediateField F K) (fixedField ⊤) ⊥
e : Gal(K/F)
h :
  (algebraMap F K : (a : F) → K) a =
    HAdd.hAdd (α := K) (β := K)
      (∑ x : ι,
          HMul.hMul (α := K) (β := K) ((algebraMap F K : (a : F) → K) (c x) : K)
            ((e : (a : K) → K) (logDeriv (u x)) : K) :
        K)
      ((e : (a : K) → K) (v′ : K) : K)
⊢ Eq (α := K) (((e : (a : K) → K) v : K)′ : K) ((e : (a : K) → K) (v′ : K) : K)
have h₁ : Eq (α := K) (((e : (a : K) → K) v : K)′ : K) (((e : (a : K) → K) v : K)′ : K)
Tactic: rw [algEquiv_deriv']
-- 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₂ L₃ : Lifts F E K
h₁₂ : L₁.carrier ≤ L₂.carrier
h₁₂' :
  ∀ (x : ↥L₁.carrier),
    Eq.{u_3 + 1} (α := K)
      ((L₂.emb : (a : ↥L₂.carrier) → K) ((inclusion h₁₂ : (a : ↥L₁.carrier) → ↥L₂.carrier) x : ↥L₂.carrier) : K)
      ((L₁.emb : (a : ↥L₁.carrier) → K) x : K)
h₂₃ : L₂.carrier ≤ L₃.carrier
h₂₃' :
  ∀ (x : ↥L₂.carrier),
    Eq.{u_3 + 1} (α := K)
      ((L₃.emb : (a : ↥L₃.carrier) → K) ((inclusion h₂₃ : (a : ↥L₂.carrier) → ↥L₃.carrier) x : ↥L₃.carrier) : K)
      ((L₂.emb : (a : ↥L₂.carrier) → K) x : K)
⊢ ∃ (h : L₁.carrier ≤ L₃.carrier),
    ∀ (x : ↥L₁.carrier),
      Eq.{u_3 + 1} (α := K)
        ((L₃.emb : (a : ↥L₃.carrier) → K) ((inclusion h : (a : ↥L₁.carrier) → ↥L₃.carrier) x : ↥L₃.carrier) : K)
        ((L₁.emb : (a : ↥L₁.carrier) → K) x : K)
have refine : ∀ (x : ↥L₁.carrier),
  Eq.{u_3 + 1} (α := K)
    ((L₃.emb : (a : ↥L₃.carrier) → K) ((inclusion sorry : (a : ↥L₁.carrier) → ↥L₃.carrier) x : ↥L₃.carrier) : K)
    ((L₁.emb : (a : ↥L₁.carrier) → K) x : K)
Tactic: refine ⟨h₁₂.trans h₂₃, fun _ ↦ ?_⟩
-- 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₂ L₃ : Lifts F E K
h₁₂ : L₁.carrier ≤ L₂.carrier
h₁₂' :
  ∀ (x : ↥L₁.carrier),
    Eq.{u_3 + 1} (α := K)
      ((L₂.emb : (a : ↥L₂.carrier) → K) ((inclusion h₁₂ : (a : ↥L₁.carrier) → ↥L₂.carrier) x : ↥L₂.carrier) : K)
      ((L₁.emb : (a : ↥L₁.carrier) → K) x : K)
h₂₃ : L₂.carrier ≤ L₃.carrier
h₂₃' :
  ∀ (x : ↥L₂.carrier),
    Eq.{u_3 + 1} (α := K)
      ((L₃.emb : (a : ↥L₃.carrier) → K) ((inclusion h₂₃ : (a : ↥L₂.carrier) → ↥L₃.carrier) x : ↥L₃.carrier) : K)
      ((L₂.emb : (a : ↥L₂.carrier) → K) x : K)
x : ↥L₁.carrier
⊢ Eq.{u_3 + 1} (α := K)
    ((L₃.emb : (a : ↥L₃.carrier) → K) ((inclusion ⋯ : (a : ↥L₁.carrier) → ↥L₃.carrier) x : ↥L₃.carrier) : K)
    ((L₁.emb : (a : ↥L₁.carrier) → K) x : K)
have rw : Eq.{u_3 + 1} (α := K)
  ((L₃.emb : (a : ↥L₃.carrier) → K)
      ((inclusion h₂₃ : (a : ↥L₂.carrier) → ↥L₃.carrier) ((inclusion h₁₂ : (a : ↥L₁.carrier) → ↥L₂.carrier) x) :
        ↥L₃.carrier) :
    K)
  ((L₁.emb : (a : ↥L₁.carrier) → K) x : K)
Tactic: rw [← inclusion_inclusion h₁₂ h₂₃, h₂₃', 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
S : Set E
L₁ L₂ L₃ : Lifts F E K
h₁₂ : L₁.carrier ≤ L₂.carrier
h₁₂' :
  ∀ (x : ↥L₁.carrier),
    Eq.{u_3 + 1} (α := K)
      ((L₂.emb : (a : ↥L₂.carrier) → K) ((inclusion h₁₂ : (a : ↥L₁.carrier) → ↥L₂.carrier) x : ↥L₂.carrier) : K)
      ((L₁.emb : (a : ↥L₁.carrier) → K) x : K)
h₂₃ : L₂.carrier ≤ L₃.carrier
h₂₃' :
  ∀ (x : ↥L₂.carrier),
    Eq.{u_3 + 1} (α := K)
      ((L₃.emb : (a : ↥L₃.carrier) → K) ((inclusion h₂₃ : (a : ↥L₂.carrier) → ↥L₃.carrier) x : ↥L₃.carrier) : K)
      ((L₂.emb : (a : ↥L₂.carrier) → K) x : K)
x : ↥L₁.carrier
rw :
  Eq.{u_3 + 1} (α := K)
    ((L₃.emb : (a : ↥L₃.carrier) → K)
        ((inclusion h₂₃ : (a : ↥L₂.carrier) → ↥L₃.carrier) ((inclusion h₁₂ : (a : ↥L₁.carrier) → ↥L₂.carrier) x) :
          ↥L₃.carrier) :
      K)
    ((L₁.emb : (a : ↥L₁.carrier) → K) x : K)
⊢ Eq.{u_3 + 1} (α := K)
    ((L₃.emb : (a : ↥L₃.carrier) → K) ((inclusion ⋯ : (a : ↥L₁.carrier) → ↥L₃.carrier) x : ↥L₃.carrier) : K)
    ((L₁.emb : (a : ↥L₁.carrier) → K) x : K)
have rw₁ : Eq.{u_3 + 1} (α := K)
  ((L₂.emb : (a : ↥L₂.carrier) → K) ((inclusion h₁₂ : (a : ↥L₁.carrier) → ↥L₂.carrier) x : ↥L₂.carrier) : K)
  ((L₁.emb : (a : ↥L₁.carrier) → K) x : K)
Tactic: rw [← inclusion_inclusion h₁₂ h₂₃, h₂₃', 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
S : Set E
L₁ L₂ L₃ : Lifts F E K
h₁₂ : L₁.carrier ≤ L₂.carrier
h₁₂' :
  ∀ (x : ↥L₁.carrier),
    Eq.{u_3 + 1} (α := K)
      ((L₂.emb : (a : ↥L₂.carrier) → K) ((inclusion h₁₂ : (a : ↥L₁.carrier) → ↥L₂.carrier) x : ↥L₂.carrier) : K)
      ((L₁.emb : (a : ↥L₁.carrier) → K) x : K)
h₂₃ : L₂.carrier ≤ L₃.carrier
h₂₃' :
  ∀ (x : ↥L₂.carrier),
    Eq.{u_3 + 1} (α := K)
      ((L₃.emb : (a : ↥L₃.carrier) → K) ((inclusion h₂₃ : (a : ↥L₂.carrier) → ↥L₃.carrier) x : ↥L₃.carrier) : K)
      ((L₂.emb : (a : ↥L₂.carrier) → K) x : K)
x : ↥L₁.carrier
rw :
  Eq.{u_3 + 1} (α := K)
    ((L₃.emb : (a : ↥L₃.carrier) → K)
        ((inclusion h₂₃ : (a : ↥L₂.carrier) → ↥L₃.carrier) ((inclusion h₁₂ : (a : ↥L₁.carrier) → ↥L₂.carrier) x) :
          ↥L₃.carrier) :
      K)
    ((L₁.emb : (a : ↥L₁.carrier) → K) x : K)
rw₁ :
  Eq.{u_3 + 1} (α := K)
    ((L₂.emb : (a : ↥L₂.carrier) → K) ((inclusion h₁₂ : (a : ↥L₁.carrier) → ↥L₂.carrier) x : ↥L₂.carrier) : K)
    ((L₁.emb : (a : ↥L₁.carrier) → K) x : K)
⊢ Eq.{u_3 + 1} (α := K)
    ((L₃.emb : (a : ↥L₃.carrier) → K) ((inclusion ⋯ : (a : ↥L₁.carrier) → ↥L₃.carrier) x : ↥L₃.carrier) : K)
    ((L₁.emb : (a : ↥L₁.carrier) → K) x : K)
have rw₂ : Eq.{u_3 + 1} (α := K) ((L₁.emb : (a : ↥L₁.carrier) → K) x : K) ((L₁.emb : (a : ↥L₁.carrier) → K) x : K)
Tactic: rw [← inclusion_inclusion h₁₂ h₂₃, h₂₃', 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
S : Set E
L₁ : IntermediateField F E
e₁ : AlgHom.{u_1, u_2, u_3} F (↥L₁) K
L₂ : IntermediateField F E
e₂ : AlgHom.{u_1, u_2, u_3} F (↥L₂) K
h₁₂ : { carrier := L₁, emb := e₁ : Lifts F E K }.carrier ≤ { carrier := L₂, emb := e₂ : Lifts F E K }.carrier
h₁₂' :
  ∀ (x : ↥{ carrier := L₁, emb := e₁ : Lifts F E K }.carrier),
    Eq.{u_3 + 1} (α := K)
      (({ carrier := L₂, emb := e₂ : Lifts F E K }.emb : (a : ↥{ carrier := L₂, emb := e₂ }.carrier) → K)
          ((inclusion h₁₂ : (a : ↥{ carrier := L₁, emb := e₁ }.carrier) → ↥{ carrier := L₂, emb := e₂ }.carrier) x :
            ↥{ carrier := L₂, emb := e₂ : Lifts F E K }.carrier) :
        K)
      (({ carrier := L₁, emb := e₁ : Lifts F E K }.emb : (a : ↥{ carrier := L₁, emb := e₁ }.carrier) → K) x : K)
h₂₁ : { carrier := L₂, emb := e₂ : Lifts F E K }.carrier ≤ { carrier := L₁, emb := e₁ : Lifts F E K }.carrier
h₂₁' :
  ∀ (x : ↥{ carrier := L₂, emb := e₂ : Lifts F E K }.carrier),
    Eq.{u_3 + 1} (α := K)
      (({ carrier := L₁, emb := e₁ : Lifts F E K }.emb : (a : ↥{ carrier := L₁, emb := e₁ }.carrier) → K)
          ((inclusion h₂₁ : (a : ↥{ carrier := L₂, emb := e₂ }.carrier) → ↥{ carrier := L₁, emb := e₁ }.carrier) x :
            ↥{ carrier := L₁, emb := e₁ : Lifts F E K }.carrier) :
        K)
      (({ carrier := L₂, emb := e₂ : Lifts F E K }.emb : (a : ↥{ carrier := L₂, emb := e₂ }.carrier) → K) x : K)
⊢ { carrier := L₁, emb := e₁ : Lifts F E K } = { carrier := L₂, emb := e₂ }
have obtain : ∀ (e₂ : AlgHom.{u_1, u_2, u_3} F (↥L₁) K)
  (h₁₂ : { carrier := L₁, emb := e₁ : Lifts F E K }.carrier ≤ { carrier := L₁, emb := e₂ : Lifts F E K }.carrier)
  (h₁₂' :
    ∀ (x : ↥{ carrier := L₁, emb := e₁ : Lifts F E K }.carrier),
      Eq.{u_3 + 1} (α := K)
        (({ carrier := L₁, emb := e₂ : Lifts F E K }.emb : (a : ↥{ carrier := L₁, emb := e₂ }.carrier) → K)
            ((inclusion h₁₂ : (a : ↥{ carrier := L₁, emb := e₁ }.carrier) → ↥{ carrier := L₁, emb := e₂ }.carrier) x :
              ↥{ carrier := L₁, emb := e₂ : Lifts F E K }.carrier) :
          K)
        (({ carrier := L₁, emb := e₁ : Lifts F E K }.emb : (a : ↥{ carrier := L₁, emb := e₁ }.carrier) → K) x : K))
  (h₂₁ : { carrier := L₁, emb := e₂ : Lifts F E K }.carrier ≤ { carrier := L₁, emb := e₁ : Lifts F E K }.carrier)
  (h₂₁' :
    ∀ (x : ↥{ carrier := L₁, emb := e₂ : Lifts F E K }.carrier),
      Eq.{u_3 + 1} (α := K)
        (({ carrier := L₁, emb := e₁ : Lifts F E K }.emb : (a : ↥{ carrier := L₁, emb := e₁ }.carrier) → K)
            ((inclusion h₂₁ : (a : ↥{ carrier := L₁, emb := e₂ }.carrier) → ↥{ carrier := L₁, emb := e₁ }.carrier) x :
              ↥{ carrier := L₁, emb := e₁ : Lifts F E K }.carrier) :
          K)
        (({ carrier := L₁, emb := e₂ : Lifts F E K }.emb : (a : ↥{ carrier := L₁, emb := e₂ }.carrier) → K) x : K)),
  { carrier := L₁, emb := e₁ : Lifts F E K } = { carrier := L₁, emb := e₂ }
Tactic: obtain rfl : L₁ = L₂ := h₁₂.antisymm h₂₁
Cleared hypotheses: L₂, e₂, h₁₂, h₁₂', h₂₁, 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
S : Set E
L₁ : IntermediateField F E
e₁ e₂ : AlgHom.{u_1, u_2, u_3} F (↥L₁) K
h₁₂ : { carrier := L₁, emb := e₁ : Lifts F E K }.carrier ≤ { carrier := L₁, emb := e₂ : Lifts F E K }.carrier
h₁₂' :
  ∀ (x : ↥{ carrier := L₁, emb := e₁ : Lifts F E K }.carrier),
    Eq.{u_3 + 1} (α := K)
      (({ carrier := L₁, emb := e₂ : Lifts F E K }.emb : (a : ↥{ carrier := L₁, emb := e₂ }.carrier) → K)
          ((inclusion h₁₂ : (a : ↥{ carrier := L₁, emb := e₁ }.carrier) → ↥{ carrier := L₁, emb := e₂ }.carrier) x :
            ↥{ carrier := L₁, emb := e₂ : Lifts F E K }.carrier) :
        K)
      (({ carrier := L₁, emb := e₁ : Lifts F E K }.emb : (a : ↥{ carrier := L₁, emb := e₁ }.carrier) → K) x : K)
h₂₁ : { carrier := L₁, emb := e₂ : Lifts F E K }.carrier ≤ { carrier := L₁, emb := e₁ : Lifts F E K }.carrier
h₂₁' :
  ∀ (x : ↥{ carrier := L₁, emb := e₂ : Lifts F E K }.carrier),
    Eq.{u_3 + 1} (α := K)
      (({ carrier := L₁, emb := e₁ : Lifts F E K }.emb : (a : ↥{ carrier := L₁, emb := e₁ }.carrier) → K)
          ((inclusion h₂₁ : (a : ↥{ carrier := L₁, emb := e₂ }.carrier) → ↥{ carrier := L₁, emb := e₁ }.carrier) x :
            ↥{ carrier := L₁, emb := e₁ : Lifts F E K }.carrier) :
        K)
      (({ carrier := L₁, emb := e₂ : Lifts F E K }.emb : (a : ↥{ carrier := L₁, emb := e₂ }.carrier) → K) x : K)
⊢ { carrier := L₁, emb := e₁ : Lifts F E K } = { carrier := L₁, emb := e₂ }
have e_emb : e₁ = e₂
Tactic: congr
-- 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 : Lifts F E K
x : ↥(carrier { carrier := ⊥, emb := AlgHom.comp (Algebra.ofId F K) (↑(botEquiv F E) : ↥⊥ →ₐ[F] F) })
⊢ Eq.{u_3 + 1} (α := K)
    ((L.emb : (a : ↥L.carrier) → K)
        ((inclusion ⋯ :
              (a : ↥{ carrier := ⊥, emb := (Algebra.ofId F K).comp (↑(botEquiv F E) : ↥⊥ →ₐ[F] F) }.carrier) →
                ↥L.carrier)
            x :
          ↥L.carrier) :
      K)
    ((emb { carrier := ⊥, emb := AlgHom.comp (Algebra.ofId F K) (↑(botEquiv F E) : ↥⊥ →ₐ[F] F) } :
          (a : ↥{ carrier := ⊥, emb := (Algebra.ofId F K).comp (↑(botEquiv F E) : ↥⊥ →ₐ[F] F) }.carrier) → K)
        x :
      K)
have obtain : ∀ (x : F),
  Eq.{u_3 + 1} (α := K)
    ((L.emb : (a : ↥L.carrier) → K)
        ((inclusion sorry :
              (a : ↥{ carrier := ⊥, emb := (Algebra.ofId F K).comp (↑(botEquiv F E) : ↥⊥ →ₐ[F] F) }.carrier) →
                ↥L.carrier)
            (((AlgEquiv.symm (botEquiv F E) : AlgEquiv.{u_1, u_1, u_2} F F ↥⊥) : (a : F) → ↥⊥) x) :
          ↥L.carrier) :
      K)
    ((emb { carrier := ⊥, emb := AlgHom.comp (Algebra.ofId F K) (↑(botEquiv F E) : ↥⊥ →ₐ[F] F) } :
          (a : ↥{ carrier := ⊥, emb := (Algebra.ofId F K).comp (↑(botEquiv F E) : ↥⊥ →ₐ[F] F) }.carrier) → K)
        (((AlgEquiv.symm (botEquiv F E) : AlgEquiv.{u_1, u_1, u_2} F F ↥⊥) : (a : F) → ↥⊥) x : ↥⊥) :
      K)
Tactic: obtain ⟨x, rfl⟩ := (botEquiv F E).symm.surjective x
Cleared hypotheses: 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 : Lifts F E K
x : F
⊢ Eq.{u_3 + 1} (α := K)
    ((L.emb : (a : ↥L.carrier) → K)
        ((inclusion ⋯ :
              (a : ↥{ carrier := ⊥, emb := (Algebra.ofId F K).comp (↑(botEquiv F E) : ↥⊥ →ₐ[F] F) }.carrier) →
                ↥L.carrier)
            (((AlgEquiv.symm (botEquiv F E) : AlgEquiv.{u_1, u_1, u_2} F F ↥⊥) : (a : F) → ↥⊥) x) :
          ↥L.carrier) :
      K)
    ((emb { carrier := ⊥, emb := AlgHom.comp (Algebra.ofId F K) (↑(botEquiv F E) : ↥⊥ →ₐ[F] F) } :
          (a : ↥{ carrier := ⊥, emb := (Algebra.ofId F K).comp (↑(botEquiv F E) : ↥⊥ →ₐ[F] F) }.carrier) → K)
        (((AlgEquiv.symm (botEquiv F E) : AlgEquiv.{u_1, u_1, u_2} F F ↥⊥) : (a : F) → ↥⊥) x : ↥⊥) :
      K)
have simp_rw : Eq.{u_3 + 1} (α := K)
  ((L.emb : (a : ↥L.carrier) → K)
      ((inclusion sorry : (a : ↥⊥) → ↥L.carrier)
          (((AlgEquiv.symm (botEquiv F E) : AlgEquiv.{u_1, u_1, u_2} F F ↥⊥) : (a : F) → ↥⊥) x) :
        ↥L.carrier) :
    K)
  ((Algebra.ofId F K : (a : F) → K) x : K)
Tactic: simp_rw [AlgHom.comp_apply, AlgEquiv.coe_algHom, AlgEquiv.apply_symm_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
L₁ L₂ : Lifts F E K
⊢ L₁ ≤ L₂ ↔ ∃ (h : L₁.carrier ≤ L₂.carrier), L₂.emb.comp (inclusion h) = L₁.emb
have simp_rw : L₁ ≤ L₂ ↔
  ∃ (h : L₁.carrier ≤ L₂.carrier),
    ∀ (x : ↥L₁.carrier),
      Eq.{u_3 + 1} (α := K) ((L₂.emb.comp (inclusion sorry) : (a : ↥L₁.carrier) → K) x : K)
        ((L₁.emb : (a : ↥L₁.carrier) → K) x : K)
Tactic: simp_rw [AlgHom.ext_iff]
-- 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
L₁ L₂ : Lifts F E K
⊢ L₁ = L₂ ↔ ∃ (h : L₁.carrier = L₂.carrier), L₂.emb.comp (inclusion ⋯) = L₁.emb
have rw : (∃ (h : L₁.carrier ≤ L₂.carrier), L₂.emb.comp (inclusion h) = L₁.emb) ∧ L₁.carrier = L₂.carrier ↔
  ∃ (h : L₁.carrier = L₂.carrier), L₂.emb.comp (inclusion sorry) = L₁.emb
Tactic: rw [eq_iff_le_carrier_eq, le_iff]
-- 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
L₁ L₂ : Lifts F E K
⊢ L₁ < L₂ ↔ L₁ ≤ L₂ ∧ L₁.carrier ≠ L₂.carrier
have rw : L₁ ≤ L₂ → (L₁ ≠ L₂ ↔ L₁.carrier ≠ L₂.carrier)
Tactic: rw [lt_iff_le_and_ne, and_congr_right]
-- 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
L₁ L₂ : Lifts F E K
h : L₁ ≤ L₂
⊢ L₁ ≠ L₂ ↔ L₁.carrier ≠ L₂.carrier
have simp_rw : ¬L₁ = L₂ ↔ ¬L₁.carrier = L₂.carrier
Tactic: simp_rw [Ne, eq_iff_le_carrier_eq, h, true_and]
-- 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
L₁ L₂ : Lifts F E K
h : L₁ ≤ L₂
simp_rw : ¬L₁ = L₂ ↔ ¬L₁.carrier = L₂.carrier
⊢ L₁ ≠ L₂ ↔ L₁.carrier ≠ L₂.carrier
have simp_rw₁ : ¬(L₁ ≤ L₂ ∧ L₁.carrier = L₂.carrier) ↔ ¬L₁.carrier = L₂.carrier
Tactic: simp_rw [Ne, eq_iff_le_carrier_eq, h, true_and]
-- 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
L₁ L₂ : Lifts F E K
h : L₁ ≤ L₂
simp_rw : ¬L₁ = L₂ ↔ ¬L₁.carrier = L₂.carrier
simp_rw₁ : ¬(L₁ ≤ L₂ ∧ L₁.carrier = L₂.carrier) ↔ ¬L₁.carrier = L₂.carrier
⊢ L₁ ≠ L₂ ↔ L₁.carrier ≠ L₂.carrier
have simp_rw₂ : ¬(True ∧ L₁.carrier = L₂.carrier) ↔ ¬L₁.carrier = L₂.carrier
Tactic: simp_rw [Ne, eq_iff_le_carrier_eq, h, true_and]
-- 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
L₁ L₂ : Lifts F E K
⊢ L₁ < L₂ ↔ ∃ (h : L₁.carrier < L₂.carrier), L₂.emb.comp (inclusion ⋯) = L₁.emb
have rw : (∃ (h : L₁.carrier ≤ L₂.carrier), L₂.emb.comp (inclusion h) = L₁.emb) ∧ L₁.carrier ≠ L₂.carrier ↔
  ∃ (h : L₁.carrier < L₂.carrier), L₂.emb.comp (inclusion sorry) = L₁.emb
Tactic: rw [lt_iff_le_carrier_ne, le_iff]
-- 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)
    (((fun (x : (↑(insert ⊥ c) : Type (max u_2 u_3))) ↦ (↑x : Lifts F E K).emb) i :
          (a : ↥(↑i : Lifts F E K).carrier) → K)
        x :
      K)
    ((AlgHom.comp ((fun (x : (↑(insert ⊥ c) : Type (max u_2 u_3))) ↦ (↑x : Lifts F E K).emb) j)
            (Subalgebra.inclusion h) :
          (a : ↥(↑i : Lifts F E K).carrier) → K)
        x :
      K)
have rw : Eq.{u_3 + 1} (α := K)
  (((fun (x : (↑(insert ⊥ c) : Type (max u_2 u_3))) ↦ (↑x : Lifts F E K).emb) i : (a : ↥(↑i : Lifts F E K).carrier) → K)
      x :
    K)
  (((fun (x : (↑(insert ⊥ c) : Type (max u_2 u_3))) ↦ (↑x : Lifts F E K).emb) j :
        (a : ↥((fun (x : (↑(insert ⊥ c) : Type (max u_2 u_3))) ↦ (t x).toSubalgebra) j)) → K)
      ((inclusion h :
            (a : ↥(↑i : Lifts F E K).carrier) →
              ↥((fun (x : (↑(insert ⊥ c) : Type (max u_2 u_3))) ↦ (t x).toSubalgebra) j))
          x :
        ↥((fun (x : (↑(insert ⊥ c) : Type (max u_2 u_3))) ↦ (t x).toSubalgebra) j)) :
    K)
Tactic: rw [AlgHom.comp_apply, ← inclusion]