awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Basic (goal)
Goal:
ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
hx : AlgebraicIndependent R x
a : A
⊢ Eq (α := A)
    ((Polynomial.aeval a : (a : Polynomial ↥(adjoin R (range x))) → A)
        ((hx.mvPolynomialOptionEquivPolynomialAdjoin :
              (a : MvPolynomial (Option ι) R) → Polynomial ↥(adjoin R (range x)))
            (X none) :
          Polynomial ↥(adjoin R (range x))) :
      A)
    ((aeval fun (o : Option ι) ↦ o.elim a x : (a : MvPolynomial (Option ι) R) → A) (X none) : A)
have refine_2 : Eq (α := A) ((Polynomial.aeval a : (a : Polynomial ↥(adjoin R (range x))) → A) Polynomial.X : A)
  ((aeval fun (o : Option ι) ↦ o.elim a x : (a : MvPolynomial (Option ι) R) → A) (X none) : A)
Tactic: rw [hx.mvPolynomialOptionEquivPolynomialAdjoin_X_none, aeval_X, Polynomial.aeval_X,
        Option.elim]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Basic (goal)
Goal:
ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
hx : AlgebraicIndependent R x
a : A
refine_2 :
  Eq (α := A) ((Polynomial.aeval a : (a : Polynomial ↥(adjoin R (range x))) → A) Polynomial.X : A)
    ((aeval fun (o : Option ι) ↦ o.elim a x : (a : MvPolynomial (Option ι) R) → A) (X none) : A)
⊢ Eq (α := A)
    ((Polynomial.aeval a : (a : Polynomial ↥(adjoin R (range x))) → A)
        ((hx.mvPolynomialOptionEquivPolynomialAdjoin :
              (a : MvPolynomial (Option ι) R) → Polynomial ↥(adjoin R (range x)))
            (X none) :
          Polynomial ↥(adjoin R (range x))) :
      A)
    ((aeval fun (o : Option ι) ↦ o.elim a x : (a : MvPolynomial (Option ι) R) → A) (X none) : A)
have refine_2₁ : (Polynomial.aeval a : (a : Polynomial ↥(adjoin R (range x))) → A) Polynomial.X = Option.elim none a x
Tactic: rw [hx.mvPolynomialOptionEquivPolynomialAdjoin_X_none, aeval_X, Polynomial.aeval_X,
        Option.elim]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Basic (goal)
Goal:
ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
hx : AlgebraicIndependent R x
a : A
refine_2 :
  Eq (α := A) ((Polynomial.aeval a : (a : Polynomial ↥(adjoin R (range x))) → A) Polynomial.X : A)
    ((aeval fun (o : Option ι) ↦ o.elim a x : (a : MvPolynomial (Option ι) R) → A) (X none) : A)
refine_2₁ : (Polynomial.aeval a : (a : Polynomial ↥(adjoin R (range x))) → A) Polynomial.X = Option.elim none a x
⊢ Eq (α := A)
    ((Polynomial.aeval a : (a : Polynomial ↥(adjoin R (range x))) → A)
        ((hx.mvPolynomialOptionEquivPolynomialAdjoin :
              (a : MvPolynomial (Option ι) R) → Polynomial ↥(adjoin R (range x)))
            (X none) :
          Polynomial ↥(adjoin R (range x))) :
      A)
    ((aeval fun (o : Option ι) ↦ o.elim a x : (a : MvPolynomial (Option ι) R) → A) (X none) : A)
have refine_2₂ : a = Option.elim none a x
Tactic: rw [hx.mvPolynomialOptionEquivPolynomialAdjoin_X_none, aeval_X, Polynomial.aeval_X,
        Option.elim]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Basic (goal)
Goal:
ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
hx : AlgebraicIndependent R x
a : A
refine_2 :
  Eq (α := A) ((Polynomial.aeval a : (a : Polynomial ↥(adjoin R (range x))) → A) Polynomial.X : A)
    ((aeval fun (o : Option ι) ↦ o.elim a x : (a : MvPolynomial (Option ι) R) → A) (X none) : A)
refine_2₁ : (Polynomial.aeval a : (a : Polynomial ↥(adjoin R (range x))) → A) Polynomial.X = Option.elim none a x
refine_2₂ : a = Option.elim none a x
⊢ Eq (α := A)
    ((Polynomial.aeval a : (a : Polynomial ↥(adjoin R (range x))) → A)
        ((hx.mvPolynomialOptionEquivPolynomialAdjoin :
              (a : MvPolynomial (Option ι) R) → Polynomial ↥(adjoin R (range x)))
            (X none) :
          Polynomial ↥(adjoin R (range x))) :
      A)
    ((aeval fun (o : Option ι) ↦ o.elim a x : (a : MvPolynomial (Option ι) R) → A) (X none) : A)
