awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 (α := T[X]) (β := T[X]) (map (algebraMap R T) p)
      ((C : (a : T) → T[X]) (HSMul.hSMul (β := T) a ((algebraMap S T : (a : S) → T) u : T)) : T[X]) =
    0

Tactic:
simpa [map_map, ← IsScalarTower.algebraMap_eq, Algebra.smul_def] using
      congr(map (algebraMap S T) $(h (a * u) p (by linear_combination e)))

Premises used: IsScalarTower.algebraMap_eq, Algebra.smul_def, 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
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 (α := T[X]) (β := T[X]) (map (algebraMap R T) p)
      ((C : (a : T) → T[X]) (HSMul.hSMul (β := T) a ((algebraMap S T : (a : S) → T) u : T)) : T[X]) =
    0

Tactic:
have : p.map (algebraMap R T) * C (a • algebraMap S T u) = 0 := by
    simpa [map_map, ← IsScalarTower.algebraMap_eq, Algebra.smul_def] using
      congr(map (algebraMap S T) $(h (a * u) p (by linear_combination e)))
-- 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
this :
  HMul.hMul (α := T[X]) (β := T[X]) (map (algebraMap R T) p)
      ((C : (a : T) → T[X]) (HSMul.hSMul (β := T) a ((algebraMap S T : (a : S) → T) u : T)) : 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:
((IsLocalization.map_units T (⟨a, haM⟩ * s)).map C).mul_right_cancel ?_

Premises used: Polynomial.C, HMul.hMul, IsLocalization.map_units, IsUnit.map, IsUnit.mul_right_cancel
-- 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
this :
  HMul.hMul (α := T[X]) (β := T[X]) (map (algebraMap R T) p)
      ((C : (a : T) → T[X]) (HSMul.hSMul (β := T) a ((algebraMap S T : (a : S) → T) u : T)) : T[X]) =
    0
refine :
  HMul.hMul (β := T[X])
      (HMul.hMul (α := T[X]) (β := T[X]) (map (algebraMap R T) p)
        ((C : (a : T) → T[X]) (IsLocalization.mk' T u s) : T[X]))
      ((C : (a : T) → T[X]) ((algebraMap S T : (a : S) → T) (↑(Subtype.mk (p := fun (x : S) ↦ x ∈ M) a haM * s) : S)) :
        T[X]) =
    HMul.hMul (α := T[X]) (β := T[X]) (0 : T[X])
      ((C : (a : T) → T[X]) ((algebraMap S T : (a : S) → T) (↑(Subtype.mk (p := fun (x : S) ↦ x ∈ M) a haM * s) : S)) :
        T[X])
⊢ 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:
refine ((IsLocalization.map_units T (⟨a, haM⟩ * s)).map C).mul_right_cancel ?_

Premises used: Polynomial.C, HMul.hMul, IsLocalization.map_units, IsUnit.map, IsUnit.mul_right_cancel
-- 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
this :
  HMul.hMul (α := T[X]) (β := T[X]) (map (algebraMap R T) p)
      ((C : (a : T) → T[X]) (HSMul.hSMul (β := T) a ((algebraMap S T : (a : S) → T) u : T)) : T[X]) =
    0
⊢ HMul.hMul (β := T[X])
      (HMul.hMul (α := T[X]) (β := T[X]) (map (algebraMap R T) p)
        ((C : (a : T) → T[X]) (IsLocalization.mk' T u s) : T[X]))
      ((C : (a : T) → T[X]) ((algebraMap S T : (a : S) → T) (↑(Subtype.mk (p := fun (x : S) ↦ x ∈ M) a haM * s) : S)) :
        T[X]) =
    HMul.hMul (α := T[X]) (β := T[X]) (0 : T[X])
      ((C : (a : T) → T[X]) ((algebraMap S T : (a : S) → T) (↑(Subtype.mk (p := fun (x : S) ↦ x ∈ M) a haM * s) : S)) :
        T[X])

Tactic:
simpa [mul_assoc, ← map_mul, mul_comm _ (algebraMap _ _ _), ← Algebra.smul_def, mul_smul]

Premises used: Algebra.algebraMap, mul_assoc, map_mul, mul_comm, Algebra.smul_def, DFunLike.coe, SemigroupAction.mul_smul
-- 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 R
inst_6 : IsLocalization M S
inst_7 : IsScalarTower R S T
x : T
h : IsStronglyTranscendental R x
t : T
p : S[X]
hp : HMul.hMul (α := T) ((aeval x : (a : S[X]) → T) p : T) t = 0
obtain :
  ∀ (a : R) (ha₁ : a ∈ M) (ha₂ : map (algebraMap R S) (IsLocalization.integerNormalization M p) = a • p),
    HMul.hMul (α := T[X]) (β := T[X]) (map (algebraMap S T) p) ((C : (a : T) → T[X]) t : T[X]) = 0
⊢ HMul.hMul (α := T[X]) (β := T[X]) (map (algebraMap S T) p) ((C : (a : T) → T[X]) t : T[X]) = 0

Tactic:
obtain ⟨a, ha₁, ha₂⟩ := IsLocalization.integerNormalization_spec M p

Premises used: IsLocalization.integerNormalization_spec
-- 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 R
inst_6 : IsLocalization M S
inst_7 : IsScalarTower R S T
x : T
h : IsStronglyTranscendental R x
t : T
p : S[X]
hp : HMul.hMul (α := T) ((aeval x : (a : S[X]) → T) p : T) t = 0
a : R
ha₁ : a ∈ M
ha₂ : map (algebraMap R S) (IsLocalization.integerNormalization M p) = a • p
⊢ (aeval x : (a : R[X]) → T) (IsLocalization.integerNormalization M p) =
    HSMul.hSMul (β := T) a ((aeval x : (a : S[X]) → T) p : T)

Tactic:
simpa [AlgHom.map_smul_of_tower] using congr(aeval x $ha₂)

Premises used: AlgHom.map_smul_of_tower
-- 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 R
inst_6 : IsLocalization M S
inst_7 : IsScalarTower R S T
x : T
h : IsStronglyTranscendental R x
t : T
p : S[X]
hp : HMul.hMul (α := T) ((aeval x : (a : S[X]) → T) p : T) t = 0
a : R
ha₁ : a ∈ M
ha₂ : map (algebraMap R S) (IsLocalization.integerNormalization M p) = a • p
⊢ (aeval x : (a : R[X]) → T) (IsLocalization.integerNormalization M p) =
    HSMul.hSMul (β := T) a ((aeval x : (a : S[X]) → T) p : T)

Tactic:
have H : aeval x (IsLocalization.integerNormalization M p) = a • aeval x p := by
    simpa [AlgHom.map_smul_of_tower] using congr(aeval x $ha₂)
-- 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 R
inst_6 : IsLocalization M S
inst_7 : IsScalarTower R S T
x : T
h : IsStronglyTranscendental R x
t : T
p : S[X]
hp : HMul.hMul (α := T) ((aeval x : (a : S[X]) → T) p : T) t = 0
a : R
ha₁ : a ∈ M
ha₂ : map (algebraMap R S) (IsLocalization.integerNormalization M p) = a • p
H :
  (aeval x : (a : R[X]) → T) (IsLocalization.integerNormalization M p) =
    HSMul.hSMul (β := T) a ((aeval x : (a : S[X]) → T) p : T)
⊢ HMul.hMul (α := T) ((aeval x : (a : R[X]) → T) (IsLocalization.integerNormalization M p) : T) t = 0

Tactic:
simp [H, 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 R
inst_6 : IsLocalization M S
inst_7 : IsScalarTower R S T
x : T
h : IsStronglyTranscendental R x
t : T
p : S[X]
hp : HMul.hMul (α := T) ((aeval x : (a : S[X]) → T) p : T) t = 0
a : R
ha₁ : a ∈ M
ha₂ : map (algebraMap R S) (IsLocalization.integerNormalization M p) = a • p
H :
  (aeval x : (a : R[X]) → T) (IsLocalization.integerNormalization M p) =
    HSMul.hSMul (β := T) a ((aeval x : (a : S[X]) → T) p : T)
⊢ HMul.hMul (α := T[X]) (β := T[X]) (map (algebraMap R T) (IsLocalization.integerNormalization M p))
      ((C : (a : T) → T[X]) t : T[X]) =
    0

Tactic:
have := h t (IsLocalization.integerNormalization M p) (by simp [H, 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 R
inst_6 : IsLocalization M S
inst_7 : IsScalarTower R S T
x : T
h : IsStronglyTranscendental R x
t : T
p : S[X]
hp : HMul.hMul (α := T) ((aeval x : (a : S[X]) → T) p : T) t = 0
a : R
ha₁ : a ∈ M
ha₂ : map (algebraMap R S) (IsLocalization.integerNormalization M p) = a • p
H :
  (aeval x : (a : R[X]) → T) (IsLocalization.integerNormalization M p) =
    HSMul.hSMul (β := T) a ((aeval x : (a : S[X]) → T) p : T)
this :
  HMul.hMul (α := T[X]) (β := T[X]) (map (algebraMap R T) (IsLocalization.integerNormalization M p))
      ((C : (a : T) → T[X]) t : T[X]) =
    0
⊢ HMul.hMul (α := T[X]) (β := T[X]) (map (algebraMap S T) (a • p)) ((C : (a : T) → T[X]) t : T[X]) = 0

Tactic:
rw [IsScalarTower.algebraMap_eq R S T, ← map_map, ha₂] at this

Premises used: IsScalarTower.algebraMap_eq, 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
inst_5 : Algebra S T
M : Submonoid R
inst_6 : IsLocalization M S
inst_7 : IsScalarTower R S T
x : T
h : IsStronglyTranscendental R x
t : T
p : S[X]
hp : HMul.hMul (α := T) ((aeval x : (a : S[X]) → T) p : T) t = 0
a : R
ha₁ : a ∈ M
ha₂ : map (algebraMap R S) (IsLocalization.integerNormalization M p) = a • p
H :
  (aeval x : (a : R[X]) → T) (IsLocalization.integerNormalization M p) =
    HSMul.hSMul (β := T) a ((aeval x : (a : S[X]) → T) p : T)
this : HMul.hMul (α := T[X]) (β := T[X]) (map (algebraMap S T) (a • p)) ((C : (a : T) → T[X]) t : T[X]) = 0
rw :
  HMul.hMul (α := T[X])
      ((C : (a : T) → T[X])
          ((algebraMap S T : (a : S) → T)
            ((algebraMap R S : (a : R) → S) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ M) a ha₁) : R) : S)) :
        T[X])
      (HMul.hMul (α := T[X]) (β := T[X]) (map (algebraMap S T) p) ((C : (a : T) → T[X]) t : T[X])) =
    HMul.hMul (α := T[X]) (β := T[X])
      ((C : (a : T) → T[X])
          ((algebraMap S T : (a : S) → T)
            ((algebraMap R S : (a : R) → S) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ M) a ha₁) : R) : S)) :
        T[X])
      (0 : T[X])
⊢ HMul.hMul (α := T[X]) (β := T[X]) (map (algebraMap S T) p) ((C : (a : T) → T[X]) t : T[X]) = 0

Tactic:
rw [← (((IsLocalization.map_units S ⟨a, ha₁⟩).map (algebraMap S T)).map C).mul_right_inj]

Premises used: Polynomial.C, Algebra.algebraMap, IsUnit.mul_right_inj, Subtype.mk, IsLocalization.map_units, IsUnit.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
inst_5 : Algebra S T
M : Submonoid R
inst_6 : IsLocalization M S
inst_7 : IsScalarTower R S T
x : T
h : IsStronglyTranscendental R x
t : T
p : S[X]
hp : HMul.hMul (α := T) ((aeval x : (a : S[X]) → T) p : T) t = 0
a : R
ha₁ : a ∈ M
ha₂ : map (algebraMap R S) (IsLocalization.integerNormalization M p) = a • p
H :
  (aeval x : (a : R[X]) → T) (IsLocalization.integerNormalization M p) =
    HSMul.hSMul (β := T) a ((aeval x : (a : S[X]) → T) p : T)
this : HMul.hMul (α := T[X]) (β := T[X]) (map (algebraMap S T) (a • p)) ((C : (a : T) → T[X]) t : T[X]) = 0
⊢ HMul.hMul (α := T[X])
      ((C : (a : T) → T[X])
          ((algebraMap S T : (a : S) → T)
            ((algebraMap R S : (a : R) → S) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ M) a ha₁) : R) : S)) :
        T[X])
      (HMul.hMul (α := T[X]) (β := T[X]) (map (algebraMap S T) p) ((C : (a : T) → T[X]) t : T[X])) =
    HMul.hMul (α := T[X]) (β := T[X])
      ((C : (a : T) → T[X])
          ((algebraMap S T : (a : S) → T)
            ((algebraMap R S : (a : R) → S) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ M) a ha₁) : R) : S)) :
        T[X])
      (0 : T[X])

