awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
⊢ Transcendental R (A := MvPolynomial σ R)
    ((Polynomial.aeval (X i) : (a : R[X]) → MvPolynomial σ R) f : MvPolynomial σ R)

Tactic:
h.restrictScalars fun _ _ heq ↦ MvPolynomial.C_injective σ R ?_

Premises used: Transcendental.restrictScalars, MvPolynomial.C_injective
-- 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 :
  ∀ (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)
⊢ Transcendental R (A := MvPolynomial σ R)
    ((Polynomial.aeval (X i) : (a : R[X]) → MvPolynomial σ R) f : MvPolynomial σ R)

Tactic:
refine h.restrictScalars fun _ _ heq ↦ MvPolynomial.C_injective σ R ?_

Premises used: Transcendental.restrictScalars, MvPolynomial.C_injective
-- 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)
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))
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)
⊢ Eq (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) x : MvPolynomial σ R)
    ((C : (a : R) → MvPolynomial σ R) x_1 : MvPolynomial σ R)

Tactic:
simp_rw [← MvPolynomial.algebraMap_eq]

Premises used: MvPolynomial.algebraMap_eq
-- 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)
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) ((algebraMap R (MvPolynomial σ R) : (a : R) → MvPolynomial σ R) x : MvPolynomial σ R)
    ((algebraMap R (MvPolynomial σ R) : (a : R) → MvPolynomial σ R) x_1 : MvPolynomial σ R)

Tactic:
congr($(heq).1)

Premises used: congrArg, id, Subtype.val
-- 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)
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) ((algebraMap R (MvPolynomial σ R) : (a : R) → MvPolynomial σ R) x : MvPolynomial σ R)
    ((algebraMap R (MvPolynomial σ R) : (a : R) → MvPolynomial σ R) x_1 : MvPolynomial σ R)

Tactic:
exact congr($(heq).1)
-- Module: Mathlib.RingTheory.Algebraic.MvPolynomial
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
i : σ
s : Set σ
h : i ∉ s
⊢ Transcendental ↥(supported R s) (A := MvPolynomial σ R) (X i)

Tactic:
simpa using transcendental_supported_polynomial_aeval_X R h (Polynomial.transcendental_X R)

Premises used: Polynomial.transcendental_X, MvPolynomial.transcendental_supported_polynomial_aeval_X
-- Module: Mathlib.RingTheory.Algebraic.MvPolynomial
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
i : σ
⊢ Transcendental R (A := MvPolynomial σ R) (X i)

Tactic:
simpa using transcendental_polynomial_aeval_X R i (Polynomial.transcendental_X R)

Premises used: Polynomial.transcendental_X, MvPolynomial.transcendental_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 σ
⊢ Transcendental ↥(supported R s) (A := MvPolynomial σ R) (X i) ↔ i ∉ s

Tactic:
simpa [Polynomial.transcendental_X] using
    transcendental_supported_polynomial_aeval_X_iff R (i := i) (s := s) (f := Polynomial.X)

Premises used: Polynomial.transcendental_X, MvPolynomial.transcendental_supported_polynomial_aeval_X_iff
-- Module: Mathlib.RingTheory.Algebraic.Pi
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : SMul R S
p : R[X]
f : R → S
x : R
⊢ (p • f) x = eval x p • f x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Algebraic.Pi
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
inst_3 : SMul S T
p : R[X]
f : S → T
x : S
⊢ (p • f) x = HSMul.hSMul.{u_2, u_3, u_3} (α := S) ((aeval x : (a : R[X]) → S) p : S) (f x)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Algebraic.Pi
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : CommSemiring T
inst_3 : Algebra R S
inst_4 : Algebra S T
z : S
⊢ Eq.{u_3 + 1} (α := T) ((algebraMap S T : (a : S) → T) ((aeval z : (a : R[X]) → S) 1 : S) : T) (1 z : T)

Tactic:
simp only [Pi.one_apply, map_one]

