awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Algebraic.MvPolynomial
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
i : σ
s : Set σ
h : i ∉ s
f : R[X]
g : MvPolynomial.{u_1, u_2} (↑s : Type u_1) R[X] →ₐ[R] MvPolynomial.{u_1, u_2} (↑s : Type u_1) R[X] :=
  mapAlgHom (Polynomial.aeval f)
u : (MvPolynomial.{u_1, u_2} (↑s : Type u_1) R)[X] →ₐ[R] MvPolynomial σ R :=
  (AlgHom.comp
        (AlgHom.comp (Subalgebra.val (supported R (insert i s)))
          (↑(AlgEquiv.trans
                (AlgEquiv.trans (AlgEquiv.symm (optionEquivRight R (↑s : Type u_1)))
                  (renameEquiv R (Set.subtypeInsertEquivOption (t := s) h).symm))
                (AlgEquiv.symm (supportedEquivMvPolynomial (insert i s)))) :
            MvPolynomial (↑s : Type u_1) R[X] →ₐ[R] ↥(supported R (insert i s))))
        g).comp
    (↑(AlgEquiv.trans (AlgEquiv.symm (optionEquivLeft R (↑s : Type u_1))) (optionEquivRight R (↑s : Type u_1))) :
      (MvPolynomial (↑s : Type u_1) R)[X] →ₐ[R] MvPolynomial (↑s : Type u_1) R[X])
v : (MvPolynomial.{u_1, u_2} (↑s : Type u_1) R)[X] →ₐ[R] MvPolynomial σ R :=
  AlgHom.comp
    (AlgHom.restrictScalars R (S := ↥(supported R s))
      (Polynomial.aeval ((Polynomial.aeval (X i) : (a : R[X]) → MvPolynomial σ R) f)))
    (↑(Polynomial.mapAlgEquiv (AlgEquiv.symm (supportedEquivMvPolynomial s))) :
      (MvPolynomial (↑s : Type u_1) R)[X] →ₐ[R] (↥(supported R s))[X])
hf :
  Function.Injective (α := (MvPolynomial.{u_1, u_2} (↑s : Type u_1) R)[X]) (β := MvPolynomial σ R)
    (⇑u : (a : (MvPolynomial (↑s : Type u_1) R)[X]) → MvPolynomial σ R)
⊢ Eq (α := MvPolynomial σ R) ((Polynomial.aeval (X i) : (a : R[X]) → MvPolynomial σ R) Polynomial.X : MvPolynomial σ R)
    ((AlgHom.comp
            (AlgHom.comp (Subalgebra.val (supported R (insert i s)))
              (↑(AlgEquiv.symm (supportedEquivMvPolynomial (insert i s))) :
                MvPolynomial (↑(insert i s) : Type u_1) R →ₐ[R] ↥(supported R (insert i s))))
            (Polynomial.aeval (X (Subtype.mk (p := fun (x : σ) ↦ x ∈ insert i s) i ⋯))) :
          (a : R[X]) → MvPolynomial σ R)
        Polynomial.X :
      MvPolynomial σ R)

Tactic:
simp
-- Module: Mathlib.RingTheory.Algebraic.MvPolynomial
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
i : σ
s : Set σ
h : i ∉ s
f : R[X]
g : MvPolynomial.{u_1, u_2} (↑s : Type u_1) R[X] →ₐ[R] MvPolynomial.{u_1, u_2} (↑s : Type u_1) R[X] :=
  mapAlgHom (Polynomial.aeval f)
u : (MvPolynomial.{u_1, u_2} (↑s : Type u_1) R)[X] →ₐ[R] MvPolynomial σ R :=
  (AlgHom.comp
        (AlgHom.comp (Subalgebra.val (supported R (insert i s)))
          (↑(AlgEquiv.trans
                (AlgEquiv.trans (AlgEquiv.symm (optionEquivRight R (↑s : Type u_1)))
                  (renameEquiv R (Set.subtypeInsertEquivOption (t := s) h).symm))
                (AlgEquiv.symm (supportedEquivMvPolynomial (insert i s)))) :
            MvPolynomial (↑s : Type u_1) R[X] →ₐ[R] ↥(supported R (insert i s))))
        g).comp
    (↑(AlgEquiv.trans (AlgEquiv.symm (optionEquivLeft R (↑s : Type u_1))) (optionEquivRight R (↑s : Type u_1))) :
      (MvPolynomial (↑s : Type u_1) R)[X] →ₐ[R] MvPolynomial (↑s : Type u_1) R[X])