Tactic:
simpa [Algebra.smul_def, mul_assoc] using this

Premises used: mul_assoc, Algebra.smul_def
-- 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
inst_6 : IsScalarTower R S T
x : T
h : IsStronglyTranscendental S x
t : T
p : R[X]
hp : HMul.hMul (α := T) ((aeval x : (a : R[X]) → T) p : T) t = 0
⊢ HMul.hMul (α := T) ((aeval x : (a : S[X]) → T) (map (algebraMap R S) p) : T) t = 0

Tactic:
simpa
-- 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
inst_6 : IsScalarTower R S T
x : T
h : IsStronglyTranscendental S x
t : T
p : R[X]
hp : HMul.hMul (α := T) ((aeval x : (a : R[X]) → T) p : T) t = 0
⊢ HMul.hMul (α := T[X]) (β := T[X]) (map (algebraMap R T) p) ((C : (a : T) → T[X]) t : T[X]) = 0

Tactic:
simpa [map_map, ← IsScalarTower.algebraMap_eq] using h t (p.map (algebraMap R S)) (by simpa)

Premises used: Algebra.algebraMap, IsScalarTower.algebraMap_eq, Polynomial.map, 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
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
x : T
h : IsStronglyTranscendental R x
H : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
t : T
p : S[X]
hp : HMul.hMul (α := T) ((aeval x : (a : S[X]) → T) p : T) t = 0
obtain :
  ∀ (p : R[X]) (hp : HMul.hMul (α := T) ((aeval x : (a : S[X]) → T) (map (algebraMap R S) p) : T) t = 0),
    HMul.hMul (α := T[X]) (β := T[X]) (map (algebraMap S T) (map (algebraMap R S) p)) ((C : (a : T) → T[X]) t : T[X]) =
      0
