awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
Goal:
R : Type u
S : Type u_1
A : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R A
B : Type u_2
inst_4 : Ring B
inst_5 : Algebra S B
FRS : Type u_3
FAB : Type u_4
inst_6 : EquivLike FRS R S
inst_7 : RingEquivClass FRS R S
inst_8 : EquivLike FAB A B
inst_9 : RingEquivClass FAB A B
f : FRS
g : FAB
h :
  Eq (α := R →+* B) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S B) (↑f : R →+* S))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑g : A →+* B) (algebraMap R A))
⊢ Algebra.Transcendental S B ↔ Algebra.Transcendental R A
have simp_rw : ¬Algebra.IsAlgebraic S B ↔ ¬Algebra.IsAlgebraic R A
Tactic: simp_rw [Algebra.transcendental_iff_not_isAlgebraic,
    Algebra.isAlgebraic_ringHom_iff_of_comp_eq f g h]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
Goal:
R : Type u
S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.IsAlgebraic (↥⊥) S
⊢ Eq (α := R →+* S)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap (↥⊥) S) (↑(algebraMap R ↥⊥) : R →+* ↥⊥))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑(RingHom.id S) : S →+* S) (algebraMap R S))
have a : ∀ (x : R),
  Eq.{u_1 + 1} (α := S)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap (↥⊥) S) (↑(algebraMap R ↥⊥) : R →+* ↥⊥) :
          (a : R) → S)
        x :
      S)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑(RingHom.id S) : S →+* S) (algebraMap R S) : (a : R) → S)
        x :
      S)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
Goal:
R : Type u
S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
h : Function.Injective.{u + 1, u_1 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
⊢ Algebra.IsAlgebraic (↥⊥) S ↔ Algebra.IsAlgebraic R S
have simp_rw : (∀ (x : S), IsAlgebraic (↥⊥) x) ↔ ∀ (x : S), IsAlgebraic R x
Tactic: simp_rw [Algebra.isAlgebraic_def, isAlgebraic_bot_iff h]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
r : A
n : ℕ
hn : 0 < n
ht : IsAlgebraic R (r ^ n)
p : R[X]
p_nonzero : p ≠ 0
hp : Eq.{v + 1} (α := A) ((aeval (r ^ n) : (a : R[X]) → A) p : A) (0 : A)
rwa : p ≠ 0
⊢ Ne (α := R[X]) ((expand R n : (a : R[X]) → R[X]) p : R[X]) (0 : R[X])
have rwa₁ : (p : R[X]) → (p_nonzero : p ≠ 0) → (hp : Eq.{v + 1} (α := A) ((aeval (r ^ n) : (a : R[X]) → A) p : A) (0 : A)) → R[X]
Tactic: rwa [expand_ne_zero hn]
Cleared hypotheses: p, p_nonzero, hp
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
Goal:
R : Type u
S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
inst_3 : Invertible x
h : IsAlgebraic R x
⊢ IsAlgebraic R (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _)
have obtain : ∀ (p : R[X]) (hp : p ≠ 0) (hp' : Eq.{u_1 + 1} (α := S) ((aeval x : (a : R[X]) → S) p : S) (0 : S)),
  IsAlgebraic R (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _)
Tactic: obtain ⟨p, hp, hp'⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
Goal:
R : Type u
S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
inst_3 : Invertible x
p : R[X]
hp : p ≠ 0
hp' : Eq.{u_1 + 1} (α := S) ((aeval x : (a : R[X]) → S) p : S) (0 : S)
⊢ IsAlgebraic R (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _)
have refine : Eq.{u_1 + 1} (α := S)
  ((aeval (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _) : (a : R[X]) → S) p.reverse : S) (0 : S)
Tactic: refine ⟨p.reverse, by simpa using hp, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
Goal:
R : Type u
S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
inst_3 : Invertible x
p : R[X]
hp : p ≠ 0
hp' : Eq.{u_1 + 1} (α := S) ((aeval x : (a : R[X]) → S) p : S) (0 : S)
⊢ Eq.{u_1 + 1} (α := S)
    ((aeval (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _) : (a : R[X]) → S) p.reverse : S) (0 : S)
have rwa : eval₂ (algebraMap R S) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _) p.reverse = 0
Tactic: rwa [Polynomial.aeval_def, Polynomial.eval₂_reverse_eq_zero_iff, ← Polynomial.aeval_def]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
Goal:
R : Type u
S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
inst_3 : Invertible x
p : R[X]
hp : p ≠ 0
hp' : Eq.{u_1 + 1} (α := S) ((aeval x : (a : R[X]) → S) p : S) (0 : S)
rwa : eval₂ (algebraMap R S) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _) p.reverse = 0
⊢ Eq.{u_1 + 1} (α := S)
    ((aeval (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _) : (a : R[X]) → S) p.reverse : S) (0 : S)
