awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
B : Type u_2
inst_3 : Ring B
inst_4 : Algebra R B
f : A →ₐ[R] B
a : A
h : IsAlgebraic R a
p : R[X]
hp : p ≠ 0
ha : Eq.{v + 1} (α := A) ((aeval a : (a : R[X]) → A) p : A) (0 : A)
⊢ Eq.{u_2 + 1} (α := B) (((aeval ((f : (a : A) → B) a) : R[X] →ₐ[R] B) : (a : R[X]) → B) p : B) (0 : B)
have rw : Eq.{u_2 + 1} (α := B) ((f.comp (aeval a) : (a : R[X]) → B) p : B) (0 : B)
Tactic: rw [aeval_algHom, f.comp_apply, ha, map_zero]
-- 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
B : Type u_2
inst_3 : Ring B
inst_4 : Algebra R B
f : A →ₐ[R] B
a : A
h : IsAlgebraic R a
p : R[X]
hp : p ≠ 0
ha : Eq.{v + 1} (α := A) ((aeval a : (a : R[X]) → A) p : A) (0 : A)
rw : Eq.{u_2 + 1} (α := B) ((f.comp (aeval a) : (a : R[X]) → B) p : B) (0 : B)
⊢ Eq.{u_2 + 1} (α := B) (((aeval ((f : (a : A) → B) a) : R[X] →ₐ[R] B) : (a : R[X]) → B) p : B) (0 : B)
have rw₁ : Eq.{u_2 + 1} (α := B) ((f : (a : A) → B) ((aeval a : (a : R[X]) → A) p : A) : B) (0 : B)
Tactic: rw [aeval_algHom, f.comp_apply, ha, map_zero]
-- 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
B : Type u_2
inst_3 : Ring B
inst_4 : Algebra R B
f : A →ₐ[R] B
a : A
h : IsAlgebraic R a
p : R[X]
hp : p ≠ 0
ha : Eq.{v + 1} (α := A) ((aeval a : (a : R[X]) → A) p : A) (0 : A)
rw : Eq.{u_2 + 1} (α := B) ((f.comp (aeval a) : (a : R[X]) → B) p : B) (0 : B)
rw₁ : Eq.{u_2 + 1} (α := B) ((f : (a : A) → B) ((aeval a : (a : R[X]) → A) p : A) : B) (0 : B)
⊢ Eq.{u_2 + 1} (α := B) (((aeval ((f : (a : A) → B) a) : R[X] →ₐ[R] B) : (a : R[X]) → B) p : B) (0 : B)
have rw₂ : Eq.{u_2 + 1} (α := B) ((f : (a : A) → B) 0 : B) (0 : B)
Tactic: rw [aeval_algHom, f.comp_apply, ha, map_zero]
-- 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
B : Type u_2
inst_3 : Ring B
inst_4 : Algebra R B
f : A →ₐ[R] B
a : A
h : IsAlgebraic R a
p : R[X]
hp : p ≠ 0
ha : Eq.{v + 1} (α := A) ((aeval a : (a : R[X]) → A) p : A) (0 : A)
rw : Eq.{u_2 + 1} (α := B) ((f.comp (aeval a) : (a : R[X]) → B) p : B) (0 : B)
rw₁ : Eq.{u_2 + 1} (α := B) ((f : (a : A) → B) ((aeval a : (a : R[X]) → A) p : A) : B) (0 : B)
rw₂ : Eq.{u_2 + 1} (α := B) ((f : (a : A) → B) 0 : B) (0 : B)
⊢ Eq.{u_2 + 1} (α := B) (((aeval ((f : (a : A) → B) a) : R[X] →ₐ[R] B) : (a : R[X]) → B) p : B) (0 : B)
have rw₃ : Eq.{u_2 + 1} (α := B) 0 0
Tactic: rw [aeval_algHom, f.comp_apply, ha, map_zero]
-- 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
B : Type u_2
inst_3 : Ring B
inst_4 : Algebra R B
f : A →ₐ[R] B
hf : Function.Injective.{v + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
a : A
h : IsAlgebraic.{u, u_2} R (A := B) ((f : (a : A) → B) a : B)
p : R[X]
hp0 : p ≠ 0
hp : Eq.{u_2 + 1} (α := B) (((aeval ((f : (a : A) → B) a) : R[X] →ₐ[R] B) : (a : R[X]) → B) p : B) (0 : B)
⊢ Eq.{u_2 + 1} (α := B) ((f : (a : A) → B) ((aeval a : (a : R[X]) → A) p : A) : B) ((f : (a : A) → B) 0 : B)
have rwa : Eq.{u_2 + 1} (α := B) ((f : (a : A) → B) ((aeval a : (a : R[X]) → A) p : A) : B) (0 : B)
Tactic: rwa [map_zero, ← f.comp_apply, ← aeval_algHom]
-- 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
B : Type u_2
inst_3 : Ring B
inst_4 : Algebra R B
f : A →ₐ[R] B
hf : Function.Injective.{v + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
a : A
h : IsAlgebraic.{u, u_2} R (A := B) ((f : (a : A) → B) a : B)
p : R[X]
hp0 : p ≠ 0
hp : Eq.{u_2 + 1} (α := B) (((aeval ((f : (a : A) → B) a) : R[X] →ₐ[R] B) : (a : R[X]) → B) p : B) (0 : B)
rwa : Eq.{u_2 + 1} (α := B) ((f : (a : A) → B) ((aeval a : (a : R[X]) → A) p : A) : B) (0 : B)
⊢ Eq.{u_2 + 1} (α := B) ((f : (a : A) → B) ((aeval a : (a : R[X]) → A) p : A) : B) ((f : (a : A) → B) 0 : B)
have rwa₁ : Eq.{u_2 + 1} (α := B) ((f.comp (aeval a) : (a : R[X]) → B) p : B) (0 : B)
Tactic: rwa [map_zero, ← f.comp_apply, ← aeval_algHom]
-- 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 : FunLike FRS R S
inst_7 : RingHomClass FRS R S
inst_8 : FunLike FAB A B
inst_9 : RingHomClass FAB A B
f : FRS
g : FAB
a : A
halg : IsAlgebraic R a
hf : Function.Injective.{u + 1, u_1 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
h :
  Eq (α := R →+* B) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S B) (↑f : R →+* S))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑g : A →+* B) (algebraMap R A))