Premises used: Pi.one_apply, map_one
-- Module: Mathlib.RingTheory.Algebraic.Pi
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : CommSemiring T
inst_3 : Algebra R S
inst_4 : Algebra S T
x x_1 : R[X]
z : S
⊢ (algebraMap S T : (a : S) → T) ((aeval z : (a : R[X]) → S) (x * x_1) : S) =
    HMul.hMul (α := S → T) (β := S → T)
      (fun (z : S) ↦ (algebraMap S T : (a : S) → T) ((aeval z : (a : R[X]) → S) x : S))
      (fun (z : S) ↦ (algebraMap S T : (a : S) → T) ((aeval z : (a : R[X]) → S) x_1 : S)) z

Tactic:
simp only [Pi.mul_apply, map_mul]

Premises used: Pi.mul_apply, map_mul
-- Module: Mathlib.RingTheory.Algebraic.Pi
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : CommSemiring T
inst_3 : Algebra R S
inst_4 : Algebra S T
z : S
⊢ Eq.{u_3 + 1} (α := T) ((algebraMap S T : (a : S) → T) ((aeval z : (a : R[X]) → S) 0 : S) : T) (0 z : T)

Tactic:
simp only [Pi.zero_apply, map_zero]

Premises used: Pi.zero_apply, map_zero
-- Module: Mathlib.RingTheory.Algebraic.Pi
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : CommSemiring T
inst_3 : Algebra R S
inst_4 : Algebra S T
x x_1 : R[X]
z : S
⊢ (algebraMap S T : (a : S) → T) ((aeval z : (a : R[X]) → S) (x + x_1) : S) =
    HAdd.hAdd (α := S → T) (β := S → T)
      (fun (z : S) ↦ (algebraMap S T : (a : S) → T) ((aeval z : (a : R[X]) → S) x : S))
      (fun (z : S) ↦ (algebraMap S T : (a : S) → T) ((aeval z : (a : R[X]) → S) x_1 : S)) z

Tactic:
simp only [Pi.add_apply, map_add]

Premises used: map_add, Pi.add_apply
-- Module: Mathlib.RingTheory.Algebraic.Pi
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : CommSemiring T
inst_3 : Algebra R S
inst_4 : Algebra S T
x : R[X]
x_1 : S → T
z : S
⊢ HMul.hMul (α := S → T)
      (({ toFun := fun (p : R[X]) (z : S) ↦ (algebraMap S T : (a : S) → T) ((aeval z : (a : R[X]) → S) p : S),
              map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ : R[X] →+* S → T } :
            (a : R[X]) → S → T)
          x :
        S → T)
      x_1 z =
    HMul.hMul (β := S → T) x_1
      (({ toFun := fun (p : R[X]) (z : S) ↦ (algebraMap S T : (a : S) → T) ((aeval z : (a : R[X]) → S) p : S),
              map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } :
            (a : R[X]) → S → T)
          x :
        S → T)
      z

Tactic:
mul_comm _ _

Premises used: mul_comm
-- Module: Mathlib.RingTheory.Algebraic.Pi
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : CommSemiring T
inst_3 : Algebra R S
inst_4 : Algebra S T
x : R[X]
x_1 : S → T
z : S
⊢ HMul.hMul (α := S → T)
      (({ toFun := fun (p : R[X]) (z : S) ↦ (algebraMap S T : (a : S) → T) ((aeval z : (a : R[X]) → S) p : S),
              map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ : R[X] →+* S → T } :
            (a : R[X]) → S → T)
          x :
        S → T)
      x_1 z =
    HMul.hMul (β := S → T) x_1
      (({ toFun := fun (p : R[X]) (z : S) ↦ (algebraMap S T : (a : S) → T) ((aeval z : (a : R[X]) → S) p : S),
              map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } :
            (a : R[X]) → S → T)
          x :
        S → T)
      z

Tactic:
exact mul_comm _ _

Premises used: mul_comm
-- Module: Mathlib.RingTheory.Algebraic.Pi
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : CommSemiring T
inst_3 : Algebra R S
inst_4 : Algebra S T
x : R[X]
x_1 : S → T
z : S
⊢ (x • x_1) z =
    HMul.hMul (α := S → T)
      (({ toFun := fun (p : R[X]) (z : S) ↦ (algebraMap S T : (a : S) → T) ((aeval z : (a : R[X]) → S) p : S),
              map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } :
            (a : R[X]) → S → T)
          x :
        S → T)
      x_1 z

