awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
s : S
hRs : IsAlgebraic R s
hs : Membership.mem (γ := Submonoid S) S⁰ s
q : R[X]
hq0 : q.coeff 0 ≠ 0
hq : Eq.{u_2 + 1} (α := S) ((aeval s : (a : R[X]) → S) q : S) (0 : S)
p : R[X]
hp :
  Eq.{u_2 + 1} (α := S)
    ((aeval s : (a : R[X]) → S) (HSub.hSub (β := R[X]) q ((C : (a : R) → R[X]) (q.coeff 0) : R[X])) : S)
    ((aeval s : (a : R[X]) → S) (X * p) : S)
rwa :
  ∀
    (hp :
      HSub.hSub (α := S) (β := S) ((aeval s : (a : R[X]) → S) q : S)
          ((aeval s : (a : R[X]) → S) ((C : (a : R) → R[X]) (q.coeff 0) : R[X]) : S) =
        (aeval s : (a : R[X]) → S) (X * p)),
    HMul.hMul (β := S) s ((aeval s : (a : R[X]) → S) p : S) = (algebraMap R S : (a : R) → S) (-q.coeff 0)
rwa₁ :
  ∀
    (hp :
      HSub.hSub (α := S) (β := S) (0 : S) ((aeval s : (a : R[X]) → S) ((C : (a : R) → R[X]) (q.coeff 0) : R[X]) : S) =
        (aeval s : (a : R[X]) → S) (X * p)),
    HMul.hMul (β := S) s ((aeval s : (a : R[X]) → S) p : S) = (algebraMap R S : (a : R) → S) (-q.coeff 0)
rwa₂ :
  ∀
    (hp :
      Eq.{u_2 + 1} (α := S) (-(aeval s : (a : R[X]) → S) ((C : (a : R) → R[X]) (q.coeff 0) : R[X]) : S)
        ((aeval s : (a : R[X]) → S) (X * p) : S)),
    HMul.hMul (β := S) s ((aeval s : (a : R[X]) → S) p : S) = (algebraMap R S : (a : R) → S) (-q.coeff 0)
rwa₃ :
  ∀
    (hp :
      -(aeval s : (a : R[X]) → S) ((C : (a : R) → R[X]) (q.coeff 0) : R[X]) =
        HMul.hMul (α := S) (β := S) ((aeval s : (a : R[X]) → S) X : S) ((aeval s : (a : R[X]) → S) p : S)),
    HMul.hMul (β := S) s ((aeval s : (a : R[X]) → S) p : S) = (algebraMap R S : (a : R) → S) (-q.coeff 0)
⊢ HMul.hMul (β := S) s ((aeval s : (a : R[X]) → S) p : S) = (algebraMap R S : (a : R) → S) (-q.coeff 0)
have rwa₄ : ∀
  (hp :
    -(aeval s : (a : R[X]) → S) ((C : (a : R) → R[X]) (q.coeff 0) : R[X]) =
      HMul.hMul (β := S) s ((aeval s : (a : R[X]) → S) p : S)),
  HMul.hMul (β := S) s ((aeval s : (a : R[X]) → S) p : S) = (algebraMap R S : (a : R) → S) (-q.coeff 0)
Tactic: rwa [map_sub, hq, zero_sub, map_mul, aeval_X, aeval_C, ← map_neg, eq_comm] at hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
s : S
hRs : IsAlgebraic R s
hs : Membership.mem (γ := Submonoid S) S⁰ s
q : R[X]
hq0 : q.coeff 0 ≠ 0
hq : Eq.{u_2 + 1} (α := S) ((aeval s : (a : R[X]) → S) q : S) (0 : S)
p : R[X]
hp :
  Eq.{u_2 + 1} (α := S)
    ((aeval s : (a : R[X]) → S) (HSub.hSub (β := R[X]) q ((C : (a : R) → R[X]) (q.coeff 0) : R[X])) : S)
    ((aeval s : (a : R[X]) → S) (X * p) : S)
rwa :
  ∀
    (hp :
      HSub.hSub (α := S) (β := S) ((aeval s : (a : R[X]) → S) q : S)
          ((aeval s : (a : R[X]) → S) ((C : (a : R) → R[X]) (q.coeff 0) : R[X]) : S) =
        (aeval s : (a : R[X]) → S) (X * p)),
    HMul.hMul (β := S) s ((aeval s : (a : R[X]) → S) p : S) = (algebraMap R S : (a : R) → S) (-q.coeff 0)
