awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.CardinalEmb
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

Tactic:
ne_of_lt ?_ this

Premises used: ne_of_lt
-- Module: Mathlib.FieldTheory.CardinalEmb
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 ↥⊤
refine : Module.rank F ↥(adjoin F s) < Module.rank F ↥⊤
⊢ False

Tactic:
refine ne_of_lt ?_ this

Premises used: ne_of_lt
-- Module: Mathlib.FieldTheory.CardinalEmb
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
rw : Module.rank F E
| Module.rank F ↥⊤

Tactic:
rw [topEquiv.toLinearEquiv.rank_eq]

Premises used: LinearEquiv.rank_eq, AlgEquiv.toLinearEquiv, IntermediateField.topEquiv
-- Module: Mathlib.FieldTheory.CardinalEmb
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
conv_rhs : Module.rank F ↥(adjoin F s) < Module.rank F E
⊢ Module.rank F ↥(adjoin F s) < Module.rank F ↥⊤

Tactic:
conv_rhs => rw [topEquiv.toLinearEquiv.rank_eq]

Premises used: LinearEquiv.rank_eq, AlgEquiv.toLinearEquiv, IntermediateField.topEquiv
-- Module: Mathlib.FieldTheory.CardinalEmb
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 E).ord.ToType).ord = Ordinal.type fun (x1 x2 : (Module.rank F E).ord.ToType) ↦ x1 < x2

Tactic:
simp
-- Module: Mathlib.FieldTheory.CardinalEmb
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
⊢ #(↑(Iio i) : Type v) < #(Module.rank F E).ord.ToType

Tactic:
have := mk_Iio_lt i (by simp)
-- Module: Mathlib.FieldTheory.CardinalEmb
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
⊢ #(↑(Iio i) : Type v) < Module.rank F E

Tactic:
rw [mk_toType, card_ord] at this

Premises used: Cardinal.card_ord, Cardinal.mk_toType
-- Module: Mathlib.FieldTheory.CardinalEmb
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
inr : ∀ (lt : ℵ₀ < Module.rank F E), Module.rank F ↥(adjoin F s) < Module.rank F E
⊢ Module.rank F ↥(adjoin F s) < Module.rank F E

Tactic:
obtain eq | lt := rank_inf.out.eq_or_lt

Premises used: LE.le.eq_or_lt, Fact.out
-- Module: Mathlib.FieldTheory.CardinalEmb
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
⊢ Finite.{v + 1} (↑(Iio i) : Type v)

Tactic:
simp_rw [← eq, mk_lt_aleph0_iff] at this

Premises used: Cardinal.mk_lt_aleph0_iff
-- Module: Mathlib.FieldTheory.CardinalEmb
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)
⊢ FiniteDimensional.{u, v} F ↥(adjoin F s)

Tactic:
have : FiniteDimensional F (adjoin F s) :=
          finiteDimensional_adjoin fun x _ ↦ (IsAlgebraic.isAlgebraic x).isIntegral
-- Module: Mathlib.FieldTheory.CardinalEmb
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_3 : Finite.{v + 1} (↑(Iio i) : Type v)
this : FiniteDimensional.{u, v} F ↥(adjoin F s)
⊢ Module.rank F ↥(adjoin F s) < Module.rank F E

Tactic:
(Module.rank_lt_aleph0 _ _).trans_eq eq

Premises used: LT.lt.trans_eq, Module.rank_lt_aleph0
-- Module: Mathlib.FieldTheory.CardinalEmb
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_3 : Finite.{v + 1} (↑(Iio i) : Type v)
this : FiniteDimensional.{u, v} F ↥(adjoin F s)
⊢ Module.rank F ↥(adjoin F s) < Module.rank F E

Tactic:
exact (Module.rank_lt_aleph0 _ _).trans_eq eq

Premises used: LT.lt.trans_eq, Module.rank_lt_aleph0
-- Module: Mathlib.FieldTheory.CardinalEmb
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
lt : ℵ₀ < Module.rank F E
⊢ Module.rank F ↥(adjoin F s) < Module.rank F E

Tactic:
(Subalgebra.equivOfEq _ _ <| adjoin_toSubalgebra_of_isAlgebraic
          fun x _ ↦ IsAlgebraic.isAlgebraic x) |>.toLinearEquiv.rank_eq.trans_lt <|
          (Algebra.rank_adjoin_le _).trans_lt (max_lt (mk_range_le.trans_lt this) lt)

Premises used: Algebra.IsAlgebraic.isAlgebraic, Set.Mem, Subalgebra.equivOfEq, Cardinal.mk_range_le, max_lt, LinearEquiv.rank_eq, IntermediateField.adjoin, AlgEquiv.toLinearEquiv, Eq.trans_lt, IntermediateField.adjoin_toSubalgebra_of_isAlgebraic, LE.le.trans_lt, Algebra.rank_adjoin_le
-- Module: Mathlib.FieldTheory.CardinalEmb
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
lt : ℵ₀ < Module.rank F E
⊢ Module.rank F ↥(adjoin F s) < Module.rank F E

