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
rw :
  Eq (α := Polynomial ↥(adjoin R (range x)))
    (Polynomial.map (↑hx.aevalEquiv : MvPolynomial ι R →+* ↥(adjoin R (range x)))
      ((aeval fun (o : Option ι) ↦
            o.elim Polynomial.X fun (s : ι) ↦
              (Polynomial.C : (a : MvPolynomial ι R) → Polynomial (MvPolynomial ι R)) (X s) :
          (a : MvPolynomial (Option ι) R) → Polynomial (MvPolynomial ι R))
        (X none)))
    Polynomial.X
rw₁ :
  Eq (α := Polynomial ↥(adjoin R (range x)))
    (Polynomial.map (↑hx.aevalEquiv : MvPolynomial ι R →+* ↥(adjoin R (range x)))
      (Option.elim none Polynomial.X fun (s : ι) ↦
        (Polynomial.C : (a : MvPolynomial ι R) → Polynomial (MvPolynomial ι R)) (X s)))
    Polynomial.X
⊢ Eq.{v + 1} (α := Polynomial ↥(adjoin R (range x)))
    ((hx.mvPolynomialOptionEquivPolynomialAdjoin : (a : MvPolynomial (Option ι) R) → Polynomial ↥(adjoin R (range x)))
        (X none) :
      Polynomial ↥(adjoin R (range x)))
    (Polynomial.X : Polynomial ↥(adjoin R (range x)))
have rw₂ : Eq (α := Polynomial ↥(adjoin R (range x)))
  (Polynomial.map (↑hx.aevalEquiv : MvPolynomial ι R →+* ↥(adjoin R (range x))) Polynomial.X) Polynomial.X
Tactic: rw [AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_apply, aeval_X, Option.elim,
    Polynomial.map_X]
-- 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
rw :
  Eq (α := Polynomial ↥(adjoin R (range x)))
    (Polynomial.map (↑hx.aevalEquiv : MvPolynomial ι R →+* ↥(adjoin R (range x)))
      ((aeval fun (o : Option ι) ↦
            o.elim Polynomial.X fun (s : ι) ↦
              (Polynomial.C : (a : MvPolynomial ι R) → Polynomial (MvPolynomial ι R)) (X s) :
          (a : MvPolynomial (Option ι) R) → Polynomial (MvPolynomial ι R))
        (X none)))
    Polynomial.X
rw₁ :
  Eq (α := Polynomial ↥(adjoin R (range x)))
    (Polynomial.map (↑hx.aevalEquiv : MvPolynomial ι R →+* ↥(adjoin R (range x)))
      (Option.elim none Polynomial.X fun (s : ι) ↦
        (Polynomial.C : (a : MvPolynomial ι R) → Polynomial (MvPolynomial ι R)) (X s)))
    Polynomial.X
rw₂ :
  Eq (α := Polynomial ↥(adjoin R (range x)))
    (Polynomial.map (↑hx.aevalEquiv : MvPolynomial ι R →+* ↥(adjoin R (range x))) Polynomial.X) Polynomial.X
⊢ Eq.{v + 1} (α := Polynomial ↥(adjoin R (range x)))
    ((hx.mvPolynomialOptionEquivPolynomialAdjoin : (a : MvPolynomial (Option ι) R) → Polynomial ↥(adjoin R (range x)))
        (X none) :
      Polynomial ↥(adjoin R (range x)))
    (Polynomial.X : Polynomial ↥(adjoin R (range x)))
have rw₃ : Eq.{v + 1} (α := Polynomial ↥(adjoin R (range x))) Polynomial.X Polynomial.X
Tactic: rw [AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_apply, aeval_X, Option.elim,
    Polynomial.map_X]
-- 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
i : ι
⊢ Eq.{v + 1} (α := Polynomial ↥(adjoin R (range x)))
    ((hx.mvPolynomialOptionEquivPolynomialAdjoin : (a : MvPolynomial (Option ι) R) → Polynomial ↥(adjoin R (range x)))
        (X (some i)) :
      Polynomial ↥(adjoin R (range x)))
    ((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)))
have rw : Eq (α := Polynomial ↥(adjoin R (range x)))
  (Polynomial.map (↑hx.aevalEquiv : MvPolynomial ι R →+* ↥(adjoin R (range x)))
    ((aeval fun (o : Option ι) ↦
          o.elim Polynomial.X fun (s : ι) ↦
            (Polynomial.C : (a : MvPolynomial ι R) → Polynomial (MvPolynomial ι R)) (X s) :
        (a : MvPolynomial (Option ι) R) → Polynomial (MvPolynomial ι R))
      (X (some i))))
  ((Polynomial.C : (a : ↥(adjoin R (range x))) → Polynomial ↥(adjoin R (range x)))
    ((hx.aevalEquiv : (a : MvPolynomial ι R) → ↥(adjoin R (range x))) (X i)))
Tactic: rw [AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_apply, aeval_X, Option.elim,
    Polynomial.map_C, RingHom.coe_coe]
