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
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:
fun halg ↦ H (halg.of_ringHom_of_comp_eq f g hf hg h)

Premises used: Algebra.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
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:
exact fun halg ↦ H (halg.of_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 : EquivLike FRS R S
inst_7 : RingEquivClass FRS R S
inst_8 : FunLike FAB A B
inst_9 : RingHomClass FAB A B
f : FRS
g : FAB
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))
a : A
⊢ IsAlgebraic.{u_1, u_2} S (A := B) ((g : (a : A) → B) a : B) ↔ IsAlgebraic R a

Tactic:
⟨fun H ↦ H.of_ringHom_of_comp_eq f g (EquivLike.surjective f) hg h,
    fun H ↦ H.ringHom_of_comp_eq f g (EquivLike.injective f) h⟩

Premises used: IsAlgebraic.ringHom_of_comp_eq, Iff.intro, EquivLike.surjective, EquivLike.injective, IsAlgebraic.of_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 : EquivLike FRS R S
inst_7 : RingEquivClass FRS R S
inst_8 : FunLike FAB A B
inst_9 : RingHomClass FAB A B
f : FRS
g : FAB
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))
a : A
⊢ Transcendental.{u_1, u_2} S (A := B) ((g : (a : A) → B) a : B) ↔ Transcendental R a

Tactic:
not_congr (isAlgebraic_ringHom_iff_of_comp_eq f g hg h)

Premises used: Transcendental, isAlgebraic_ringHom_iff_of_comp_eq, not_congr
-- 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 : 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.IsAlgebraic S B ↔ Algebra.IsAlgebraic R A

Tactic:
⟨fun H ↦ H.of_ringHom_of_comp_eq f g (EquivLike.surjective f) (EquivLike.injective g) h,
    fun H ↦ H.ringHom_of_comp_eq f g (EquivLike.injective f) (EquivLike.surjective g) h⟩

Premises used: Algebra.IsAlgebraic.of_ringHom_of_comp_eq, Algebra.IsAlgebraic.ringHom_of_comp_eq, Iff.intro, EquivLike.surjective, EquivLike.injective
-- 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 : 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))
simp_rw : ¬Algebra.IsAlgebraic S B ↔ ¬Algebra.IsAlgebraic R A
⊢ Algebra.Transcendental S B ↔ Algebra.Transcendental R A

Tactic:
simp_rw [Algebra.transcendental_iff_not_isAlgebraic,
    Algebra.isAlgebraic_ringHom_iff_of_comp_eq f g h]

Premises used: Algebra.transcendental_iff_not_isAlgebraic, Algebra.isAlgebraic_ringHom_iff_of_comp_eq
-- Module: Mathlib.RingTheory.Algebraic.Basic
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)
inst_5 : Algebra.IsAlgebraic R B
⊢ Algebra.IsAlgebraic R A

Tactic:
⟨fun _ ↦ (isAlgebraic_algHom_iff f hf).mp (Algebra.IsAlgebraic.isAlgebraic _)⟩

Premises used: Algebra.IsAlgebraic.isAlgebraic, isAlgebraic_algHom_iff, Algebra.IsAlgebraic.mk, Iff.mp, DFunLike.coe
-- Module: Mathlib.RingTheory.Algebraic.Basic
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
e : A ≃ₐ[R] B
inst_5 : Algebra.IsAlgebraic R A
⊢ Algebra.IsAlgebraic R B

Tactic:
Algebra.IsAlgebraic.of_injective e.symm.toAlgHom e.symm.injective

Premises used: AlgEquiv.toAlgHom, AlgEquiv.symm, AlgEquiv.injective, Algebra.IsAlgebraic.of_injective
-- Module: Mathlib.RingTheory.Algebraic.Basic
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
e : A ≃ₐ[R] B
⊢ Algebra.IsAlgebraic R A ↔ Algebra.IsAlgebraic R B

Tactic:
⟨fun _ ↦ e.isAlgebraic, fun _ ↦ e.symm.isAlgebraic⟩

Premises used: AlgEquiv.isAlgebraic, AlgEquiv.symm, Iff.intro
-- 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
inst_4 : Algebra R S
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
a : S
h : Function.Injective.{u_1 + 1, v + 1} (α := S) (β := A) (⇑(algebraMap S A) : (a : S) → A)
⊢ IsAlgebraic.{u, v} R (A := A) ((algebraMap S A : (a : S) → A) a : A) ↔ IsAlgebraic R a

