awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
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_1 :
  ∀ (r : R),
    Eq (α := A)
      ((Polynomial.aeval a : (a : Polynomial ↥(adjoin R (range x))) → A)
          ((hx.mvPolynomialOptionEquivPolynomialAdjoin :
                (a : MvPolynomial (Option ι) R) → Polynomial ↥(adjoin R (range x)))
              ((C : (a : R) → MvPolynomial (Option ι) R) r) :
            Polynomial ↥(adjoin R (range x))) :
        A)
      ((aeval fun (o : Option ι) ↦ o.elim a x : (a : MvPolynomial (Option ι) R) → A)
          ((C : (a : R) → MvPolynomial (Option ι) R) r : MvPolynomial.{u, u_2} (Option ι) R) :
        A)
⊢ ∀ (r : R),
    Eq.{v + 1} (α := A)
      ((RingHom.comp (↑(Polynomial.aeval a) : Polynomial ↥(adjoin R (range x)) →+* A)
              hx.mvPolynomialOptionEquivPolynomialAdjoin.toRingHom :
            (a : MvPolynomial (Option ι) R) → A)
          ((C : (a : R) → MvPolynomial (Option ι) R) r : MvPolynomial.{u, u_2} (Option ι) R) :
        A)
      (((↑(aeval fun (o : Option ι) ↦ o.elim a x) : MvPolynomial (Option ι) R →+* A) :
            (a : MvPolynomial (Option ι) R) → A)
          ((C : (a : R) → MvPolynomial (Option ι) R) r : MvPolynomial.{u, u_2} (Option ι) R) :
        A)

Tactic:
simp only [RingHom.comp_apply, RingEquiv.toRingHom_eq_coe, RingEquiv.coe_toRingHom,
      AlgHom.coe_toRingHom, AlgHom.coe_toRingHom]

Premises used: AlgHom.coe_toRingHom, RingHom.comp_apply, RingEquiv.toRingHom_eq_coe, RingEquiv.coe_toRingHom
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
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 :
  ∀ (i : Option ι),
    Eq (α := A)
      ((Polynomial.aeval a : (a : Polynomial ↥(adjoin R (range x))) → A)
          ((hx.mvPolynomialOptionEquivPolynomialAdjoin :
                (a : MvPolynomial (Option ι) R) → Polynomial ↥(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 i) : A)
⊢ ∀ (i : Option ι),
    Eq.{v + 1} (α := A)
      ((RingHom.comp (↑(Polynomial.aeval a) : Polynomial ↥(adjoin R (range x)) →+* A)
              hx.mvPolynomialOptionEquivPolynomialAdjoin.toRingHom :
            (a : MvPolynomial (Option ι) R) → A)
          (X i) :
        A)
      (((↑(aeval fun (o : Option ι) ↦ o.elim a x) : MvPolynomial (Option ι) R →+* A) :
            (a : MvPolynomial (Option ι) R) → A)
          (X i) :
        A)

Tactic:
simp only [RingHom.comp_apply, RingEquiv.toRingHom_eq_coe, RingEquiv.coe_toRingHom,
      AlgHom.coe_toRingHom, AlgHom.coe_toRingHom]

Premises used: AlgHom.coe_toRingHom, RingHom.comp_apply, RingEquiv.toRingHom_eq_coe, RingEquiv.coe_toRingHom
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
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
r : R
refine_1 :
  Eq (α := A)
    ((Polynomial.aeval a : (a : Polynomial ↥(adjoin R (range x))) → A)
        ((Polynomial.C : (a : ↥(adjoin R (range x))) → Polynomial ↥(adjoin R (range x)))
            ((algebraMap R ↥(adjoin R (range x)) : (a : R) → ↥(adjoin R (range x))) r) :
          Polynomial ↥(adjoin R (range x))) :
      A)
    ((aeval fun (o : Option ι) ↦ o.elim a x : (a : MvPolynomial (Option ι) R) → A)
        ((C : (a : R) → MvPolynomial (Option ι) R) r : MvPolynomial.{u, u_2} (Option ι) R) :
      A)
refine_1₁ :
  Eq (α := A)
    ((Polynomial.aeval a : (a : Polynomial ↥(adjoin R (range x))) → A)
        ((Polynomial.C : (a : ↥(adjoin R (range x))) → Polynomial ↥(adjoin R (range x)))
            ((algebraMap R ↥(adjoin R (range x)) : (a : R) → ↥(adjoin R (range x))) r) :
          Polynomial ↥(adjoin R (range x))) :
      A)
    ((algebraMap R A : (a : R) → A) r : A)
refine_1₂ :
  Eq (α := A)
    ((algebraMap (↥(adjoin R (range x))) A : (a : ↥(adjoin R (range x))) → A)
        ((algebraMap R ↥(adjoin R (range x)) : (a : R) → ↥(adjoin R (range x))) r : ↥(adjoin R (range x))) :
      A)
    ((algebraMap R A : (a : R) → A) r : A)
refine_1₃ refine_1₄ :
  Eq (α := A)
    ((algebraMap (↥(adjoin R (range x))) A : (a : ↥(adjoin R (range x))) → A)
        ((algebraMap R ↥(adjoin R (range x)) : (a : R) → ↥(adjoin R (range x))) r : ↥(adjoin R (range x))) :
      A)
    ((algebraMap (↥(adjoin R (range x))) A : (a : ↥(adjoin R (range x))) → A)
        ((algebraMap R ↥(adjoin R (range x)) : (a : R) → ↥(adjoin R (range x))) r : ↥(adjoin R (range x))) :
      A)
⊢ Eq (α := A)
    ((Polynomial.aeval a : (a : Polynomial ↥(adjoin R (range x))) → A)
        ((hx.mvPolynomialOptionEquivPolynomialAdjoin :
              (a : MvPolynomial (Option ι) R) → Polynomial ↥(adjoin R (range x)))
            ((C : (a : R) → MvPolynomial (Option ι) R) r) :
          Polynomial ↥(adjoin R (range x))) :
      A)
    ((aeval fun (o : Option ι) ↦ o.elim a x : (a : MvPolynomial (Option ι) R) → A)
        ((C : (a : R) → MvPolynomial (Option ι) R) r : MvPolynomial.{u, u_2} (Option ι) R) :
      A)

Tactic:
rw [hx.mvPolynomialOptionEquivPolynomialAdjoin_C, aeval_C, Polynomial.aeval_C,
      IsScalarTower.algebraMap_apply R (adjoin R (range x)) A]

Premises used: AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_C, Algebra.adjoin, Membership.mem, Subtype, Polynomial.aeval_C, MvPolynomial.aeval_C, Set.range, IsScalarTower.algebraMap_apply
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
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
refine_2₃ refine_2₄ : 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)

Tactic:
rw [hx.mvPolynomialOptionEquivPolynomialAdjoin_X_none, aeval_X, Polynomial.aeval_X,
        Option.elim]

Premises used: MvPolynomial.aeval_X, AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_X_none, Option.elim, Polynomial.aeval_X
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
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
refine_2₅ refine_2₆ : x i = x 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)

