awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.MvPolynomial (hypothesis)
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)
hf :
  Function.Injective (α := MvPolynomial.{u_1, u_2} (↑s : Type u_1) R[X]) (β :=
    MvPolynomial.{u_1, u_2} (↑s : Type u_1) R[X])
    (⇑g : (a : MvPolynomial (↑s : Type u_1) R[X]) → MvPolynomial (↑s : Type u_1) R[X])
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])
⊢ 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)
have 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)
Tactic: replace hf : Function.Injective u := by
    simp only [AlgHom.coe_comp, Subalgebra.coe_val,
      AlgEquiv.coe_algHom, AlgEquiv.coe_trans, Function.comp_assoc, u]
    apply Subtype.val_injective.comp
    simp only [EquivLike.comp_injective]
    apply hf.comp
    simp only [EquivLike.comp_injective, EquivLike.injective]
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.MvPolynomial (goal)
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 ⋯))))
have hX : 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 sorry))) :
        (a : R[X]) → MvPolynomial σ R)
      Polynomial.X :
    MvPolynomial σ R)
Tactic: ext1
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.MvPolynomial (hypothesis)
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)
⊢ 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)
have 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 sorry))))
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
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.MvPolynomial (hypothesis)
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 ⋯))))
⊢ 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)
have h2 : 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]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.MvPolynomial (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
i : σ
s : Set σ
h : i ∉ s
f : R[X]
hf : Transcendental R f
⊢ Transcendental ↥(supported R s) (A := MvPolynomial σ R)
    ((Polynomial.aeval (X i) : (a : R[X]) → MvPolynomial σ R) f : MvPolynomial σ R)
have rw : ∀ (hf : Function.Injective (α := R[X]) (β := R[X]) (⇑(Polynomial.aeval f) : (a : R[X]) → R[X])),
  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: classical
  rw [transcendental_iff_injective] at hf ⊢
  let g := MvPolynomial.mapAlgHom (R := R) (σ := s) (Polynomial.aeval (R := R) f)
  replace hf : Function.Injective g := MvPolynomial.map_injective _ hf
  let u := (Subalgebra.val _).comp
    ((optionEquivRight R s).symm |>.trans
      (renameEquiv R (Set.subtypeInsertEquivOption h).symm) |>.trans
      (supportedEquivMvPolynomial _).symm).toAlgHom |>.comp
    g |>.comp
    ((optionEquivLeft R s).symm.trans (optionEquivRight R s)).toAlgHom
  let v := ((Polynomial.aeval (R := supported R s)
    (Polynomial.aeval (X i : MvPolynomial σ R) f)).restrictScalars R).comp
      (Polynomial.mapAlgEquiv (supportedEquivMvPolynomial s).symm).toAlgHom
  replace hf : Function.Injective u := by
    simp only [AlgHom.coe_comp, Subalgebra.coe_val,
      AlgEquiv.coe_algHom, AlgEquiv.coe_trans, Function.comp_assoc, u]
    apply Subtype.val_injective.comp
    simp only [EquivLike.comp_injective]
    apply hf.comp
    simp only [EquivLike.comp_injective, EquivLike.injective]
  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
  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]
  simpa only [h2, v, AlgHom.coe_comp, AlgEquiv.coe_algHom,
    EquivLike.injective_comp, AlgHom.coe_restrictScalars'] using hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.MvPolynomial (hypothesis)
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
i : σ
f : R[X]
hf : Transcendental R f
⊢ Transcendental R (A := MvPolynomial σ R)
    ((Polynomial.aeval (X i) : (a : R[X]) → MvPolynomial σ R) f : MvPolynomial σ R)
have this : 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
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.MvPolynomial (goal)
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 ∅) ⊥ ⋯))
⊢ 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)))
have 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)
Tactic: ext1
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.MvPolynomial (goal)
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 ∅) ⊥ ⋯))
⊢ Transcendental R (A := MvPolynomial σ R)
    ((Polynomial.aeval (X i) : (a : R[X]) → MvPolynomial σ R) f : MvPolynomial σ R)
have rwa : ¬IsAlgebraic 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]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.MvPolynomial (goal)
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)
⊢ Transcendental R (A := MvPolynomial σ R)
    ((Polynomial.aeval (X i) : (a : R[X]) → MvPolynomial σ R) f : MvPolynomial σ R)
have 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)
Tactic: rwa [Transcendental, ← isAlgebraic_ringHom_iff_of_comp_eq g (RingHom.id (MvPolynomial σ R))
    Function.injective_id (by ext1; rfl), RingHom.id_apply, ← Transcendental]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.MvPolynomial (goal)
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)
⊢ Transcendental R (A := MvPolynomial σ R)
    ((Polynomial.aeval (X i) : (a : R[X]) → MvPolynomial σ R) f : MvPolynomial σ R)