v : (MvPolynomial.{u_1, u_2} (↑s : Type u_1) R)[X] →ₐ[R] MvPolynomial σ R :=
  AlgHom.comp
    (AlgHom.restrictScalars R (S := ↥(supported R s))
      (Polynomial.aeval ((Polynomial.aeval (X i) : (a : R[X]) → MvPolynomial σ R) f)))
    (↑(Polynomial.mapAlgEquiv (AlgEquiv.symm (supportedEquivMvPolynomial s))) :
      (MvPolynomial (↑s : Type u_1) R)[X] →ₐ[R] (↥(supported R s))[X])
hf :
  Function.Injective (α := (MvPolynomial.{u_1, u_2} (↑s : Type u_1) R)[X]) (β := MvPolynomial σ R)
    (⇑u : (a : (MvPolynomial (↑s : Type u_1) R)[X]) → MvPolynomial σ R)
⊢ Eq (α := R[X] →ₐ[R] MvPolynomial σ R) (Polynomial.aeval (X i))
    (AlgHom.comp
      (AlgHom.comp (Subalgebra.val (supported R (insert i s)))
        (↑(AlgEquiv.symm (supportedEquivMvPolynomial (insert i s))) :
          MvPolynomial (↑(insert i s) : Type u_1) R →ₐ[R] ↥(supported R (insert i s))))
      (Polynomial.aeval (X (Subtype.mk (p := fun (x : σ) ↦ x ∈ insert i s) i ⋯))))

Tactic:
have h1 : Polynomial.aeval (X i : MvPolynomial σ R) = ((Subalgebra.val _).comp
      (supportedEquivMvPolynomial _).symm.toAlgHom |>.comp
      (Polynomial.aeval (X ⟨i, s.mem_insert i⟩ : MvPolynomial ↑(insert i s) R))) := by
    ext1; simp
-- Module: Mathlib.RingTheory.Algebraic.MvPolynomial
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
i : σ
s : Set σ
h : i ∉ s
f : R[X]
g : MvPolynomial.{u_1, u_2} (↑s : Type u_1) R[X] →ₐ[R] MvPolynomial.{u_1, u_2} (↑s : Type u_1) R[X] :=
  mapAlgHom (Polynomial.aeval f)
u : (MvPolynomial.{u_1, u_2} (↑s : Type u_1) R)[X] →ₐ[R] MvPolynomial σ R :=
  (AlgHom.comp
        (AlgHom.comp (Subalgebra.val (supported R (insert i s)))
          (↑(AlgEquiv.trans
                (AlgEquiv.trans (AlgEquiv.symm (optionEquivRight R (↑s : Type u_1)))
                  (renameEquiv R (Set.subtypeInsertEquivOption (t := s) h).symm))
                (AlgEquiv.symm (supportedEquivMvPolynomial (insert i s)))) :
            MvPolynomial (↑s : Type u_1) R[X] →ₐ[R] ↥(supported R (insert i s))))
        g).comp
    (↑(AlgEquiv.trans (AlgEquiv.symm (optionEquivLeft R (↑s : Type u_1))) (optionEquivRight R (↑s : Type u_1))) :
      (MvPolynomial (↑s : Type u_1) R)[X] →ₐ[R] MvPolynomial (↑s : Type u_1) R[X])
v : (MvPolynomial.{u_1, u_2} (↑s : Type u_1) R)[X] →ₐ[R] MvPolynomial σ R :=
  AlgHom.comp
    (AlgHom.restrictScalars R (S := ↥(supported R s))
      (Polynomial.aeval ((Polynomial.aeval (X i) : (a : R[X]) → MvPolynomial σ R) f)))
    (↑(Polynomial.mapAlgEquiv (AlgEquiv.symm (supportedEquivMvPolynomial s))) :
      (MvPolynomial (↑s : Type u_1) R)[X] →ₐ[R] (↥(supported R s))[X])