Tactic:
isAlgebraic_algHom_iff (IsScalarTower.toAlgHom R S A) h

Premises used: isAlgebraic_algHom_iff, IsScalarTower.toAlgHom
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
S : Subalgebra R A
x : ↥S
⊢ IsAlgebraic R x ↔ IsAlgebraic R (↑x : A)

Tactic:
(isAlgebraic_algHom_iff S.val Subtype.val_injective).symm

Premises used: isAlgebraic_algHom_iff, Subtype.val_injective, Subalgebra.val, Iff.symm
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
S : Subalgebra R A
x : ↥S
⊢ Transcendental R x ↔ Transcendental R (↑x : A)

Tactic:
isAlgebraic_iff_isAlgebraic_val.not

Premises used: Iff.not, Transcendental, Subalgebra.isAlgebraic_iff_isAlgebraic_val
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
R : Type u
S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
halg : IsAlgebraic (↥⊥) x
r : R
⊢ ∃ (a : R),
    Eq.{u_1 + 1} (α := ↥⊥) ((algebraMap R ↥⊥ : (a : R) → ↥⊥) a : ↥⊥)
      (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) ⊥ x)
          ((AlgHom.toRingHom (Algebra.ofId R S) : (a : R) → S) r) ⋯ :
        ↥⊥)

Tactic:
⟨r, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
R : Type u
S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
halg : IsAlgebraic (↥⊥) x
r : R
⊢ ∃ (a : R),
    Eq.{u_1 + 1} (α := ↥⊥) ((algebraMap R ↥⊥ : (a : R) → ↥⊥) a : ↥⊥)
      (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) ⊥ x)
          ((AlgHom.toRingHom (Algebra.ofId R S) : (a : R) → S) r) ⋯ :
        ↥⊥)

Tactic:
exact ⟨r, rfl⟩
-- Module: Mathlib.RingTheory.Algebraic.Basic
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)
x : S
⊢ Eq (α := R →+* S)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap (↥⊥) S)
      (↑(Algebra.botEquivOfInjective h).symm : R →+* ↥⊥))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑(RingHom.id S) : S →+* S) (algebraMap R S))

Tactic:
rfl
-- Module: Mathlib.RingTheory.Algebraic.Basic
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
r : R
⊢ ∃ (a : R),
    Eq.{u_1 + 1} (α := ↥⊥) ((algebraMap R ↥⊥ : (a : R) → ↥⊥) a : ↥⊥)
      (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) ⊥ x)
          ((AlgHom.toRingHom (Algebra.ofId R S) : (a : R) → S) r) ⋯ :
        ↥⊥)

Tactic:
⟨r, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.RingTheory.Algebraic.Basic
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
r : R
⊢ ∃ (a : R),
    Eq.{u_1 + 1} (α := ↥⊥) ((algebraMap R ↥⊥ : (a : R) → ↥⊥) a : ↥⊥)
      (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) ⊥ x)
          ((AlgHom.toRingHom (Algebra.ofId R S) : (a : R) → S) r) ⋯ :
        ↥⊥)

Tactic:
exact ⟨r, rfl⟩
-- Module: Mathlib.RingTheory.Algebraic.Basic
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
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)
⊢ Eq (α := R →+* S)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap (↥⊥) S) (↑(algebraMap R ↥⊥) : R →+* ↥⊥))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑(RingHom.id S) : S →+* S) (algebraMap R S))

Tactic:
ext
-- Module: Mathlib.RingTheory.Algebraic.Basic
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
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:
rfl
-- Module: Mathlib.RingTheory.Algebraic.Basic
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)
simp_rw : (∀ (x : S), IsAlgebraic (↥⊥) x) ↔ ∀ (x : S), IsAlgebraic R x
⊢ Algebra.IsAlgebraic (↥⊥) S ↔ Algebra.IsAlgebraic R S

Tactic:
simp_rw [Algebra.isAlgebraic_def, isAlgebraic_bot_iff h]

Premises used: Algebra.isAlgebraic_def, Subalgebra.isAlgebraic_bot_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
inst_4 : Algebra R S
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : Nontrivial R
x : R
⊢ IsAlgebraic.{u, u_1} R (A := ↥⊥)
    (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) ⊥ x)
        ((AlgHom.toRingHom (Algebra.ofId R S) : (a : R) → S) x) ⋯ :
      ↥⊥)

