awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Defs
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
A : Type u_5
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
e : ι ≃ ι'
f : ι' → A
g : ι → A
h : f ∘ (⇑e : (a : ι) → ι') = g
⊢ IsTranscendenceBasis R g ↔ IsTranscendenceBasis R f

Tactic:
h ▸ isTranscendenceBasis_equiv e

Premises used: Eq.rec, isTranscendenceBasis_equiv
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Defs
Goal:
R : Type u_3
A : Type u_5
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
ι : Type u_7
f : ι → A
hf : Injective f
⊢ IsTranscendenceBasis.{u_5, u_3, u_5} (ι := { x : A // x ∈ range f }) R
      (Subtype.val (p := fun (x : A) ↦ x ∈ range f)) ↔
    IsTranscendenceBasis R f

Tactic:
.symm <| isTranscendenceBasis_equiv' (Equiv.ofInjective f hf) rfl

Premises used: Equiv.ofInjective, isTranscendenceBasis_equiv', Iff.symm, rfl
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Defs
Goal:
R : Type u_3
A : Type u_5
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
ι : Type u_7
s : Set ι
f : ι → A
hf : InjOn f s
⊢ (IsTranscendenceBasis.{u_7, u_3, u_5} R (A := A) fun (x : (↑s : Type u_7)) ↦ f (↑x : ι)) ↔
    IsTranscendenceBasis R (A := A) fun (x : (↑(f '' s) : Type u_5)) ↦ (↑x : A)

Tactic:
isTranscendenceBasis_equiv' (Equiv.Set.imageOfInjOn _ _ hf) rfl

Premises used: Equiv.Set.imageOfInjOn, isTranscendenceBasis_equiv', rfl
-- Module: Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality
Goal:
F : Type u
E : Type v
inst : CommRing F
inst_1 : Nontrivial F
inst_2 : CommRing E
inst_3 : IsDomain E
inst_4 : Algebra F E
ι : Type w
x : ι → E
inst_5 : Nonempty ι
hx : IsTranscendenceBasis F x
K : Subalgebra F E := adjoin F (range x)
this : #E = #↥K
⊢ lift.{max u w, v} #E = max (max (lift.{max v w, u} #F) (lift.{max u v, w} #ι)) ℵ₀

Tactic:
simp [K, this, ← lift_mk_eq'.2 ⟨hx.1.aevalEquiv.toEquiv⟩]

Premises used: Iff.mpr, AlgebraicIndependent.aevalEquiv, Cardinal.lift_mk_eq', Nonempty.intro, And.left, AlgEquiv.toEquiv
-- Module: Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality
Goal:
F : Type u
E : Type v
inst : CommRing F
inst_1 : Nontrivial F
inst_2 : CommRing E
inst_3 : IsDomain E
inst_4 : Algebra F E
ι : Type w
x : ι → E
inst_5 : Nonempty ι
hx : IsTranscendenceBasis F x
K : Subalgebra F E := adjoin F (range x)
suffices : #E = #↥K
⊢ lift.{max u w, v} #E = max (max (lift.{max v w, u} #F) (lift.{max u v, w} #ι)) ℵ₀

Tactic:
suffices #E = #K by simp [K, this, ← lift_mk_eq'.2 ⟨hx.1.aevalEquiv.toEquiv⟩]
-- Module: Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality
Goal:
F : Type u
E : Type v
inst : CommRing F
inst_1 : Nontrivial F
inst_2 : CommRing E
inst_3 : IsDomain E
inst_4 : Algebra F E
ι : Type w
x : ι → E
inst_5 : Nonempty ι
hx : IsTranscendenceBasis F x
K : Subalgebra F E := adjoin F (range x)
⊢ Algebra.IsAlgebraic (↥K) E

Tactic:
haveI : Algebra.IsAlgebraic K E := hx.isAlgebraic
-- Module: Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality
Goal:
F : Type u
E : Type v
inst : CommRing F
inst_1 : Nontrivial F
inst_2 : CommRing E
inst_3 : IsDomain E
inst_4 : Algebra F E
ι : Type w
x : ι → E
inst_5 : Nonempty ι
hx : IsTranscendenceBasis F x
K : Subalgebra F E := adjoin F (range x)
this : Algebra.IsAlgebraic (↥K) E
⊢ #E = #↥K

Tactic:
le_antisymm ?_ (mk_le_of_injective Subtype.val_injective)

Premises used: Subtype.val_injective, le_antisymm, Cardinal.mk_le_of_injective
-- Module: Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality
Goal:
F : Type u
E : Type v
inst : CommRing F
inst_1 : Nontrivial F
inst_2 : CommRing E
inst_3 : IsDomain E
inst_4 : Algebra F E
ι : Type w
x : ι → E
inst_5 : Nonempty ι
hx : IsTranscendenceBasis F x
K : Subalgebra F E := adjoin F (range x)
this : Algebra.IsAlgebraic (↥K) E
refine : #E ≤ #↥K
⊢ #E = #↥K

Tactic:
refine le_antisymm ?_ (mk_le_of_injective Subtype.val_injective)

Premises used: Subtype.val_injective, le_antisymm, Cardinal.mk_le_of_injective
-- Module: Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality
Goal:
F : Type u
E : Type v
inst : CommRing F
inst_1 : Nontrivial F
inst_2 : CommRing E
inst_3 : IsDomain E
inst_4 : Algebra F E
ι : Type w
x : ι → E
inst_5 : Nonempty ι
hx : IsTranscendenceBasis F x
K : Subalgebra F E := adjoin F (range x)
this : Algebra.IsAlgebraic (↥K) E
⊢ Infinite.{v + 1} ↥K

Tactic:
haveI : Infinite K := hx.1.aevalEquiv.infinite_iff.1 inferInstance
-- Module: Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality
Goal:
F : Type u
E : Type v
inst : CommRing F
inst_1 : Nontrivial F
inst_2 : CommRing E
inst_3 : IsDomain E
inst_4 : Algebra F E
ι : Type w
x : ι → E
inst_5 : Nonempty ι
hx : IsTranscendenceBasis F x
K : Subalgebra F E := adjoin F (range x)
this_1 : Algebra.IsAlgebraic (↥K) E
this : Infinite.{v + 1} ↥K
⊢ #E ≤ #↥K

Tactic:
simpa only [sup_eq_left.2 (aleph0_le_mk K)] using Algebra.IsAlgebraic.cardinalMk_le_max K E

Premises used: Iff.mpr, Algebra.IsAlgebraic.cardinalMk_le_max, Membership.mem, Subtype, sup_eq_left, Cardinal.aleph0_le_mk
-- Module: Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
ι : Type w
x : ι → E
inst_3 : Nonempty ι
hx : IsTranscendenceBasis F x
K : IntermediateField F E := IntermediateField.adjoin F (range x)
⊢ Algebra.IsAlgebraic (↥K) E

Tactic:
haveI : Algebra.IsAlgebraic K E := hx.isAlgebraic_field
-- Module: Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
ι : Type w
x : ι → E
inst_3 : Nonempty ι
hx : IsTranscendenceBasis F x
K : IntermediateField F E := IntermediateField.adjoin F (range x)
this : Algebra.IsAlgebraic (↥K) E
rw :
  max (max (lift.{max w v, u} #F) (lift.{max u v, w} #ι)) ℵ₀ * lift.{max u w, v} (Module.rank (↥K) E) =
    max (max (lift.{max v w, u} #F) (lift.{max u v, w} #ι)) ℵ₀
⊢ lift.{max u w, v} (Module.rank F E) = max (max (lift.{max v w, u} #F) (lift.{max u v, w} #ι)) ℵ₀

Tactic:
rw [← rank_mul_rank F K E, lift_mul, ← hx.1.aevalEquivField.toLinearEquiv.lift_rank_eq,
    MvRatFunc.rank_eq_max_lift, lift_max, lift_max, lift_lift, lift_lift, lift_aleph0]

Premises used: Cardinal.lift_lift, rank_mul_rank, LinearEquiv.lift_rank_eq, AlgebraicIndependent.aevalEquivField, Membership.mem, Subtype, And.left, AlgEquiv.toLinearEquiv, Cardinal.lift_mul, Cardinal.lift_aleph0, MvRatFunc.rank_eq_max_lift, Cardinal.lift_max
-- Module: Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
ι : Type w
x : ι → E
inst_3 : Nonempty ι
hx : IsTranscendenceBasis F x
K : IntermediateField F E := IntermediateField.adjoin F (range x)
this : Algebra.IsAlgebraic (↥K) E
⊢ lift.{max u w, v} (Module.rank (↥K) E) ≠ 0

Tactic:
simp [rank_pos.ne']

Premises used: LT.lt.ne', rank_pos
-- Module: Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
ι : Type w
x : ι → E
inst_3 : Nonempty ι
hx : IsTranscendenceBasis F x
K : IntermediateField F E := IntermediateField.adjoin F (range x)
this : Algebra.IsAlgebraic (↥K) E
refine : lift.{max u w, v} (max #↥K ℵ₀) = max (max (lift.{max w v, u} #F) (lift.{max u v, w} #ι)) ℵ₀
⊢ max (max (lift.{max w v, u} #F) (lift.{max u v, w} #ι)) ℵ₀ * lift.{max u w, v} (Module.rank (↥K) E) =
    max (max (lift.{max v w, u} #F) (lift.{max u v, w} #ι)) ℵ₀

Tactic:
refine mul_eq_left le_sup_right ((lift_le.2 ((rank_le_card K E).trans
    (Algebra.IsAlgebraic.cardinalMk_le_max K E))).trans_eq ?_) (by simp [rank_pos.ne'])

Premises used: Iff.mpr, LE.le.trans_eq, Cardinal.mul_eq_left, Algebra.IsAlgebraic.cardinalMk_le_max, Membership.mem, Subtype, le_sup_right, rank_le_card, LE.le.trans, Cardinal.lift_le
-- Module: Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
ι : Type w
x : ι → E
inst_3 : Nonempty ι
hx : IsTranscendenceBasis F x
K : IntermediateField F E := IntermediateField.adjoin F (range x)
this : Algebra.IsAlgebraic (↥K) E
⊢ lift.{max u w, v} (max #↥K ℵ₀) = max (max (lift.{max w v, u} #F) (lift.{max u v, w} #ι)) ℵ₀

Tactic:
simp [K, ← lift_mk_eq'.2 ⟨hx.1.aevalEquivField.toEquiv⟩]

Premises used: Iff.mpr, AlgebraicIndependent.aevalEquivField, Cardinal.lift_mk_eq', Nonempty.intro, And.left, AlgEquiv.toEquiv
-- Module: Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.Transcendental F E
obtain : ∀ (ι : Type v) (x : ι → E) (hx : IsTranscendenceBasis F x), Module.rank F E = #E
⊢ Module.rank F E = #E

Tactic:
obtain ⟨ι, x, hx⟩ := exists_isTranscendenceBasis' F E

Premises used: exists_isTranscendenceBasis'
-- Module: Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.Transcendental F E
ι : Type v
x : ι → E
hx : IsTranscendenceBasis F x
⊢ Nonempty ι

Tactic:
haveI := hx.nonempty_iff_transcendental.2 ‹_›
-- Module: Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.Transcendental F E
ι : Type v
x : ι → E
hx : IsTranscendenceBasis F x
this : Nonempty ι
⊢ Module.rank F E = #E

Tactic:
simpa [← hx.lift_cardinalMk_eq_max_lift] using hx.lift_rank_eq_max_lift

Premises used: IsTranscendenceBasis.lift_cardinalMk_eq_max_lift, IsTranscendenceBasis.lift_rank_eq_max_lift
-- Module: Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A B : IntermediateField F E
pos : ∀ (hA : Algebra.IsAlgebraic.{u, v} F ↥A), Module.rank F ↥(A ⊔ B) ≤ Module.rank F ↥A * Module.rank F ↥B
neg : ∀ (hA : ¬Algebra.IsAlgebraic.{u, v} F ↥A), Module.rank F ↥(A ⊔ B) ≤ Module.rank F ↥A * Module.rank F ↥B
⊢ Module.rank F ↥(A ⊔ B) ≤ Module.rank F ↥A * Module.rank F ↥B

Tactic:
by_cases hA : Algebra.IsAlgebraic F A

Premises used: Membership.mem, Subtype, Algebra.IsAlgebraic
-- Module: Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A B : IntermediateField F E
hA : Algebra.IsAlgebraic.{u, v} F ↥A
⊢ Module.rank F ↥(A ⊔ B) ≤ Module.rank F ↥A * Module.rank F ↥B

Tactic:
rank_sup_le_of_isAlgebraic A B (Or.inl hA)

Premises used: IntermediateField.rank_sup_le_of_isAlgebraic, Or.inl
-- Module: Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A B : IntermediateField F E
hA : Algebra.IsAlgebraic.{u, v} F ↥A
⊢ Module.rank F ↥(A ⊔ B) ≤ Module.rank F ↥A * Module.rank F ↥B

Tactic:
exact rank_sup_le_of_isAlgebraic A B (Or.inl hA)

Premises used: IntermediateField.rank_sup_le_of_isAlgebraic, Or.inl
-- Module: Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A B : IntermediateField F E
hA : ¬Algebra.IsAlgebraic.{u, v} F ↥A
pos : ∀ (hB : Algebra.IsAlgebraic.{u, v} F ↥B), Module.rank F ↥(A ⊔ B) ≤ Module.rank F ↥A * Module.rank F ↥B
neg : ∀ (hB : ¬Algebra.IsAlgebraic.{u, v} F ↥B), Module.rank F ↥(A ⊔ B) ≤ Module.rank F ↥A * Module.rank F ↥B
⊢ Module.rank F ↥(A ⊔ B) ≤ Module.rank F ↥A * Module.rank F ↥B

Tactic:
by_cases hB : Algebra.IsAlgebraic F B

Premises used: Membership.mem, Subtype, Algebra.IsAlgebraic
-- Module: Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A B : IntermediateField F E
hA : ¬Algebra.IsAlgebraic.{u, v} F ↥A
hB : Algebra.IsAlgebraic.{u, v} F ↥B
⊢ Module.rank F ↥(A ⊔ B) ≤ Module.rank F ↥A * Module.rank F ↥B

Tactic:
rank_sup_le_of_isAlgebraic A B (Or.inr hB)

Premises used: IntermediateField.rank_sup_le_of_isAlgebraic, Or.inr
-- Module: Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A B : IntermediateField F E
hA : ¬Algebra.IsAlgebraic.{u, v} F ↥A
hB : Algebra.IsAlgebraic.{u, v} F ↥B
⊢ Module.rank F ↥(A ⊔ B) ≤ Module.rank F ↥A * Module.rank F ↥B

Tactic:
exact rank_sup_le_of_isAlgebraic A B (Or.inr hB)

Premises used: IntermediateField.rank_sup_le_of_isAlgebraic, Or.inr
-- Module: Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A B : IntermediateField F E
hA : ¬Algebra.IsAlgebraic.{u, v} F ↥A
hB : ¬Algebra.IsAlgebraic.{u, v} F ↥B
⊢ Algebra.Transcendental.{u, v} F ↥A

Tactic:
rw [← Algebra.transcendental_iff_not_isAlgebraic] at hA hB

Premises used: Algebra.transcendental_iff_not_isAlgebraic
-- Module: Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A B : IntermediateField F E
hA : ¬Algebra.IsAlgebraic.{u, v} F ↥A
hB : ¬Algebra.IsAlgebraic.{u, v} F ↥B
hA₁ : Algebra.Transcendental.{u, v} F ↥A
⊢ Algebra.Transcendental.{u, v} F ↥B

Tactic:
rw [← Algebra.transcendental_iff_not_isAlgebraic] at hA hB

Premises used: Algebra.transcendental_iff_not_isAlgebraic
-- Module: Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A B : IntermediateField F E
hA : Algebra.Transcendental.{u, v} F ↥A
hB : Algebra.Transcendental.{u, v} F ↥B
⊢ Algebra.Transcendental.{u, v} F ↥(A ⊔ B)

Tactic:
haveI : Algebra.Transcendental F ↥(A ⊔ B) := .ringHom_of_comp_eq (RingHom.id F)
    (inclusion le_sup_left) Function.surjective_id (inclusion_injective _) rfl
-- Module: Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A B : IntermediateField F E
hA : Algebra.Transcendental.{u, v} F ↥A
hB : Algebra.Transcendental.{u, v} F ↥B
this : Algebra.Transcendental.{u, v} F ↥(A ⊔ B)
⊢ Infinite.{v + 1} ↥A

Tactic:
haveI := Algebra.Transcendental.infinite F A
-- Module: Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A B : IntermediateField F E
hA : Algebra.Transcendental.{u, v} F ↥A
hB : Algebra.Transcendental.{u, v} F ↥B
this_1 : Algebra.Transcendental.{u, v} F ↥(A ⊔ B)
this : Infinite.{v + 1} ↥A
⊢ Infinite.{v + 1} ↥B

Tactic:
haveI := Algebra.Transcendental.infinite F B
-- Module: Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A B : IntermediateField F E
hA : Algebra.Transcendental.{u, v} F ↥A
hB : Algebra.Transcendental.{u, v} F ↥B
this_1 : Algebra.Transcendental.{u, v} F ↥(A ⊔ B)
this_2 : Infinite.{v + 1} ↥A
this : Infinite.{v + 1} ↥B
neg : #↥(A ⊔ B) ≤ #↥A * #↥B
⊢ Module.rank F ↥(A ⊔ B) ≤ Module.rank F ↥A * Module.rank F ↥B

Tactic:
simp_rw [Algebra.Transcendental.rank_eq_cardinalMk]

Premises used: Algebra.Transcendental.rank_eq_cardinalMk
-- Module: Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A B : IntermediateField F E
hA : Algebra.Transcendental.{u, v} F ↥A
hB : Algebra.Transcendental.{u, v} F ↥B
this_1 : Algebra.Transcendental.{u, v} F ↥(A ⊔ B)
this_2 : Infinite.{v + 1} ↥A
this : Infinite.{v + 1} ↥B
neg : Cardinal.lift.{u, v} #↥(adjoin F ((↑A : Set E) ∪ (↑B : Set E))) ≤ Cardinal.lift.{u, v} (max #↥A #↥B)
⊢ #↥(A ⊔ B) ≤ #↥A * #↥B

Tactic:
rw [sup_def, mul_mk_eq_max, ← Cardinal.lift_le.{u}]

Premises used: IntermediateField.sup_def, Cardinal.mul_mk_eq_max
-- Module: Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A B : IntermediateField F E
hA : Algebra.Transcendental.{u, v} F ↥A
hB : Algebra.Transcendental.{u, v} F ↥B
this_1 : Algebra.Transcendental.{u, v} F ↥(A ⊔ B)
this_2 : Infinite.{v + 1} ↥A
this : Infinite.{v + 1} ↥B
⊢ Cardinal.lift.{u, v} #↥(adjoin F ((↑A : Set E) ∪ (↑B : Set E))) ≤ Cardinal.lift.{u, v} (max #↥A #↥B)

Tactic:
(lift_cardinalMk_adjoin_le _ _).trans ?_

Premises used: IntermediateField.lift_cardinalMk_adjoin_le, LE.le.trans
-- Module: Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A B : IntermediateField F E
hA : Algebra.Transcendental.{u, v} F ↥A
hB : Algebra.Transcendental.{u, v} F ↥B
this_1 : Algebra.Transcendental.{u, v} F ↥(A ⊔ B)
this_2 : Infinite.{v + 1} ↥A
this : Infinite.{v + 1} ↥B
neg :
  max (max (Cardinal.lift.{v, u} #F) (Cardinal.lift.{u, v} #(↑((↑A : Set E) ∪ (↑B : Set E)) : Type v))) ℵ₀ ≤
    Cardinal.lift.{u, v} (max #↥A #↥B)
⊢ Cardinal.lift.{u, v} #↥(adjoin F ((↑A : Set E) ∪ (↑B : Set E))) ≤ Cardinal.lift.{u, v} (max #↥A #↥B)

Tactic:
refine (lift_cardinalMk_adjoin_le _ _).trans ?_

Premises used: IntermediateField.lift_cardinalMk_adjoin_le, LE.le.trans
-- Module: Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A B : IntermediateField F E
hA : Algebra.Transcendental.{u, v} F ↥A
hB : Algebra.Transcendental.{u, v} F ↥B
this_1 : Algebra.Transcendental.{u, v} F ↥(A ⊔ B)
this_2 : Infinite.{v + 1} ↥A
this : Infinite.{v + 1} ↥B
h₁ : Cardinal.lift.{u, v} #(↑((↑A : Set E) ∪ (↑B : Set E)) : Type v) ≤ Cardinal.lift.{u, v} (max #↥A #↥B)
⊢ max (max (Cardinal.lift.{v, u} #F) (Cardinal.lift.{u, v} #(↑((↑A : Set E) ∪ (↑B : Set E)) : Type v))) ℵ₀ ≤
    max (max (Cardinal.lift.{v, u} #F) (Cardinal.lift.{u, v} (max #↥A #↥B))) ℵ₀

Tactic:
gcongr
-- Module: Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A B : IntermediateField F E
hA : Algebra.Transcendental.{u, v} F ↥A
hB : Algebra.Transcendental.{u, v} F ↥B
this_1 : Algebra.Transcendental.{u, v} F ↥(A ⊔ B)
this_2 : Infinite.{v + 1} ↥A
this : Infinite.{v + 1} ↥B
h₁ : #(↑((↑A : Set E) ∪ (↑B : Set E)) : Type v) ≤ max #↥A #↥B
⊢ Cardinal.lift.{u, v} #(↑((↑A : Set E) ∪ (↑B : Set E)) : Type v) ≤ Cardinal.lift.{u, v} (max #↥A #↥B)

Tactic:
rw [Cardinal.lift_le]

Premises used: Cardinal.lift_le
-- Module: Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A B : IntermediateField F E
hA : Algebra.Transcendental.{u, v} F ↥A
hB : Algebra.Transcendental.{u, v} F ↥B
this_1 : Algebra.Transcendental.{u, v} F ↥(A ⊔ B)
this_2 : Infinite.{v + 1} ↥A
this : Infinite.{v + 1} ↥B
⊢ #(↑(↑A : Set E) : Type v) + #(↑(↑B : Set E) : Type v) = max #↥A #↥B

Tactic:
simp
-- Module: Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A B : IntermediateField F E
hA : Algebra.Transcendental.{u, v} F ↥A
hB : Algebra.Transcendental.{u, v} F ↥B
this_1 : Algebra.Transcendental.{u, v} F ↥(A ⊔ B)
this_2 : Infinite.{v + 1} ↥A
this : Infinite.{v + 1} ↥B
⊢ #(↑((↑A : Set E) ∪ (↑B : Set E)) : Type v) ≤ max #↥A #↥B

Tactic:
exact (mk_union_le _ _).trans_eq (by simp)

Premises used: LE.le.trans_eq, Cardinal.mk_union_le
-- Module: Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A B : IntermediateField F E
hA : Algebra.Transcendental.{u, v} F ↥A
hB : Algebra.Transcendental.{u, v} F ↥B
this_1 : Algebra.Transcendental.{u, v} F ↥(A ⊔ B)
this_2 : Infinite.{v + 1} ↥A
this : Infinite.{v + 1} ↥B
⊢ max (max (Cardinal.lift.{v, u} #F) (Cardinal.lift.{u, v} (max #↥A #↥B))) ℵ₀ = Cardinal.lift.{u, v} (max #↥A #↥B)

Tactic:
simp [lift_mk_le_lift_mk_of_injective (algebraMap F A).injective]

Premises used: Algebra.algebraMap, Membership.mem, Subtype, RingHom.injective, Cardinal.lift_mk_le_lift_mk_of_injective
-- Module: Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A B : IntermediateField F E
hA : Algebra.Transcendental.{u, v} F ↥A
hB : Algebra.Transcendental.{u, v} F ↥B
this_1 : Algebra.Transcendental.{u, v} F ↥(A ⊔ B)
this_2 : Infinite.{v + 1} ↥A
this : Infinite.{v + 1} ↥B
_ :
  max (max (Cardinal.lift.{v, u} #F) (Cardinal.lift.{u, v} #(↑((↑A : Set E) ∪ (↑B : Set E)) : Type v))) ℵ₀ ≤
    max (max (Cardinal.lift.{v, u} #F) (Cardinal.lift.{u, v} (max #↥A #↥B))) ℵ₀
_₁ : max (max (Cardinal.lift.{v, u} #F) (Cardinal.lift.{u, v} (max #↥A #↥B))) ℵ₀ = Cardinal.lift.{u, v} (max #↥A #↥B)
⊢ max (max (Cardinal.lift.{v, u} #F) (Cardinal.lift.{u, v} #(↑((↑A : Set E) ∪ (↑B : Set E)) : Type v))) ℵ₀ ≤
    Cardinal.lift.{u, v} (max #↥A #↥B)

Tactic:
calc
    _ ≤ Cardinal.lift.{v} #F ⊔ Cardinal.lift.{u} (#A ⊔ #B) ⊔ ℵ₀ := by
      gcongr
      rw [Cardinal.lift_le]
      exact (mk_union_le _ _).trans_eq (by simp)
    _ = _ := by
      simp [lift_mk_le_lift_mk_of_injective (algebraMap F A).injective]
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
R : Type u_1
A : Type w
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
s : Set A
hs : AlgebraicIndepOn R _root_.id s
⊢ ∃ (t : Set A),
    s ⊆ t ∧ IsTranscendenceBasis.{w, u_1, w} (ι := { x : A // x ∈ t }) R (Subtype.val (p := fun (x : A) ↦ x ∈ t))

Tactic:
simpa [← isTranscendenceBasis_iff_maximal]
    using exists_maximal_algebraicIndependent s _ (subset_univ _) hs

Premises used: Set.subset_univ, isTranscendenceBasis_iff_maximal, exists_maximal_algebraicIndependent
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
R : Type u_1
A : Type w
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
⊢ ∃ (s : Set A), IsTranscendenceBasis.{w, u_1, w} (ι := { x : A // x ∈ s }) R (Subtype.val (p := fun (x : A) ↦ x ∈ s))

Tactic:
simpa using exists_isTranscendenceBasis_superset
    ((algebraicIndependent_empty_iff R A).mpr (FaithfulSMul.algebraMap_injective R A))

Premises used: Iff.mpr, algebraicIndependent_empty_iff, exists_isTranscendenceBasis_superset, FaithfulSMul.algebraMap_injective
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
R : Type u_1
A : Type w
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
⊢ ∃ (ι : Type w) (x : ι → A), IsTranscendenceBasis R x

Tactic:
have ⟨s, h⟩ := exists_isTranscendenceBasis R A
  ⟨s, Subtype.val, h⟩

Premises used: exists_isTranscendenceBasis, _private.0.exists_isTranscendenceBasis'.match_1, Exists, Set.Elem, IsTranscendenceBasis, Exists.intro, Subtype.val
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
R : Type u_1
A : Type w
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
⊢ trdeg R A =
    ⨆ (ι :
      { s : Set A //
        IsTranscendenceBasis.{w, u_1, w} (ι := { x : A // x ∈ s }) R (Subtype.val (p := fun (x : A) ↦ x ∈ s)) }),
      #(↑(↑ι : Set A) : Type w)

Tactic:
(ciSup_le' fun s ↦ ?_).antisymm
    (ciSup_le' fun s ↦ le_ciSup_of_le bddAbove_of_small ⟨s, s.2.1⟩ le_rfl)

Premises used: le_rfl, le_ciSup_of_le, LE.le.antisymm, ciSup_le', Algebra.trdeg, Subtype.mk, And.left, Cardinal.bddAbove_of_small, Subtype.val, Subtype.property
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
R : Type u_1
A : Type w
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
refine :
  ∀ (s : { s : Set A // AlgebraicIndepOn R _root_.id s }),
    #(↑(↑s : Set A) : Type w) ≤
      ⨆ (ι :
        { s : Set A //
          IsTranscendenceBasis.{w, u_1, w} (ι := { x : A // x ∈ s }) R (Subtype.val (p := fun (x : A) ↦ x ∈ s)) }),
        #(↑(↑ι : Set A) : Type w)
⊢ trdeg R A =
    ⨆ (ι :
      { s : Set A //
        IsTranscendenceBasis.{w, u_1, w} (ι := { x : A // x ∈ s }) R (Subtype.val (p := fun (x : A) ↦ x ∈ s)) }),
      #(↑(↑ι : Set A) : Type w)

Tactic:
refine (ciSup_le' fun s ↦ ?_).antisymm
    (ciSup_le' fun s ↦ le_ciSup_of_le bddAbove_of_small ⟨s, s.2.1⟩ le_rfl)

Premises used: le_ciSup_of_le, LE.le.antisymm, ciSup_le', Cardinal.bddAbove_of_small