⊢ IsAlgebraic.{u_1, u_2} S (A := B) ((g : (a : A) → B) a : B)
have obtain : ∀ (p : R[X]) (h1 : p ≠ 0) (h2 : Eq.{v + 1} (α := A) ((aeval a : (a : R[X]) → A) p : A) (0 : A)),
  IsAlgebraic.{u_1, u_2} S (A := B) ((g : (a : A) → B) a : B)
Tactic: obtain ⟨p, h1, h2⟩ := halg
Cleared hypotheses: halg
-- 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 : FunLike FRS R S
inst_7 : RingHomClass FRS R S
inst_8 : FunLike FAB A B
inst_9 : RingHomClass FAB A B
f : FRS
g : FAB
a : A
hf : Function.Injective.{u + 1, u_1 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
h :
  Eq (α := R →+* B) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S B) (↑f : R →+* S))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑g : A →+* B) (algebraMap R A))
p : R[X]
h1 : p ≠ 0
h2 : Eq.{v + 1} (α := A) ((aeval a : (a : R[X]) → A) p : A) (0 : A)
⊢ IsAlgebraic.{u_1, u_2} S (A := B) ((g : (a : A) → B) a : B)
have refine : Eq.{u_2 + 1} (α := B) (((aeval ((g : (a : A) → B) a) : S[X] →ₐ[S] B) : (a : S[X]) → B) (map (↑f : R →+* S) p) : B)
  (0 : B)
Tactic: refine ⟨p.map f, (Polynomial.map_ne_zero_iff hf).2 h1, ?_⟩
-- 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 : FunLike FRS R S
inst_7 : RingHomClass FRS R S
inst_8 : FunLike FAB A B
inst_9 : RingHomClass FAB A B
f : FRS
g : FAB
a : A
hf : Function.Injective.{u + 1, u_1 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
h :
  Eq (α := R →+* B) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S B) (↑f : R →+* S))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑g : A →+* B) (algebraMap R A))