Tactic:
isAlgebraic_algebraMap _

Premises used: isAlgebraic_algebraMap
-- 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
inst_4 : Algebra R S
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : Nontrivial R
x : R
⊢ IsAlgebraic.{u, u_1} R (A := ↥⊥)
    (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) ⊥ x)
        ((AlgHom.toRingHom (Algebra.ofId R S) : (a : R) → S) x) ⋯ :
      ↥⊥)

Tactic:
exact isAlgebraic_algebraMap _

Premises used: isAlgebraic_algebraMap
-- Module: Mathlib.RingTheory.Algebraic.Basic
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
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]
rwa₂ : p ≠ 0
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]
rwa₄ : p ≠ 0
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]
rwa₆ : p ≠ 0
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]
⊢ Ne (α := R[X]) ((expand R n : (a : R[X]) → R[X]) p : R[X]) (0 : R[X])

Tactic:
rwa [expand_ne_zero hn]

Premises used: Polynomial.expand_ne_zero
-- Module: Mathlib.RingTheory.Algebraic.Basic
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 rwa rwa₁ rwa₂ rwa₃ : Eq.{v + 1} (α := A) ((aeval (r ^ n) : (a : R[X]) → A) p : A) (0 : A)
⊢ Eq.{v + 1} (α := A) ((aeval r : (a : R[X]) → A) ((expand R n : (a : R[X]) → R[X]) p : R[X]) : A) (0 : A)

Tactic:
rwa [expand_aeval n p r]

Premises used: Polynomial.expand_aeval
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
r : A
ht : Transcendental R r
n : ℕ
hn : 0 < n
⊢ Transcendental R (r ^ n)

Tactic:
fun ht' ↦ ht <| ht'.of_pow hn

Premises used: IsAlgebraic.of_pow, Transcendental, Not
-- Module: Mathlib.RingTheory.Algebraic.Basic
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
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 _)
⊢ IsAlgebraic R (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _)

Tactic:
obtain ⟨p, hp, hp'⟩ := h
-- Module: Mathlib.RingTheory.Algebraic.Basic
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)
⊢ p.reverse ≠ 0

Tactic:
simpa using hp
-- Module: Mathlib.RingTheory.Algebraic.Basic
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)
refine :
  Eq.{u_1 + 1} (α := S)
    ((aeval (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _) : (a : R[X]) → S) p.reverse : S) (0 : S)
⊢ IsAlgebraic R (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _)

Tactic:
refine ⟨p.reverse, by simpa using hp, ?_⟩
-- Module: Mathlib.RingTheory.Algebraic.Basic
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
rwa₁ : eval₂ (algebraMap R S) x p = 0
rwa₂ rwa₃ rwa₄ rwa₅ : 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)

Tactic:
rwa [Polynomial.aeval_def, Polynomial.eval₂_reverse_eq_zero_iff, ← Polynomial.aeval_def]

Premises used: Polynomial.aeval_def, Polynomial.eval₂_reverse_eq_zero_iff
-- Module: Mathlib.RingTheory.Algebraic.Basic
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
⊢ IsAlgebraic R (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _) ↔ IsAlgebraic R x

Tactic:
⟨IsAlgebraic.invOf, IsAlgebraic.invOf⟩

Premises used: IsAlgebraic.invOf, Iff.intro
-- Module: Mathlib.RingTheory.Algebraic.Basic
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
neg : ∀ (hx : ¬x = 0), IsAlgebraic R x⁻¹ ↔ IsAlgebraic R x
⊢ IsAlgebraic R x⁻¹ ↔ IsAlgebraic R x

Tactic:
by_cases hx : x = 0
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
R : Type u
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
x : K
hx : x = 0
⊢ IsAlgebraic R x⁻¹ ↔ IsAlgebraic R x

Tactic:
simp [hx]
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
R : Type u
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
x : K
hx : ¬x = 0
this : Invertible x := invertibleOfNonzero hx
⊢ IsAlgebraic R x⁻¹ ↔ IsAlgebraic R x

Tactic:
IsAlgebraic.invOf_iff (R := R) (x := x)

Premises used: IsAlgebraic.invOf_iff
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
R : Type u
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
x : K
hx : ¬x = 0
this : Invertible x := invertibleOfNonzero hx
⊢ IsAlgebraic R x⁻¹ ↔ IsAlgebraic R x