⊢ HMul.hMul (α := T[X]) (β := T[X]) (map (algebraMap S T) p) ((C : (a : T) → T[X]) t : T[X]) = 0

Tactic:
obtain ⟨p, rfl⟩ := map_surjective _ H p

Premises used: Polynomial.map_surjective, rfl
-- 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
inst_6 : IsScalarTower R S T
x : T
h : IsStronglyTranscendental R x
H : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
t : T
p : R[X]
hp : HMul.hMul (α := T) ((aeval x : (a : S[X]) → T) (map (algebraMap R S) p) : T) t = 0
⊢ HMul.hMul (α := T) ((aeval x : (a : R[X]) → T) p : T) t = 0

Tactic:
simpa using 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
inst_6 : IsScalarTower R S T
x : T
h : IsStronglyTranscendental R x
H : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
t : T
p : R[X]
hp : HMul.hMul (α := T) ((aeval x : (a : S[X]) → T) (map (algebraMap R S) p) : T) t = 0
⊢ HMul.hMul (α := T[X]) (β := T[X]) (map (algebraMap S T) (map (algebraMap R S) p)) ((C : (a : T) → T[X]) t : T[X]) = 0

Tactic:
simpa [map_map, ← IsScalarTower.algebraMap_eq] using h t p (by simpa using hp)

