awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Field (goal)
Goal:
F : Type u_2
K : Type u_3
L : Type u_4
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
s : Finset K
refine_1 :
  (∀ (x : K), Membership.mem (γ := Finset K) ∅ x → IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))) →
    Nonempty (AlgHom.{u_2, u_3, u_4} F (↥(Algebra.adjoin F (↑∅ : Set K))) L)
⊢ (∀ x ∈ s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))) →
    Nonempty (AlgHom.{u_2, u_3, u_4} F (↥(Algebra.adjoin F (↑s : Set K))) L)
have refine_2 : ∀ (a : K) (s : Finset K),
  a ∉ s →
    ∀
      (ih :
        (∀ x ∈ s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))) →
          Nonempty (AlgHom.{u_2, u_3, u_4} F (↥(Algebra.adjoin F (↑s : Set K))) L))
      (H : ∀ x ∈ insert a s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))),
      Nonempty (AlgHom.{u_2, u_3, u_4} F (↥(Algebra.adjoin F (↑(insert a s) : Set K))) L)
Tactic: classical
    refine Finset.induction_on s (fun _ ↦ ?_) fun a s _ ih H ↦ ?_
    · rw [coe_empty, Algebra.adjoin_empty]
      exact ⟨(Algebra.ofId F L).comp (Algebra.botEquiv F K)⟩
    rw [forall_mem_insert] at H
    rcases H with ⟨⟨H1, H2⟩, H3⟩
    obtain ⟨f⟩ := ih H3
    choose H3 _ using H3
    rw [coe_insert, Set.insert_eq, Set.union_comm, Algebra.adjoin_union_eq_adjoin_adjoin]
    set Ks := Algebra.adjoin F (s : Set K)
    haveI : FiniteDimensional F Ks := ((Submodule.fg_iff_finiteDimensional _).1
      (fg_adjoin_of_finite s.finite_toSet H3)).of_subalgebra_toSubmodule
    letI := fieldOfFiniteDimensional F Ks
    letI := (f : Ks →+* L).toAlgebra
    have H5 : IsIntegral Ks a := H1.tower_top
    have H6 : ((minpoly Ks a).map (algebraMap Ks L)).Splits := by
      refine Splits.of_dvd H2 (map_ne_zero (minpoly.ne_zero H1)) ?_
      rw [IsScalarTower.algebraMap_eq F Ks L, ← map_map, map_dvd_map']
      exact minpoly.dvd_map_of_isScalarTower F Ks a
    obtain ⟨y, hy⟩ := H6.exists_eval_eq_zero (by simp [(minpoly.degree_pos H5).ne'])
    rw [eval_map] at hy
    exact ⟨Subalgebra.ofRestrictScalars F _ <| Algebra.adjoin.liftSingleton Ks a y hy⟩
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Field (goal)
Goal:
F : Type u_2
K : Type u_3
L : Type u_4
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
s : Finset K
refine_1 :
  (∀ (x : K), Membership.mem (γ := Finset K) ∅ x → IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))) →
    Nonempty (AlgHom.{u_2, u_3, u_4} F (↥(Algebra.adjoin F (↑∅ : Set K))) L)
refine_2 refine_2₁ :
  ∀ (a : K) (s : Finset K),
    a ∉ s →
      ∀
        (ih :
          (∀ x ∈ s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))) →
            Nonempty (AlgHom.{u_2, u_3, u_4} F (↥(Algebra.adjoin F (↑s : Set K))) L))
        (H : ∀ x ∈ insert a s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))),
        Nonempty (AlgHom.{u_2, u_3, u_4} F (↥(Algebra.adjoin F (↑(insert a s) : Set K))) L)
⊢ (∀ x ∈ s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))) →
    Nonempty (AlgHom.{u_2, u_3, u_4} F (↥(Algebra.adjoin F (↑s : Set K))) L)
