awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.CardinalEmb (hypothesis)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst_3 : Algebra.IsAlgebraic F E
i : (Module.rank F E).ord.ToType
ih : (y : (Module.rank F E).ord.ToType) → y < i → (Module.rank F E).ord.ToType
s : Set E :=
  range fun (j : (↑(Iio i) : Type v)) ↦
    (b : (a : (Module.rank F E).ord.ToType) → E) (ih (↑j : (Module.rank F E).ord.ToType) ⋯)
this :
  ∀ (x : (Module.rank F E).ord.ToType),
    Membership.mem (α := E) (γ := IntermediateField F E) (adjoin F s)
      ((b : (a : (Module.rank F E).ord.ToType) → E) x : E)
⊢ False
have this₁ : LE.le (α := IntermediateField F E)
  (adjoin F (range («ι» := (Module.rank F E).ord.ToType) (⇑b : (a : (Module.rank F E).ord.ToType) → E))) (adjoin F s)
Tactic: have := adjoin_le_iff.mpr (range_subset_iff.mpr this)
-- Lean 4 proof step from Mathlib.FieldTheory.CardinalEmb (hypothesis)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst_3 : Algebra.IsAlgebraic F E
i : (Module.rank F E).ord.ToType
ih : (y : (Module.rank F E).ord.ToType) → y < i → (Module.rank F E).ord.ToType
s : Set E :=
  range fun (j : (↑(Iio i) : Type v)) ↦
    (b : (a : (Module.rank F E).ord.ToType) → E) (ih (↑j : (Module.rank F E).ord.ToType) ⋯)
this_1 :
  ∀ (x : (Module.rank F E).ord.ToType),
    Membership.mem (α := E) (γ := IntermediateField F E) (adjoin F s)
      ((b : (a : (Module.rank F E).ord.ToType) → E) x : E)
this :
  LE.le (α := IntermediateField F E)
    (adjoin F (range («ι» := (Module.rank F E).ord.ToType) (⇑b : (a : (Module.rank F E).ord.ToType) → E))) (adjoin F s)