Premises used: IsScalarTower.algebraMap_eq, 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
inst_5 : Algebra S T
M : Submonoid S
hM : M ≤ S⁰
inst_6 : IsLocalization M T
inst_7 : IsScalarTower R S T
x : S
⊢ IsStronglyTranscendental.{u_1, u_3} R (S := T) ((algebraMap S T : (a : S) → T) x : T) ↔ IsStronglyTranscendental R x

Tactic:
⟨fun h ↦ .of_map (f := IsScalarTower.toAlgHom R S T) (IsLocalization.injective _ hM) h,
    fun h ↦ .of_isLocalization M h⟩

Premises used: IsStronglyTranscendental.of_map, IsLocalization.injective, Iff.intro, IsStronglyTranscendental.of_isLocalization
-- 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
K : Type u_4
inst_3 : Field K
inst_4 : Algebra R K
inst_5 : Algebra S K
inst_6 : IsScalarTower R S K
inst_7 : FaithfulSMul R S
inst_8 : IsFractionRing S K
x : S
⊢ FaithfulSMul R K

Tactic:
have : FaithfulSMul R K := .trans R S K
-- 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
K : Type u_4
inst_3 : Field K
inst_4 : Algebra R K
inst_5 : Algebra S K
inst_6 : IsScalarTower R S K
inst_7 : FaithfulSMul R S
inst_8 : IsFractionRing S K
x : S
this : FaithfulSMul R K
rw :
  IsStronglyTranscendental.{u_1, u_4} R (S := K) ((algebraMap S K : (a : S) → K) x : K) ↔
    Transcendental.{u_1, u_4} R (A := K) ((algebraMap S K : (a : S) → K) x : K)