have refine_2₂ : ∀ (a : K) (s : Finset K),
  a ∉ s →
    ∀
      (ih :
        (∀ x ∈ s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))) →
          Nonempty (AlgHom.{u_2, u_3, u_4} F (↥(Algebra.adjoin F (↑s : Set K))) L))
      (H :
        (IsIntegral F a ∧ Splits (map (algebraMap F L) (minpoly F a))) ∧
          ∀ x ∈ s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))),
      Nonempty (AlgHom.{u_2, u_3, u_4} F (↥(Algebra.adjoin F (↑(insert a s) : Set K))) L)
Tactic: classical
    refine Finset.induction_on s (fun _ ↦ ?_) fun a s _ ih H ↦ ?_
    · rw [coe_empty, Algebra.adjoin_empty]
      exact ⟨(Algebra.ofId F L).comp (Algebra.botEquiv F K)⟩
    rw [forall_mem_insert] at H
    rcases H with ⟨⟨H1, H2⟩, H3⟩
    obtain ⟨f⟩ := ih H3
    choose H3 _ using H3
    rw [coe_insert, Set.insert_eq, Set.union_comm, Algebra.adjoin_union_eq_adjoin_adjoin]
    set Ks := Algebra.adjoin F (s : Set K)
    haveI : FiniteDimensional F Ks := ((Submodule.fg_iff_finiteDimensional _).1
      (fg_adjoin_of_finite s.finite_toSet H3)).of_subalgebra_toSubmodule
    letI := fieldOfFiniteDimensional F Ks
    letI := (f : Ks →+* L).toAlgebra
    have H5 : IsIntegral Ks a := H1.tower_top
    have H6 : ((minpoly Ks a).map (algebraMap Ks L)).Splits := by
      refine Splits.of_dvd H2 (map_ne_zero (minpoly.ne_zero H1)) ?_
      rw [IsScalarTower.algebraMap_eq F Ks L, ← map_map, map_dvd_map']
      exact minpoly.dvd_map_of_isScalarTower F Ks a
    obtain ⟨y, hy⟩ := H6.exists_eval_eq_zero (by simp [(minpoly.degree_pos H5).ne'])
    rw [eval_map] at hy
    exact ⟨Subalgebra.ofRestrictScalars F _ <| Algebra.adjoin.liftSingleton Ks a y hy⟩
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Field (goal)
Goal:
F : Type u_2
K : Type u_3
L : Type u_4
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
s : Finset K
refine_1 :
  (∀ (x : K), Membership.mem (γ := Finset K) ∅ x → IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))) →
    Nonempty (AlgHom.{u_2, u_3, u_4} F (↥(Algebra.adjoin F (↑∅ : Set K))) L)
refine_2 refine_2₁ :
  ∀ (a : K) (s : Finset K),
    a ∉ s →
      ∀
        (ih :
          (∀ x ∈ s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))) →
            Nonempty (AlgHom.{u_2, u_3, u_4} F (↥(Algebra.adjoin F (↑s : Set K))) L))
        (H : ∀ x ∈ insert a s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))),
        Nonempty (AlgHom.{u_2, u_3, u_4} F (↥(Algebra.adjoin F (↑(insert a s) : Set K))) L)
refine_2₂ :
  ∀ (a : K) (s : Finset K),
    a ∉ s →
      ∀
        (ih :
          (∀ x ∈ s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))) →
            Nonempty (AlgHom.{u_2, u_3, u_4} F (↥(Algebra.adjoin F (↑s : Set K))) L))
        (H :
          (IsIntegral F a ∧ Splits (map (algebraMap F L) (minpoly F a))) ∧
            ∀ x ∈ s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))),
        Nonempty (AlgHom.{u_2, u_3, u_4} F (↥(Algebra.adjoin F (↑(insert a s) : Set K))) L)
⊢ (∀ x ∈ s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))) →
    Nonempty (AlgHom.{u_2, u_3, u_4} F (↥(Algebra.adjoin F (↑s : Set K))) L)