rwa₁ :
  ∀
    (hp :
      HSub.hSub (α := S) (β := S) (0 : S) ((aeval s : (a : R[X]) → S) ((C : (a : R) → R[X]) (q.coeff 0) : R[X]) : S) =
        (aeval s : (a : R[X]) → S) (X * p)),
    HMul.hMul (β := S) s ((aeval s : (a : R[X]) → S) p : S) = (algebraMap R S : (a : R) → S) (-q.coeff 0)
rwa₂ :
  ∀
    (hp :
      Eq.{u_2 + 1} (α := S) (-(aeval s : (a : R[X]) → S) ((C : (a : R) → R[X]) (q.coeff 0) : R[X]) : S)
        ((aeval s : (a : R[X]) → S) (X * p) : S)),
    HMul.hMul (β := S) s ((aeval s : (a : R[X]) → S) p : S) = (algebraMap R S : (a : R) → S) (-q.coeff 0)
rwa₃ :
  ∀
    (hp :
      -(aeval s : (a : R[X]) → S) ((C : (a : R) → R[X]) (q.coeff 0) : R[X]) =
        HMul.hMul (α := S) (β := S) ((aeval s : (a : R[X]) → S) X : S) ((aeval s : (a : R[X]) → S) p : S)),
    HMul.hMul (β := S) s ((aeval s : (a : R[X]) → S) p : S) = (algebraMap R S : (a : R) → S) (-q.coeff 0)
rwa₄ :
  ∀
    (hp :
      -(aeval s : (a : R[X]) → S) ((C : (a : R) → R[X]) (q.coeff 0) : R[X]) =
        HMul.hMul (β := S) s ((aeval s : (a : R[X]) → S) p : S)),
    HMul.hMul (β := S) s ((aeval s : (a : R[X]) → S) p : S) = (algebraMap R S : (a : R) → S) (-q.coeff 0)
⊢ HMul.hMul (β := S) s ((aeval s : (a : R[X]) → S) p : S) = (algebraMap R S : (a : R) → S) (-q.coeff 0)
have rwa₅ : ∀ (hp : -(algebraMap R S : (a : R) → S) (q.coeff 0) = HMul.hMul (β := S) s ((aeval s : (a : R[X]) → S) p : S)),
  HMul.hMul (β := S) s ((aeval s : (a : R[X]) → S) p : S) = (algebraMap R S : (a : R) → S) (-q.coeff 0)
Tactic: rwa [map_sub, hq, zero_sub, map_mul, aeval_X, aeval_C, ← map_neg, eq_comm] at hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
s : S
hRs : IsAlgebraic R s
hs : Membership.mem (γ := Submonoid S) S⁰ s
q : R[X]
hq0 : q.coeff 0 ≠ 0
hq : Eq.{u_2 + 1} (α := S) ((aeval s : (a : R[X]) → S) q : S) (0 : S)
p : R[X]
hp :
  Eq.{u_2 + 1} (α := S)
    ((aeval s : (a : R[X]) → S) (HSub.hSub (β := R[X]) q ((C : (a : R) → R[X]) (q.coeff 0) : R[X])) : S)
    ((aeval s : (a : R[X]) → S) (X * p) : S)
rwa :
  ∀
    (hp :
      HSub.hSub (α := S) (β := S) ((aeval s : (a : R[X]) → S) q : S)
          ((aeval s : (a : R[X]) → S) ((C : (a : R) → R[X]) (q.coeff 0) : R[X]) : S) =
        (aeval s : (a : R[X]) → S) (X * p)),
    HMul.hMul (β := S) s ((aeval s : (a : R[X]) → S) p : S) = (algebraMap R S : (a : R) → S) (-q.coeff 0)
rwa₁ :
  ∀
    (hp :
      HSub.hSub (α := S) (β := S) (0 : S) ((aeval s : (a : R[X]) → S) ((C : (a : R) → R[X]) (q.coeff 0) : R[X]) : S) =
        (aeval s : (a : R[X]) → S) (X * p)),
    HMul.hMul (β := S) s ((aeval s : (a : R[X]) → S) p : S) = (algebraMap R S : (a : R) → S) (-q.coeff 0)