Tactic:
exact IsAlgebraic.invOf_iff (R := R) (x := x)

Premises used: IsAlgebraic.invOf_iff
-- Module: Mathlib.RingTheory.Algebraic.Basic
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 = ⊥
rwa₃ rwa₄ rwa₅ rwa₆ : ¬p = 0
⊢ Ne (α := S[X]) (map (algebraMap R S) p) 0

Tactic:
rwa [Ne, ← degree_eq_bot, degree_map_eq_of_injective hinj, degree_eq_bot]

Premises used: Ne, Polynomial.degree_map_eq_of_injective, Polynomial.degree_eq_bot
-- Module: Mathlib.RingTheory.Algebraic.Basic
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)
⊢ Eq.{u_5 + 1} (α := A) ((aeval x : (a : S[X]) → A) (map (algebraMap R S) p) : A) (0 : A)

Tactic:
simpa
-- Module: Mathlib.RingTheory.Algebraic.Basic
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
⊢ IsScalarTower (↥A) (↥B) S

Tactic:
haveI : IsScalarTower A B S := .of_algebraMap_eq fun _ ↦ rfl
-- Module: Mathlib.RingTheory.Algebraic.Basic
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_1 : Algebra ↥A ↥B := (Subalgebra.inclusion hle).toAlgebra
this : IsScalarTower (↥A) (↥B) S
⊢ IsAlgebraic (↥B) x

Tactic:
h.extendScalars (Subalgebra.inclusion_injective hle)

Premises used: IsAlgebraic.extendScalars, Subalgebra.inclusion_injective
-- Module: Mathlib.RingTheory.Algebraic.Basic
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_1 : Algebra ↥A ↥B := (Subalgebra.inclusion hle).toAlgebra
this : IsScalarTower (↥A) (↥B) S
⊢ IsAlgebraic (↥B) x

Tactic:
exact h.extendScalars (Subalgebra.inclusion_injective hle)

Premises used: IsAlgebraic.extendScalars, Subalgebra.inclusion_injective
-- Module: Mathlib.RingTheory.Algebraic.Basic
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
h : Transcendental S x
⊢ Transcendental R x

Tactic:
fun H ↦ h (H.extendScalars hinj)

Premises used: IsAlgebraic.extendScalars, Transcendental, Not
-- Module: Mathlib.RingTheory.Algebraic.Basic
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 : Transcendental (↥B) x
⊢ Transcendental (↥A) x

Tactic:
fun H ↦ h (H.tower_top_of_subalgebra_le hle)

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

Tactic:
⟨fun _ ↦ (Algebra.IsAlgebraic.isAlgebraic _).extendScalars hinj⟩

Premises used: Algebra.IsAlgebraic.isAlgebraic, IsAlgebraic.extendScalars, Algebra.IsAlgebraic.mk
-- Module: Mathlib.RingTheory.Algebraic.Basic
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
inst_7 : Algebra.IsAlgebraic R A
hinj : Function.Injective.{u_4 + 1, u_5 + 1} (α := S) (β := A) (⇑(algebraMap S A) : (a : S) → A)
x : S
⊢ IsAlgebraic R x

Tactic:
simpa [isAlgebraic_algebraMap_iff hinj] using isAlgebraic (R := R) (A := A) (algebraMap _ _ x)

Premises used: Algebra.IsAlgebraic.isAlgebraic, Algebra.algebraMap, isAlgebraic_algebraMap_iff, DFunLike.coe
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
K : Type u_1
L : Type u_2
A : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Ring A
inst_3 : Algebra K L
inst_4 : Algebra L A
inst_5 : Algebra K A
inst_6 : IsScalarTower K L A
x : A
A_alg : IsAlgebraic K x
⊢ IsAlgebraic L x

Tactic:
A_alg.extendScalars (algebraMap K L).injective

Premises used: Algebra.algebraMap, IsAlgebraic.extendScalars, RingHom.injective
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
K : Type u_1
L : Type u_2
A : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Ring A
inst_3 : Algebra K L
inst_4 : Algebra L A
inst_5 : Algebra K A
inst_6 : IsScalarTower K L A
x : A
h : Transcendental L x
⊢ Transcendental K x

Tactic:
fun H ↦ h (H.tower_top L)

Premises used: IsAlgebraic.tower_top, Transcendental, Not