rw₁ rw₂ :
  Transcendental.{u_1, u_4} R (A := K) ((algebraMap S K : (a : S) → K) x : K) ↔
    Transcendental.{u_1, u_4} R (A := K) ((algebraMap S K : (a : S) → K) x : K)
⊢ IsStronglyTranscendental R x ↔ Transcendental.{u_1, u_4} R (A := K) ((algebraMap S K : (a : S) → K) x : K)

Tactic:
rw [← IsStronglyTranscendental.iff_of_isLocalization (T := K) le_rfl,
    isStronglyTranscendental_iff_of_field]

Premises used: le_rfl, isStronglyTranscendental_iff_of_field, IsStronglyTranscendental.iff_of_isLocalization
-- 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
K : Type u_4
inst_3 : Field K
inst_4 : Algebra R K
inst_5 : Algebra S K
inst_6 : IsScalarTower R S K
inst_7 : FaithfulSMul R S
inst_8 : FaithfulSMul S K
x : S
H : Transcendental.{u_1, u_4} R (A := K) ((algebraMap S K : (a : S) → K) x : K)
⊢ FaithfulSMul R K

Tactic:
have : FaithfulSMul R K := .trans R S K
-- 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
K : Type u_4
inst_3 : Field K
inst_4 : Algebra R K
inst_5 : Algebra S K
inst_6 : IsScalarTower R S K
inst_7 : FaithfulSMul R S
inst_8 : FaithfulSMul S K
x : S
H : Transcendental.{u_1, u_4} R (A := K) ((algebraMap S K : (a : S) → K) x : K)
this : FaithfulSMul R K
⊢ IsStronglyTranscendental.{u_1, u_4} R (S := K) ((algebraMap S K : (a : S) → K) x : K)

Tactic:
rw [← isStronglyTranscendental_iff_of_field] at H

