awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.StronglyTranscendental (goal)
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
have refine : ∀ (h : Transcendental R x), IsStronglyTranscendental R x
Tactic: refine ⟨fun h ↦ h.transcendental, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.StronglyTranscendental (goal)
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
have 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
Tactic: refine fun u p hp ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.StronglyTranscendental (goal)
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) (β := T) (((aeval ((f : (a : S) → T) x) : R[X] →ₐ[R] T) : (a : R[X]) → T) p : T)
      ((f : (a : S) → T) u : T) =
    0
have 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
Tactic: rw [aeval_algHom_apply, ← map_mul, hp, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.StronglyTranscendental (goal)
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
⊢ 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
have 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)
Tactic: rw [aeval_algHom_apply, ← map_mul, hp, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.StronglyTranscendental (goal)
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)
⊢ 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
have rw₂ : Eq.{u_3 + 1} (α := T) ((f : (a : S) → T) 0 : T) (0 : T)
Tactic: rw [aeval_algHom_apply, ← map_mul, hp, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.StronglyTranscendental (goal)
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)
⊢ 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
have rw₃ : Eq.{u_3 + 1} (α := T) 0 0
Tactic: rw [aeval_algHom_apply, ← map_mul, hp, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.StronglyTranscendental (hypothesis)
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 (α := S[X]) (β := S[X]) (map (algebraMap R S) p) ((C : (a : S) → S[X]) u : S[X]) = 0
have 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
Tactic: have := h (f u) p (by rw [aeval_algHom_apply, ← map_mul, hp, map_zero])
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.StronglyTranscendental (goal)
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
⊢ HMul.hMul (α := S[X]) (β := S[X]) (map (algebraMap R S) p) ((C : (a : S) → S[X]) u : S[X]) = 0
have 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])
Tactic: rwa [← f.comp_algebraMap, ← map_map, ← f.coe_toRingHom, ← map_C, ← Polynomial.map_mul,
    ← coe_mapRingHom, map_eq_zero_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.StronglyTranscendental (goal)
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)
have 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
Tactic: refine fun u p hp ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.StronglyTranscendental (goal)
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
⊢ HMul.hMul (α := T[X]) (β := T[X]) (map (algebraMap R T) p) ((C : (a : T) → T[X]) u : T[X]) = 0
have 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
Tactic: obtain ⟨u, s, rfl⟩ := IsLocalization.exists_mk'_eq M u
Cleared hypotheses: u, hp
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.StronglyTranscendental (goal)
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
⊢ HMul.hMul (α := T[X]) (β := T[X]) (map (algebraMap R T) p) ((C : (a : T) → T[X]) (IsLocalization.mk' T u s) : T[X]) =
    0
have 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
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
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.StronglyTranscendental (hypothesis)
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]) (IsLocalization.mk' T u s) : T[X]) =
    0
have 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
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)))
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.StronglyTranscendental (goal)
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
have 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])
Tactic: refine ((IsLocalization.map_units T (⟨a, haM⟩ * s)).map C).mul_right_cancel ?_
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.StronglyTranscendental (goal)
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
⊢ HMul.hMul (α := T[X]) (β := T[X]) (map (algebraMap S T) p) ((C : (a : T) → T[X]) t : T[X]) = 0
have 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
Tactic: obtain ⟨a, ha₁, ha₂⟩ := IsLocalization.integerNormalization_spec M p
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.StronglyTranscendental (hypothesis)
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
⊢ HMul.hMul (α := T[X]) (β := T[X]) (map (algebraMap S T) p) ((C : (a : T) → T[X]) t : T[X]) = 0
have H : (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₂)
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.StronglyTranscendental (hypothesis)
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 S T) p) ((C : (a : T) → T[X]) t : T[X]) = 0
have this : 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])
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.StronglyTranscendental (hypothesis)
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) p) ((C : (a : T) → T[X]) t : T[X]) = 0
have this₁ : 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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.StronglyTranscendental (goal)
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]) (β := T[X]) (map (algebraMap S T) p) ((C : (a : T) → T[X]) t : T[X]) = 0
have 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])
Tactic: rw [← (((IsLocalization.map_units S ⟨a, ha₁⟩).map (algebraMap S T)).map C).mul_right_inj]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.StronglyTranscendental (goal)
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
⊢ HMul.hMul (α := T[X]) (β := T[X]) (map (algebraMap S T) p) ((C : (a : T) → T[X]) t : T[X]) = 0
have 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
Tactic: obtain ⟨p, rfl⟩ := map_surjective _ H p
Cleared hypotheses: p, hp
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.StronglyTranscendental (hypothesis)
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
⊢ IsStronglyTranscendental R x ↔ Transcendental.{u_1, u_4} R (A := K) ((algebraMap S K : (a : S) → K) x : K)
have this : FaithfulSMul R K
Tactic: have : FaithfulSMul R K := .trans R S K
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.StronglyTranscendental (goal)
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
⊢ IsStronglyTranscendental R x ↔ Transcendental.{u_1, u_4} R (A := K) ((algebraMap S K : (a : S) → K) x : K)
have 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)
Tactic: rw [← IsStronglyTranscendental.iff_of_isLocalization (T := K) le_rfl,
    isStronglyTranscendental_iff_of_field]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.StronglyTranscendental (goal)
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)
⊢ IsStronglyTranscendental R x ↔ Transcendental.{u_1, u_4} R (A := K) ((algebraMap S K : (a : S) → K) x : K)
have 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)
Tactic: rw [← IsStronglyTranscendental.iff_of_isLocalization (T := K) le_rfl,
    isStronglyTranscendental_iff_of_field]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.StronglyTranscendental (hypothesis)
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)
⊢ IsStronglyTranscendental R x
have this : FaithfulSMul R K
Tactic: have : FaithfulSMul R K := .trans R S K
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.StronglyTranscendental (hypothesis)
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 R x
have H₁ : IsStronglyTranscendental.{u_1, u_4} R (S := K) ((algebraMap S K : (a : S) → K) x : K)
Tactic: rw [← isStronglyTranscendental_iff_of_field] at H
Cleared hypotheses: H, this
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.StronglyTranscendental (goal)
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)
have 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
Tactic: refine Ideal.Quotient.mk_surjective.forall.mpr fun u p e ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.StronglyTranscendental (hypothesis)
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
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
have e₁ : HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) p : S) u ∈ q
Tactic: rw [← Ideal.Quotient.algebraMap_eq, aeval_algebraMap_apply, Ideal.Quotient.algebraMap_eq,
    ← map_mul, Ideal.Quotient.eq_zero_iff_mem] at e
Cleared hypotheses: e