rwa₂ :
  ∀
    (hp :
      Eq.{u_2 + 1} (α := S) (-(aeval s : (a : R[X]) → S) ((C : (a : R) → R[X]) (q.coeff 0) : R[X]) : S)
        ((aeval s : (a : R[X]) → S) (X * p) : S)),
    HMul.hMul (β := S) s ((aeval s : (a : R[X]) → S) p : S) = (algebraMap R S : (a : R) → S) (-q.coeff 0)
rwa₃ :
  ∀
    (hp :
      -(aeval s : (a : R[X]) → S) ((C : (a : R) → R[X]) (q.coeff 0) : R[X]) =
        HMul.hMul (α := S) (β := S) ((aeval s : (a : R[X]) → S) X : S) ((aeval s : (a : R[X]) → S) p : S)),
    HMul.hMul (β := S) s ((aeval s : (a : R[X]) → S) p : S) = (algebraMap R S : (a : R) → S) (-q.coeff 0)
rwa₄ :
  ∀
    (hp :
      -(aeval s : (a : R[X]) → S) ((C : (a : R) → R[X]) (q.coeff 0) : R[X]) =
        HMul.hMul (β := S) s ((aeval s : (a : R[X]) → S) p : S)),
    HMul.hMul (β := S) s ((aeval s : (a : R[X]) → S) p : S) = (algebraMap R S : (a : R) → S) (-q.coeff 0)
rwa₅ :
  ∀ (hp : -(algebraMap R S : (a : R) → S) (q.coeff 0) = HMul.hMul (β := S) s ((aeval s : (a : R[X]) → S) p : S)),
    HMul.hMul (β := S) s ((aeval s : (a : R[X]) → S) p : S) = (algebraMap R S : (a : R) → S) (-q.coeff 0)
⊢ HMul.hMul (β := S) s ((aeval s : (a : R[X]) → S) p : S) = (algebraMap R S : (a : R) → S) (-q.coeff 0)
have rwa₆ : ∀ (hp : (algebraMap R S : (a : R) → S) (-q.coeff 0) = HMul.hMul (β := S) s ((aeval s : (a : R[X]) → S) p : S)),
  HMul.hMul (β := S) s ((aeval s : (a : R[X]) → S) p : S) = (algebraMap R S : (a : R) → S) (-q.coeff 0)
Tactic: rwa [map_sub, hq, zero_sub, map_mul, aeval_X, aeval_C, ← map_neg, eq_comm] at hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
s : S
hRs : IsAlgebraic R s
hs : Membership.mem (γ := Submonoid S) S⁰ s
q : R[X]
hq0 : q.coeff 0 ≠ 0
hq : Eq.{u_2 + 1} (α := S) ((aeval s : (a : R[X]) → S) q : S) (0 : S)
p : R[X]
hp :
  Eq.{u_2 + 1} (α := S)
    ((aeval s : (a : R[X]) → S) (HSub.hSub (β := R[X]) q ((C : (a : R) → R[X]) (q.coeff 0) : R[X])) : S)
    ((aeval s : (a : R[X]) → S) (X * p) : S)
rwa :
  ∀
    (hp :
      HSub.hSub (α := S) (β := S) ((aeval s : (a : R[X]) → S) q : S)
          ((aeval s : (a : R[X]) → S) ((C : (a : R) → R[X]) (q.coeff 0) : R[X]) : S) =
        (aeval s : (a : R[X]) → S) (X * p)),
    HMul.hMul (β := S) s ((aeval s : (a : R[X]) → S) p : S) = (algebraMap R S : (a : R) → S) (-q.coeff 0)
rwa₁ :
  ∀
    (hp :
      HSub.hSub (α := S) (β := S) (0 : S) ((aeval s : (a : R[X]) → S) ((C : (a : R) → R[X]) (q.coeff 0) : R[X]) : S) =
        (aeval s : (a : R[X]) → S) (X * p)),
    HMul.hMul (β := S) s ((aeval s : (a : R[X]) → S) p : S) = (algebraMap R S : (a : R) → S) (-q.coeff 0)