have rwa₁ : eval₂ (algebraMap R S) x p = 0
Tactic: rwa [Polynomial.aeval_def, Polynomial.eval₂_reverse_eq_zero_iff, ← Polynomial.aeval_def]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
Goal:
R : Type u
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
x : K
⊢ IsAlgebraic R x⁻¹ ↔ IsAlgebraic R x
have pos : ∀ (hx : x = 0), IsAlgebraic R x⁻¹ ↔ IsAlgebraic R x
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
Goal:
R : Type u
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
x : K
pos : ∀ (hx : x = 0), IsAlgebraic R x⁻¹ ↔ IsAlgebraic R x
⊢ IsAlgebraic R x⁻¹ ↔ IsAlgebraic R x
have neg : ∀ (hx : ¬x = 0), IsAlgebraic R x⁻¹ ↔ IsAlgebraic R x
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
Goal:
R : Type u_3
S : Type u_4
A : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra S A
inst_5 : Algebra R A
inst_6 : IsScalarTower R S A
hinj : Function.Injective.{u_3 + 1, u_4 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
x : A
A_alg : IsAlgebraic R x
p : R[X]
hp₁ : p ≠ 0
hp₂ : Eq.{u_5 + 1} (α := A) ((aeval x : (a : R[X]) → A) p : A) (0 : A)
⊢ Ne (α := S[X]) (map (algebraMap R S) p) 0
have rwa : ¬Eq (α := S[X]) (map (algebraMap R S) p) 0
Tactic: rwa [Ne, ← degree_eq_bot, degree_map_eq_of_injective hinj, degree_eq_bot]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
Goal:
R : Type u_3
S : Type u_4
A : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra S A
inst_5 : Algebra R A
inst_6 : IsScalarTower R S A
hinj : Function.Injective.{u_3 + 1, u_4 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
x : A
A_alg : IsAlgebraic R x
p : R[X]
hp₁ : p ≠ 0
hp₂ : Eq.{u_5 + 1} (α := A) ((aeval x : (a : R[X]) → A) p : A) (0 : A)
rwa : ¬Eq (α := S[X]) (map (algebraMap R S) p) 0
⊢ Ne (α := S[X]) (map (algebraMap R S) p) 0
have rwa₁ : ¬degree (map (algebraMap R S) p) = ⊥
Tactic: rwa [Ne, ← degree_eq_bot, degree_map_eq_of_injective hinj, degree_eq_bot]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
Goal:
R : Type u_3
S : Type u_4
A : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra S A
inst_5 : Algebra R A
inst_6 : IsScalarTower R S A
hinj : Function.Injective.{u_3 + 1, u_4 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
x : A
A_alg : IsAlgebraic R x
p : R[X]
hp₁ : p ≠ 0
hp₂ : Eq.{u_5 + 1} (α := A) ((aeval x : (a : R[X]) → A) p : A) (0 : A)
rwa : ¬Eq (α := S[X]) (map (algebraMap R S) p) 0
rwa₁ : ¬degree (map (algebraMap R S) p) = ⊥
⊢ Ne (α := S[X]) (map (algebraMap R S) p) 0
have rwa₂ : ¬p.degree = ⊥
Tactic: rwa [Ne, ← degree_eq_bot, degree_map_eq_of_injective hinj, degree_eq_bot]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
Goal:
R : Type u_3
S : Type u_4
A : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra S A
inst_5 : Algebra R A
inst_6 : IsScalarTower R S A
hinj : Function.Injective.{u_3 + 1, u_4 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
x : A
A_alg : IsAlgebraic R x
p : R[X]
hp₁ : p ≠ 0
hp₂ : Eq.{u_5 + 1} (α := A) ((aeval x : (a : R[X]) → A) p : A) (0 : A)
rwa : ¬Eq (α := S[X]) (map (algebraMap R S) p) 0
rwa₁ : ¬degree (map (algebraMap R S) p) = ⊥
rwa₂ : ¬p.degree = ⊥
⊢ Ne (α := S[X]) (map (algebraMap R S) p) 0
have rwa₃ : ¬p = 0
Tactic: rwa [Ne, ← degree_eq_bot, degree_map_eq_of_injective hinj, degree_eq_bot]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (hypothesis)
Goal:
R : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A B : Subalgebra R S
hle : A ≤ B
x : S
h : IsAlgebraic (↥A) x
this : Algebra ↥A ↥B := (Subalgebra.inclusion hle).toAlgebra
⊢ IsAlgebraic (↥B) x
have this₁ : IsScalarTower (↥A) (↥B) S
Tactic: haveI : IsScalarTower A B S := .of_algebraMap_eq fun _ ↦ rfl
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
Goal:
K : Type u_1
L : Type u_2
inst : CommRing K
inst_1 : IsDomain K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : IsTorsionFree K L
inst_5 : Algebra.IsAlgebraic K L
f : L →ₐ[K] L
⊢ Function.Bijective (α := L) (β := L) (⇑f : (a : L) → L)
have refine : ∀ (b : L), ∃ (a : L), (f : (a : L) → L) a = b
Tactic: refine ⟨f.injective, fun b ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
Goal:
K : Type u_1
L : Type u_2
inst : CommRing K
inst_1 : IsDomain K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : IsTorsionFree K L
inst_5 : Algebra.IsAlgebraic K L
f : L →ₐ[K] L
b : L
⊢ ∃ (a : L), (f : (a : L) → L) a = b
have obtain : ∀ (p : K[X]) (hp : p ≠ 0) (he : Eq.{u_2 + 1} (α := L) ((aeval b : (a : K[X]) → L) p : L) (0 : L)),
  ∃ (a : L), (f : (a : L) → L) a = b
Tactic: obtain ⟨p, hp, he⟩ := Algebra.IsAlgebraic.isAlgebraic (R := K) b
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (hypothesis)
Goal:
K : Type u_1
L : Type u_2
inst : CommRing K
inst_1 : IsDomain K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : IsTorsionFree K L
inst_5 : Algebra.IsAlgebraic K L
f : L →ₐ[K] L
b : L
p : K[X]
hp : p ≠ 0
he : Eq.{u_2 + 1} (α := L) ((aeval b : (a : K[X]) → L) p : L) (0 : L)
f' : (↑(p.rootSet L) : Type u_2) → (↑(p.rootSet L) : Type u_2) :=
  Set.MapsTo.restrict (⇑f : (a : L) → L) (p.rootSet L) (p.rootSet L) ⋯
⊢ ∃ (a : L), (f : (a : L) → L) a = b
have this : Function.Surjective f'
Tactic: have : f'.Surjective := Finite.injective_iff_surjective.1
    fun _ _ h ↦ Subtype.ext <| f.injective <| Subtype.ext_iff.1 h
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
Goal:
K : Type u_1
L : Type u_2
inst : CommRing K
inst_1 : IsDomain K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : IsTorsionFree K L
inst_5 : Algebra.IsAlgebraic K L
f : L →ₐ[K] L
b : L
p : K[X]
hp : p ≠ 0
he : Eq.{u_2 + 1} (α := L) ((aeval b : (a : K[X]) → L) p : L) (0 : L)
f' : (↑(p.rootSet L) : Type u_2) → (↑(p.rootSet L) : Type u_2) :=
  Set.MapsTo.restrict (⇑f : (a : L) → L) (p.rootSet L) (p.rootSet L) ⋯
this : Function.Surjective f'
⊢ ∃ (a : L), (f : (a : L) → L) a = b
have obtain : ∀ (a : (↑(p.rootSet L) : Type u_2)) (ha : f' a = Subtype.mk (p := fun (x : L) ↦ x ∈ p.rootSet L) b sorry),
  ∃ (a : L), (f : (a : L) → L) a = b
Tactic: obtain ⟨a, ha⟩ := this ⟨b, mem_rootSet.2 ⟨hp, he⟩⟩
-- 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]), q.coeff 0 ≠ 0 ∧ Eq.{u_2 + 1} (α := S) ((aeval s : (a : R[X]) → S) q : S) (0 : S)
have obtain : ∀ (p : R[X]) (hp0 : p ≠ 0) (hp : Eq.{u_2 + 1} (α := S) ((aeval s : (a : R[X]) → S) p : S) (0 : S)),
  ∃ (q : R[X]), q.coeff 0 ≠ 0 ∧ Eq.{u_2 + 1} (α := S) ((aeval s : (a : R[X]) → S) q : S) (0 : S)
Tactic: obtain ⟨p, hp0, hp⟩ := hRs
Cleared hypotheses: hRs
-- 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
hs : Membership.mem (γ := Submonoid S) S⁰ s
p : R[X]
hp0 : p ≠ 0
hp : Eq.{u_2 + 1} (α := S) ((aeval s : (a : R[X]) → S) p : S) (0 : S)
⊢ ∃ (q : R[X]), q.coeff 0 ≠ 0 ∧ Eq.{u_2 + 1} (α := S) ((aeval s : (a : R[X]) → S) q : S) (0 : S)
have obtain : ∀ (q : R[X]) (hpq : p = HSub.hSub (α := R[X]) X ((C : (a : R) → R[X]) 0) ^ rootMultiplicity 0 p * q)
  (hq : ¬HSub.hSub (α := R[X]) X ((C : (a : R) → R[X]) 0) ∣ q),
  ∃ (q : R[X]), q.coeff 0 ≠ 0 ∧ Eq.{u_2 + 1} (α := S) ((aeval s : (a : R[X]) → S) q : S) (0 : S)
Tactic: obtain ⟨q, hpq, hq⟩ := exists_eq_pow_rootMultiplicity_mul_and_not_dvd p hp0 0
-- 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
hs : Membership.mem (γ := Submonoid S) S⁰ s
p : R[X]
hp0 : p ≠ 0
hp : Eq.{u_2 + 1} (α := S) ((aeval s : (a : R[X]) → S) p : S) (0 : S)
q : R[X]
hpq : p = HSub.hSub (α := R[X]) X ((C : (a : R) → R[X]) 0) ^ rootMultiplicity 0 p * q
hq : ¬HSub.hSub (α := R[X]) X ((C : (a : R) → R[X]) 0) ∣ q
⊢ ∃ (q : R[X]), q.coeff 0 ≠ 0 ∧ Eq.{u_2 + 1} (α := S) ((aeval s : (a : R[X]) → S) q : S) (0 : S)
have hpq₁ : p = q * HPow.hPow (α := R[X]) X (rootMultiplicity 0 p)
Tactic: simp only [C_0, sub_zero, X_pow_mul, X_dvd_iff] at hpq hq
Cleared hypotheses: hpq, hq
-- 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
hs : Membership.mem (γ := Submonoid S) S⁰ s
p : R[X]
hp0 : p ≠ 0
hp : Eq.{u_2 + 1} (α := S) ((aeval s : (a : R[X]) → S) p : S) (0 : S)
q : R[X]
hpq : p = HSub.hSub (α := R[X]) X ((C : (a : R) → R[X]) 0) ^ rootMultiplicity 0 p * q
hq : ¬HSub.hSub (α := R[X]) X ((C : (a : R) → R[X]) 0) ∣ q
hpq₁ : p = q * HPow.hPow (α := R[X]) X (rootMultiplicity 0 p)
⊢ ∃ (q : R[X]), q.coeff 0 ≠ 0 ∧ Eq.{u_2 + 1} (α := S) ((aeval s : (a : R[X]) → S) q : S) (0 : S)
have hq₁ : ¬q.coeff 0 = 0
Tactic: simp only [C_0, sub_zero, X_pow_mul, X_dvd_iff] at hpq hq
Cleared hypotheses: hpq, hq
-- 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
hs : Membership.mem (γ := Submonoid S) S⁰ s
p : R[X]
hp0 : p ≠ 0
hp : Eq.{u_2 + 1} (α := S) ((aeval s : (a : R[X]) → S) p : S) (0 : S)
q : R[X]
hpq : p = q * HPow.hPow (α := R[X]) X (rootMultiplicity 0 p)
hq : ¬q.coeff 0 = 0
⊢ ∃ (q : R[X]), q.coeff 0 ≠ 0 ∧ Eq.{u_2 + 1} (α := S) ((aeval s : (a : R[X]) → S) q : S) (0 : S)
have hp₁ : HMul.hMul (α := S) ((aeval s : (a : R[X]) → S) q : S) (s ^ rootMultiplicity 0 p) = 0
Tactic: rw [hpq, map_mul, aeval_X_pow] at hp
Cleared hypotheses: hp, hpq, hq
-- 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
⊢ ∃ (t : S), Membership.mem (γ := Subalgebra R S) R[s] t ∧ ∃ (r : R), r ≠ 0 ∧ s * t = (algebraMap R S : (a : R) → S) r
have have : ∀ (q : R[X]) (hq0 : q.coeff 0 ≠ 0) (hq : Eq.{u_2 + 1} (α := S) ((aeval s : (a : R[X]) → S) q : S) (0 : S)),
  ∃ (t : S), Membership.mem (γ := Subalgebra R S) R[s] t ∧ ∃ (r : R), r ≠ 0 ∧ s * t = (algebraMap R S : (a : R) → S) r
Tactic: have ⟨q, hq0, hq⟩ := hRs.exists_nonzero_coeff_and_aeval_eq_zero hs
-- 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)
⊢ ∃ (t : S), Membership.mem (γ := Subalgebra R S) R[s] t ∧ ∃ (r : R), r ≠ 0 ∧ s * t = (algebraMap R S : (a : R) → S) r
have have : ∀ (p : R[X]) (hp : HSub.hSub (β := R[X]) q ((C : (a : R) → R[X]) (q.coeff 0) : R[X]) = X * p),
  ∃ (t : S), Membership.mem (γ := Subalgebra R S) R[s] t ∧ ∃ (r : R), r ≠ 0 ∧ s * t = (algebraMap R S : (a : R) → S) r
Tactic: have ⟨p, hp⟩ := X_dvd_sub_C (p := q)
-- 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 : HSub.hSub (β := R[X]) q ((C : (a : R) → R[X]) (q.coeff 0) : R[X]) = X * p
⊢ ∃ (t : S), Membership.mem (γ := Subalgebra R S) R[s] t ∧ ∃ (r : R), r ≠ 0 ∧ s * t = (algebraMap R S : (a : R) → S) r
have refine : HMul.hMul (β := S) s ((aeval s : (a : R[X]) → S) p : S) = (algebraMap R S : (a : R) → S) (-q.coeff 0)
Tactic: refine ⟨aeval s p, aeval_mem_adjoin_singleton _ _, _, neg_ne_zero.mpr hq0, ?_⟩
-- 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)
p : R[X]
hp : HSub.hSub (β := R[X]) q ((C : (a : R) → R[X]) (q.coeff 0) : R[X]) = X * p
⊢ HMul.hMul (β := S) s ((aeval s : (a : R[X]) → S) p : S) = (algebraMap R S : (a : R) → S) (-q.coeff 0)
have 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)
Tactic: apply_fun aeval s 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)
⊢ HMul.hMul (β := S) s ((aeval s : (a : R[X]) → S) p : S) = (algebraMap R S : (a : R) → S) (-q.coeff 0)
have 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)
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)
⊢ HMul.hMul (β := S) s ((aeval s : (a : R[X]) → S) p : S) = (algebraMap R S : (a : R) → S) (-q.coeff 0)
have 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)
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)
⊢ HMul.hMul (β := S) s ((aeval s : (a : R[X]) → S) p : S) = (algebraMap R S : (a : R) → S) (-q.coeff 0)
have 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)
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)
⊢ 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) 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)
Tactic: rwa [map_sub, hq, zero_sub, map_mul, aeval_X, aeval_C, ← map_neg, eq_comm] at hp
Cleared hypotheses: hp