⊢ False
have this₁ : Eq (α := IntermediateField F E) (adjoin F s) ⊤
Tactic: rw [adjoin_basis_eq_top, ← eq_top_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.FieldTheory.CardinalEmb (hypothesis)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst_3 : Algebra.IsAlgebraic F E
i : (Module.rank F E).ord.ToType
ih : (y : (Module.rank F E).ord.ToType) → y < i → (Module.rank F E).ord.ToType
s : Set E :=
  range fun (j : (↑(Iio i) : Type v)) ↦
    (b : (a : (Module.rank F E).ord.ToType) → E) (ih (↑j : (Module.rank F E).ord.ToType) ⋯)
this_1 :
  ∀ (x : (Module.rank F E).ord.ToType),
    Membership.mem (α := E) (γ := IntermediateField F E) (adjoin F s)
      ((b : (a : (Module.rank F E).ord.ToType) → E) x : E)
this : Eq (α := IntermediateField F E) (adjoin F s) ⊤
⊢ False
have this₁ : Module.rank F ↥(adjoin F s) = Module.rank F ↥⊤
Tactic: apply_fun Module.rank F at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.FieldTheory.CardinalEmb (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst_3 : Algebra.IsAlgebraic F E
i : (Module.rank F E).ord.ToType
ih : (y : (Module.rank F E).ord.ToType) → y < i → (Module.rank F E).ord.ToType
s : Set E :=
  range fun (j : (↑(Iio i) : Type v)) ↦
    (b : (a : (Module.rank F E).ord.ToType) → E) (ih (↑j : (Module.rank F E).ord.ToType) ⋯)
this_1 :
  ∀ (x : (Module.rank F E).ord.ToType),
    Membership.mem (α := E) (γ := IntermediateField F E) (adjoin F s)
      ((b : (a : (Module.rank F E).ord.ToType) → E) x : E)
this : Module.rank F ↥(adjoin F s) = Module.rank F ↥⊤
⊢ False
have refine : Module.rank F ↥(adjoin F s) < Module.rank F ↥⊤
Tactic: refine ne_of_lt ?_ this
-- Lean 4 proof step from Mathlib.FieldTheory.CardinalEmb (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst_3 : Algebra.IsAlgebraic F E
i : (Module.rank F E).ord.ToType
ih : (y : (Module.rank F E).ord.ToType) → y < i → (Module.rank F E).ord.ToType
s : Set E :=
  range fun (j : (↑(Iio i) : Type v)) ↦
    (b : (a : (Module.rank F E).ord.ToType) → E) (ih (↑j : (Module.rank F E).ord.ToType) ⋯)
this_1 :
  ∀ (x : (Module.rank F E).ord.ToType),
    Membership.mem (α := E) (γ := IntermediateField F E) (adjoin F s)
      ((b : (a : (Module.rank F E).ord.ToType) → E) x : E)
this : Module.rank F ↥(adjoin F s) = Module.rank F ↥⊤
x : AddCommMonoid ↥⊤ := inferInstance
| Module.rank F ↥⊤
have rw : Module.rank F E
Tactic: rw [topEquiv.toLinearEquiv.rank_eq]
-- Lean 4 proof step from Mathlib.FieldTheory.CardinalEmb (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst_3 : Algebra.IsAlgebraic F E
i : (Module.rank F E).ord.ToType
ih : (y : (Module.rank F E).ord.ToType) → y < i → (Module.rank F E).ord.ToType
s : Set E :=
  range fun (j : (↑(Iio i) : Type v)) ↦
    (b : (a : (Module.rank F E).ord.ToType) → E) (ih (↑j : (Module.rank F E).ord.ToType) ⋯)
this_1 :
  ∀ (x : (Module.rank F E).ord.ToType),
    Membership.mem (α := E) (γ := IntermediateField F E) (adjoin F s)
      ((b : (a : (Module.rank F E).ord.ToType) → E) x : E)
this : Module.rank F ↥(adjoin F s) = Module.rank F ↥⊤
x : AddCommMonoid ↥⊤ := inferInstance
⊢ Module.rank F ↥(adjoin F s) < Module.rank F ↥⊤
have conv_rhs : Module.rank F ↥(adjoin F s) < Module.rank F E
Tactic: conv_rhs => rw [topEquiv.toLinearEquiv.rank_eq]
-- Lean 4 proof step from Mathlib.FieldTheory.CardinalEmb (hypothesis)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst_3 : Algebra.IsAlgebraic F E
i : (Module.rank F E).ord.ToType
ih : (y : (Module.rank F E).ord.ToType) → y < i → (Module.rank F E).ord.ToType
s : Set E :=
  range fun (j : (↑(Iio i) : Type v)) ↦
    (b : (a : (Module.rank F E).ord.ToType) → E) (ih (↑j : (Module.rank F E).ord.ToType) ⋯)
this_1 :
  ∀ (x : (Module.rank F E).ord.ToType),
    Membership.mem (α := E) (γ := IntermediateField F E) (adjoin F s)
      ((b : (a : (Module.rank F E).ord.ToType) → E) x : E)
this : Module.rank F ↥(adjoin F s) = Module.rank F ↥⊤
x : AddCommMonoid ↥⊤ := inferInstance
⊢ Module.rank F ↥(adjoin F s) < Module.rank F E
have this₁ : #(↑(Iio i) : Type v) < #(Module.rank F E).ord.ToType
Tactic: have := mk_Iio_lt i (by simp)
-- Lean 4 proof step from Mathlib.FieldTheory.CardinalEmb (hypothesis)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst_3 : Algebra.IsAlgebraic F E
i : (Module.rank F E).ord.ToType
ih : (y : (Module.rank F E).ord.ToType) → y < i → (Module.rank F E).ord.ToType
s : Set E :=
  range fun (j : (↑(Iio i) : Type v)) ↦
    (b : (a : (Module.rank F E).ord.ToType) → E) (ih (↑j : (Module.rank F E).ord.ToType) ⋯)
this_1 :
  ∀ (x : (Module.rank F E).ord.ToType),
    Membership.mem (α := E) (γ := IntermediateField F E) (adjoin F s)
      ((b : (a : (Module.rank F E).ord.ToType) → E) x : E)
this_2 : Module.rank F ↥(adjoin F s) = Module.rank F ↥⊤
x : AddCommMonoid ↥⊤ := inferInstance
this : #(↑(Iio i) : Type v) < #(Module.rank F E).ord.ToType
⊢ Module.rank F ↥(adjoin F s) < Module.rank F E
have this₁ : #(↑(Iio i) : Type v) < Module.rank F E
Tactic: rw [mk_toType, card_ord] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.FieldTheory.CardinalEmb (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst_3 : Algebra.IsAlgebraic F E
i : (Module.rank F E).ord.ToType
ih : (y : (Module.rank F E).ord.ToType) → y < i → (Module.rank F E).ord.ToType
s : Set E :=
  range fun (j : (↑(Iio i) : Type v)) ↦
    (b : (a : (Module.rank F E).ord.ToType) → E) (ih (↑j : (Module.rank F E).ord.ToType) ⋯)
this_1 :
  ∀ (x : (Module.rank F E).ord.ToType),
    Membership.mem (α := E) (γ := IntermediateField F E) (adjoin F s)
      ((b : (a : (Module.rank F E).ord.ToType) → E) x : E)
this_2 : Module.rank F ↥(adjoin F s) = Module.rank F ↥⊤
x : AddCommMonoid ↥⊤ := inferInstance
this : #(↑(Iio i) : Type v) < Module.rank F E
⊢ Module.rank F ↥(adjoin F s) < Module.rank F E
have inl : ∀ (eq : ℵ₀ = Module.rank F E), Module.rank F ↥(adjoin F s) < Module.rank F E
Tactic: obtain eq | lt := rank_inf.out.eq_or_lt
-- Lean 4 proof step from Mathlib.FieldTheory.CardinalEmb (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst_3 : Algebra.IsAlgebraic F E
i : (Module.rank F E).ord.ToType
ih : (y : (Module.rank F E).ord.ToType) → y < i → (Module.rank F E).ord.ToType
s : Set E :=
  range fun (j : (↑(Iio i) : Type v)) ↦
    (b : (a : (Module.rank F E).ord.ToType) → E) (ih (↑j : (Module.rank F E).ord.ToType) ⋯)
this_1 :
  ∀ (x : (Module.rank F E).ord.ToType),
    Membership.mem (α := E) (γ := IntermediateField F E) (adjoin F s)
      ((b : (a : (Module.rank F E).ord.ToType) → E) x : E)
this_2 : Module.rank F ↥(adjoin F s) = Module.rank F ↥⊤
x : AddCommMonoid ↥⊤ := inferInstance
this : #(↑(Iio i) : Type v) < Module.rank F E
inl : ∀ (eq : ℵ₀ = Module.rank F E), Module.rank F ↥(adjoin F s) < Module.rank F E
⊢ Module.rank F ↥(adjoin F s) < Module.rank F E
have inr : ∀ (lt : ℵ₀ < Module.rank F E), Module.rank F ↥(adjoin F s) < Module.rank F E
Tactic: obtain eq | lt := rank_inf.out.eq_or_lt
-- Lean 4 proof step from Mathlib.FieldTheory.CardinalEmb (hypothesis)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst_3 : Algebra.IsAlgebraic F E
i : (Module.rank F E).ord.ToType
ih : (y : (Module.rank F E).ord.ToType) → y < i → (Module.rank F E).ord.ToType
s : Set E :=
  range fun (j : (↑(Iio i) : Type v)) ↦
    (b : (a : (Module.rank F E).ord.ToType) → E) (ih (↑j : (Module.rank F E).ord.ToType) ⋯)
this_1 :
  ∀ (x : (Module.rank F E).ord.ToType),
    Membership.mem (α := E) (γ := IntermediateField F E) (adjoin F s)
      ((b : (a : (Module.rank F E).ord.ToType) → E) x : E)
this_2 : Module.rank F ↥(adjoin F s) = Module.rank F ↥⊤
x : AddCommMonoid ↥⊤ := inferInstance
this : #(↑(Iio i) : Type v) < Module.rank F E
eq : ℵ₀ = Module.rank F E
⊢ Module.rank F ↥(adjoin F s) < Module.rank F E
have this₁ : Finite.{v + 1} (↑(Iio i) : Type v)
Tactic: simp_rw [← eq, mk_lt_aleph0_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.FieldTheory.CardinalEmb (hypothesis)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst_3 : Algebra.IsAlgebraic F E
i : (Module.rank F E).ord.ToType
ih : (y : (Module.rank F E).ord.ToType) → y < i → (Module.rank F E).ord.ToType
s : Set E :=
  range fun (j : (↑(Iio i) : Type v)) ↦
    (b : (a : (Module.rank F E).ord.ToType) → E) (ih (↑j : (Module.rank F E).ord.ToType) ⋯)
this_1 :
  ∀ (x : (Module.rank F E).ord.ToType),
    Membership.mem (α := E) (γ := IntermediateField F E) (adjoin F s)
      ((b : (a : (Module.rank F E).ord.ToType) → E) x : E)
this_2 : Module.rank F ↥(adjoin F s) = Module.rank F ↥⊤
x : AddCommMonoid ↥⊤ := inferInstance
eq : ℵ₀ = Module.rank F E
this : Finite.{v + 1} (↑(Iio i) : Type v)
⊢ Module.rank F ↥(adjoin F s) < Module.rank F E
have this₁ : FiniteDimensional.{u, v} F ↥(adjoin F s)
Tactic: have : FiniteDimensional F (adjoin F s) :=
          finiteDimensional_adjoin fun x _ ↦ (IsAlgebraic.isAlgebraic x).isIntegral
-- Lean 4 proof step from Mathlib.FieldTheory.CardinalEmb (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst_3 : Algebra.IsAlgebraic F E
i : (Module.rank F E).ord.ToType
⊢ IsLeast
    {k : (Module.rank F E).ord.ToType |
      ((b : (a : (Module.rank F E).ord.ToType) → E) k : E) ∉
        adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio i)}
    (φ i)
have rw : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: rw [image_eq_range, leastExt, wellFounded_lt.fix_eq]
-- Lean 4 proof step from Mathlib.FieldTheory.CardinalEmb (hypothesis)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst_3 : Algebra.IsAlgebraic F E
i j : (Module.rank F E).ord.ToType
h : i < j
⊢ φ i < φ j
have least : ∀ (i : (Module.rank F E).ord.ToType),
  IsLeast
    {k : (Module.rank F E).ord.ToType |
      ((b : (a : (Module.rank F E).ord.ToType) → E) k : E) ∉
        adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio i)}
    (φ i)
Tactic: have least := isLeast_leastExt (F := F) (E := E)
-- Lean 4 proof step from Mathlib.FieldTheory.CardinalEmb (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst_3 : Algebra.IsAlgebraic F E
i j : (Module.rank F E).ord.ToType
h : i < j
least :
  ∀ (i : (Module.rank F E).ord.ToType),
    IsLeast
      {k : (Module.rank F E).ord.ToType |
        ((b : (a : (Module.rank F E).ord.ToType) → E) k : E) ∉
          adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio i)}
      (φ i)
⊢ φ i < φ j
have by_contra! : ∀ (this : φ j ≤ φ i), False
Tactic: by_contra!
-- Lean 4 proof step from Mathlib.FieldTheory.CardinalEmb (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst_3 : Algebra.IsAlgebraic F E
i j : (Module.rank F E).ord.ToType
h : i < j
least :
  ∀ (i : (Module.rank F E).ord.ToType),
    IsLeast
      {k : (Module.rank F E).ord.ToType |
        ((b : (a : (Module.rank F E).ord.ToType) → E) k : E) ∉
          adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio i)}
      (φ i)
this : φ j ≤ φ i
⊢ False
have inl : ∀ (eq : φ j = φ i), False
Tactic: obtain eq | lt := this.eq_or_lt
-- Lean 4 proof step from Mathlib.FieldTheory.CardinalEmb (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst_3 : Algebra.IsAlgebraic F E
i j : (Module.rank F E).ord.ToType
h : i < j
least :
  ∀ (i : (Module.rank F E).ord.ToType),
    IsLeast
      {k : (Module.rank F E).ord.ToType |
        ((b : (a : (Module.rank F E).ord.ToType) → E) k : E) ∉
          adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio i)}
      (φ i)
this : φ j ≤ φ i
inl : ∀ (eq : φ j = φ i), False
⊢ False
have inr : ∀ (lt : φ j < φ i), False
Tactic: obtain eq | lt := this.eq_or_lt
-- Lean 4 proof step from Mathlib.FieldTheory.CardinalEmb (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst_3 : Algebra.IsAlgebraic F E
i j : (Module.rank F E).ord.ToType
h : i < j
least :
  ∀ (i : (Module.rank F E).ord.ToType),
    IsLeast
      {k : (Module.rank F E).ord.ToType |
        ((b : (a : (Module.rank F E).ord.ToType) → E) k : E) ∉
          adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio i)}
      (φ i)
this : φ j ≤ φ i
lt : φ j < φ i
⊢ False
have inr : Membership.mem (α := E) (γ := IntermediateField F E)
    (adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio i))
    ((b : (a : (Module.rank F E).ord.ToType) → E) (φ j) : E) →
  Iio i ⊆ Iio j
Tactic: refine ((least i).2 <| mt (adjoin.mono _ _ _ (image_mono ?_) ·) (least j).1).not_gt lt
-- Lean 4 proof step from Mathlib.FieldTheory.CardinalEmb (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst_3 : Algebra.IsAlgebraic F E
i : (Module.rank F E).ord.ToType
⊢ Eq (α := IntermediateField F E) (adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio i))
    (adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) '' Iio (φ i)))
have refine_1 : Subset (α := Set E) ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio i)
  ((⇑b : (a : (Module.rank F E).ord.ToType) → E) '' Iio (φ i))
Tactic: refine le_antisymm (adjoin.mono _ _ _ ?_) (adjoin_le_iff.mpr ?_)
-- Lean 4 proof step from Mathlib.FieldTheory.CardinalEmb (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst_3 : Algebra.IsAlgebraic F E
i : (Module.rank F E).ord.ToType
refine_1 :
  Subset (α := Set E) ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio i)
    ((⇑b : (a : (Module.rank F E).ord.ToType) → E) '' Iio (φ i))
⊢ Eq (α := IntermediateField F E) (adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio i))
    (adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) '' Iio (φ i)))