rwa₂ :
  ∀
    (hp :
      Eq.{u_2 + 1} (α := S) (-(aeval s : (a : R[X]) → S) ((C : (a : R) → R[X]) (q.coeff 0) : R[X]) : S)
        ((aeval s : (a : R[X]) → S) (X * p) : S)),
    HMul.hMul (β := S) s ((aeval s : (a : R[X]) → S) p : S) = (algebraMap R S : (a : R) → S) (-q.coeff 0)
rwa₃ :
  ∀
    (hp :
      -(aeval s : (a : R[X]) → S) ((C : (a : R) → R[X]) (q.coeff 0) : R[X]) =
        HMul.hMul (α := S) (β := S) ((aeval s : (a : R[X]) → S) X : S) ((aeval s : (a : R[X]) → S) p : S)),
    HMul.hMul (β := S) s ((aeval s : (a : R[X]) → S) p : S) = (algebraMap R S : (a : R) → S) (-q.coeff 0)
rwa₄ :
  ∀
    (hp :
      -(aeval s : (a : R[X]) → S) ((C : (a : R) → R[X]) (q.coeff 0) : R[X]) =
        HMul.hMul (β := S) s ((aeval s : (a : R[X]) → S) p : S)),
    HMul.hMul (β := S) s ((aeval s : (a : R[X]) → S) p : S) = (algebraMap R S : (a : R) → S) (-q.coeff 0)
rwa₅ :
  ∀ (hp : -(algebraMap R S : (a : R) → S) (q.coeff 0) = HMul.hMul (β := S) s ((aeval s : (a : R[X]) → S) p : S)),
    HMul.hMul (β := S) s ((aeval s : (a : R[X]) → S) p : S) = (algebraMap R S : (a : R) → S) (-q.coeff 0)
rwa₆ :
  ∀ (hp : (algebraMap R S : (a : R) → S) (-q.coeff 0) = HMul.hMul (β := S) s ((aeval s : (a : R[X]) → S) p : S)),
    HMul.hMul (β := S) s ((aeval s : (a : R[X]) → S) p : S) = (algebraMap R S : (a : R) → S) (-q.coeff 0)
⊢ HMul.hMul (β := S) s ((aeval s : (a : R[X]) → S) p : S) = (algebraMap R S : (a : R) → S) (-q.coeff 0)
have rwa₇ : ∀ (hp : HMul.hMul (β := S) s ((aeval s : (a : R[X]) → S) p : S) = (algebraMap R S : (a : R) → S) (-q.coeff 0)),
  HMul.hMul (β := S) s ((aeval s : (a : R[X]) → S) p : S) = (algebraMap R S : (a : R) → S) (-q.coeff 0)
Tactic: rwa [map_sub, hq, zero_sub, map_mul, aeval_X, aeval_C, ← map_neg, eq_comm] at hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
s : S
hRs : IsAlgebraic R s
hs : Membership.mem (γ := Submonoid S) S⁰ s
⊢ ∃ (r : R), r ≠ 0 ∧ s ∣ (algebraMap R S : (a : R) → S) r
have obtain : ∀ (q : R[X]) (hq0 : q.coeff 0 ≠ 0) (hq : Eq.{u_2 + 1} (α := S) ((aeval s : (a : R[X]) → S) q : S) (0 : S)),
  ∃ (r : R), r ≠ 0 ∧ s ∣ (algebraMap R S : (a : R) → S) r
Tactic: obtain ⟨q, hq0, hq⟩ := hRs.exists_nonzero_coeff_and_aeval_eq_zero hs
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
s : S
hRs : IsAlgebraic R s
hs : Membership.mem (γ := Submonoid S) S⁰ s
q : R[X]
hq0 : q.coeff 0 ≠ 0
hq : Eq.{u_2 + 1} (α := S) ((aeval s : (a : R[X]) → S) q : S) (0 : S)
⊢ ∃ (r : R), r ≠ 0 ∧ s ∣ (algebraMap R S : (a : R) → S) r
have key : Dvd.dvd.{u_2} (α := S) ((aeval s : (a : R[X]) → S) X : S)
  ((aeval s : (a : R[X]) → S) (HSub.hSub (β := R[X]) q ((C : (a : R) → R[X]) (q.coeff 0) : R[X])) : S)