Tactic:
simp only [polynomial_smul_apply', Algebra.algebraMap_eq_smul_one, RingHom.coe_mk,
      MonoidHom.coe_mk, OneHom.coe_mk, Pi.mul_apply, Algebra.smul_mul_assoc, one_mul]

Premises used: polynomial_smul_apply', Pi.mul_apply, OneHom.coe_mk, Algebra.algebraMap_eq_smul_one, MonoidHom.coe_mk, RingHom.coe_mk, Algebra.smul_mul_assoc, one_mul
-- Module: Mathlib.RingTheory.Algebraic.Pi
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : CommSemiring T
inst_3 : Algebra R S
inst_4 : Algebra S T
⊢ Eq (α := (a : R[X]) → S → T) (⇑(algebraMap R[X] (S → T)) : (a : R[X]) → S → T) fun (p : R[X]) (z : S) ↦
    (algebraMap S T : (a : S) → T) ((aeval z : (a : R[X]) → S) p : S)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Algebraic.Pi
Goal:
R : Type u_1
inst : CommSemiring R
⊢ Eq.{u_1 + 1} (α := (a : R[X]) → R → R) (⇑(algebraMap R[X] (R → R)) : (a : R[X]) → R → R) fun (p : R[X]) (z : R) ↦
    eval z p

Tactic:
rfl

Premises used: Polynomial.eval, MonoidHomClass.toMonoidHom, RingHomClass.toRingHom, rfl
-- Module: Mathlib.RingTheory.Algebraic.StronglyTranscendental
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
h : IsStronglyTranscendental R x
inst_3 : FaithfulSMul R S
p : R[X]
hp : Eq.{u_2 + 1} (α := S) ((aeval x : (a : R[X]) → S) p : S) (0 : S)
⊢ ∀ (n : ℕ), p.coeff n = coeff 0 n

Tactic:
simpa [Algebra.smul_def, hp, Polynomial.ext_iff] using h 1 p

Premises used: Polynomial.ext_iff, Algebra.smul_def, OfNat.ofNat
-- Module: Mathlib.RingTheory.Algebraic.StronglyTranscendental
Goal:
R : Type u_1
inst : CommRing R
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : FaithfulSMul R K
x : K
⊢ IsStronglyTranscendental R x ↔ Transcendental R x

Tactic:
⟨fun h ↦ h.transcendental, fun h ↦ ?_⟩

Premises used: IsStronglyTranscendental.transcendental, Iff.intro
-- Module: Mathlib.RingTheory.Algebraic.StronglyTranscendental
Goal:
R : Type u_1
inst : CommRing R
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : FaithfulSMul R K
x : K
refine : ∀ (h : Transcendental R x), IsStronglyTranscendental R x
⊢ IsStronglyTranscendental R x ↔ Transcendental R x

Tactic:
refine ⟨fun h ↦ h.transcendental, fun h ↦ ?_⟩
-- Module: Mathlib.RingTheory.Algebraic.StronglyTranscendental
Goal:
R : Type u_1
inst : CommRing R
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : FaithfulSMul R K
x : K
h : Transcendental R x
⊢ IsStronglyTranscendental R x

Tactic:
simpa [IsStronglyTranscendental, or_imp, forall_and, @forall_comm K, ← subsingleton_iff_forall_eq,
    not_subsingleton, ext_iff, forall_or_left, ← imp_iff_or_not, transcendental_iff] using h

Premises used: Polynomial.ext_iff, forall_comm, or_imp, subsingleton_iff_forall_eq, not_subsingleton, forall_or_left, IsStronglyTranscendental, imp_iff_or_not, transcendental_iff, forall_and
-- Module: Mathlib.RingTheory.Algebraic.StronglyTranscendental
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing T
inst_4 : Algebra R T
x : S
f : S →ₐ[R] T
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := S) (β := T) (⇑f : (a : S) → T)
h : IsStronglyTranscendental.{u_1, u_3} R (S := T) ((f : (a : S) → T) x : T)
⊢ IsStronglyTranscendental R x

Tactic:
fun u p hp ↦ ?_