hf :
  Function.Injective (α := (MvPolynomial.{u_1, u_2} (↑s : Type u_1) R)[X]) (β := MvPolynomial σ R)
    (⇑u : (a : (MvPolynomial (↑s : Type u_1) R)[X]) → MvPolynomial σ R)
h1 :
  Eq (α := R[X] →ₐ[R] MvPolynomial σ R) (Polynomial.aeval (X i))
    (AlgHom.comp
      (AlgHom.comp (Subalgebra.val (supported R (insert i s)))
        (↑(AlgEquiv.symm (supportedEquivMvPolynomial (insert i s))) :
          MvPolynomial (↑(insert i s) : Type u_1) R →ₐ[R] ↥(supported R (insert i s))))
      (Polynomial.aeval (X (Subtype.mk (p := fun (x : σ) ↦ x ∈ insert i s) i ⋯))))
simp :
  (AlgHom.comp
          (AlgHom.comp (Subalgebra.val (supported R (insert i s)))
            (↑(AlgEquiv.trans
                  (AlgEquiv.trans (AlgEquiv.symm (optionEquivRight R (↑s : Type u_1)))
                    (renameEquiv R (Set.subtypeInsertEquivOption (t := s) h).symm))
                  (AlgEquiv.symm (supportedEquivMvPolynomial (insert i s)))) :
              MvPolynomial (↑s : Type u_1) R[X] →ₐ[R] ↥(supported R (insert i s))))
          (mapAlgHom (Polynomial.aeval f))).comp
      (↑(AlgEquiv.trans (AlgEquiv.symm (optionEquivLeft R (↑s : Type u_1))) (optionEquivRight R (↑s : Type u_1))) :
        (MvPolynomial (↑s : Type u_1) R)[X] →ₐ[R] MvPolynomial (↑s : Type u_1) R[X]) =
    AlgHom.comp
      (AlgHom.restrictScalars R (S := ↥(supported R s))
        (Polynomial.aeval ((Polynomial.aeval (X i) : (a : R[X]) → MvPolynomial σ R) f)))
      (↑(Polynomial.mapAlgEquiv (AlgEquiv.symm (supportedEquivMvPolynomial s))) :
        (MvPolynomial (↑s : Type u_1) R)[X] →ₐ[R] (↥(supported R s))[X])
⊢ u = v

Tactic:
simp only [u, v, g]
-- Module: Mathlib.RingTheory.Algebraic.MvPolynomial
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
i : σ
s : Set σ
h : i ∉ s
f : R[X]
g : MvPolynomial.{u_1, u_2} (↑s : Type u_1) R[X] →ₐ[R] MvPolynomial.{u_1, u_2} (↑s : Type u_1) R[X] :=
  mapAlgHom (Polynomial.aeval f)
u : (MvPolynomial.{u_1, u_2} (↑s : Type u_1) R)[X] →ₐ[R] MvPolynomial σ R :=
  (AlgHom.comp
        (AlgHom.comp (Subalgebra.val (supported R (insert i s)))
          (↑(AlgEquiv.trans
                (AlgEquiv.trans (AlgEquiv.symm (optionEquivRight R (↑s : Type u_1)))
                  (renameEquiv R (Set.subtypeInsertEquivOption (t := s) h).symm))
                (AlgEquiv.symm (supportedEquivMvPolynomial (insert i s)))) :
            MvPolynomial (↑s : Type u_1) R[X] →ₐ[R] ↥(supported R (insert i s))))
        g).comp
    (↑(AlgEquiv.trans (AlgEquiv.symm (optionEquivLeft R (↑s : Type u_1))) (optionEquivRight R (↑s : Type u_1))) :
      (MvPolynomial (↑s : Type u_1) R)[X] →ₐ[R] MvPolynomial (↑s : Type u_1) R[X])
v : (MvPolynomial.{u_1, u_2} (↑s : Type u_1) R)[X] →ₐ[R] MvPolynomial σ R :=
  AlgHom.comp
    (AlgHom.restrictScalars R (S := ↥(supported R s))
      (Polynomial.aeval ((Polynomial.aeval (X i) : (a : R[X]) → MvPolynomial σ R) f)))
    (↑(Polynomial.mapAlgEquiv (AlgEquiv.symm (supportedEquivMvPolynomial s))) :
      (MvPolynomial (↑s : Type u_1) R)[X] →ₐ[R] (↥(supported R s))[X])