Tactic:
exact (Subalgebra.equivOfEq _ _ <| adjoin_toSubalgebra_of_isAlgebraic
          fun x _ ↦ IsAlgebraic.isAlgebraic x) |>.toLinearEquiv.rank_eq.trans_lt <|
          (Algebra.rank_adjoin_le _).trans_lt (max_lt (mk_range_le.trans_lt this) lt)

Premises used: Algebra.IsAlgebraic.isAlgebraic, Subalgebra.equivOfEq, Cardinal.mk_range_le, max_lt, LinearEquiv.rank_eq, AlgEquiv.toLinearEquiv, Eq.trans_lt, IntermediateField.adjoin_toSubalgebra_of_isAlgebraic, LE.le.trans_lt, Algebra.rank_adjoin_le
-- Module: Mathlib.FieldTheory.CardinalEmb
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
rw : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ 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:
rw [image_eq_range, leastExt, wellFounded_lt.fix_eq]

Premises used: Set.image_eq_range, wellFounded_lt, WellFounded.fix_eq, Field.Emb.Cardinal.leastExt
-- Module: Mathlib.FieldTheory.CardinalEmb
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
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
⟨wellFounded_lt.min_mem _ _, fun _ ↦ (wellFounded_lt.min_le ·)⟩

Premises used: WellFounded.min_mem, WellFounded.min_le, IsLeast, wellFounded_lt, And.intro
-- Module: Mathlib.FieldTheory.CardinalEmb
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
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
exact ⟨wellFounded_lt.min_mem _ _, fun _ ↦ (wellFounded_lt.min_le ·)⟩
-- Module: Mathlib.FieldTheory.CardinalEmb
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 : (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)
-- Module: Mathlib.FieldTheory.CardinalEmb
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)
by_contra! : ∀ (this : φ j ≤ φ i), False
⊢ φ i < φ j

Tactic:
by_contra!
-- Module: Mathlib.FieldTheory.CardinalEmb
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
inr : ∀ (lt : φ j < φ i), False
⊢ False

Tactic:
obtain eq | lt := this.eq_or_lt

Premises used: LE.le.eq_or_lt
-- Module: Mathlib.FieldTheory.CardinalEmb
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
eq : φ j = φ i
⊢ False

Tactic:
(least j).1 (subset_adjoin _ _ ⟨i, h, congr_arg b eq.symm⟩)

Premises used: Field.Emb.Cardinal.wellOrderedBasis, IntermediateField.subset_adjoin, congr_arg, And.left, And.intro, Exists.intro, Eq.symm, DFunLike.coe
-- Module: Mathlib.FieldTheory.CardinalEmb
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
eq : φ j = φ i
⊢ False

Tactic:
exact (least j).1 (subset_adjoin _ _ ⟨i, h, congr_arg b eq.symm⟩)
-- Module: Mathlib.FieldTheory.CardinalEmb
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

Tactic:
((least i).2 <| mt (adjoin.mono _ _ _ (image_mono ?_) ·) (least j).1).not_gt lt

Premises used: IntermediateField.adjoin.mono, Set.image_mono, Function.comp, mt, Field.Emb.Cardinal.wellOrderedBasis, And.right, LE.le.not_gt, And.left, Set.image, Set.Iio, DFunLike.coe, Field.Emb.Cardinal.leastExt
-- Module: Mathlib.FieldTheory.CardinalEmb
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
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
⊢ False

Tactic:
refine ((least i).2 <| mt (adjoin.mono _ _ _ (image_mono ?_) ·) (least j).1).not_gt lt

Premises used: IntermediateField.adjoin.mono, Set.image_mono, Function.comp, mt, Field.Emb.Cardinal.wellOrderedBasis, And.right, LE.le.not_gt, And.left, Set.image, Set.Iio, DFunLike.coe, Field.Emb.Cardinal.leastExt
-- Module: Mathlib.FieldTheory.CardinalEmb
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
h_1 :
  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:
fun k (hk : k < i) ↦ hk.trans h

Premises used: Set.Mem, setOf, Set.Subset, LT.lt.trans, Set.Iio
-- Module: Mathlib.FieldTheory.CardinalEmb
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
h_1 :
  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:
exact fun k (hk : k < i) ↦ hk.trans h

Premises used: LT.lt.trans
-- Module: Mathlib.FieldTheory.CardinalEmb
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)))

Tactic:
le_antisymm (adjoin.mono _ _ _ ?_) (adjoin_le_iff.mpr ?_)

Premises used: Iff.mpr, IntermediateField.adjoin.mono, IntermediateField.adjoin_le_iff, le_antisymm
-- Module: Mathlib.FieldTheory.CardinalEmb
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))
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)
⊢ 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)))

Tactic:
refine le_antisymm (adjoin.mono _ _ _ ?_) (adjoin_le_iff.mpr ?_)

Premises used: Iff.mpr, IntermediateField.adjoin.mono, IntermediateField.adjoin_le_iff, le_antisymm
-- Module: Mathlib.FieldTheory.CardinalEmb
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))
⊢ 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]

Premises used: Set.image_comp