Premises used: isStronglyTranscendental_iff_of_field
-- 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
K : Type u_4
inst_3 : Field K
inst_4 : Algebra R K
inst_5 : Algebra S K
inst_6 : IsScalarTower R S K
inst_7 : FaithfulSMul R S
inst_8 : FaithfulSMul S K
x : S
H : Transcendental.{u_1, u_4} R (A := K) ((algebraMap S K : (a : S) → K) x : K)
this : FaithfulSMul R K
H₁ : IsStronglyTranscendental.{u_1, u_4} R (S := K) ((algebraMap S K : (a : S) → K) x : K)
⊢ FaithfulSMul R K

Tactic:
rw [← isStronglyTranscendental_iff_of_field] at H

Premises used: isStronglyTranscendental_iff_of_field
-- 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
K : Type u_4
inst_3 : Field K
inst_4 : Algebra R K
inst_5 : Algebra S K
inst_6 : IsScalarTower R S K
inst_7 : FaithfulSMul R S
inst_8 : FaithfulSMul S K
x : S
H : IsStronglyTranscendental.{u_1, u_4} R (S := K) ((algebraMap S K : (a : S) → K) x : K)
this : FaithfulSMul R K
⊢ IsStronglyTranscendental R x

Tactic:
.of_map (f := IsScalarTower.toAlgHom R S K) (FaithfulSMul.algebraMap_injective _ _) H

Premises used: IsStronglyTranscendental.of_map, FaithfulSMul.algebraMap_injective
-- 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
K : Type u_4
inst_3 : Field K
inst_4 : Algebra R K
inst_5 : Algebra S K
inst_6 : IsScalarTower R S K
inst_7 : FaithfulSMul R S
inst_8 : FaithfulSMul S K
x : S
H : IsStronglyTranscendental.{u_1, u_4} R (S := K) ((algebraMap S K : (a : S) → K) x : K)
this : FaithfulSMul R K
⊢ IsStronglyTranscendental R x

Tactic:
exact .of_map (f := IsScalarTower.toAlgHom R S K) (FaithfulSMul.algebraMap_injective _ _) H
-- 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
inst_3 : IsReduced S
x : S
hx : IsStronglyTranscendental R x
q : Ideal S
hq : Membership.mem (γ := Set (Ideal S)) (minimalPrimes S) q
⊢ IsStronglyTranscendental R (S := S ⧸ q) ((Ideal.Quotient.mk q : (a : S) → S ⧸ q) x : S ⧸ q)

Tactic:
Ideal.Quotient.mk_surjective.forall.mpr fun u p e ↦ ?_

Premises used: Iff.mpr, Function.Surjective.forall, Ideal.Quotient.mk_surjective, IsStronglyTranscendental
-- 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
inst_3 : IsReduced S
x : S
hx : IsStronglyTranscendental R x
q : Ideal S
hq : Membership.mem (γ := Set (Ideal S)) (minimalPrimes S) q
refine :
  ∀ (u : S) (p : R[X])
    (e :
      HMul.hMul (α := S ⧸ q) (β := S ⧸ q)
          (((aeval ((Ideal.Quotient.mk q : (a : S) → S ⧸ q) x) : AlgHom.{u_1, u_1, u_2} R R[X] (S ⧸ q)) :
                (a : R[X]) → S ⧸ q)
              p :
            S ⧸ q)
          ((Ideal.Quotient.mk q : (a : S) → S ⧸ q) u : S ⧸ q) =
        0),
    HMul.hMul (α := (S ⧸ q)[X]) (β := (S ⧸ q)[X]) (map (algebraMap R (S ⧸ q)) p)
        ((C : (a : S ⧸ q) → (S ⧸ q)[X]) ((Ideal.Quotient.mk q : (a : S) → S ⧸ q) u) : (S ⧸ q)[X]) =
      0
⊢ IsStronglyTranscendental R (S := S ⧸ q) ((Ideal.Quotient.mk q : (a : S) → S ⧸ q) x : S ⧸ q)

Tactic:
refine Ideal.Quotient.mk_surjective.forall.mpr fun u p e ↦ ?_

Premises used: Iff.mpr, Function.Surjective.forall, Ideal.Quotient.mk_surjective