hf :
  Function.Injective (α := (MvPolynomial.{u_1, u_2} (↑s : Type u_1) R)[X]) (β := MvPolynomial σ R)
    (⇑u : (a : (MvPolynomial (↑s : Type u_1) R)[X]) → MvPolynomial σ R)
h1 :
  Eq (α := R[X] →ₐ[R] MvPolynomial σ R) (Polynomial.aeval (X i))
    (AlgHom.comp
      (AlgHom.comp (Subalgebra.val (supported R (insert i s)))
        (↑(AlgEquiv.symm (supportedEquivMvPolynomial (insert i s))) :
          MvPolynomial (↑(insert i s) : Type u_1) R →ₐ[R] ↥(supported R (insert i s))))
      (Polynomial.aeval (X (Subtype.mk (p := fun (x : σ) ↦ x ∈ insert i s) i ⋯))))
⊢ u = v

Tactic:
have h2 : u = v := by
    simp only [u, v, g]
    ext1
    · ext1
      simp [Set.subtypeInsertEquivOption, Subalgebra.algebraMap_eq, optionEquivLeft_symm_apply]
    · simp [Set.subtypeInsertEquivOption, h1, optionEquivLeft_symm_apply]
-- Module: Mathlib.RingTheory.Algebraic.MvPolynomial
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
i : σ
s : Set σ
h : i ∉ s
f : R[X]
g : MvPolynomial.{u_1, u_2} (↑s : Type u_1) R[X] →ₐ[R] MvPolynomial.{u_1, u_2} (↑s : Type u_1) R[X] :=
  mapAlgHom (Polynomial.aeval f)
u : (MvPolynomial.{u_1, u_2} (↑s : Type u_1) R)[X] →ₐ[R] MvPolynomial σ R :=
  (AlgHom.comp
        (AlgHom.comp (Subalgebra.val (supported R (insert i s)))
          (↑(AlgEquiv.trans
                (AlgEquiv.trans (AlgEquiv.symm (optionEquivRight R (↑s : Type u_1)))
                  (renameEquiv R (Set.subtypeInsertEquivOption (t := s) h).symm))
                (AlgEquiv.symm (supportedEquivMvPolynomial (insert i s)))) :
            MvPolynomial (↑s : Type u_1) R[X] →ₐ[R] ↥(supported R (insert i s))))
        g).comp
    (↑(AlgEquiv.trans (AlgEquiv.symm (optionEquivLeft R (↑s : Type u_1))) (optionEquivRight R (↑s : Type u_1))) :
      (MvPolynomial (↑s : Type u_1) R)[X] →ₐ[R] MvPolynomial (↑s : Type u_1) R[X])
v : (MvPolynomial.{u_1, u_2} (↑s : Type u_1) R)[X] →ₐ[R] MvPolynomial σ R :=
  AlgHom.comp
    (AlgHom.restrictScalars R (S := ↥(supported R s))
      (Polynomial.aeval ((Polynomial.aeval (X i) : (a : R[X]) → MvPolynomial σ R) f)))
    (↑(Polynomial.mapAlgEquiv (AlgEquiv.symm (supportedEquivMvPolynomial s))) :
      (MvPolynomial (↑s : Type u_1) R)[X] →ₐ[R] (↥(supported R s))[X])
hf :
  Function.Injective (α := (MvPolynomial.{u_1, u_2} (↑s : Type u_1) R)[X]) (β := MvPolynomial σ R)
    (⇑u : (a : (MvPolynomial (↑s : Type u_1) R)[X]) → MvPolynomial σ R)
h1 :
  Eq (α := R[X] →ₐ[R] MvPolynomial σ R) (Polynomial.aeval (X i))
    (AlgHom.comp
      (AlgHom.comp (Subalgebra.val (supported R (insert i s)))
        (↑(AlgEquiv.symm (supportedEquivMvPolynomial (insert i s))) :
          MvPolynomial (↑(insert i s) : Type u_1) R →ₐ[R] ↥(supported R (insert i s))))
      (Polynomial.aeval (X (Subtype.mk (p := fun (x : σ) ↦ x ∈ insert i s) i ⋯))))