-- 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
i : ι
rw :
  Eq (α := Polynomial ↥(adjoin R (range x)))
    (Polynomial.map (↑hx.aevalEquiv : MvPolynomial ι R →+* ↥(adjoin R (range x)))
      ((aeval fun (o : Option ι) ↦
            o.elim Polynomial.X fun (s : ι) ↦
              (Polynomial.C : (a : MvPolynomial ι R) → Polynomial (MvPolynomial ι R)) (X s) :
          (a : MvPolynomial (Option ι) R) → Polynomial (MvPolynomial ι R))
        (X (some i))))
    ((Polynomial.C : (a : ↥(adjoin R (range x))) → Polynomial ↥(adjoin R (range x)))
      ((hx.aevalEquiv : (a : MvPolynomial ι R) → ↥(adjoin R (range x))) (X i)))
⊢ Eq.{v + 1} (α := Polynomial ↥(adjoin R (range x)))
    ((hx.mvPolynomialOptionEquivPolynomialAdjoin : (a : MvPolynomial (Option ι) R) → Polynomial ↥(adjoin R (range x)))
        (X (some i)) :
      Polynomial ↥(adjoin R (range x)))
    ((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)))
have rw₁ : Eq (α := Polynomial ↥(adjoin R (range x)))
  (Polynomial.map (↑hx.aevalEquiv : MvPolynomial ι R →+* ↥(adjoin R (range x)))
    ((some i).elim Polynomial.X fun (s : ι) ↦
      (Polynomial.C : (a : MvPolynomial ι R) → Polynomial (MvPolynomial ι R)) (X s)))
  ((Polynomial.C : (a : ↥(adjoin R (range x))) → Polynomial ↥(adjoin R (range x)))
    ((hx.aevalEquiv : (a : MvPolynomial ι R) → ↥(adjoin R (range x))) (X i)))
Tactic: rw [AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_apply, aeval_X, Option.elim,
    Polynomial.map_C, RingHom.coe_coe]
-- 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
i : ι
rw :
  Eq (α := Polynomial ↥(adjoin R (range x)))
    (Polynomial.map (↑hx.aevalEquiv : MvPolynomial ι R →+* ↥(adjoin R (range x)))
      ((aeval fun (o : Option ι) ↦
            o.elim Polynomial.X fun (s : ι) ↦
              (Polynomial.C : (a : MvPolynomial ι R) → Polynomial (MvPolynomial ι R)) (X s) :
          (a : MvPolynomial (Option ι) R) → Polynomial (MvPolynomial ι R))
        (X (some i))))
    ((Polynomial.C : (a : ↥(adjoin R (range x))) → Polynomial ↥(adjoin R (range x)))
      ((hx.aevalEquiv : (a : MvPolynomial ι R) → ↥(adjoin R (range x))) (X i)))
rw₁ :
  Eq (α := Polynomial ↥(adjoin R (range x)))
    (Polynomial.map (↑hx.aevalEquiv : MvPolynomial ι R →+* ↥(adjoin R (range x)))
      ((some i).elim Polynomial.X fun (s : ι) ↦
        (Polynomial.C : (a : MvPolynomial ι R) → Polynomial (MvPolynomial ι R)) (X s)))
    ((Polynomial.C : (a : ↥(adjoin R (range x))) → Polynomial ↥(adjoin R (range x)))
      ((hx.aevalEquiv : (a : MvPolynomial ι R) → ↥(adjoin R (range x))) (X i)))
⊢ Eq.{v + 1} (α := Polynomial ↥(adjoin R (range x)))
    ((hx.mvPolynomialOptionEquivPolynomialAdjoin : (a : MvPolynomial (Option ι) R) → Polynomial ↥(adjoin R (range x)))
        (X (some i)) :
      Polynomial ↥(adjoin R (range x)))
    ((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)))
have rw₂ : Eq (α := Polynomial ↥(adjoin R (range x)))
  (Polynomial.map (↑hx.aevalEquiv : MvPolynomial ι R →+* ↥(adjoin R (range x)))
    ((Polynomial.C : (a : MvPolynomial ι R) → Polynomial (MvPolynomial ι R)) (X i)))
  ((Polynomial.C : (a : ↥(adjoin R (range x))) → Polynomial ↥(adjoin R (range x)))
    ((hx.aevalEquiv : (a : MvPolynomial ι R) → ↥(adjoin R (range x))) (X i)))
Tactic: rw [AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_apply, aeval_X, Option.elim,
    Polynomial.map_C, RingHom.coe_coe]
-- 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
i : ι
rw :
  Eq (α := Polynomial ↥(adjoin R (range x)))
    (Polynomial.map (↑hx.aevalEquiv : MvPolynomial ι R →+* ↥(adjoin R (range x)))
      ((aeval fun (o : Option ι) ↦
            o.elim Polynomial.X fun (s : ι) ↦
              (Polynomial.C : (a : MvPolynomial ι R) → Polynomial (MvPolynomial ι R)) (X s) :
          (a : MvPolynomial (Option ι) R) → Polynomial (MvPolynomial ι R))
        (X (some i))))
    ((Polynomial.C : (a : ↥(adjoin R (range x))) → Polynomial ↥(adjoin R (range x)))
      ((hx.aevalEquiv : (a : MvPolynomial ι R) → ↥(adjoin R (range x))) (X i)))