Premises used: IsStronglyTranscendental
-- Module: Mathlib.RingTheory.Algebraic.StronglyTranscendental
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing T
inst_4 : Algebra R T
x : S
f : S →ₐ[R] T
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := S) (β := T) (⇑f : (a : S) → T)
h : IsStronglyTranscendental.{u_1, u_3} R (S := T) ((f : (a : S) → T) x : T)
refine :
  ∀ (u : S) (p : R[X]) (hp : HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) p : S) u = 0),
    HMul.hMul (α := S[X]) (β := S[X]) (map (algebraMap R S) p) ((C : (a : S) → S[X]) u : S[X]) = 0
⊢ IsStronglyTranscendental R x

Tactic:
refine fun u p hp ↦ ?_
-- Module: Mathlib.RingTheory.Algebraic.StronglyTranscendental
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing T
inst_4 : Algebra R T
x : S
f : S →ₐ[R] T
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := S) (β := T) (⇑f : (a : S) → T)
h : IsStronglyTranscendental.{u_1, u_3} R (S := T) ((f : (a : S) → T) x : T)
u : S
p : R[X]
hp : HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) p : S) u = 0
rw :
  HMul.hMul (α := T) (β := T) ((f : (a : S) → T) ((aeval x : (a : R[X]) → S) p : S) : T) ((f : (a : S) → T) u : T) = 0
rw₁ : Eq.{u_3 + 1} (α := T) ((f : (a : S) → T) (HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) p : S) u) : T) (0 : T)
rw₂ : Eq.{u_3 + 1} (α := T) ((f : (a : S) → T) 0 : T) (0 : T)
rw₃ rw₄ : Eq.{u_3 + 1} (α := T) 0 0
⊢ HMul.hMul (α := T) (β := T) (((aeval ((f : (a : S) → T) x) : R[X] →ₐ[R] T) : (a : R[X]) → T) p : T)
      ((f : (a : S) → T) u : T) =
    0

Tactic:
rw [aeval_algHom_apply, ← map_mul, hp, map_zero]

Premises used: map_zero, map_mul, Polynomial.aeval_algHom_apply
-- Module: Mathlib.RingTheory.Algebraic.StronglyTranscendental
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing T
inst_4 : Algebra R T
x : S
f : S →ₐ[R] T
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := S) (β := T) (⇑f : (a : S) → T)
h : IsStronglyTranscendental.{u_1, u_3} R (S := T) ((f : (a : S) → T) x : T)
u : S
p : R[X]
hp : HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) p : S) u = 0
⊢ HMul.hMul (α := T[X]) (β := T[X]) (map (algebraMap R T) p) ((C : (a : T) → T[X]) ((f : (a : S) → T) u) : T[X]) = 0

Tactic:
have := h (f u) p (by rw [aeval_algHom_apply, ← map_mul, hp, map_zero])
-- Module: Mathlib.RingTheory.Algebraic.StronglyTranscendental
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing T
inst_4 : Algebra R T
x : S
f : S →ₐ[R] T
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := S) (β := T) (⇑f : (a : S) → T)
h : IsStronglyTranscendental.{u_1, u_3} R (S := T) ((f : (a : S) → T) x : T)
u : S
p : R[X]
hp : HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) p : S) u = 0
this :
  HMul.hMul (α := T[X]) (β := T[X]) (map (algebraMap R T) p) ((C : (a : T) → T[X]) ((f : (a : S) → T) u) : T[X]) = 0
hf₁ :
  ∀
    (this :
      Eq.{u_3 + 1} (α := T[X])
        (((mapRingHom (↑f : S →+* T) : RingHom.{u_2, u_3} S[X] T[X]) : (a : S[X]) → T[X])
            (HMul.hMul (α := S[X]) (β := S[X]) (map (algebraMap R S) p) ((C : (a : S) → S[X]) u : S[X])) :
          T[X])
        (0 : T[X])),
    Function.Injective.{u_2 + 1, u_3 + 1} (α := S[X]) (β := T[X]) (⇑(mapRingHom (↑f : S →+* T)) : (a : S[X]) → T[X])
⊢ HMul.hMul (α := S[X]) (β := S[X]) (map (algebraMap R S) p) ((C : (a : S) → S[X]) u : S[X]) = 0

Tactic:
rwa [← f.comp_algebraMap, ← map_map, ← f.coe_toRingHom, ← map_C, ← Polynomial.map_mul,
    ← coe_mapRingHom, map_eq_zero_iff] at this