Tactic: have key := map_dvd (aeval s) (X_dvd_sub_C (p := q))
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
s : S
hRs : IsAlgebraic R s
hs : Membership.mem (γ := Submonoid S) S⁰ s
q : R[X]
hq0 : q.coeff 0 ≠ 0
hq : Eq.{u_2 + 1} (α := S) ((aeval s : (a : R[X]) → S) q : S) (0 : S)
key :
  Dvd.dvd.{u_2} (α := S) ((aeval s : (a : R[X]) → S) X : S)
    ((aeval s : (a : R[X]) → S) (HSub.hSub (β := R[X]) q ((C : (a : R) → R[X]) (q.coeff 0) : R[X])) : S)
⊢ ∃ (r : R), r ≠ 0 ∧ s ∣ (algebraMap R S : (a : R) → S) r
have key₁ : s ∣ (algebraMap R S : (a : R) → S) (q.coeff 0)
Tactic: rw [map_sub, hq, zero_sub, dvd_neg, aeval_X, aeval_C] at key
Cleared hypotheses: key
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
a b : S
hRb : IsAlgebraic R b
hb : Membership.mem (γ := Submonoid S) S⁰ b
r : R
hr : r ≠ 0
s : S
h : (algebraMap R S : (a : R) → S) r = b * s
⊢ r • a = b * (s * a)
have rw : HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) r : S) a = b * (s * a)
Tactic: rw [smul_def, h, mul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
a b : S
hRb : IsAlgebraic R b
hb : Membership.mem (γ := Submonoid S) S⁰ b
r : R
hr : r ≠ 0
s : S
h : (algebraMap R S : (a : R) → S) r = b * s
rw : HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) r : S) a = b * (s * a)
⊢ r • a = b * (s * a)
have rw₁ : b * s * a = b * (s * a)
Tactic: rw [smul_def, h, mul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
a b : S
hRb : IsAlgebraic R b
hb : Membership.mem (γ := Submonoid S) S⁰ b
r : R
hr : r ≠ 0
s : S
h : (algebraMap R S : (a : R) → S) r = b * s
rw : HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) r : S) a = b * (s * a)
rw₁ : b * s * a = b * (s * a)
⊢ r • a = b * (s * a)
have rw₂ : b * (s * a) = b * (s * a)
Tactic: rw [smul_def, h, mul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
s : S
h : Transcendental R s
⊢ Function.Bijective.{u_1 + 1, u_2 + 1} (α := R[X]) (β := ↥R[s])
    (⇑(aeval (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) R[s] x) s ⋯)) : (a : R[X]) → ↥R[s])
have refine_1 : Transcendental R (A := ↥R[s]) (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) R[s] x) s sorry)
Tactic: refine ⟨transcendental_iff_injective.mp ?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
s : S
h : Transcendental R s
refine_1 :
  Transcendental R (A := ↥R[s]) (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) R[s] x) s ⋯)
⊢ Function.Bijective.{u_1 + 1, u_2 + 1} (α := R[X]) (β := ↥R[s])
    (⇑(aeval (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) R[s] x) s ⋯)) : (a : R[X]) → ↥R[s])
have refine_2 : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R[X]) (β := ↥R[s])
  (⇑(aeval (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) R[s] x) s sorry)) : (a : R[X]) → ↥R[s])
Tactic: refine ⟨transcendental_iff_injective.mp ?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
s : S
h : Transcendental R s
⊢ Transcendental R (A := ↥R[s]) (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) R[s] x) s ⋯)
have refine_1 : Transcendental R (↑(Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) R[s] x) s sorry) : S)
Tactic: rwa [Subalgebra.transcendental_iff_transcendental_val]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
s : S
h : Transcendental R s
⊢ Function.Surjective.{u_1 + 1, u_2 + 1} (α := R[X]) (β := ↥R[s])
    (⇑(aeval (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) R[s] x) s ⋯)) : (a : R[X]) → ↥R[s])
have refine_2 : LE.le (α := Subalgebra R ↥R[s]) ⊤
  (AlgHom.range (aeval (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) R[s] x) s sorry)))
Tactic: rw [← AlgHom.range_eq_top, _root_.eq_top_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
s : S
h : Transcendental R s
t : S
ht : Membership.mem (γ := Subalgebra R S) R[s] t
h_1 :
  Membership.mem (γ := Subalgebra R ↥R[s]) ⊤
    (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) R[s] x) t ht)