have rwa₂ : ¬IsAlgebraic ↥(supported 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]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.MvPolynomial (goal)
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
have refine : 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⟩
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.MvPolynomial (goal)
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
have simp_rw : IsAlgebraic R f →
  IsAlgebraic R (A := MvPolynomial σ R) ((Polynomial.aeval (X i) : (a : R[X]) → MvPolynomial σ R) f : MvPolynomial σ R)
Tactic: simp_rw [Transcendental, not_imp_not]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.MvPolynomial (goal)
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
have refine_1 : ∀
  (h :
    Transcendental ↥(supported R s) (A := MvPolynomial σ R)
      ((Polynomial.aeval (X i) : (a : R[X]) → MvPolynomial σ R) f : MvPolynomial σ R)),
  i ∉ s
Tactic: refine ⟨fun h ↦ ⟨?_, ?_⟩, fun ⟨h, hf⟩ ↦ transcendental_supported_polynomial_aeval_X R h hf⟩
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.MvPolynomial (goal)
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
⊢ Transcendental ↥(supported R s) (A := MvPolynomial σ R)
      ((Polynomial.aeval (X i) : (a : R[X]) → MvPolynomial σ R) f : MvPolynomial σ R) ↔
    i ∉ s ∧ Transcendental R f
have 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
Tactic: refine ⟨fun h ↦ ⟨?_, ?_⟩, fun ⟨h, hf⟩ ↦ transcendental_supported_polynomial_aeval_X R h hf⟩
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.MvPolynomial (hypothesis)
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)
⊢ i ∉ s
have h₁ : ¬IsAlgebraic ↥(supported R s) (A := MvPolynomial σ R)
    ((Polynomial.aeval (X i) : (a : R[X]) → MvPolynomial σ R) f : MvPolynomial σ R)
Tactic: rw [Transcendental] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.MvPolynomial (goal)
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)
⊢ i ∉ s
have refine_1 : ∀ (h : i ∈ s),
  IsAlgebraic ↥(supported R s) (A := MvPolynomial σ R)
    ((Polynomial.aeval (X i) : (a : R[X]) → MvPolynomial σ R) f : MvPolynomial σ R)
Tactic: contrapose h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.MvPolynomial (goal)
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)
have 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)
Tactic: refine isAlgebraic_algebraMap (⟨Polynomial.aeval (X i) f, ?_⟩ : supported R s)
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.MvPolynomial (goal)
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)
⊢ Transcendental R f
have refine_2 : Transcendental R (A := MvPolynomial σ R) ((Polynomial.aeval (X i) : (a : R[X]) → MvPolynomial σ R) f : MvPolynomial σ R)
Tactic: rw [← transcendental_polynomial_aeval_X_iff R i]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.MvPolynomial (goal)
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)
⊢ Transcendental R (A := MvPolynomial σ R)
    ((Polynomial.aeval (X i) : (a : R[X]) → MvPolynomial σ R) f : MvPolynomial σ R)
have refine_2 : ∀ (x x_1 : R)
  (heq :
    Eq (α := ↥(supported R s)) ((algebraMap R ↥(supported R s) : (a : R) → ↥(supported R s)) x : ↥(supported R s))
      ((algebraMap R ↥(supported R s) : (a : R) → ↥(supported R s)) x_1 : ↥(supported R s))),
  Eq (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) x : MvPolynomial σ R)
    ((C : (a : R) → MvPolynomial σ R) x_1 : MvPolynomial σ R)
Tactic: refine h.restrictScalars fun _ _ heq ↦ MvPolynomial.C_injective σ R ?_
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.MvPolynomial (goal)
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)
x x_1 : R
heq :
  Eq (α := ↥(supported R s)) ((algebraMap R ↥(supported R s) : (a : R) → ↥(supported R s)) x : ↥(supported R s))
    ((algebraMap R ↥(supported R s) : (a : R) → ↥(supported R s)) x_1 : ↥(supported R s))
⊢ Eq (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) x : MvPolynomial σ R)
    ((C : (a : R) → MvPolynomial σ R) x_1 : MvPolynomial σ R)
have refine_2 : Eq (α := MvPolynomial σ R) ((algebraMap R (MvPolynomial σ R) : (a : R) → MvPolynomial σ R) x : MvPolynomial σ R)
  ((algebraMap R (MvPolynomial σ R) : (a : R) → MvPolynomial σ R) x_1 : MvPolynomial σ R)
Tactic: simp_rw [← MvPolynomial.algebraMap_eq]