have refine_2₃ : a = a
Tactic: rw [hx.mvPolynomialOptionEquivPolynomialAdjoin_X_none, aeval_X, Polynomial.aeval_X,
        Option.elim]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Basic (goal)
Goal:
ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
hx : AlgebraicIndependent R x
a : A
i : ι
⊢ Eq (α := A)
    ((Polynomial.aeval a : (a : Polynomial ↥(adjoin R (range x))) → A)
        ((hx.mvPolynomialOptionEquivPolynomialAdjoin :
              (a : MvPolynomial (Option ι) R) → Polynomial ↥(adjoin R (range x)))
            (X (some i)) :
          Polynomial ↥(adjoin R (range x))) :
      A)
    ((aeval fun (o : Option ι) ↦ o.elim a x : (a : MvPolynomial (Option ι) R) → A) (X (some i)) : A)
have refine_2 : Eq (α := A)
  ((Polynomial.aeval a : (a : Polynomial ↥(adjoin R (range x))) → A)
      ((Polynomial.C : (a : ↥(adjoin R (range x))) → Polynomial ↥(adjoin R (range x)))
          ((hx.aevalEquiv : (a : MvPolynomial ι R) → ↥(adjoin R (range x))) (X i)) :
        Polynomial ↥(adjoin R (range x))) :
    A)
  ((aeval fun (o : Option ι) ↦ o.elim a x : (a : MvPolynomial (Option ι) R) → A) (X (some i)) : A)
Tactic: rw [hx.mvPolynomialOptionEquivPolynomialAdjoin_X_some, Polynomial.aeval_C,
        hx.algebraMap_aevalEquiv, aeval_X, aeval_X, Option.elim]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Basic (goal)
Goal:
ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
hx : AlgebraicIndependent R x
a : A
i : ι
refine_2 :
  Eq (α := A)
    ((Polynomial.aeval a : (a : Polynomial ↥(adjoin R (range x))) → A)
        ((Polynomial.C : (a : ↥(adjoin R (range x))) → Polynomial ↥(adjoin R (range x)))
            ((hx.aevalEquiv : (a : MvPolynomial ι R) → ↥(adjoin R (range x))) (X i)) :
          Polynomial ↥(adjoin R (range x))) :
      A)
    ((aeval fun (o : Option ι) ↦ o.elim a x : (a : MvPolynomial (Option ι) R) → A) (X (some i)) : A)
⊢ Eq (α := A)
    ((Polynomial.aeval a : (a : Polynomial ↥(adjoin R (range x))) → A)
        ((hx.mvPolynomialOptionEquivPolynomialAdjoin :
              (a : MvPolynomial (Option ι) R) → Polynomial ↥(adjoin R (range x)))
            (X (some i)) :
          Polynomial ↥(adjoin R (range x))) :
      A)
    ((aeval fun (o : Option ι) ↦ o.elim a x : (a : MvPolynomial (Option ι) R) → A) (X (some i)) : A)
have refine_2₁ : Eq (α := A)
  ((algebraMap (↥(adjoin R (range x))) A : (a : ↥(adjoin R (range x))) → A)
      ((hx.aevalEquiv : (a : MvPolynomial ι R) → ↥(adjoin R (range x))) (X i) : ↥(adjoin R (range x))) :
    A)
  ((aeval fun (o : Option ι) ↦ o.elim a x : (a : MvPolynomial (Option ι) R) → A) (X (some i)) : A)
Tactic: rw [hx.mvPolynomialOptionEquivPolynomialAdjoin_X_some, Polynomial.aeval_C,
        hx.algebraMap_aevalEquiv, aeval_X, aeval_X, Option.elim]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Basic (goal)
Goal:
ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
hx : AlgebraicIndependent R x
a : A
i : ι
refine_2 :
  Eq (α := A)
    ((Polynomial.aeval a : (a : Polynomial ↥(adjoin R (range x))) → A)
        ((Polynomial.C : (a : ↥(adjoin R (range x))) → Polynomial ↥(adjoin R (range x)))
            ((hx.aevalEquiv : (a : MvPolynomial ι R) → ↥(adjoin R (range x))) (X i)) :
          Polynomial ↥(adjoin R (range x))) :
      A)
    ((aeval fun (o : Option ι) ↦ o.elim a x : (a : MvPolynomial (Option ι) R) → A) (X (some i)) : A)