Tactic:
rw [hx.mvPolynomialOptionEquivPolynomialAdjoin_X_some, Polynomial.aeval_C,
        hx.algebraMap_aevalEquiv, aeval_X, aeval_X, Option.elim]

Premises used: MvPolynomial.aeval_X, AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_X_some, AlgebraicIndependent.algebraMap_aevalEquiv, Polynomial.aeval_C, Option.elim
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
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
rw : Injective.{u_3 + 1, v + 1} (α := K) (β := A) (⇑(algebraMap K A) : (a : K) → A)
⊢ AlgebraicIndependent K x

Tactic:
rw [algebraicIndependent_empty_type_iff]

Premises used: algebraicIndependent_empty_type_iff
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
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
⊢ Injective.{u_3 + 1, v + 1} (α := K) (β := A) (⇑(algebraMap K A) : (a : K) → A)

Tactic:
RingHom.injective _

Premises used: RingHom.injective
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
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
⊢ Injective.{u_3 + 1, v + 1} (α := K) (β := A) (⇑(algebraMap K A) : (a : K) → A)

Tactic:
exact RingHom.injective _

Premises used: RingHom.injective
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
Goal:
A : Type v
inst : CommRing A
K : Type u_3
inst_1 : Field K
inst_2 : Algebra K A
inst_3 : Nontrivial A
⊢ AlgebraicIndependent.{v, u_3, v} (ι := { x : A // Membership.mem (γ := Set A) ∅ x }) K
    (Subtype.val (p := fun (x : A) ↦ Membership.mem (γ := Set A) ∅ x))

Tactic:
algebraicIndependent_empty_type

Premises used: algebraicIndependent_empty_type
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Defs
Goal:
ι : Type u_1
R : Type u_3
A : Type u_5
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
⊢ AlgebraicIndependent R x ↔
    ∀ (p : MvPolynomial ι R), Eq.{u_5 + 1} (α := A) ((aeval x : (a : MvPolynomial ι R) → A) p : A) (0 : A) → p = 0

Tactic:
injective_iff_map_eq_zero _

Premises used: AlgebraicIndependent, injective_iff_map_eq_zero
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Defs
Goal:
ι : Type u_1
R : Type u_3
A : Type u_5
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
h : AlgebraicIndependent R x
⊢ ∀ (p : MvPolynomial ι R), Eq.{u_5 + 1} (α := A) ((aeval x : (a : MvPolynomial ι R) → A) p : A) (0 : A) → p = 0

Tactic:
algebraicIndependent_iff.1 h

Premises used: algebraicIndependent_iff, Iff.mp
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Defs
Goal:
ι : Type u_1
R : Type u_3
A : Type u_5
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
⊢ AlgebraicIndependent R x ↔ Injective (α := MvPolynomial ι R) (β := A) (⇑(aeval x) : (a : MvPolynomial ι R) → A)

Tactic:
Iff.rfl

Premises used: AlgebraicIndependent, Iff.rfl
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Defs
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)
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')
⊢ aeval ((⇑f : (a : A) → A') ∘ x) = f.comp (aeval x)

Tactic:
ext
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Defs
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)
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:
simp
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Defs
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)

Tactic:
have : aeval (f ∘ x) = f.comp (aeval x) := by ext; simp
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Defs
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)
⊢ 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