h2 : u = v
⊢ Function.Injective (α := (↥(supported R s))[X]) (β := MvPolynomial σ R)
    (⇑(Polynomial.aeval ((Polynomial.aeval (X i) : (a : R[X]) → MvPolynomial σ R) f) :
          (↥(supported R s))[X] →ₐ[↥(supported R s)] MvPolynomial σ R) :
      (a : (↥(supported R s))[X]) → MvPolynomial σ R)

Tactic:
simpa only [h2, v, AlgHom.coe_comp, AlgEquiv.coe_algHom,
    EquivLike.injective_comp, AlgHom.coe_restrictScalars'] using hf

Premises used: EquivLike.injective_comp, AlgHom.coe_comp, AlgHom.coe_restrictScalars', AlgEquiv.coe_algHom
-- Module: Mathlib.RingTheory.Algebraic.MvPolynomial
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
i : σ
f : R[X]
hf : Transcendental R f
⊢ Transcendental ↥(supported R ∅) (A := MvPolynomial σ R)
    ((Polynomial.aeval (X i) : (a : R[X]) → MvPolynomial σ R) f : MvPolynomial σ R)

Tactic:
have := transcendental_supported_polynomial_aeval_X R (Set.notMem_empty i) hf
-- Module: Mathlib.RingTheory.Algebraic.MvPolynomial
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
i : σ
f : R[X]
hf : Transcendental R f
this :
  Transcendental ↥(supported R ∅) (A := MvPolynomial σ R)
    ((Polynomial.aeval (X i) : (a : R[X]) → MvPolynomial σ R) f : MvPolynomial σ R)
g : R ≃ₐ[R] ↥(supported R ∅) :=
  AlgEquiv.trans (AlgEquiv.symm (Algebra.botEquivOfInjective ⋯))
    (AlgEquiv.symm (Subalgebra.equivOfEq (supported R ∅) ⊥ ⋯))
a :
  ∀ (x : R),
    Eq (α := MvPolynomial σ R)
      ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap (↥(supported R ∅)) (MvPolynomial σ R))
              (↑g : R →+* ↥(supported R ∅)) :
            (a : R) → MvPolynomial σ R)
          x :
        MvPolynomial σ R)
      ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
              (↑(RingHom.id (MvPolynomial σ R)) : MvPolynomial σ R →+* MvPolynomial σ R)
              (algebraMap R (MvPolynomial σ R)) :
            (a : R) → MvPolynomial σ R)
          x :
        MvPolynomial σ R)
⊢ Eq (α := R →+* MvPolynomial σ R)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap (↥(supported R ∅)) (MvPolynomial σ R))
      (↑g : R →+* ↥(supported R ∅)))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (↑(RingHom.id (MvPolynomial σ R)) : MvPolynomial σ R →+* MvPolynomial σ R) (algebraMap R (MvPolynomial σ R)))

Tactic:
ext1
-- Module: Mathlib.RingTheory.Algebraic.MvPolynomial
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
i : σ
f : R[X]
hf : Transcendental R f
this :
  Transcendental ↥(supported R ∅) (A := MvPolynomial σ R)
    ((Polynomial.aeval (X i) : (a : R[X]) → MvPolynomial σ R) f : MvPolynomial σ R)
g : R ≃ₐ[R] ↥(supported R ∅) :=
  AlgEquiv.trans (AlgEquiv.symm (Algebra.botEquivOfInjective ⋯))
    (AlgEquiv.symm (Subalgebra.equivOfEq (supported R ∅) ⊥ ⋯))
x : R
⊢ Eq (α := MvPolynomial σ R)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap (↥(supported R ∅)) (MvPolynomial σ R))
            (↑g : R →+* ↥(supported R ∅)) :
          (a : R) → MvPolynomial σ R)
        x :
      MvPolynomial σ R)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
            (↑(RingHom.id (MvPolynomial σ R)) : MvPolynomial σ R →+* MvPolynomial σ R)
            (algebraMap R (MvPolynomial σ R)) :
          (a : R) → MvPolynomial σ R)
        x :
      MvPolynomial σ R)