refine_2₁ :
  Eq (α := A)
    ((algebraMap (↥(adjoin R (range x))) A : (a : ↥(adjoin R (range x))) → A)
        ((hx.aevalEquiv : (a : MvPolynomial ι R) → ↥(adjoin R (range x))) (X i) : ↥(adjoin R (range x))) :
      A)
    ((aeval fun (o : Option ι) ↦ o.elim a x : (a : MvPolynomial (Option ι) R) → A) (X (some i)) : A)
⊢ Eq (α := A)
    ((Polynomial.aeval a : (a : Polynomial ↥(adjoin R (range x))) → A)
        ((hx.mvPolynomialOptionEquivPolynomialAdjoin :
              (a : MvPolynomial (Option ι) R) → Polynomial ↥(adjoin R (range x)))
            (X (some i)) :
          Polynomial ↥(adjoin R (range x))) :
      A)
    ((aeval fun (o : Option ι) ↦ o.elim a x : (a : MvPolynomial (Option ι) R) → A) (X (some i)) : A)
have refine_2₂ : Eq.{v + 1} (α := A) ((aeval x : (a : MvPolynomial ι R) → A) (X i) : A)
  ((aeval fun (o : Option ι) ↦ o.elim a x : (a : MvPolynomial (Option ι) R) → A) (X (some i)) : A)
Tactic: rw [hx.mvPolynomialOptionEquivPolynomialAdjoin_X_some, Polynomial.aeval_C,
        hx.algebraMap_aevalEquiv, aeval_X, aeval_X, Option.elim]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Basic (goal)
Goal:
ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
hx : AlgebraicIndependent R x
a : A
i : ι
refine_2 :
  Eq (α := A)
    ((Polynomial.aeval a : (a : Polynomial ↥(adjoin R (range x))) → A)
        ((Polynomial.C : (a : ↥(adjoin R (range x))) → Polynomial ↥(adjoin R (range x)))
            ((hx.aevalEquiv : (a : MvPolynomial ι R) → ↥(adjoin R (range x))) (X i)) :
          Polynomial ↥(adjoin R (range x))) :
      A)
    ((aeval fun (o : Option ι) ↦ o.elim a x : (a : MvPolynomial (Option ι) R) → A) (X (some i)) : A)
refine_2₁ :
  Eq (α := A)
    ((algebraMap (↥(adjoin R (range x))) A : (a : ↥(adjoin R (range x))) → A)
        ((hx.aevalEquiv : (a : MvPolynomial ι R) → ↥(adjoin R (range x))) (X i) : ↥(adjoin R (range x))) :
      A)
    ((aeval fun (o : Option ι) ↦ o.elim a x : (a : MvPolynomial (Option ι) R) → A) (X (some i)) : A)
refine_2₂ :
  Eq.{v + 1} (α := A) ((aeval x : (a : MvPolynomial ι R) → A) (X i) : A)
    ((aeval fun (o : Option ι) ↦ o.elim a x : (a : MvPolynomial (Option ι) R) → A) (X (some i)) : A)
⊢ Eq (α := A)
    ((Polynomial.aeval a : (a : Polynomial ↥(adjoin R (range x))) → A)
        ((hx.mvPolynomialOptionEquivPolynomialAdjoin :
              (a : MvPolynomial (Option ι) R) → Polynomial ↥(adjoin R (range x)))
            (X (some i)) :
          Polynomial ↥(adjoin R (range x))) :
      A)
    ((aeval fun (o : Option ι) ↦ o.elim a x : (a : MvPolynomial (Option ι) R) → A) (X (some i)) : A)
have refine_2₃ : x i = (aeval fun (o : Option ι) ↦ o.elim a x : (a : MvPolynomial (Option ι) R) → A) (X (some i))
Tactic: rw [hx.mvPolynomialOptionEquivPolynomialAdjoin_X_some, Polynomial.aeval_C,
        hx.algebraMap_aevalEquiv, aeval_X, aeval_X, Option.elim]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Basic (goal)
Goal:
ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
hx : AlgebraicIndependent R x
a : A
i : ι
refine_2 :
  Eq (α := A)
    ((Polynomial.aeval a : (a : Polynomial ↥(adjoin R (range x))) → A)
        ((Polynomial.C : (a : ↥(adjoin R (range x))) → Polynomial ↥(adjoin R (range x)))
            ((hx.aevalEquiv : (a : MvPolynomial ι R) → ↥(adjoin R (range x))) (X i)) :
          Polynomial ↥(adjoin R (range x))) :
      A)
    ((aeval fun (o : Option ι) ↦ o.elim a x : (a : MvPolynomial (Option ι) R) → A) (X (some i)) : A)