p : R[X]
h1 : p ≠ 0
h2 : Eq.{v + 1} (α := A) ((aeval a : (a : R[X]) → A) p : A) (0 : A)
⊢ Eq.{u_2 + 1} (α := B) (((aeval ((g : (a : A) → B) a) : S[X] →ₐ[S] B) : (a : S[X]) → B) (map (↑f : R →+* S) p) : B)
    (0 : B)
have change : Eq.{u_2 + 1} (α := B)
  (((aeval (((↑g : A →+* B) : (a : A) → B) a) : S[X] →ₐ[S] B) : (a : S[X]) → B) (map (↑f : R →+* S) p) : B) (0 : B)
Tactic: change aeval ((g : A →+* B) a) _ = 0
-- 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 : FunLike FRS R S
inst_7 : RingHomClass FRS R S
inst_8 : FunLike FAB A B
inst_9 : RingHomClass FAB A B
f : FRS
g : FAB
a : A
hf : Function.Injective.{u + 1, u_1 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
h :
  Eq (α := R →+* B) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S B) (↑f : R →+* S))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑g : A →+* B) (algebraMap R A))
p : R[X]
h1 : p ≠ 0
h2 : Eq.{v + 1} (α := A) ((aeval a : (a : R[X]) → A) p : A) (0 : A)
⊢ Eq.{u_2 + 1} (α := B)
    (((aeval (((↑g : A →+* B) : (a : A) → B) a) : S[X] →ₐ[S] B) : (a : S[X]) → B) (map (↑f : R →+* S) p) : B) (0 : B)
have rw : Eq.{u_2 + 1} (α := B) (((↑g : A →+* B) : (a : A) → B) ((aeval a : (a : R[X]) → A) p : A) : B) (0 : B)
Tactic: rw [← map_aeval_eq_aeval_map h, h2, map_zero]
-- 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 : FunLike FRS R S
inst_7 : RingHomClass FRS R S
inst_8 : FunLike FAB A B
inst_9 : RingHomClass FAB A B
f : FRS
g : FAB
a : A
hf : Function.Injective.{u + 1, u_1 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
h :
  Eq (α := R →+* B) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S B) (↑f : R →+* S))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑g : A →+* B) (algebraMap R A))
p : R[X]
h1 : p ≠ 0
h2 : Eq.{v + 1} (α := A) ((aeval a : (a : R[X]) → A) p : A) (0 : A)
rw : Eq.{u_2 + 1} (α := B) (((↑g : A →+* B) : (a : A) → B) ((aeval a : (a : R[X]) → A) p : A) : B) (0 : B)
⊢ Eq.{u_2 + 1} (α := B)
    (((aeval (((↑g : A →+* B) : (a : A) → B) a) : S[X] →ₐ[S] B) : (a : S[X]) → B) (map (↑f : R →+* S) p) : B) (0 : B)
have rw₁ : Eq.{u_2 + 1} (α := B) (((↑g : A →+* B) : (a : A) → B) 0 : B) (0 : B)
Tactic: rw [← map_aeval_eq_aeval_map h, h2, map_zero]
-- 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 : FunLike FRS R S
inst_7 : RingHomClass FRS R S
inst_8 : FunLike FAB A B
inst_9 : RingHomClass FAB A B
f : FRS
g : FAB
a : A
hf : Function.Injective.{u + 1, u_1 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
h :
  Eq (α := R →+* B) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S B) (↑f : R →+* S))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑g : A →+* B) (algebraMap R A))
p : R[X]
h1 : p ≠ 0
h2 : Eq.{v + 1} (α := A) ((aeval a : (a : R[X]) → A) p : A) (0 : A)
rw : Eq.{u_2 + 1} (α := B) (((↑g : A →+* B) : (a : A) → B) ((aeval a : (a : R[X]) → A) p : A) : B) (0 : B)
rw₁ : Eq.{u_2 + 1} (α := B) (((↑g : A →+* B) : (a : A) → B) 0 : B) (0 : B)
⊢ Eq.{u_2 + 1} (α := B)
    (((aeval (((↑g : A →+* B) : (a : A) → B) a) : S[X] →ₐ[S] B) : (a : S[X]) → B) (map (↑f : R →+* S) p) : B) (0 : B)