⊢ Membership.mem (γ := Subalgebra R ↥R[s])
    (AlgHom.range (aeval (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) R[s] x) s ⋯)))
    (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) R[s] x) t ht)
have refine_2 : ∀ (r : R[X]) (ht : Membership.mem (α := S) (γ := Subalgebra R S) R[s] ((aeval s : (a : R[X]) → S) r : S)),
  Membership.mem.{u_2, u_2} (α := ↥R[s]) (γ := Subalgebra R ↥R[s]) ⊤
      (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) R[s] x) ((aeval s : (a : R[X]) → S) r) ht :
        ↥R[s]) →
    Membership.mem (α := ↥R[s]) (γ := Subalgebra R ↥R[s])
      (AlgHom.range (aeval (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) R[s] x) s sorry)))
      (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) R[s] x) ((aeval s : (a : R[X]) → S) r) ht :
        ↥R[s])
Tactic: obtain ⟨r, rfl⟩ := adjoin_mem_exists_aeval _ _ ht
Cleared hypotheses: t, ht, h_1
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
s : S
h : Transcendental R s
r : R[X]
ht : Membership.mem (α := S) (γ := Subalgebra R S) R[s] ((aeval s : (a : R[X]) → S) r : S)
h_1 :
  Membership.mem.{u_2, u_2} (α := ↥R[s]) (γ := Subalgebra R ↥R[s]) ⊤
    (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) R[s] x) ((aeval s : (a : R[X]) → S) r) ht :
      ↥R[s])
⊢ Eq.{u_2 + 1} (α := ↥R[s])
    ((AlgHom.toRingHom (aeval (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) R[s] x) s ⋯)) :
          (a : R[X]) → ↥R[s])
        r :
      ↥R[s])
    (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) R[s] x) ((aeval s : (a : R[X]) → S) r) ht :
      ↥R[s])
have a : Eq.{u_2 + 1} (α := S)
  ((↑((AlgHom.toRingHom (aeval (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) R[s] x) s sorry)) :
            (a : R[X]) → ↥R[s])
          r) :
      S) :
    S)
  ((↑(Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) R[s] x) ((aeval s : (a : R[X]) → S) r) ht) :
      S) :
    S)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
s : S
h : Transcendental R s
f : R[X]
⊢ ((algEquivOfTranscendental R s h).symm : (a : ↥R[s]) → R[X])
      ((aeval (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) R[s] x) s ⋯) : (a : R[X]) → ↥R[s])
        f) =
    f
have a : Eq.{u_2 + 1} (α := ↥R[s])
  (((algEquivOfTranscendental R s h).toEquiv : (a : R[X]) → ↥R[s])
      (((algEquivOfTranscendental R s h).symm : (a : ↥R[s]) → R[X])
        ((aeval (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) R[s] x) s sorry) : (a : R[X]) → ↥R[s])
          f)) :
    ↥R[s])
  (((algEquivOfTranscendental R s h).toEquiv : (a : R[X]) → ↥R[s]) f : ↥R[s])
Tactic: apply (algEquivOfTranscendental R s h).toEquiv.injective
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
s : S
h : Transcendental R s
⊢ Eq.{u_1 + 1} (α := R[X])
    (((algEquivOfTranscendental R s h).symm : (a : ↥R[s]) → R[X])
        (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) R[s] x) s ⋯) :
      R[X])
    (X : R[X])
have a : Eq.{u_2 + 1} (α := ↥R[s])
  (((algEquivOfTranscendental R s h).toEquiv : (a : R[X]) → ↥R[s])
      (((algEquivOfTranscendental R s h).symm : (a : ↥R[s]) → R[X])
        (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) R[s] x) s sorry)) :
    ↥R[s])
  (((algEquivOfTranscendental R s h).toEquiv : (a : R[X]) → ↥R[s]) X : ↥R[s])
