awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Algebraic.Basic
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)

Tactic:
⟨p.map f, (Polynomial.map_ne_zero_iff hf).2 h1, ?_⟩

Premises used: Iff.mpr, IsAlgebraic, And.intro, Exists.intro, Polynomial.map, Polynomial.map_ne_zero_iff
-- Module: Mathlib.RingTheory.Algebraic.Basic
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)
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)
⊢ IsAlgebraic.{u_1, u_2} S (A := B) ((g : (a : A) → B) a : B)

Tactic:
refine ⟨p.map f, (Polynomial.map_ne_zero_iff hf).2 h1, ?_⟩
-- Module: Mathlib.RingTheory.Algebraic.Basic
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)
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)
⊢ 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:
change aeval ((g : A →+* B) a) _ = 0

Premises used: RingHomClass.toRingHom, Polynomial.aeval, DFunLike.coe
-- Module: Mathlib.RingTheory.Algebraic.Basic
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)
rw₂ rw₃ : Eq.{u_2 + 1} (α := B) 0 0
⊢ 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:
rw [← map_aeval_eq_aeval_map h, h2, map_zero]

Premises used: map_zero, Polynomial.map_aeval_eq_aeval_map
-- Module: Mathlib.RingTheory.Algebraic.Basic
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
H : Transcendental.{u_1, u_2} S (A := B) ((g : (a : A) → B) a : B)
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))
⊢ Transcendental R a

Tactic:
fun halg ↦ H (halg.ringHom_of_comp_eq f g hf h)

Premises used: Transcendental, IsAlgebraic.ringHom_of_comp_eq, Not
-- Module: Mathlib.RingTheory.Algebraic.Basic
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

Tactic:
⟨fun b ↦ ?_⟩

Premises used: Algebra.IsAlgebraic.mk
-- Module: Mathlib.RingTheory.Algebraic.Basic
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))
refine : ∀ (b : B), IsAlgebraic S b
⊢ Algebra.IsAlgebraic S B

Tactic:
refine ⟨fun b ↦ ?_⟩
-- Module: Mathlib.RingTheory.Algebraic.Basic
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
obtain : ∀ (a : A), IsAlgebraic.{u_1, u_2} S (A := B) ((g : (a : A) → B) a : B)
⊢ IsAlgebraic S b

Tactic:
obtain ⟨a, rfl⟩ := hg b

Premises used: rfl
-- Module: Mathlib.RingTheory.Algebraic.Basic
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))
a : A
⊢ IsAlgebraic.{u_1, u_2} S (A := B) ((g : (a : A) → B) a : B)

Tactic:
(Algebra.IsAlgebraic.isAlgebraic a).ringHom_of_comp_eq f g hf h

Premises used: Algebra.IsAlgebraic.isAlgebraic, IsAlgebraic.ringHom_of_comp_eq
-- Module: Mathlib.RingTheory.Algebraic.Basic
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))
a : A
⊢ IsAlgebraic.{u_1, u_2} S (A := B) ((g : (a : A) → B) a : B)

Tactic:
exact (Algebra.IsAlgebraic.isAlgebraic a).ringHom_of_comp_eq f g hf h

Premises used: Algebra.IsAlgebraic.isAlgebraic, IsAlgebraic.ringHom_of_comp_eq
-- Module: Mathlib.RingTheory.Algebraic.Basic
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))
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
⊢ Algebra.Transcendental R A

Tactic:
rw [Algebra.transcendental_iff_not_isAlgebraic] at H ⊢

Premises used: Algebra.transcendental_iff_not_isAlgebraic
-- Module: Mathlib.RingTheory.Algebraic.Basic
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.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:
fun halg ↦ H (halg.ringHom_of_comp_eq f g hf hg h)

Premises used: Algebra.IsAlgebraic.ringHom_of_comp_eq, Not
-- Module: Mathlib.RingTheory.Algebraic.Basic
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.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:
exact fun halg ↦ H (halg.ringHom_of_comp_eq f g hf hg h)
-- Module: Mathlib.RingTheory.Algebraic.Basic
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))
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
⊢ IsAlgebraic R a

Tactic:
obtain ⟨p, h1, h2⟩ := halg
-- Module: Mathlib.RingTheory.Algebraic.Basic
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)
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
⊢ IsAlgebraic R a

Tactic:
obtain ⟨q, rfl⟩ := map_surjective (f : R →+* S) hf p

Premises used: Polynomial.map_surjective, RingHomClass.toRingHom, rfl
-- Module: Mathlib.RingTheory.Algebraic.Basic
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)
h' : q = 0
⊢ False

Tactic:
simp [h'] at h1
-- Module: Mathlib.RingTheory.Algebraic.Basic
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)
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)
⊢ IsAlgebraic R a

Tactic:
refine ⟨q, fun h' ↦ by simp [h'] at h1, hg ?_⟩
-- Module: Mathlib.RingTheory.Algebraic.Basic
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)
    (((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

Premises used: RingHomClass.toRingHom, Polynomial.aeval, DFunLike.coe
-- Module: Mathlib.RingTheory.Algebraic.Basic
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)
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)
⊢ 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:
change (g : A →+* B) _ = _

Premises used: RingHomClass.toRingHom, DFunLike.coe
-- Module: Mathlib.RingTheory.Algebraic.Basic
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)
rw₂ rw₃ : Eq.{u_2 + 1} (α := B) 0 0
⊢ 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:
rw [map_zero, map_aeval_eq_aeval_map h, h2]

Premises used: map_zero, Polynomial.map_aeval_eq_aeval_map
-- Module: Mathlib.RingTheory.Algebraic.Basic
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
H : 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))
⊢ Transcendental.{u_1, u_2} S (A := B) ((g : (a : A) → B) a : B)

Tactic:
fun halg ↦ H (halg.of_ringHom_of_comp_eq f g hf hg h)

Premises used: Transcendental, IsAlgebraic.of_ringHom_of_comp_eq, Not
-- Module: Mathlib.RingTheory.Algebraic.Basic
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 S 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))
⊢ Algebra.IsAlgebraic R A

Tactic:
⟨fun a ↦ (Algebra.IsAlgebraic.isAlgebraic (g a)).of_ringHom_of_comp_eq f g hf hg h⟩

Premises used: Algebra.IsAlgebraic.isAlgebraic, Algebra.IsAlgebraic.mk, IsAlgebraic.of_ringHom_of_comp_eq, DFunLike.coe
-- Module: Mathlib.RingTheory.Algebraic.Basic
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))
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
⊢ Algebra.Transcendental S B

Tactic:
rw [Algebra.transcendental_iff_not_isAlgebraic] at H ⊢

Premises used: Algebra.transcendental_iff_not_isAlgebraic