have rw₂ : Eq.{u_2 + 1} (α := B) 0 0
Tactic: rw [← map_aeval_eq_aeval_map h, h2, map_zero]
-- 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 : FunLike FRS R S
inst_7 : RingHomClass FRS R S
inst_8 : FunLike FAB A B
inst_9 : RingHomClass FAB A B
f : FRS
g : FAB
inst_10 : Algebra.IsAlgebraic R A
hf : Function.Injective.{u + 1, u_1 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
hg : Function.Surjective.{v + 1, u_2 + 1} (α := A) (β := B) (⇑g : (a : A) → B)
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.IsAlgebraic S B
have refine : ∀ (b : B), IsAlgebraic S b
Tactic: refine ⟨fun b ↦ ?_⟩
-- 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 : FunLike FRS R S
inst_7 : RingHomClass FRS R S
inst_8 : FunLike FAB A B
inst_9 : RingHomClass FAB A B
f : FRS
g : FAB
inst_10 : Algebra.IsAlgebraic R A
hf : Function.Injective.{u + 1, u_1 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
hg : Function.Surjective.{v + 1, u_2 + 1} (α := A) (β := B) (⇑g : (a : A) → B)
h :
  Eq (α := R →+* B) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S B) (↑f : R →+* S))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑g : A →+* B) (algebraMap R A))
b : B
⊢ IsAlgebraic S b
have obtain : ∀ (a : A), IsAlgebraic.{u_1, u_2} S (A := B) ((g : (a : A) → B) a : B)
Tactic: obtain ⟨a, rfl⟩ := hg b
Cleared hypotheses: b
-- 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 : FunLike FRS R S
inst_7 : RingHomClass FRS R S
inst_8 : FunLike FAB A B
inst_9 : RingHomClass FAB A B
f : FRS
g : FAB
H : Algebra.Transcendental S B
hf : Function.Injective.{u + 1, u_1 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
hg : Function.Surjective.{v + 1, u_2 + 1} (α := A) (β := B) (⇑g : (a : A) → B)
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 R A
have rw : ∀ (H : ¬Algebra.IsAlgebraic S B) (hf : Function.Injective.{u + 1, u_1 + 1} (α := R) (β := S) (⇑f : (a : R) → S))
  (hg : Function.Surjective.{v + 1, u_2 + 1} (α := A) (β := B) (⇑g : (a : A) → B))
  (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.IsAlgebraic R A
Tactic: rw [Algebra.transcendental_iff_not_isAlgebraic] at H ⊢
Cleared hypotheses: H, hf, hg, h
-- 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 : FunLike FRS R S
inst_7 : RingHomClass FRS R S
inst_8 : FunLike FAB A B
inst_9 : RingHomClass FAB A B
f : FRS
g : FAB
a : A
halg : IsAlgebraic.{u_1, u_2} S (A := B) ((g : (a : A) → B) a : B)
hf : Function.Surjective.{u + 1, u_1 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
hg : Function.Injective.{v + 1, u_2 + 1} (α := A) (β := B) (⇑g : (a : A) → B)
h :
  Eq (α := R →+* B) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S B) (↑f : R →+* S))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑g : A →+* B) (algebraMap R A))
⊢ IsAlgebraic R a
have obtain : ∀ (p : S[X]) (h1 : p ≠ 0)
  (h2 : Eq.{u_2 + 1} (α := B) (((aeval ((g : (a : A) → B) a) : S[X] →ₐ[S] B) : (a : S[X]) → B) p : B) (0 : B)),
  IsAlgebraic R a
Tactic: obtain ⟨p, h1, h2⟩ := halg
Cleared hypotheses: halg
-- 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 : FunLike FRS R S
inst_7 : RingHomClass FRS R S
inst_8 : FunLike FAB A B
inst_9 : RingHomClass FAB A B
f : FRS
g : FAB
a : A
hf : Function.Surjective.{u + 1, u_1 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
hg : Function.Injective.{v + 1, u_2 + 1} (α := A) (β := B) (⇑g : (a : A) → B)
h :
  Eq (α := R →+* B) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S B) (↑f : R →+* S))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑g : A →+* B) (algebraMap R A))