refine_2₁ :
  Eq (α := A)
    ((algebraMap (↥(adjoin R (range x))) A : (a : ↥(adjoin R (range x))) → A)
        ((hx.aevalEquiv : (a : MvPolynomial ι R) → ↥(adjoin R (range x))) (X i) : ↥(adjoin R (range x))) :
      A)
    ((aeval fun (o : Option ι) ↦ o.elim a x : (a : MvPolynomial (Option ι) R) → A) (X (some i)) : A)
refine_2₂ :
  Eq.{v + 1} (α := A) ((aeval x : (a : MvPolynomial ι R) → A) (X i) : A)
    ((aeval fun (o : Option ι) ↦ o.elim a x : (a : MvPolynomial (Option ι) R) → A) (X (some i)) : A)
refine_2₃ : x i = (aeval fun (o : Option ι) ↦ o.elim a x : (a : MvPolynomial (Option ι) R) → A) (X (some i))
⊢ Eq (α := A)
    ((Polynomial.aeval a : (a : Polynomial ↥(adjoin R (range x))) → A)
        ((hx.mvPolynomialOptionEquivPolynomialAdjoin :
              (a : MvPolynomial (Option ι) R) → Polynomial ↥(adjoin R (range x)))
            (X (some i)) :
          Polynomial ↥(adjoin R (range x))) :
      A)
    ((aeval fun (o : Option ι) ↦ o.elim a x : (a : MvPolynomial (Option ι) R) → A) (X (some i)) : A)
have refine_2₄ : x i = (some i).elim a x
Tactic: rw [hx.mvPolynomialOptionEquivPolynomialAdjoin_X_some, Polynomial.aeval_C,
        hx.algebraMap_aevalEquiv, aeval_X, aeval_X, Option.elim]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Basic (goal)
Goal:
ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
hx : AlgebraicIndependent R x
a : A
i : ι
refine_2 :
  Eq (α := A)
    ((Polynomial.aeval a : (a : Polynomial ↥(adjoin R (range x))) → A)
        ((Polynomial.C : (a : ↥(adjoin R (range x))) → Polynomial ↥(adjoin R (range x)))
            ((hx.aevalEquiv : (a : MvPolynomial ι R) → ↥(adjoin R (range x))) (X i)) :
          Polynomial ↥(adjoin R (range x))) :
      A)
    ((aeval fun (o : Option ι) ↦ o.elim a x : (a : MvPolynomial (Option ι) R) → A) (X (some i)) : A)
refine_2₁ :
  Eq (α := A)
    ((algebraMap (↥(adjoin R (range x))) A : (a : ↥(adjoin R (range x))) → A)
        ((hx.aevalEquiv : (a : MvPolynomial ι R) → ↥(adjoin R (range x))) (X i) : ↥(adjoin R (range x))) :
      A)
    ((aeval fun (o : Option ι) ↦ o.elim a x : (a : MvPolynomial (Option ι) R) → A) (X (some i)) : A)
refine_2₂ :
  Eq.{v + 1} (α := A) ((aeval x : (a : MvPolynomial ι R) → A) (X i) : A)
    ((aeval fun (o : Option ι) ↦ o.elim a x : (a : MvPolynomial (Option ι) R) → A) (X (some i)) : A)
refine_2₃ : x i = (aeval fun (o : Option ι) ↦ o.elim a x : (a : MvPolynomial (Option ι) R) → A) (X (some i))
refine_2₄ : x i = (some i).elim a x
⊢ Eq (α := A)
    ((Polynomial.aeval a : (a : Polynomial ↥(adjoin R (range x))) → A)
        ((hx.mvPolynomialOptionEquivPolynomialAdjoin :
              (a : MvPolynomial (Option ι) R) → Polynomial ↥(adjoin R (range x)))
            (X (some i)) :
          Polynomial ↥(adjoin R (range x))) :
      A)
    ((aeval fun (o : Option ι) ↦ o.elim a x : (a : MvPolynomial (Option ι) R) → A) (X (some i)) : A)
have refine_2₅ : x i = x i
Tactic: rw [hx.mvPolynomialOptionEquivPolynomialAdjoin_X_some, Polynomial.aeval_C,
        hx.algebraMap_aevalEquiv, aeval_X, aeval_X, Option.elim]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Basic (goal)