have refine_2 : (⇑b : (a : (Module.rank F E).ord.ToType) → E) '' Iio (φ i) ⊆
  (↑(adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio i)) : Set E)
Tactic: refine le_antisymm (adjoin.mono _ _ _ ?_) (adjoin_le_iff.mpr ?_)
-- Lean 4 proof step from Mathlib.FieldTheory.CardinalEmb (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst_3 : Algebra.IsAlgebraic F E
i : (Module.rank F E).ord.ToType
⊢ Subset (α := Set E) ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio i)
    ((⇑b : (a : (Module.rank F E).ord.ToType) → E) '' Iio (φ i))
have refine_1 : Subset (α := Set E) ((⇑b : (a : (Module.rank F E).ord.ToType) → E) '' φ '' Iio i)
  ((⇑b : (a : (Module.rank F E).ord.ToType) → E) '' Iio (φ i))
Tactic: rw [image_comp]
-- Lean 4 proof step from Mathlib.FieldTheory.CardinalEmb (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst_3 : Algebra.IsAlgebraic F E
i : (Module.rank F E).ord.ToType
⊢ Subset (α := Set E) ((⇑b : (a : (Module.rank F E).ord.ToType) → E) '' φ '' Iio i)
    ((⇑b : (a : (Module.rank F E).ord.ToType) → E) '' Iio (φ i))
have refine_1 : φ '' Iio i ⊆ Iio (φ i)
Tactic: apply image_mono
-- Lean 4 proof step from Mathlib.FieldTheory.CardinalEmb (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst_3 : Algebra.IsAlgebraic F E
i j : (Module.rank F E).ord.ToType
hj : j ∈ Iio (φ i)
⊢ Membership.mem (α := E) (↑(adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio i)) : Set E)
    ((b : (a : (Module.rank F E).ord.ToType) → E) j : E)
have refine_2 : ∀
  (hj :
    ((b : (a : (Module.rank F E).ord.ToType) → E) j : E) ∉
      (↑(adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio i)) : Set E)),
  j ∉ Iio (φ i)