Tactic: apply (algEquivOfTranscendental R s h).toEquiv.injective
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
A : Type u_3
inst_1 : CommRing S
inst_2 : NoZeroDivisors S
inst_3 : Algebra R S
alg : Algebra.IsAlgebraic R S
inst_4 : Ring A
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : IsScalarTower R S A
inj : Injective.{u_1 + 1, u_3 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
⊢ Injective.{u_2 + 1, u_3 + 1} (α := S) (β := A) (⇑(algebraMap S A) : (a : S) → A)
have refine : ∀ (s : S) (eq : Eq.{u_3 + 1} (α := A) ((algebraMap S A : (a : S) → A) s : A) (0 : A)) (ne : ¬s = 0), False
Tactic: refine (injective_iff_map_eq_zero _).mpr fun s eq ↦ of_not_not fun ne ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
A : Type u_3
inst_1 : CommRing S
inst_2 : NoZeroDivisors S
inst_3 : Algebra R S
alg : Algebra.IsAlgebraic R S
inst_4 : Ring A
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : IsScalarTower R S A
inj : Injective.{u_1 + 1, u_3 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
s : S
eq : Eq.{u_3 + 1} (α := A) ((algebraMap S A : (a : S) → A) s : A) (0 : A)
ne : ¬s = 0
⊢ False
have have : ∀ (r : R) (ne : r ≠ 0) (dvd : s ∣ (algebraMap R S : (a : R) → S) r), False
Tactic: have ⟨r, ne, dvd⟩ := (alg.1 s).exists_nonzero_dvd (mem_nonZeroDivisors_of_ne_zero ne)
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
A : Type u_3
inst_1 : CommRing S
inst_2 : NoZeroDivisors S
inst_3 : Algebra R S
alg : Algebra.IsAlgebraic R S
inst_4 : Ring A
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : IsScalarTower R S A
inj : Injective.{u_1 + 1, u_3 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
s : S
eq : Eq.{u_3 + 1} (α := A) ((algebraMap S A : (a : S) → A) s : A) (0 : A)
ne_1 : ¬s = 0
r : R
ne : r ≠ 0
dvd : s ∣ (algebraMap R S : (a : R) → S) r
⊢ False
have refine : Dvd.dvd.{u_3} (α := A) (0 : A) ((algebraMap R A : (a : R) → A) r : A)
Tactic: refine ne (inj <| map_zero (algebraMap R A) ▸ zero_dvd_iff.mp ?_)
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
A : Type u_3
inst_1 : CommRing S
inst_2 : NoZeroDivisors S
inst_3 : Algebra R S
alg : Algebra.IsAlgebraic R S
inst_4 : Ring A
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : IsScalarTower R S A
inj : Injective.{u_1 + 1, u_3 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
s : S
eq : Eq.{u_3 + 1} (α := A) ((algebraMap S A : (a : S) → A) s : A) (0 : A)
ne_1 : ¬s = 0
r : R
ne : r ≠ 0
dvd : s ∣ (algebraMap R S : (a : R) → S) r
⊢ Dvd.dvd.{u_3} (α := A) (0 : A) ((algebraMap R A : (a : R) → A) r : A)
have simp_rw : Dvd.dvd.{u_3} (α := A) ((algebraMap S A : (a : S) → A) s : A) ((algebraMap R A : (a : R) → A) r : A)
Tactic: simp_rw [← eq, IsScalarTower.algebraMap_apply R S A, map_dvd (algebraMap S A) dvd]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
A : Type u_3
inst_1 : CommRing S
inst_2 : NoZeroDivisors S
inst_3 : Algebra R S
alg : Algebra.IsAlgebraic R S
inst_4 : Ring A
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : IsScalarTower R S A
inj : Injective.{u_1 + 1, u_3 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
s : S
eq : Eq.{u_3 + 1} (α := A) ((algebraMap S A : (a : S) → A) s : A) (0 : A)
ne_1 : ¬s = 0
r : R
ne : r ≠ 0
dvd : s ∣ (algebraMap R S : (a : R) → S) r
simp_rw : Dvd.dvd.{u_3} (α := A) ((algebraMap S A : (a : S) → A) s : A) ((algebraMap R A : (a : R) → A) r : A)
⊢ Dvd.dvd.{u_3} (α := A) (0 : A) ((algebraMap R A : (a : R) → A) r : A)
have simp_rw₁ : Dvd.dvd.{u_3} (α := A) ((algebraMap S A : (a : S) → A) s : A)
  ((algebraMap S A : (a : S) → A) ((algebraMap R S : (a : R) → S) r : S) : A)
Tactic: simp_rw [← eq, IsScalarTower.algebraMap_apply R S A, map_dvd (algebraMap S A) dvd]