p : S[X]
h1 : p ≠ 0
h2 : Eq.{u_2 + 1} (α := B) (((aeval ((g : (a : A) → B) a) : S[X] →ₐ[S] B) : (a : S[X]) → B) p : B) (0 : B)
⊢ IsAlgebraic R a
have obtain : ∀ (q : R[X]) (h1 : Ne (α := S[X]) (map (↑f : R →+* S) q) 0)
  (h2 :
    Eq.{u_2 + 1} (α := B) (((aeval ((g : (a : A) → B) a) : S[X] →ₐ[S] B) : (a : S[X]) → B) (map (↑f : R →+* S) q) : B)
      (0 : B)),
  IsAlgebraic R a
Tactic: obtain ⟨q, rfl⟩ := map_surjective (f : R →+* S) hf p
Cleared hypotheses: p, h1, h2
-- 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 : FunLike FRS R S
inst_7 : RingHomClass FRS R S
inst_8 : FunLike FAB A B
inst_9 : RingHomClass FAB A B
f : FRS
g : FAB
a : A
hf : Function.Surjective.{u + 1, u_1 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
hg : Function.Injective.{v + 1, u_2 + 1} (α := A) (β := B) (⇑g : (a : A) → B)
h :
  Eq (α := R →+* B) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S B) (↑f : R →+* S))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑g : A →+* B) (algebraMap R A))
q : R[X]
h1 : Ne (α := S[X]) (map (↑f : R →+* S) q) 0
h2 :
  Eq.{u_2 + 1} (α := B) (((aeval ((g : (a : A) → B) a) : S[X] →ₐ[S] B) : (a : S[X]) → B) (map (↑f : R →+* S) q) : B)
    (0 : B)
⊢ IsAlgebraic R a
have refine : Eq.{u_2 + 1} (α := B) ((g : (a : A) → B) ((aeval a : (a : R[X]) → A) q : A) : B) ((g : (a : A) → B) 0 : B)
Tactic: refine ⟨q, fun h' ↦ by simp [h'] at h1, hg ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (hypothesis)
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 : FunLike FRS R S
inst_7 : RingHomClass FRS R S
inst_8 : FunLike FAB A B
inst_9 : RingHomClass FAB A B
f : FRS
g : FAB
a : A
hf : Function.Surjective.{u + 1, u_1 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
hg : Function.Injective.{v + 1, u_2 + 1} (α := A) (β := B) (⇑g : (a : A) → B)
h :
  Eq (α := R →+* B) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S B) (↑f : R →+* S))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑g : A →+* B) (algebraMap R A))
q : R[X]
h1 : Ne (α := S[X]) (map (↑f : R →+* S) q) 0
h2 :
  Eq.{u_2 + 1} (α := B) (((aeval ((g : (a : A) → B) a) : S[X] →ₐ[S] B) : (a : S[X]) → B) (map (↑f : R →+* S) q) : B)
    (0 : B)
⊢ Eq.{u_2 + 1} (α := B) ((g : (a : A) → B) ((aeval a : (a : R[X]) → A) q : A) : B) ((g : (a : A) → B) 0 : B)
have h2₁ : Eq.{u_2 + 1} (α := B)
  (((aeval (((↑g : A →+* B) : (a : A) → B) a) : S[X] →ₐ[S] B) : (a : S[X]) → B) (map (↑f : R →+* S) q) : B) (0 : B)
Tactic: change aeval ((g : A →+* B) a) _ = 0 at h2
Cleared hypotheses: h2
-- 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 : FunLike FRS R S
inst_7 : RingHomClass FRS R S
inst_8 : FunLike FAB A B
inst_9 : RingHomClass FAB A B
f : FRS
g : FAB
a : A
hf : Function.Surjective.{u + 1, u_1 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
hg : Function.Injective.{v + 1, u_2 + 1} (α := A) (β := B) (⇑g : (a : A) → B)
h :
  Eq (α := R →+* B) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S B) (↑f : R →+* S))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑g : A →+* B) (algebraMap R A))
q : R[X]
h1 : Ne (α := S[X]) (map (↑f : R →+* S) q) 0
h2 :
  Eq.{u_2 + 1} (α := B)
    (((aeval (((↑g : A →+* B) : (a : A) → B) a) : S[X] →ₐ[S] B) : (a : S[X]) → B) (map (↑f : R →+* S) q) : B) (0 : B)