Tactic: contrapose hj
Cleared hypotheses: hj
-- Lean 4 proof step from Mathlib.FieldTheory.CardinalEmb (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst_3 : Algebra.IsAlgebraic F E
⊢ Eq.{v + 1} (α := IntermediateField F E)
    (⨆ (i : (Module.rank F E).ord.ToType), adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio i)) ⊤
have simp_rw : range («ι» := (Module.rank F E).ord.ToType) (⇑b : (a : (Module.rank F E).ord.ToType) → E) ⊆
  (↑(⨆ (i : (Module.rank F E).ord.ToType), adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) '' Iio (φ i))) :
    Set E)
Tactic: simp_rw [adjoin_image_leastExt, eq_top_iff, ← adjoin_basis_eq_top, adjoin_le_iff]
-- Lean 4 proof step from Mathlib.FieldTheory.CardinalEmb (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst_3 : Algebra.IsAlgebraic F E
i : (Module.rank F E).ord.ToType
⊢ Membership.mem (α := E)
    (↑(⨆ (i : (Module.rank F E).ord.ToType), adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) '' Iio (φ i))) :
      Set E)
    ((b : (a : (Module.rank F E).ord.ToType) → E) i : E)
have refine : i ∈ Iio (φ (i⁺))
Tactic: refine le_iSup (α := IntermediateField F E) _ (i⁺) (subset_adjoin _ _ ⟨i, ?_, rfl⟩)
-- Lean 4 proof step from Mathlib.FieldTheory.CardinalEmb (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst_3 : Algebra.IsAlgebraic F E
i : (Module.rank F E).ord.ToType
⊢ Eq (α := IntermediateField F E) (adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio (i⁺)))
    (IntermediateField.restrictScalars F (L' :=
      ↥(adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio i)))
      (↥(adjoin F
            ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ ''
              Iio i)))⟮((b : (a : (Module.rank F E).ord.ToType) → E) (φ i) : E)⟯)