Tactic:
rfl
-- Module: Mathlib.RingTheory.Algebraic.MvPolynomial
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
i : σ
f : R[X]
hf : Transcendental R f
this :
  Transcendental ↥(supported R ∅) (A := MvPolynomial σ R)
    ((Polynomial.aeval (X i) : (a : R[X]) → MvPolynomial σ R) f : MvPolynomial σ R)
g : R ≃ₐ[R] ↥(supported R ∅) :=
  AlgEquiv.trans (AlgEquiv.symm (Algebra.botEquivOfInjective ⋯))
    (AlgEquiv.symm (Subalgebra.equivOfEq (supported R ∅) ⊥ ⋯))
rwa :
  ¬IsAlgebraic R (A := MvPolynomial σ R) ((Polynomial.aeval (X i) : (a : R[X]) → MvPolynomial σ R) f : MvPolynomial σ R)
rwa₁ :
  ¬IsAlgebraic ↥(supported R ∅) (A := MvPolynomial σ R)
      ((RingHom.id (MvPolynomial σ R) : (a : MvPolynomial σ R) → MvPolynomial σ R)
          ((Polynomial.aeval (X i) : (a : R[X]) → MvPolynomial σ R) f) :
        MvPolynomial σ R)
rwa₂ :
  ¬IsAlgebraic ↥(supported R ∅) (A := MvPolynomial σ R)
      ((Polynomial.aeval (X i) : (a : R[X]) → MvPolynomial σ R) f : MvPolynomial σ R)
rwa₃ rwa₄ rwa₅ rwa₆ :
  Transcendental ↥(supported R ∅) (A := MvPolynomial σ R)
    ((Polynomial.aeval (X i) : (a : R[X]) → MvPolynomial σ R) f : MvPolynomial σ R)
⊢ Transcendental R (A := MvPolynomial σ R)
    ((Polynomial.aeval (X i) : (a : R[X]) → MvPolynomial σ R) f : MvPolynomial σ R)

Tactic:
rwa [Transcendental, ← isAlgebraic_ringHom_iff_of_comp_eq g (RingHom.id (MvPolynomial σ R))
    Function.injective_id (by ext1; rfl), RingHom.id_apply, ← Transcendental]

Premises used: RingHom.id_apply, Function.injective_id, Transcendental, MvPolynomial, isAlgebraic_ringHom_iff_of_comp_eq, RingHom.id
-- Module: Mathlib.RingTheory.Algebraic.MvPolynomial
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
i : σ
f : R[X]
⊢ Transcendental R (A := MvPolynomial σ R)
      ((Polynomial.aeval (X i) : (a : R[X]) → MvPolynomial σ R) f : MvPolynomial σ R) ↔
    Transcendental R f

Tactic:
⟨?_, transcendental_polynomial_aeval_X R i⟩

Premises used: Iff.intro, MvPolynomial.transcendental_polynomial_aeval_X
-- Module: Mathlib.RingTheory.Algebraic.MvPolynomial
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
i : σ
f : R[X]
refine :
  Transcendental R (A := MvPolynomial σ R)
      ((Polynomial.aeval (X i) : (a : R[X]) → MvPolynomial σ R) f : MvPolynomial σ R) →
    Transcendental R f
⊢ Transcendental R (A := MvPolynomial σ R)
      ((Polynomial.aeval (X i) : (a : R[X]) → MvPolynomial σ R) f : MvPolynomial σ R) ↔
    Transcendental R f

Tactic:
refine ⟨?_, transcendental_polynomial_aeval_X R i⟩
-- Module: Mathlib.RingTheory.Algebraic.MvPolynomial
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
i : σ
f : R[X]
simp_rw :
  IsAlgebraic R f →
    IsAlgebraic R (A := MvPolynomial σ R)
      ((Polynomial.aeval (X i) : (a : R[X]) → MvPolynomial σ R) f : MvPolynomial σ R)
⊢ Transcendental R (A := MvPolynomial σ R)
      ((Polynomial.aeval (X i) : (a : R[X]) → MvPolynomial σ R) f : MvPolynomial σ R) →
    Transcendental R f

Tactic:
simp_rw [Transcendental, not_imp_not]