have refine_2₃ : ∀ (a : K) (s : Finset K),
  a ∉ s →
    ∀
      (ih :
        (∀ x ∈ s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))) →
          Nonempty (AlgHom.{u_2, u_3, u_4} F (↥(Algebra.adjoin F (↑s : Set K))) L))
      (H3 : ∀ x ∈ s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))) (H1 : IsIntegral F a)
      (H2 : Splits (map (algebraMap F L) (minpoly F a))),
      Nonempty (AlgHom.{u_2, u_3, u_4} F (↥(Algebra.adjoin F (↑(insert a s) : Set K))) L)
Tactic: classical
    refine Finset.induction_on s (fun _ ↦ ?_) fun a s _ ih H ↦ ?_
    · rw [coe_empty, Algebra.adjoin_empty]
      exact ⟨(Algebra.ofId F L).comp (Algebra.botEquiv F K)⟩
    rw [forall_mem_insert] at H
    rcases H with ⟨⟨H1, H2⟩, H3⟩
    obtain ⟨f⟩ := ih H3
    choose H3 _ using H3
    rw [coe_insert, Set.insert_eq, Set.union_comm, Algebra.adjoin_union_eq_adjoin_adjoin]
    set Ks := Algebra.adjoin F (s : Set K)
    haveI : FiniteDimensional F Ks := ((Submodule.fg_iff_finiteDimensional _).1
      (fg_adjoin_of_finite s.finite_toSet H3)).of_subalgebra_toSubmodule
    letI := fieldOfFiniteDimensional F Ks
    letI := (f : Ks →+* L).toAlgebra
    have H5 : IsIntegral Ks a := H1.tower_top
    have H6 : ((minpoly Ks a).map (algebraMap Ks L)).Splits := by
      refine Splits.of_dvd H2 (map_ne_zero (minpoly.ne_zero H1)) ?_
      rw [IsScalarTower.algebraMap_eq F Ks L, ← map_map, map_dvd_map']
      exact minpoly.dvd_map_of_isScalarTower F Ks a
    obtain ⟨y, hy⟩ := H6.exists_eval_eq_zero (by simp [(minpoly.degree_pos H5).ne'])
    rw [eval_map] at hy
    exact ⟨Subalgebra.ofRestrictScalars F _ <| Algebra.adjoin.liftSingleton Ks a y hy⟩
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Field (goal)
Goal:
R : Type u_1
K : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra R K
x : L
inst_4 : Algebra R L
int : IsIntegral R x
h : Splits (Polynomial.map (algebraMap R K) (minpoly R x))
f : K →ₐ[R] L
⊢ Membership.mem (γ := Set L) ((⇑f : (a : K) → L) '' rootSet (minpoly R x) K) x
have rw : Ne (α := L[X]) (Polynomial.map (algebraMap R L) (minpoly R x)) 0 ∧
  Eq.{u_3 + 1} (α := L) ((aeval x : (a : R[X]) → L) (minpoly R x) : L) (0 : L)
Tactic: rw [h.image_rootSet, mem_rootSet']
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Field (goal)
Goal:
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x : L
g : Splits (map (algebraMap K L) (minpoly K x))
⊢ Splits (map (algebraMap K L) (minpoly K (-x)))
have rw : (HMul.hMul (α := L[X]) (map (algebraMap K L) (HPow.hPow (α := K[X]) (-1) (natDegree (minpoly K x))))
    (map (algebraMap K L) (comp (minpoly K x) (-X)))).Splits
Tactic: rw [minpoly.neg, Polynomial.map_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Field (goal)
Goal:
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x : L
g : Splits (map (algebraMap K L) (minpoly K x))
⊢ (HMul.hMul (α := L[X]) (map (algebraMap K L) (HPow.hPow (α := K[X]) (-1) (natDegree (minpoly K x))))
      (map (algebraMap K L) (comp (minpoly K x) (-X)))).Splits
have apply : Splits (map (algebraMap K L) (HPow.hPow (α := K[X]) (-1) (natDegree (minpoly K x))))
Tactic: apply Splits.mul _ (by simpa [map_comp] using g.comp_neg_X)
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Field (goal)
Goal:
R : Type u_1
K : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : Field K
inst_2 : Field L
inst_3 : CommRing M
inst_4 : Algebra R K
inst_5 : Algebra R M
inst_6 : Algebra K M
inst_7 : IsScalarTower R K M
x : M
int : IsIntegral R x
f : K →+* L
h : (Polynomial.map (f.comp (algebraMap R K)) (minpoly R x)).Splits
⊢ Polynomial.map f (minpoly K x) ∣ Polynomial.map (f.comp (algebraMap R K)) (minpoly R x)
have rw : Dvd.dvd (α := K[X]) (minpoly K x) (Polynomial.map (algebraMap R K) (minpoly R x))
Tactic: rw [← map_map, map_dvd_map']
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Field (hypothesis)
Goal:
R : Type u_1
K : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : Field K
inst_2 : Field L
inst_3 : CommRing M
inst_4 : Algebra R K
inst_5 : Algebra R M
inst_6 : Algebra K M
inst_7 : IsScalarTower R K M
x : M
inst_8 : Algebra K L
inst_9 : Algebra R L
inst_10 : IsScalarTower R K L
int : IsIntegral R x
h : Splits (Polynomial.map (algebraMap R L) (minpoly R x))
⊢ Splits (Polynomial.map (algebraMap K L) (minpoly K x))
have h₁ : Splits
  (Polynomial.map (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap K L) (algebraMap R K)) (minpoly R x))
Tactic: rw [IsScalarTower.algebraMap_eq R K L] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Field (goal)
Goal:
F : Type u_5
E : Type u_6
K : Type u_7
inst : CommSemiring F
inst_1 : StrongRankCondition F
inst_2 : CommSemiring E
inst_3 : StrongRankCondition E
inst_4 : Semiring K
inst_5 : SMul F E
inst_6 : Algebra E K
inst_7 : Algebra F K
inst_8 : IsScalarTower F E K
L : Subalgebra F K
inst_9 : Module.Free.{u_5, u_7} F ↥L
⊢ Module.rank E ↥(Algebra.adjoin E (↑L : Set K)) ≤ Module.rank F ↥L
have rw : Module.rank E
    ↥(Submodule.span E
        (Set.range fun (i : Module.Free.ChooseBasisIndex F ↥L) ↦
          (↑((Module.Free.chooseBasis F ↥L : (a : Module.Free.ChooseBasisIndex F ↥L) → ↥L) i) : K))) ≤
  Cardinal.mk (Module.Free.ChooseBasisIndex F ↥L)
Tactic: rw [← rank_toSubmodule, Module.Free.rank_eq_card_chooseBasisIndex F L,
    L.adjoin_eq_span_basis E (Module.Free.chooseBasis F L)]
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
⊢ Eq (α := Subalgebra R R[X]) R[ X] ⊤
have refine : ∀ (p : R[X]) (_hp : Membership.mem (γ := Subalgebra R R[X]) ⊤ p), Membership.mem (γ := Subalgebra R R[X]) R[ X] p
Tactic: refine top_unique fun p _hp => ?_
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
p : R[X]
_hp : Membership.mem (γ := Subalgebra R R[X]) ⊤ p
S : Subalgebra R R[X] := R[ X]
⊢ p ∈ S
have rw : (p.sum fun (n : ℕ) (a : R) ↦ (monomial n : (a : R) → R[X]) a) ∈ S
Tactic: rw [← sum_monomial_eq p]
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
p : R[X]
_hp : Membership.mem (γ := Subalgebra R R[X]) ⊤ p
S : Subalgebra R R[X] := R[ X]
⊢ (p.sum fun (n : ℕ) (a : R) ↦ (monomial n : (a : R) → R[X]) a) ∈ S
have simp : (p.sum fun (n : ℕ) (a : R) ↦ a • HPow.hPow (α := R[X]) X n) ∈ S
Tactic: simp only [← smul_X_eq_monomial]
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Polynomial.Basic (goal)
Goal:
R : Type u
A : Type z
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
x : A
⊢ Eq (α := Subalgebra R A) R[x] (AlgHom.range (aeval x))
have rw : Eq (α := Subalgebra R A) R[x] (Subalgebra.map (aeval x) ⊤)
Tactic: rw [← Algebra.map_top, ← adjoin_X, AlgHom.map_adjoin, Set.image_singleton, aeval_X]
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Polynomial.Basic (goal)
Goal:
R : Type u
A : Type z
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
x : A
rw : Eq (α := Subalgebra R A) R[x] (Subalgebra.map (aeval x) ⊤)
⊢ Eq (α := Subalgebra R A) R[x] (AlgHom.range (aeval x))
have rw₁ : Eq (α := Subalgebra R A) R[x] (Subalgebra.map (aeval x) R[ X])
Tactic: rw [← Algebra.map_top, ← adjoin_X, AlgHom.map_adjoin, Set.image_singleton, aeval_X]
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Polynomial.Basic (goal)
Goal:
R : Type u
A : Type z
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
x : A
rw : Eq (α := Subalgebra R A) R[x] (Subalgebra.map (aeval x) ⊤)
rw₁ : Eq (α := Subalgebra R A) R[x] (Subalgebra.map (aeval x) R[ X])
⊢ Eq (α := Subalgebra R A) R[x] (AlgHom.range (aeval x))
have rw₂ : Eq (α := Subalgebra R A) R[x] (adjoin R (Set.image (α := R[X]) (⇑(aeval x) : (a : R[X]) → A) {X}))
Tactic: rw [← Algebra.map_top, ← adjoin_X, AlgHom.map_adjoin, Set.image_singleton, aeval_X]
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Polynomial.Basic (goal)
Goal:
R : Type u
A : Type z
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
x : A
rw : Eq (α := Subalgebra R A) R[x] (Subalgebra.map (aeval x) ⊤)
rw₁ : Eq (α := Subalgebra R A) R[x] (Subalgebra.map (aeval x) R[ X])
rw₂ : Eq (α := Subalgebra R A) R[x] (adjoin R (Set.image (α := R[X]) (⇑(aeval x) : (a : R[X]) → A) {X}))
⊢ Eq (α := Subalgebra R A) R[x] (AlgHom.range (aeval x))
have rw₃ : Eq (α := Subalgebra R A) R[x] R[((aeval x : (a : R[X]) → A) X : A)]
Tactic: rw [← Algebra.map_top, ← adjoin_X, AlgHom.map_adjoin, Set.image_singleton, aeval_X]
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Polynomial.Basic (goal)
Goal:
R : Type u
A : Type z
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
x : A
rw : Eq (α := Subalgebra R A) R[x] (Subalgebra.map (aeval x) ⊤)
rw₁ : Eq (α := Subalgebra R A) R[x] (Subalgebra.map (aeval x) R[ X])
rw₂ : Eq (α := Subalgebra R A) R[x] (adjoin R (Set.image (α := R[X]) (⇑(aeval x) : (a : R[X]) → A) {X}))
rw₃ : Eq (α := Subalgebra R A) R[x] R[((aeval x : (a : R[X]) → A) X : A)]
⊢ Eq (α := Subalgebra R A) R[x] (AlgHom.range (aeval x))
have rw₄ : Eq (α := Subalgebra R A) R[x] R[x]
Tactic: rw [← Algebra.map_top, ← adjoin_X, AlgHom.map_adjoin, Set.image_singleton, aeval_X]
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Polynomial.Basic (hypothesis)
Goal:
R : Type u
A : Type z
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
x a : A
h : Membership.mem (γ := Subalgebra R A) R[x] a
⊢ ∃ (p : R[X]), (aeval x : (a : R[X]) → A) p = a
have h₁ : Membership.mem (γ := Subalgebra R A) (AlgHom.range (aeval x)) a
Tactic: rw [Algebra.adjoin_singleton_eq_range_aeval] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Polynomial.Basic (hypothesis)
Goal:
R : Type u
A : Type z
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
x : A
a : ↥R[x]
⊢ ∃ (p : R[X]), (aeval x : (a : R[X]) → A) p = (↑a : A)
have this : Membership.mem (γ := Subalgebra R A) R[x] (↑a : A)
Tactic: have : (a : A) ∈ R[x] := by simp
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Polynomial.Basic (goal)
Goal:
R : Type u
A : Type z
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
x : A
a : ↥R[x]
this : Membership.mem (γ := Subalgebra R A) R[x] (↑a : A)
⊢ ∃ (p : R[X]), (aeval x : (a : R[X]) → A) p = (↑a : A)
have set : let y := (↑a : A);
∀ (this : Membership.mem (γ := Subalgebra R A) R[x] y) (h : y = (↑a : A)),
  ∃ (p : R[X]), (aeval x : (a : R[X]) → A) p = y
Tactic: set y := (a : A) with h
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Polynomial.Basic (hypothesis)
Goal:
R : Type u
A : Type z
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
x : A
a : ↥R[x]
y : A := (↑a : A)
this : Membership.mem (γ := Subalgebra R A) R[x] y
h : y = (↑a : A)
⊢ ∃ (p : R[X]), (aeval x : (a : R[X]) → A) p = y
have this₁ : Membership.mem (γ := Subalgebra R A) (AlgHom.range (aeval x)) y
Tactic: rw [Algebra.adjoin_singleton_eq_range_aeval] at this
Cleared hypotheses: this, h
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Polynomial.Basic (goal)
Goal:
R : Type u
A : Type z
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
x : A
M : ↥R[x] → Prop
a : ↥R[x]
f :
  ∀ (p : R[X]),
    M (Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Subalgebra R A) R[x] x_1) ((aeval x : (a : R[X]) → A) p) ⋯)
⊢ M a
have obtain : ∀ (p : R[X]) (hp : (aeval x : (a : R[X]) → A) p = (↑a : A)), M a
Tactic: obtain ⟨p, hp⟩ := Algebra.adjoin_eq_exists_aeval _ x a
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Polynomial.Basic (goal)
Goal:
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B : Type u_2
a b : R
n : ℕ
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : CommSemiring A'
inst_3 : Semiring B
inst_4 : Algebra R A
inst_5 : Algebra R B
p_1 q_1 : R[X]
x : A
x_1 x_2 : ↥R[x]
p : A
hp : Membership.mem (γ := Subalgebra R A) R[x] p
q : A
hq : Membership.mem (γ := Subalgebra R A) R[x] q
⊢ Subtype.mk (p := fun (x_3 : A) ↦ Membership.mem (γ := Subalgebra R A) R[x] x_3) p hp *
      Subtype.mk (p := fun (x_3 : A) ↦ Membership.mem (γ := Subalgebra R A) R[x] x_3) q hq =
    Subtype.mk (p := fun (x_3 : A) ↦ Membership.mem (γ := Subalgebra R A) R[x] x_3) q hq *
      Subtype.mk (p := fun (x_3 : A) ↦ Membership.mem (γ := Subalgebra R A) R[x] x_3) p hp
have obtain : ∀ (p' : R[X])
  (hp : Membership.mem (α := A) (γ := Subalgebra R A) R[x] ((AlgHom.toRingHom (aeval x) : (a : R[X]) → A) p' : A)),
  HMul.hMul (α := ↥R[x])
      (Subtype.mk (p := fun (x_3 : A) ↦ Membership.mem (γ := Subalgebra R A) R[x] x_3)
          ((AlgHom.toRingHom (aeval x) : (a : R[X]) → A) p') hp :
        ↥R[x])
      (Subtype.mk (p := fun (x_3 : A) ↦ Membership.mem (γ := Subalgebra R A) R[x] x_3) q hq) =
    HMul.hMul (β := ↥R[x]) (Subtype.mk (p := fun (x_3 : A) ↦ Membership.mem (γ := Subalgebra R A) R[x] x_3) q hq)
      (Subtype.mk (p := fun (x_3 : A) ↦ Membership.mem (γ := Subalgebra R A) R[x] x_3)
          ((AlgHom.toRingHom (aeval x) : (a : R[X]) → A) p') hp :
        ↥R[x])
Tactic: obtain ⟨p', rfl⟩ := Algebra.adjoin_singleton_eq_range_aeval R x ▸ hp
Cleared hypotheses: p, hp
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Polynomial.Basic (goal)
Goal:
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B : Type u_2
a b : R
n : ℕ
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : CommSemiring A'
inst_3 : Semiring B
inst_4 : Algebra R A
inst_5 : Algebra R B
p q_1 : R[X]
x : A
x_1 x_2 : ↥R[x]
q : A
hq : Membership.mem (γ := Subalgebra R A) R[x] q
p' : R[X]
hp : Membership.mem (α := A) (γ := Subalgebra R A) R[x] ((AlgHom.toRingHom (aeval x) : (a : R[X]) → A) p' : A)
⊢ HMul.hMul (α := ↥R[x])
      (Subtype.mk (p := fun (x_3 : A) ↦ Membership.mem (γ := Subalgebra R A) R[x] x_3)
          ((AlgHom.toRingHom (aeval x) : (a : R[X]) → A) p') hp :
        ↥R[x])
      (Subtype.mk (p := fun (x_3 : A) ↦ Membership.mem (γ := Subalgebra R A) R[x] x_3) q hq) =
    HMul.hMul (β := ↥R[x]) (Subtype.mk (p := fun (x_3 : A) ↦ Membership.mem (γ := Subalgebra R A) R[x] x_3) q hq)
      (Subtype.mk (p := fun (x_3 : A) ↦ Membership.mem (γ := Subalgebra R A) R[x] x_3)
          ((AlgHom.toRingHom (aeval x) : (a : R[X]) → A) p') hp :
        ↥R[x])
have obtain : ∀ (q' : R[X])
  (hq : Membership.mem (α := A) (γ := Subalgebra R A) R[x] ((AlgHom.toRingHom (aeval x) : (a : R[X]) → A) q' : A)),
  HMul.hMul (α := ↥R[x]) (β := ↥R[x])
      (Subtype.mk (p := fun (x_3 : A) ↦ Membership.mem (γ := Subalgebra R A) R[x] x_3)
          ((AlgHom.toRingHom (aeval x) : (a : R[X]) → A) p') hp :
        ↥R[x])
      (Subtype.mk (p := fun (x_3 : A) ↦ Membership.mem (γ := Subalgebra R A) R[x] x_3)
          ((AlgHom.toRingHom (aeval x) : (a : R[X]) → A) q') hq :
        ↥R[x]) =
    HMul.hMul (α := ↥R[x]) (β := ↥R[x])
      (Subtype.mk (p := fun (x_3 : A) ↦ Membership.mem (γ := Subalgebra R A) R[x] x_3)
          ((AlgHom.toRingHom (aeval x) : (a : R[X]) → A) q') hq :
        ↥R[x])
      (Subtype.mk (p := fun (x_3 : A) ↦ Membership.mem (γ := Subalgebra R A) R[x] x_3)
          ((AlgHom.toRingHom (aeval x) : (a : R[X]) → A) p') hp :
        ↥R[x])
Tactic: obtain ⟨q', rfl⟩ := Algebra.adjoin_singleton_eq_range_aeval R x ▸ hq
Cleared hypotheses: q, hq