Premises used: AlgHom.coe_toRingHom, Polynomial.map_mul, AlgHom.comp_algebraMap, Polynomial.coe_mapRingHom, map_eq_zero_iff, Polynomial.map_C, Polynomial.map_map
-- Module: Mathlib.RingTheory.Algebraic.StronglyTranscendental
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing T
inst_4 : Algebra R T
x : S
f : S →ₐ[R] T
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := S) (β := T) (⇑f : (a : S) → T)
h : IsStronglyTranscendental.{u_1, u_3} R (S := T) ((f : (a : S) → T) x : T)
u : S
p : R[X]
hp : HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) p : S) u = 0
this :
  Eq.{u_3 + 1} (α := T[X])
    (((mapRingHom (↑f : S →+* T) : RingHom.{u_2, u_3} S[X] T[X]) : (a : S[X]) → T[X])
        (HMul.hMul (α := S[X]) (β := S[X]) (map (algebraMap R S) p) ((C : (a : S) → S[X]) u : S[X])) :
      T[X])
    (0 : T[X])
⊢ Function.Injective.{u_2 + 1, u_3 + 1} (α := S[X]) (β := T[X]) (⇑(mapRingHom (↑f : S →+* T)) : (a : S[X]) → T[X])

Tactic:
map_injective f.toRingHom hf

Premises used: MonoidHomClass.toMonoidHom, Polynomial.map_injective, AlgHom.toRingHom, RingHomClass.toRingHom, Polynomial.map
-- Module: Mathlib.RingTheory.Algebraic.StronglyTranscendental
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing T
inst_4 : Algebra R T
x : S
f : S →ₐ[R] T
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := S) (β := T) (⇑f : (a : S) → T)
h : IsStronglyTranscendental.{u_1, u_3} R (S := T) ((f : (a : S) → T) x : T)
u : S
p : R[X]
hp : HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) p : S) u = 0
this :
  Eq.{u_3 + 1} (α := T[X])
    (((mapRingHom (↑f : S →+* T) : RingHom.{u_2, u_3} S[X] T[X]) : (a : S[X]) → T[X])
        (HMul.hMul (α := S[X]) (β := S[X]) (map (algebraMap R S) p) ((C : (a : S) → S[X]) u : S[X])) :
      T[X])
    (0 : T[X])
⊢ Function.Injective.{u_2 + 1, u_3 + 1} (α := S[X]) (β := T[X]) (⇑(mapRingHom (↑f : S →+* T)) : (a : S[X]) → T[X])

Tactic:
exact map_injective f.toRingHom hf

Premises used: Polynomial.map_injective, AlgHom.toRingHom
-- Module: Mathlib.RingTheory.Algebraic.StronglyTranscendental
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
M : Submonoid S
inst_6 : IsLocalization M T
inst_7 : IsScalarTower R S T
x : S
h : IsStronglyTranscendental R x
⊢ IsStronglyTranscendental.{u_1, u_3} R (S := T) ((algebraMap S T : (a : S) → T) x : T)

Tactic:
fun u p hp ↦ ?_

Premises used: IsStronglyTranscendental
-- Module: Mathlib.RingTheory.Algebraic.StronglyTranscendental
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
M : Submonoid S
inst_6 : IsLocalization M T
inst_7 : IsScalarTower R S T
x : S
h : IsStronglyTranscendental R x
refine :
  ∀ (u : T) (p : R[X])
    (hp :
      HMul.hMul (α := T) (((aeval ((algebraMap S T : (a : S) → T) x) : R[X] →ₐ[R] T) : (a : R[X]) → T) p : T) u = 0),
    HMul.hMul (α := T[X]) (β := T[X]) (map (algebraMap R T) p) ((C : (a : T) → T[X]) u : T[X]) = 0
⊢ IsStronglyTranscendental.{u_1, u_3} R (S := T) ((algebraMap S T : (a : S) → T) x : T)