Premises used: Transcendental, not_imp_not
-- Module: Mathlib.RingTheory.Algebraic.MvPolynomial
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
i : σ
f : R[X]
⊢ IsAlgebraic R f →
    IsAlgebraic R (A := MvPolynomial σ R)
      ((Polynomial.aeval (X i) : (a : R[X]) → MvPolynomial σ R) f : MvPolynomial σ R)

Tactic:
fun h ↦ h.algHom _

Premises used: IsAlgebraic.algHom, MvPolynomial.X, Polynomial.aeval
-- Module: Mathlib.RingTheory.Algebraic.MvPolynomial
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
i : σ
f : R[X]
⊢ IsAlgebraic R f →
    IsAlgebraic R (A := MvPolynomial σ R)
      ((Polynomial.aeval (X i) : (a : R[X]) → MvPolynomial σ R) f : MvPolynomial σ R)

Tactic:
exact fun h ↦ h.algHom _
-- Module: Mathlib.RingTheory.Algebraic.MvPolynomial
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : Nontrivial R
i : σ
s : Set σ
f : R[X]
⊢ Transcendental ↥(supported R s) (A := MvPolynomial σ R)
      ((Polynomial.aeval (X i) : (a : R[X]) → MvPolynomial σ R) f : MvPolynomial σ R) ↔
    i ∉ s ∧ Transcendental R f

Tactic:
⟨fun h ↦ ⟨?_, ?_⟩, fun ⟨h, hf⟩ ↦ transcendental_supported_polynomial_aeval_X R h hf⟩

Premises used: MvPolynomial.X, Membership.mem, Subtype, _private.0.MvPolynomial.transcendental_supported_polynomial_aeval_X_iff.match_1, Transcendental, And.intro, Iff.intro, MvPolynomial.supported, Polynomial.aeval, DFunLike.coe, MvPolynomial.transcendental_supported_polynomial_aeval_X
-- Module: Mathlib.RingTheory.Algebraic.MvPolynomial
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : Nontrivial R
i : σ
s : Set σ
f : R[X]
refine_1 :
  ∀
    (h :
      Transcendental ↥(supported R s) (A := MvPolynomial σ R)
        ((Polynomial.aeval (X i) : (a : R[X]) → MvPolynomial σ R) f : MvPolynomial σ R)),
    i ∉ s
refine_2 :
  ∀
    (h :
      Transcendental ↥(supported R s) (A := MvPolynomial σ R)
        ((Polynomial.aeval (X i) : (a : R[X]) → MvPolynomial σ R) f : MvPolynomial σ R)),
    Transcendental R f
⊢ Transcendental ↥(supported R s) (A := MvPolynomial σ R)
      ((Polynomial.aeval (X i) : (a : R[X]) → MvPolynomial σ R) f : MvPolynomial σ R) ↔
    i ∉ s ∧ Transcendental R f

Tactic:
refine ⟨fun h ↦ ⟨?_, ?_⟩, fun ⟨h, hf⟩ ↦ transcendental_supported_polynomial_aeval_X R h hf⟩
-- Module: Mathlib.RingTheory.Algebraic.MvPolynomial
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : Nontrivial R
i : σ
s : Set σ
f : R[X]
h :
  Transcendental ↥(supported R s) (A := MvPolynomial σ R)
    ((Polynomial.aeval (X i) : (a : R[X]) → MvPolynomial σ R) f : MvPolynomial σ R)
⊢ ¬IsAlgebraic ↥(supported R s) (A := MvPolynomial σ R)
      ((Polynomial.aeval (X i) : (a : R[X]) → MvPolynomial σ R) f : MvPolynomial σ R)

Tactic:
rw [Transcendental] at h

Premises used: Transcendental
-- Module: Mathlib.RingTheory.Algebraic.MvPolynomial
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : Nontrivial R
i : σ
s : Set σ
f : R[X]
h :
  ¬IsAlgebraic ↥(supported R s) (A := MvPolynomial σ R)
      ((Polynomial.aeval (X i) : (a : R[X]) → MvPolynomial σ R) f : MvPolynomial σ R)
refine_1 :
  ∀ (h : i ∈ s),
    IsAlgebraic ↥(supported R s) (A := MvPolynomial σ R)
      ((Polynomial.aeval (X i) : (a : R[X]) → MvPolynomial σ R) f : MvPolynomial σ R)