rw₁ :
  Eq (α := Polynomial ↥(adjoin R (range x)))
    (Polynomial.map (↑hx.aevalEquiv : MvPolynomial ι R →+* ↥(adjoin R (range x)))
      ((some i).elim Polynomial.X fun (s : ι) ↦
        (Polynomial.C : (a : MvPolynomial ι R) → Polynomial (MvPolynomial ι R)) (X s)))
    ((Polynomial.C : (a : ↥(adjoin R (range x))) → Polynomial ↥(adjoin R (range x)))
      ((hx.aevalEquiv : (a : MvPolynomial ι R) → ↥(adjoin R (range x))) (X i)))
rw₂ :
  Eq (α := Polynomial ↥(adjoin R (range x)))
    (Polynomial.map (↑hx.aevalEquiv : MvPolynomial ι R →+* ↥(adjoin R (range x)))
      ((Polynomial.C : (a : MvPolynomial ι R) → Polynomial (MvPolynomial ι R)) (X i)))
    ((Polynomial.C : (a : ↥(adjoin R (range x))) → Polynomial ↥(adjoin R (range x)))
      ((hx.aevalEquiv : (a : MvPolynomial ι R) → ↥(adjoin R (range x))) (X i)))
⊢ Eq.{v + 1} (α := Polynomial ↥(adjoin R (range x)))
    ((hx.mvPolynomialOptionEquivPolynomialAdjoin : (a : MvPolynomial (Option ι) R) → Polynomial ↥(adjoin R (range x)))
        (X (some i)) :
      Polynomial ↥(adjoin R (range x)))
    ((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)))
have rw₃ : Eq.{v + 1} (α := Polynomial ↥(adjoin R (range x)))
  ((Polynomial.C : (a : ↥(adjoin R (range x))) → Polynomial ↥(adjoin R (range x)))
      (((↑hx.aevalEquiv : MvPolynomial ι R →+* ↥(adjoin R (range x))) : (a : MvPolynomial ι R) → ↥(adjoin R (range x)))
        (X i)) :
    Polynomial ↥(adjoin R (range x)))
  ((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)))
Tactic: rw [AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_apply, aeval_X, Option.elim,
    Polynomial.map_C, RingHom.coe_coe]
-- 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 (α := MvPolynomial.{u, u_2} (Option ι) R →+* A)
    (RingHom.comp (↑(Polynomial.aeval a) : Polynomial ↥(adjoin R (range x)) →+* A)
      hx.mvPolynomialOptionEquivPolynomialAdjoin.toRingHom)
    (↑(aeval fun (o : Option ι) ↦ o.elim a x) : MvPolynomial (Option ι) R →+* A)
have refine_1 : ∀ (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: refine MvPolynomial.ringHom_ext ?_ ?_
-- 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_1 :
  ∀ (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)
⊢ Eq (α := MvPolynomial.{u, u_2} (Option ι) R →+* A)
    (RingHom.comp (↑(Polynomial.aeval a) : Polynomial ↥(adjoin R (range x)) →+* A)
      hx.mvPolynomialOptionEquivPolynomialAdjoin.toRingHom)
    (↑(aeval fun (o : Option ι) ↦ o.elim a x) : MvPolynomial (Option ι) R →+* A)
have refine_2 : ∀ (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: refine MvPolynomial.ringHom_ext ?_ ?_
-- 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
⊢ ∀ (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)
have 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)
Tactic: simp only [RingHom.comp_apply, RingEquiv.toRingHom_eq_coe, RingEquiv.coe_toRingHom,
      AlgHom.coe_toRingHom, AlgHom.coe_toRingHom]
-- 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 : 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)
have 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)
Tactic: simp only [RingHom.comp_apply, RingEquiv.toRingHom_eq_coe, RingEquiv.coe_toRingHom,
      AlgHom.coe_toRingHom, AlgHom.coe_toRingHom]
-- 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
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)
have 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)
Tactic: rw [hx.mvPolynomialOptionEquivPolynomialAdjoin_C, aeval_C, Polynomial.aeval_C,
      IsScalarTower.algebraMap_apply R (adjoin R (range x)) A]
-- 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
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)
⊢ 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)
have 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)
Tactic: rw [hx.mvPolynomialOptionEquivPolynomialAdjoin_C, aeval_C, Polynomial.aeval_C,
      IsScalarTower.algebraMap_apply R (adjoin R (range x)) A]
-- 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
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)
⊢ 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)
have 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)
Tactic: rw [hx.mvPolynomialOptionEquivPolynomialAdjoin_C, aeval_C, Polynomial.aeval_C,
      IsScalarTower.algebraMap_apply R (adjoin R (range x)) A]
-- 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
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)
⊢ 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)
have 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)
Tactic: rw [hx.mvPolynomialOptionEquivPolynomialAdjoin_C, aeval_C, Polynomial.aeval_C,
      IsScalarTower.algebraMap_apply R (adjoin R (range x)) A]