⊢ Eq.{u_2 + 1} (α := B) ((g : (a : A) → B) ((aeval a : (a : R[X]) → A) q : A) : B) ((g : (a : A) → B) 0 : B)
have change : Eq.{u_2 + 1} (α := B) (((↑g : A →+* B) : (a : A) → B) ((aeval a : (a : R[X]) → A) q : A) : B) ((g : (a : A) → B) 0 : B)
Tactic: change (g : A →+* B) _ = _
-- 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 : FunLike FRS R S
inst_7 : RingHomClass FRS R S
inst_8 : FunLike FAB A B
inst_9 : RingHomClass FAB A B
f : FRS
g : FAB
a : A
hf : Function.Surjective.{u + 1, u_1 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
hg : Function.Injective.{v + 1, u_2 + 1} (α := A) (β := B) (⇑g : (a : A) → B)
h :
  Eq (α := R →+* B) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S B) (↑f : R →+* S))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑g : A →+* B) (algebraMap R A))
q : R[X]
h1 : Ne (α := S[X]) (map (↑f : R →+* S) q) 0
h2 :
  Eq.{u_2 + 1} (α := B)
    (((aeval (((↑g : A →+* B) : (a : A) → B) a) : S[X] →ₐ[S] B) : (a : S[X]) → B) (map (↑f : R →+* S) q) : B) (0 : B)
⊢ Eq.{u_2 + 1} (α := B) (((↑g : A →+* B) : (a : A) → B) ((aeval a : (a : R[X]) → A) q : A) : B)
    ((g : (a : A) → B) 0 : B)
have rw : Eq.{u_2 + 1} (α := B) (((↑g : A →+* B) : (a : A) → B) ((aeval a : (a : R[X]) → A) q : A) : B) (0 : B)
Tactic: rw [map_zero, map_aeval_eq_aeval_map h, h2]
-- 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 : FunLike FRS R S
inst_7 : RingHomClass FRS R S
inst_8 : FunLike FAB A B
inst_9 : RingHomClass FAB A B
f : FRS
g : FAB
a : A
hf : Function.Surjective.{u + 1, u_1 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
hg : Function.Injective.{v + 1, u_2 + 1} (α := A) (β := B) (⇑g : (a : A) → B)
h :
  Eq (α := R →+* B) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S B) (↑f : R →+* S))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑g : A →+* B) (algebraMap R A))
q : R[X]
h1 : Ne (α := S[X]) (map (↑f : R →+* S) q) 0
h2 :
  Eq.{u_2 + 1} (α := B)
    (((aeval (((↑g : A →+* B) : (a : A) → B) a) : S[X] →ₐ[S] B) : (a : S[X]) → B) (map (↑f : R →+* S) q) : B) (0 : B)
rw : Eq.{u_2 + 1} (α := B) (((↑g : A →+* B) : (a : A) → B) ((aeval a : (a : R[X]) → A) q : A) : B) (0 : B)
rw₁ :
  Eq.{u_2 + 1} (α := B)
    (((aeval (((↑g : A →+* B) : (a : A) → B) a) : S[X] →ₐ[S] B) : (a : S[X]) → B) (map (↑f : R →+* S) q) : B) (0 : B)
⊢ Eq.{u_2 + 1} (α := B) (((↑g : A →+* B) : (a : A) → B) ((aeval a : (a : R[X]) → A) q : A) : B)
    ((g : (a : A) → B) 0 : B)
have rw₂ : Eq.{u_2 + 1} (α := B) 0 0
Tactic: rw [map_zero, map_aeval_eq_aeval_map h, h2]
-- 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 : FunLike FRS R S
inst_7 : RingHomClass FRS R S
inst_8 : FunLike FAB A B
inst_9 : RingHomClass FAB A B
f : FRS
g : FAB
H : Algebra.Transcendental R A
hf : Function.Surjective.{u + 1, u_1 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
hg : Function.Injective.{v + 1, u_2 + 1} (α := A) (β := B) (⇑g : (a : A) → B)
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
have rw : ∀ (H : ¬Algebra.IsAlgebraic R A) (hf : Function.Surjective.{u + 1, u_1 + 1} (α := R) (β := S) (⇑f : (a : R) → S))
  (hg : Function.Injective.{v + 1, u_2 + 1} (α := A) (β := B) (⇑g : (a : A) → B))
  (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.IsAlgebraic S B
Tactic: rw [Algebra.transcendental_iff_not_isAlgebraic] at H ⊢
Cleared hypotheses: H, hf, hg, h