Goal:
ι : Type u
A : Type v
x : ι → A
inst : CommRing A
K : Type u_3
inst_1 : Field K
inst_2 : Algebra K A
inst_3 : IsEmpty ι
inst_4 : Nontrivial A
⊢ AlgebraicIndependent K x
have rw : Injective.{u_3 + 1, v + 1} (α := K) (β := A) (⇑(algebraMap K A) : (a : K) → A)
Tactic: rw [algebraicIndependent_empty_type_iff]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Defs (goal)
Goal:
ι : Type u_1
R : Type u_3
A : Type u_5
A' : Type u_6
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing A'
inst_3 : Algebra R A
inst_4 : Algebra R A'
f : A →ₐ[R] A'
hfv : AlgebraicIndependent.{u_1, u_3, u_6} R (A := A') ((⇑f : (a : A) → A') ∘ x)
⊢ aeval ((⇑f : (a : A) → A') ∘ x) = f.comp (aeval x)
have hf : ∀ (i : ι),
  Eq.{u_6 + 1} (α := A') ((aeval ((⇑f : (a : A) → A') ∘ x) : (a : MvPolynomial ι R) → A') (X i) : A')
    ((f.comp (aeval x) : (a : MvPolynomial ι R) → A') (X i) : A')
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Defs (hypothesis)
Goal:
ι : Type u_1
R : Type u_3
A : Type u_5
A' : Type u_6
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing A'
inst_3 : Algebra R A
inst_4 : Algebra R A'
f : A →ₐ[R] A'
hfv : AlgebraicIndependent.{u_1, u_3, u_6} R (A := A') ((⇑f : (a : A) → A') ∘ x)
⊢ AlgebraicIndependent R x
have this : aeval ((⇑f : (a : A) → A') ∘ x) = f.comp (aeval x)
Tactic: have : aeval (f ∘ x) = f.comp (aeval x) := by ext; simp
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Defs (hypothesis)
Goal:
ι : Type u_1
R : Type u_3
A : Type u_5
A' : Type u_6
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing A'
inst_3 : Algebra R A
inst_4 : Algebra R A'
f : A →ₐ[R] A'
hfv : AlgebraicIndependent.{u_1, u_3, u_6} R (A := A') ((⇑f : (a : A) → A') ∘ x)
this : aeval ((⇑f : (a : A) → A') ∘ x) = f.comp (aeval x)
⊢ AlgebraicIndependent R x
have hfv₁ : Injective (α := MvPolynomial ι R) (β := A')
  (comp (β := A) (⇑f : (a : A) → A') (⇑(aeval x) : (a : MvPolynomial ι R) → A))
Tactic: rw [AlgebraicIndependent, this, AlgHom.coe_comp] at hfv
Cleared hypotheses: hfv, this
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Defs (goal)
Goal:
R : Type u_3
A : Type u_5
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
s : Set A
⊢ IsTranscendenceBasis.{u_5, u_3, u_5} (ι := { x : A // x ∈ s }) R (Subtype.val (p := fun (x : A) ↦ x ∈ s)) ↔
    Maximal (AlgebraicIndepOn R _root_.id) s
have rw : (AlgebraicIndependent.{u_5, u_3, u_5} (ι := { x : A // x ∈ s }) R (Subtype.val (p := fun (x : A) ↦ x ∈ s)) ∧
    ∀ (s_1 : Set A), AlgebraicIndepOn R _root_.id s_1 → s ⊆ s_1 → s = s_1) ↔
  AlgebraicIndepOn R _root_.id s ∧ ∀ ⦃y : Set A⦄, AlgebraicIndepOn R _root_.id y → s ≤ y → s = y
Tactic: rw [IsTranscendenceBasis, maximal_iff, Subtype.range_val]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Defs (goal)
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
⊢ IsTranscendenceBasis.{u_1, u_3, u_5} (ι := ι) R (f ∘ (⇑e : (a : ι) → ι')) ↔ IsTranscendenceBasis R f
have simp_rw : (AlgebraicIndependent.{u_1, u_3, u_5} (ι := ι) R (f ∘ (⇑e : (a : ι) → ι')) ∧
    ∀ (s : Set A),
      AlgebraicIndepOn R _root_.id s →
        range.{u_5, u_1 + 1} (ι := ι) (f ∘ (⇑e : (a : ι) → ι')) ⊆ s →
          range.{u_5, u_1 + 1} (ι := ι) (f ∘ (⇑e : (a : ι) → ι')) = s) ↔
  AlgebraicIndependent R f ∧ ∀ (s : Set A), AlgebraicIndepOn R _root_.id s → range f ⊆ s → range f = s
Tactic: simp_rw [IsTranscendenceBasis, algebraicIndependent_equiv, EquivLike.range_comp]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Defs (goal)
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
simp_rw :
  (AlgebraicIndependent.{u_1, u_3, u_5} (ι := ι) R (f ∘ (⇑e : (a : ι) → ι')) ∧
      ∀ (s : Set A),
        AlgebraicIndepOn R _root_.id s →
          range.{u_5, u_1 + 1} (ι := ι) (f ∘ (⇑e : (a : ι) → ι')) ⊆ s →
            range.{u_5, u_1 + 1} (ι := ι) (f ∘ (⇑e : (a : ι) → ι')) = s) ↔
    AlgebraicIndependent R f ∧ ∀ (s : Set A), AlgebraicIndepOn R _root_.id s → range f ⊆ s → range f = s
⊢ IsTranscendenceBasis.{u_1, u_3, u_5} (ι := ι) R (f ∘ (⇑e : (a : ι) → ι')) ↔ IsTranscendenceBasis R f
have simp_rw₁ : (AlgebraicIndependent R f ∧
    ∀ (s : Set A),
      AlgebraicIndepOn R _root_.id s →
        range.{u_5, u_1 + 1} (ι := ι) (f ∘ (⇑e : (a : ι) → ι')) ⊆ s →
          range.{u_5, u_1 + 1} (ι := ι) (f ∘ (⇑e : (a : ι) → ι')) = s) ↔
  AlgebraicIndependent R f ∧ ∀ (s : Set A), AlgebraicIndepOn R _root_.id s → range f ⊆ s → range f = s
Tactic: simp_rw [IsTranscendenceBasis, algebraicIndependent_equiv, EquivLike.range_comp]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality (goal)
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)
⊢ lift.{max u w, v} #E = max (max (lift.{max v w, u} #F) (lift.{max u v, w} #ι)) ℵ₀
have suffices : #E = #↥K
Tactic: suffices #E = #K by simp [K, this, ← lift_mk_eq'.2 ⟨hx.1.aevalEquiv.toEquiv⟩]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality (hypothesis)
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)
⊢ #E = #↥K
have this : Algebra.IsAlgebraic (↥K) E
Tactic: haveI : Algebra.IsAlgebraic K E := hx.isAlgebraic
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality (goal)
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
have refine : #E ≤ #↥K
Tactic: refine le_antisymm ?_ (mk_le_of_injective Subtype.val_injective)
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality (hypothesis)
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
have this₁ : Infinite.{v + 1} ↥K
Tactic: haveI : Infinite K := hx.1.aevalEquiv.infinite_iff.1 inferInstance
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality (hypothesis)
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)
⊢ lift.{max u w, v} (Module.rank F E) = max (max (lift.{max v w, u} #F) (lift.{max u v, w} #ι)) ℵ₀
have this : Algebra.IsAlgebraic (↥K) E
Tactic: haveI : Algebra.IsAlgebraic K E := hx.isAlgebraic_field
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality (goal)
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 F E) = max (max (lift.{max v w, u} #F) (lift.{max u v, w} #ι)) ℵ₀
have 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} #ι)) ℵ₀
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]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality (goal)
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
⊢ 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} #ι)) ℵ₀
have refine : lift.{max u w, v} (max #↥K ℵ₀) = max (max (lift.{max w v, 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'])
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality (goal)
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
⊢ Module.rank F E = #E
have obtain : ∀ (ι : Type v) (x : ι → E) (hx : IsTranscendenceBasis F x), Module.rank F E = #E
Tactic: obtain ⟨ι, x, hx⟩ := exists_isTranscendenceBasis' F E
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality (hypothesis)
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
⊢ Module.rank F E = #E
have this : Nonempty ι
Tactic: haveI := hx.nonempty_iff_transcendental.2 ‹_›
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A B : IntermediateField F E
⊢ Module.rank F ↥(A ⊔ B) ≤ Module.rank F ↥A * Module.rank F ↥B
have pos : ∀ (hA : Algebra.IsAlgebraic.{u, v} F ↥A), Module.rank F ↥(A ⊔ B) ≤ Module.rank F ↥A * Module.rank F ↥B
Tactic: by_cases hA : Algebra.IsAlgebraic F A