have rw : Eq (α := IntermediateField F E)
  (adjoin F
    ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio i ∪
      {((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ) i}))
  (adjoin F
    ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio i ∪
      singleton (α := E) ((b : (a : (Module.rank F E).ord.ToType) → E) (φ i) : E)))
Tactic: rw [Iio_succ, ← Iio_insert, image_insert_eq, ← union_singleton, adjoin_adjoin_left]
-- Lean 4 proof step from Mathlib.FieldTheory.CardinalEmb (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst_3 : Algebra.IsAlgebraic F E
i : (Module.rank F E).ord.ToType
f : ↥(adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio (i⁺))) →ₐ[F] Ē
⊢ ((succEquiv i :
          (a : ↥(adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio (i⁺))) →ₐ[F] Ē) →
            (↥(adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio i)) →ₐ[F] Ē) ×
              Emb ↥(adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio i))
                ↥(↥(adjoin F
                        ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ ''
                          Iio i)))⟮(b : (a : (Module.rank F E).ord.ToType) → E) (φ i)⟯)
        f).1 =
    f.comp (Subalgebra.inclusion ⋯)
have H : ∀ (x : ↥(adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio i))),
  Eq (α := Ē)
    ((((succEquiv i :
                (a : ↥(adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio (i⁺))) →ₐ[F] Ē) →
                  (↥(adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio i)) →ₐ[F] Ē) ×
                    Emb ↥(adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio i))
                      ↥(↥(adjoin F
                              ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ ''
                                Iio i)))⟮(b : (a : (Module.rank F E).ord.ToType) → E) (φ i)⟯)
              f).1 :
          (a : ↥(adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio i))) → Ē)
        x :
      Ē)
    ((f.comp (Subalgebra.inclusion sorry) :
          (a : ↥(adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio i))) → Ē)
        x :
      Ē)