Premises used: AlgebraicIndependent, AlgHom.coe_comp
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Defs
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)
hfv₁ :
  Injective (α := MvPolynomial ι R) (β := A')
    (comp (β := A) (⇑f : (a : A) → A') (⇑(aeval x) : (a : MvPolynomial ι R) → A))
⊢ aeval ((⇑f : (a : A) → A') ∘ x) = f.comp (aeval x)

Tactic:
rw [AlgebraicIndependent, this, AlgHom.coe_comp] at hfv

Premises used: AlgebraicIndependent, AlgHom.coe_comp
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Defs
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 :
  Injective (α := MvPolynomial ι R) (β := A')
    (comp (β := A) (⇑f : (a : A) → A') (⇑(aeval x) : (a : MvPolynomial ι R) → A))
this : aeval ((⇑f : (a : A) → A') ∘ x) = f.comp (aeval x)
⊢ AlgebraicIndependent R x

Tactic:
hfv.of_comp

Premises used: AlgebraicIndependent, Function.Injective.of_comp
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Defs
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 :
  Injective (α := MvPolynomial ι R) (β := A')
    (comp (β := A) (⇑f : (a : A) → A') (⇑(aeval x) : (a : MvPolynomial ι R) → A))
this : aeval ((⇑f : (a : A) → A') ∘ x) = f.comp (aeval x)
⊢ AlgebraicIndependent R x

Tactic:
exact hfv.of_comp

Premises used: Function.Injective.of_comp
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Defs
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
A : Type u_5
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
hx : AlgebraicIndependent R x
f : ι' → ι
hf : Injective f
p q : MvPolynomial ι' R
⊢ Eq.{u_5 + 1} (α := A) ((aeval (x ∘ f) : (a : MvPolynomial ι' R) → A) p : A)
      ((aeval (x ∘ f) : (a : MvPolynomial ι' R) → A) q : A) →
    p = q

Tactic:
simpa [aeval_rename, (rename_injective f hf).eq_iff] using @hx (rename f p) (rename f q)

Premises used: Function.Injective.eq_iff, MvPolynomial.rename_injective, MvPolynomial.aeval_rename
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Defs
Goal:
ι : Type u_1
R : Type u_3
A : Type u_5
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
hx : AlgebraicIndependent R x
⊢ AlgebraicIndependent.{u_5, u_3, u_5} (ι := { x_1 : A // x_1 ∈ range x }) R
    (Subtype.val (p := fun (x_1 : A) ↦ x_1 ∈ range x))

Tactic:
simpa using hx.comp _ (rangeSplitting_injective x)

Premises used: AlgebraicIndependent.comp, Set.rangeSplitting_injective
-- 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
⊢ AlgebraicIndependent.{u_1, u_3, u_5} (ι := ι) R (f ∘ (⇑e : (a : ι) → ι')) ↔ AlgebraicIndependent R f

Tactic:
⟨fun h => Function.comp_id f ▸ e.self_comp_symm ▸ h.comp _ e.symm.injective,
    fun h => h.comp _ e.injective⟩

Premises used: Function.comp_id, AlgebraicIndependent.comp, Eq.rec, Equiv.self_comp_symm, Iff.intro, Equiv.injective, Equiv.symm, DFunLike.coe
-- 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
⊢ AlgebraicIndependent R g ↔ AlgebraicIndependent R f

Tactic:
h ▸ algebraicIndependent_equiv e

Premises used: Eq.rec, algebraicIndependent_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
⊢ AlgebraicIndependent.{u_5, u_3, u_5} (ι := { x : A // x ∈ range f }) R
      (Subtype.val (p := fun (x : A) ↦ x ∈ range f)) ↔
    AlgebraicIndependent R f

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

Premises used: algebraicIndependent_equiv', Equiv.ofInjective, 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
⊢ (AlgebraicIndependent.{u_7, u_3, u_5} R (A := A) fun (x : (↑s : Type u_7)) ↦ f (↑x : ι)) ↔
    AlgebraicIndependent R (A := A) fun (x : (↑(f '' s) : Type u_5)) ↦ (↑x : A)

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

Premises used: algebraicIndependent_equiv', Equiv.Set.imageOfInjOn, rfl
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Defs
Goal:
ι : Type u_1
R : Type u_3
A : Type u_5
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
s t : Set ι
H : AlgebraicIndepOn R x t
hst : s ⊆ t
⊢ AlgebraicIndepOn R x s

Tactic:
simpa [Function.comp] using H.comp (Set.inclusion hst) (Set.inclusion_injective hst)

Premises used: AlgebraicIndependent.comp, Function.comp, Set.inclusion_injective, Set.inclusion
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Defs
Goal:
ι : Type u_1
R : Type u_3
A : Type u_5
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
⊢ AlgebraicIndepOn R x Set.univ ↔ AlgebraicIndependent R x

Tactic:
algebraicIndependent_equiv (Equiv.Set.univ ι)

Premises used: algebraicIndependent_equiv, Equiv.Set.univ
-- 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
t s : Set A
h : t ⊆ s
hx : AlgebraicIndependent.{u_5, u_3, u_5} (ι := { x : A // x ∈ s }) R (Subtype.val (p := fun (x : A) ↦ x ∈ s))
⊢ AlgebraicIndependent.{u_5, u_3, u_5} (ι := { x : A // x ∈ t }) R (Subtype.val (p := fun (x : A) ↦ x ∈ t))

Tactic:
AlgebraicIndepOn.mono (x := id) hx h

Premises used: AlgebraicIndepOn.mono
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Defs
Goal:
ι : Type u_1
R : Type u_3
A : Type u_5
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
hx : AlgebraicIndependent R x
p : MvPolynomial ι R
⊢ Eq (α := A)
    ((algebraMap (↥(adjoin R (range x))) A : (a : ↥(adjoin R (range x))) → A)
        ((hx.aevalEquiv : (a : MvPolynomial ι R) → ↥(adjoin R (range x))) p : ↥(adjoin R (range x))) :
      A)
    ((aeval x : (a : MvPolynomial ι R) → A) p : A)

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, MvPolynomial.eval₂, Finset.sum, rfl
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Defs
Goal:
ι : Type u_1
R : Type u_3
A : Type u_5
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
hx : AlgebraicIndependent R x
p : ↥(adjoin R (range x))
⊢ (aeval x : (a : MvPolynomial ι R) → A)
      ((hx.repr : (a : ↥(adjoin R (range x))) → MvPolynomial ι R) p : MvPolynomial ι R) =
    (↑p : A)

Tactic:
Subtype.ext_iff.1 (AlgEquiv.apply_symm_apply hx.aevalEquiv p)

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, MvPolynomial.eval₂, AlgebraicIndependent.aevalEquiv, AlgEquiv.apply_symm_apply, Subtype.ext_iff, Iff.mp, Finset.sum
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Defs
Goal:
ι : Type u_1
R : Type u_3
A : Type u_5
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
hx : AlgebraicIndependent R x
⊢ AlgHom.comp (aeval x) hx.repr = val (adjoin R (range x))

Tactic:
AlgHom.ext hx.aeval_repr

Premises used: AlgHom.ext, AlgebraicIndependent.aeval_repr
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Defs
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
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'
hx_1 : AlgebraicIndependent R x
s : Set ι
hx : AlgebraicIndepOn R x s
⊢ (range fun (i : (↑s : Type u_1)) ↦ x (↑i : ι)) = x '' s

Tactic:
aesop
-- 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
s : Set A
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
⊢ 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

Tactic:
rw [IsTranscendenceBasis, maximal_iff, Subtype.range_val]

Premises used: IsTranscendenceBasis, Subtype.range_val, maximal_iff
-- 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
s : Set A
⊢ (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:
rfl
-- 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
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
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
⊢ IsTranscendenceBasis.{u_1, u_3, u_5} (ι := ι) R (f ∘ (⇑e : (a : ι) → ι')) ↔ IsTranscendenceBasis R f

Tactic:
simp_rw [IsTranscendenceBasis, algebraicIndependent_equiv, EquivLike.range_comp]

Premises used: IsTranscendenceBasis, EquivLike.range_comp, algebraicIndependent_equiv