Tactic:
refine fun u p hp ↦ ?_
-- Module: Mathlib.RingTheory.Algebraic.StronglyTranscendental
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
M : Submonoid S
inst_6 : IsLocalization M T
inst_7 : IsScalarTower R S T
x : S
h : IsStronglyTranscendental R x
u : T
p : R[X]
hp : HMul.hMul (α := T) (((aeval ((algebraMap S T : (a : S) → T) x) : R[X] →ₐ[R] T) : (a : R[X]) → T) p : T) u = 0
obtain :
  ∀ (u : S) (s : ↥M)
    (hp :
      HMul.hMul (α := T) (((aeval ((algebraMap S T : (a : S) → T) x) : R[X] →ₐ[R] T) : (a : R[X]) → T) p : T)
          (IsLocalization.mk' T u s) =
        0),
    HMul.hMul (α := T[X]) (β := T[X]) (map (algebraMap R T) p)
        ((C : (a : T) → T[X]) (IsLocalization.mk' T u s) : T[X]) =
      0
⊢ HMul.hMul (α := T[X]) (β := T[X]) (map (algebraMap R T) p) ((C : (a : T) → T[X]) u : T[X]) = 0

Tactic:
obtain ⟨u, s, rfl⟩ := IsLocalization.exists_mk'_eq M u

Premises used: rfl, IsLocalization.exists_mk'_eq
-- Module: Mathlib.RingTheory.Algebraic.StronglyTranscendental
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
M : Submonoid S
inst_6 : IsLocalization M T
inst_7 : IsScalarTower R S T
x : S
h : IsStronglyTranscendental R x
p : R[X]
u : S
s : ↥M
hp :
  HMul.hMul (α := T) (((aeval ((algebraMap S T : (a : S) → T) x) : R[X] →ₐ[R] T) : (a : R[X]) → T) p : T)
      (IsLocalization.mk' T u s) =
    0
⊢ ∃ a ∈ M, a * HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) p : S) u = 0

Tactic:
simpa [aeval_algebraMap_apply, ← Algebra.smul_def, IsLocalization.smul_mk',
      IsLocalization.mk'_eq_zero_iff] using hp

Premises used: IsLocalization.smul_mk', IsLocalization.mk'_eq_zero_iff, Algebra.smul_def, Polynomial.aeval_algebraMap_apply
-- Module: Mathlib.RingTheory.Algebraic.StronglyTranscendental
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
M : Submonoid S
inst_6 : IsLocalization M T
inst_7 : IsScalarTower R S T
x : S
h : IsStronglyTranscendental R x
p : R[X]
u : S
s : ↥M
hp :
  HMul.hMul (α := T) (((aeval ((algebraMap S T : (a : S) → T) x) : R[X] →ₐ[R] T) : (a : R[X]) → T) p : T)
      (IsLocalization.mk' T u s) =
    0
obtain :
  ∀ (a : S) (haM : a ∈ M) (e : a * HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) p : S) u = 0),
    HMul.hMul (α := T[X]) (β := T[X]) (map (algebraMap R T) p)
        ((C : (a : T) → T[X]) (IsLocalization.mk' T u s) : T[X]) =
      0
⊢ HMul.hMul (α := T[X]) (β := T[X]) (map (algebraMap R T) p) ((C : (a : T) → T[X]) (IsLocalization.mk' T u s) : T[X]) =
    0

Tactic:
obtain ⟨a, haM, e⟩ : ∃ a ∈ M, a * ((aeval x) p * u) = 0 := by
    simpa [aeval_algebraMap_apply, ← Algebra.smul_def, IsLocalization.smul_mk',
      IsLocalization.mk'_eq_zero_iff] using hp

Premises used: HMul.hMul, Polynomial.aeval, DFunLike.coe
-- Module: Mathlib.RingTheory.Algebraic.StronglyTranscendental
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
M : Submonoid S
inst_6 : IsLocalization M T
inst_7 : IsScalarTower R S T
x : S
h : IsStronglyTranscendental R x
p : R[X]
u : S
s : ↥M
hp :
  HMul.hMul (α := T) (((aeval ((algebraMap S T : (a : S) → T) x) : R[X] →ₐ[R] T) : (a : R[X]) → T) p : T)
      (IsLocalization.mk' T u s) =
    0
a : S
haM : a ∈ M
e : a * HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) p : S) u = 0
⊢ HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) p : S) (a * u) = 0

Tactic:
linear_combination e