Tactic: ext
-- Lean 4 proof step from Mathlib.FieldTheory.CardinalEmb (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst_3 : Algebra.IsAlgebraic F E
i j : WithTop (Module.rank F E).ord.ToType
h : i < j
⊢ LT.lt.{v} (α := IntermediateField F E)
    ((fun (i : WithTop (Module.rank F E).ord.ToType) ↦
        (recTopCoe (C := fun (x : WithTop (Module.rank F E).ord.ToType) ↦ IntermediateField F E) ⊤
            (fun (x : (Module.rank F E).ord.ToType) ↦
              adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio x))
            i :
          IntermediateField F E))
      i)
    ((fun (i : WithTop (Module.rank F E).ord.ToType) ↦
        (recTopCoe (C := fun (x : WithTop (Module.rank F E).ord.ToType) ↦ IntermediateField F E) ⊤
            (fun (x : (Module.rank F E).ord.ToType) ↦
              adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio x))
            i :
          IntermediateField F E))
      j)
have top : ∀ (h : i < ⊤),
  LT.lt.{v} (α := IntermediateField F E)
    ((fun (i : WithTop (Module.rank F E).ord.ToType) ↦
        (recTopCoe (C := fun (x : WithTop (Module.rank F E).ord.ToType) ↦ IntermediateField F E) ⊤
            (fun (x : (Module.rank F E).ord.ToType) ↦
              adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio x))
            i :
          IntermediateField F E))
      i)
    ((fun (i : WithTop (Module.rank F E).ord.ToType) ↦
        (recTopCoe (C := fun (x : WithTop (Module.rank F E).ord.ToType) ↦ IntermediateField F E) ⊤
            (fun (x : (Module.rank F E).ord.ToType) ↦
              adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio x))
            i :
          IntermediateField F E))
      ⊤)
Tactic: cases j
Cleared hypotheses: j, h