⊢ i ∉ s

Tactic:
contrapose h
-- Module: Mathlib.RingTheory.Algebraic.MvPolynomial
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : Nontrivial R
i : σ
s : Set σ
f : R[X]
h : i ∈ s
⊢ IsAlgebraic ↥(supported R s) (A := MvPolynomial σ R)
    ((Polynomial.aeval (X i) : (a : R[X]) → MvPolynomial σ R) f : MvPolynomial σ R)

Tactic:
isAlgebraic_algebraMap (⟨Polynomial.aeval (X i) f, ?_⟩ : supported R s)

Premises used: MvPolynomial.X, Subtype.mk, isAlgebraic_algebraMap, Polynomial.aeval, DFunLike.coe
-- Module: Mathlib.RingTheory.Algebraic.MvPolynomial
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : Nontrivial R
i : σ
s : Set σ
f : R[X]
h : i ∈ s
refine_1 :
  Membership.mem (α := MvPolynomial σ R) (γ := Subalgebra R (MvPolynomial σ R)) (supported R s)
    ((Polynomial.aeval (X i) : (a : R[X]) → MvPolynomial σ R) f : MvPolynomial σ R)
⊢ IsAlgebraic ↥(supported R s) (A := MvPolynomial σ R)
    ((Polynomial.aeval (X i) : (a : R[X]) → MvPolynomial σ R) f : MvPolynomial σ R)

Tactic:
refine isAlgebraic_algebraMap (⟨Polynomial.aeval (X i) f, ?_⟩ : supported R s)

Premises used: MvPolynomial.X, Subtype.mk, isAlgebraic_algebraMap, Polynomial.aeval, DFunLike.coe
-- Module: Mathlib.RingTheory.Algebraic.MvPolynomial
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : Nontrivial R
i : σ
s : Set σ
f : R[X]
h : i ∈ s
⊢ Membership.mem (α := MvPolynomial σ R) (γ := Subalgebra R (MvPolynomial σ R)) (supported R s)
    ((Polynomial.aeval (X i) : (a : R[X]) → MvPolynomial σ R) f : MvPolynomial σ R)

Tactic:
Algebra.adjoin_mono (Set.singleton_subset_iff.2 (Set.mem_image_of_mem _ h))
      (Polynomial.aeval_mem_adjoin_singleton _ _)

Premises used: Iff.mpr, Set.singleton_subset_iff, Set.Mem, setOf, Set.mem_image_of_mem, Algebra.adjoin_mono, Polynomial.aeval_mem_adjoin_singleton
-- Module: Mathlib.RingTheory.Algebraic.MvPolynomial
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : Nontrivial R
i : σ
s : Set σ
f : R[X]
h : i ∈ s
⊢ Membership.mem (α := MvPolynomial σ R) (γ := Subalgebra R (MvPolynomial σ R)) (supported R s)
    ((Polynomial.aeval (X i) : (a : R[X]) → MvPolynomial σ R) f : MvPolynomial σ R)

Tactic:
exact Algebra.adjoin_mono (Set.singleton_subset_iff.2 (Set.mem_image_of_mem _ h))
      (Polynomial.aeval_mem_adjoin_singleton _ _)

Premises used: Iff.mpr, Set.singleton_subset_iff, Set.mem_image_of_mem, Algebra.adjoin_mono, Polynomial.aeval_mem_adjoin_singleton
-- Module: Mathlib.RingTheory.Algebraic.MvPolynomial
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : Nontrivial R
i : σ
s : Set σ
f : R[X]
h :
  Transcendental ↥(supported R s) (A := MvPolynomial σ R)
    ((Polynomial.aeval (X i) : (a : R[X]) → MvPolynomial σ R) f : MvPolynomial σ R)
refine_2 :
  Transcendental R (A := MvPolynomial σ R)
    ((Polynomial.aeval (X i) : (a : R[X]) → MvPolynomial σ R) f : MvPolynomial σ R)
⊢ Transcendental R f

Tactic:
rw [← transcendental_polynomial_aeval_X_iff R i]

Premises used: MvPolynomial.transcendental_polynomial_aeval_X_iff