awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
H : ∀ (p : R[X]), Eq.{v + 1} (α := A) ((Polynomial.aeval r : (a : R[X]) → A) p : A) (0 : A) → p = 0
f : R[X]
hf : ∀ (p : R[X]), Eq (α := R[X]) ((Polynomial.aeval f : (a : R[X]) → R[X]) p : R[X]) (0 : R[X]) → p = 0
p : R[X]
hp :
  Eq.{v + 1} (α := A)
    (((Polynomial.aeval ((Polynomial.aeval r : (a : R[X]) → A) f) : R[X] →ₐ[R] A) : (a : R[X]) → A) p : A) (0 : A)
rwa :
  ∀ (hp : Eq.{v + 1} (α := A) ((Polynomial.aeval r : (a : R[X]) → A) (p.comp f) : A) (0 : A)),
    Eq.{v + 1} (α := A) ((Polynomial.aeval r : (a : R[X]) → A) ((Polynomial.aeval f : (a : R[X]) → R[X]) p : R[X]) : A)
      (0 : A)
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀
    (hp :
      Eq.{v + 1} (α := A)
        ((Polynomial.aeval r : (a : R[X]) → A) ((Polynomial.aeval f : (a : R[X]) → R[X]) p : R[X]) : A) (0 : A)),
    Eq.{v + 1} (α := A) ((Polynomial.aeval r : (a : R[X]) → A) ((Polynomial.aeval f : (a : R[X]) → R[X]) p : R[X]) : A)
      (0 : A)
⊢ Eq.{v + 1} (α := A) ((Polynomial.aeval r : (a : R[X]) → A) ((Polynomial.aeval f : (a : R[X]) → R[X]) p : R[X]) : A)
    (0 : A)

Tactic:
rwa [← aeval_comp, comp_eq_aeval] at hp

Premises used: Polynomial.aeval_comp, Polynomial.comp_eq_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
H : ∀ (p : R[X]), Eq.{v + 1} (α := A) ((Polynomial.aeval r : (a : R[X]) → A) p : A) (0 : A) → p = 0
f : R[X]
hf : ∀ (p : R[X]), Eq (α := R[X]) ((Polynomial.aeval f : (a : R[X]) → R[X]) p : R[X]) (0 : R[X]) → p = 0
p : R[X]
hp :
  Eq.{v + 1} (α := A)
    (((Polynomial.aeval ((Polynomial.aeval r : (a : R[X]) → A) f) : R[X] →ₐ[R] A) : (a : R[X]) → A) p : A) (0 : A)
⊢ p = 0

Tactic:
exact hf _ (H _ (by rwa [← aeval_comp, comp_eq_aeval] at hp))
-- 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
f : R[X]
H : Transcendental.{u, v} R (A := A) ((Polynomial.aeval r : (a : R[X]) → A) f : A)
rw :
  ∀
    (H :
      ∀ (p : R[X]),
        Eq.{v + 1} (α := A)
            (((Polynomial.aeval ((Polynomial.aeval r : (a : R[X]) → A) f) : R[X] →ₐ[R] A) : (a : R[X]) → A) p : A)
            (0 : A) →
          p = 0)
    (p : R[X]), Eq (α := R[X]) ((Polynomial.aeval f : (a : R[X]) → R[X]) p : R[X]) (0 : R[X]) → p = 0
⊢ Transcendental R f

Tactic:
rw [transcendental_iff] at H ⊢

Premises used: transcendental_iff
-- 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
f : R[X]
H :
  ∀ (p : R[X]),
    Eq.{v + 1} (α := A)
        (((Polynomial.aeval ((Polynomial.aeval r : (a : R[X]) → A) f) : R[X] →ₐ[R] A) : (a : R[X]) → A) p : A) (0 : A) →
      p = 0
p : R[X]
hp : Eq (α := R[X]) ((Polynomial.aeval f : (a : R[X]) → R[X]) p : R[X]) (0 : R[X])
rw : Eq.{v + 1} (α := A) ((Polynomial.aeval r : (a : R[X]) → A) (p.comp f) : A) (0 : A)
rw₁ :
  Eq.{v + 1} (α := A) ((Polynomial.aeval r : (a : R[X]) → A) ((Polynomial.aeval f : (a : R[X]) → R[X]) p : R[X]) : A)
    (0 : A)
rw₂ : Eq.{v + 1} (α := A) ((Polynomial.aeval r : (a : R[X]) → A) 0 : A) (0 : A)
rw₃ rw₄ : Eq.{v + 1} (α := A) 0 0
⊢ Eq.{v + 1} (α := A)
    (((Polynomial.aeval ((Polynomial.aeval r : (a : R[X]) → A) f) : R[X] →ₐ[R] A) : (a : R[X]) → A) p : A) (0 : A)

Tactic:
rw [← aeval_comp, comp_eq_aeval, hp, map_zero]

Premises used: Polynomial.aeval_comp, map_zero, Polynomial.comp_eq_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
f : R[X]
H :
  ∀ (p : R[X]),
    Eq.{v + 1} (α := A)
        (((Polynomial.aeval ((Polynomial.aeval r : (a : R[X]) → A) f) : R[X] →ₐ[R] A) : (a : R[X]) → A) p : A) (0 : A) →
      p = 0
p : R[X]
hp : Eq (α := R[X]) ((Polynomial.aeval f : (a : R[X]) → R[X]) p : R[X]) (0 : R[X])
⊢ p = 0

Tactic:
exact H p (by rw [← aeval_comp, comp_eq_aeval, hp, map_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
f : R[X]
H : IsAlgebraic.{u, v} R (A := A) ((aeval r : (a : R[X]) → A) f : A)
hf : Transcendental R f
contrapose : ∀ (H : ¬IsAlgebraic R r), ¬IsAlgebraic.{u, v} R (A := A) ((aeval r : (a : R[X]) → A) f : A)
⊢ IsAlgebraic R r

Tactic:
contrapose H
-- 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
f : R[X]
hf : Transcendental R f
H : ¬IsAlgebraic R r
⊢ ¬IsAlgebraic.{u, v} R (A := A) ((aeval r : (a : R[X]) → A) f : A)

Tactic:
Transcendental.aeval_of_transcendental H hf

Premises used: Transcendental, Transcendental.aeval_of_transcendental
-- 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
f : R[X]
hf : Transcendental R f
H : ¬IsAlgebraic R r
⊢ ¬IsAlgebraic.{u, v} R (A := A) ((aeval r : (a : R[X]) → A) f : A)

Tactic:
exact Transcendental.aeval_of_transcendental H hf

Premises used: Transcendental.aeval_of_transcendental
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
R : Type u
inst : CommRing R
f : R[X]
hf : f.natDegree ≠ 0
hf' : Membership.mem (γ := Submonoid R) R⁰ f.leadingCoeff
⊢ Transcendental R f

Tactic:
simpa using (transcendental_X R).aeval f hf hf'

Premises used: Polynomial.transcendental_X, Transcendental.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
x : A
⊢ IsAlgebraic R x ↔ ¬Function.Injective.{u + 1, v + 1} (α := R[X]) (β := A) (⇑(aeval x) : (a : R[X]) → A)

Tactic:
simp only [IsAlgebraic, injective_iff_map_eq_zero, not_forall, and_comm, exists_prop]

Premises used: IsAlgebraic, and_comm, exists_prop, injective_iff_map_eq_zero, Classical.not_forall
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
x : A
⊢ Transcendental R x ↔ Function.Injective.{u + 1, v + 1} (α := R[X]) (β := A) (⇑(aeval x) : (a : R[X]) → A)

Tactic:
isAlgebraic_iff_not_injective.not_left

Premises used: Transcendental, Iff.not_left, isAlgebraic_iff_not_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
x : A
rw :
  Function.Injective.{u + 1, v + 1} (α := R[X]) (β := A) (⇑(aeval x) : (a : R[X]) → A) ↔
    Eq (α := Ideal R[X]) (RingHom.ker (F := R[X] →ₐ[R] A) (aeval x)) ⊥
rw₁ rw₂ :
  Eq (α := Ideal R[X]) (RingHom.ker (F := R[X] →ₐ[R] A) (aeval x)) ⊥ ↔
    Eq (α := Ideal R[X]) (RingHom.ker (F := R[X] →ₐ[R] A) (aeval x)) ⊥
⊢ Transcendental R x ↔ Eq (α := Ideal R[X]) (RingHom.ker (F := R[X] →ₐ[R] A) (aeval x)) ⊥

Tactic:
rw [transcendental_iff_injective, RingHom.injective_iff_ker_eq_bot]

Premises used: transcendental_iff_injective, RingHom.injective_iff_ker_eq_bot
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
h : ¬Function.Injective.{u + 1, v + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
a : A
inj : Function.Injective.{u + 1, v + 1} (α := R[X]) (β := A) (⇑(aeval a) : (a : R[X]) → A)
⊢ Function.Injective.{u + 1, v + 1} (α := R) (β := A)
    (Function.comp (β := R[X]) (⇑(aeval a) : (a : R[X]) → A) (⇑C : (a : R) → R[X]))

Tactic:
inj.comp C_injective

Premises used: Function.Injective.comp, Polynomial.C_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
h : ¬Function.Injective.{u + 1, v + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
a : A
inj : Function.Injective.{u + 1, v + 1} (α := R[X]) (β := A) (⇑(aeval a) : (a : R[X]) → A)
h₁ :
  Eq (α := R → A) (⇑(algebraMap R A) : (a : R) → A)
    (Function.comp (β := R[X]) (⇑(aeval a) : (a : R[X]) → A) (⇑C : (a : R) → R[X]))
⊢ Function.Injective.{u + 1, v + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)

Tactic:
convert! inj.comp C_injective

Premises used: Function.Injective.comp, Polynomial.C_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
h : ¬Function.Injective.{u + 1, v + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
a : A
inj : Function.Injective.{u + 1, v + 1} (α := R[X]) (β := A) (⇑(aeval a) : (a : R[X]) → A)
h₁ :
  ∀ (x : R),
    Eq.{v + 1} (α := A) ((algebraMap R A : (a : R) → A) x : A)
      (Function.comp (β := R[X]) (⇑(aeval a) : (a : R[X]) → A) (⇑C : (a : R) → R[X]) x : A)
⊢ Eq (α := R → A) (⇑(algebraMap R A) : (a : R) → A)
    (Function.comp (β := R[X]) (⇑(aeval a) : (a : R[X]) → A) (⇑C : (a : R) → R[X]))

Tactic:
ext
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
h : ¬Function.Injective.{u + 1, v + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
a : A
inj : Function.Injective.{u + 1, v + 1} (α := R[X]) (β := A) (⇑(aeval a) : (a : R[X]) → A)
x : R
⊢ Eq.{v + 1} (α := A) ((algebraMap R A : (a : R) → A) x : A)
    (Function.comp (β := R[X]) (⇑(aeval a) : (a : R[X]) → A) (⇑C : (a : R) → R[X]) x : A)

Tactic:
simp
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
h : Algebra.Transcendental R A
⊢ ¬Algebra.IsAlgebraic R A

Tactic:
rw [transcendental_iff_not_isAlgebraic] at h

Premises used: Algebra.transcendental_iff_not_isAlgebraic
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
h : ¬Algebra.IsAlgebraic R A
contrapose :
  ∀ (h : ¬Function.Injective.{u + 1, v + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)),
    Algebra.IsAlgebraic R A
⊢ Function.Injective.{u + 1, v + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)

Tactic:
contrapose h
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
h : ¬Function.Injective.{u + 1, v + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
⊢ Algebra.IsAlgebraic R A

Tactic:
isAlgebraic_of_not_injective h

Premises used: Algebra.isAlgebraic_of_not_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
h : ¬Function.Injective.{u + 1, v + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
⊢ Algebra.IsAlgebraic R A

Tactic:
exact isAlgebraic_of_not_injective h

Premises used: Algebra.isAlgebraic_of_not_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
inst_3 : Nontrivial R
⊢ IsAlgebraic.{u, v} R (A := A) 0

Tactic:
⟨_, X_ne_zero, aeval_X 0⟩

Premises used: IsAlgebraic, And.intro, Exists.intro, Polynomial.X_ne_zero, OfNat.ofNat, Polynomial.aeval_X
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : Nontrivial R
x : R
rw :
  HSub.hSub (α := A) (β := A) (((aeval ((algebraMap R A : (a : R) → A) x) : R[X] →ₐ[R] A) : (a : R[X]) → A) X : A)
      (((aeval ((algebraMap R A : (a : R) → A) x) : R[X] →ₐ[R] A) : (a : R[X]) → A) ((C : (a : R) → R[X]) x : R[X]) :
        A) =
    0
rw₁ :
  HSub.hSub (α := A) (β := A) ((algebraMap R A : (a : R) → A) x : A)
      (((aeval ((algebraMap R A : (a : R) → A) x) : R[X] →ₐ[R] A) : (a : R[X]) → A) ((C : (a : R) → R[X]) x : R[X]) :
        A) =
    0
rw₂ : HSub.hSub (α := A) (β := A) ((algebraMap R A : (a : R) → A) x : A) ((algebraMap R A : (a : R) → A) x : A) = 0
rw₃ rw₄ : Eq.{v + 1} (α := A) 0 0
⊢ Eq.{v + 1} (α := A)
    (((aeval ((algebraMap R A : (a : R) → A) x) : R[X] →ₐ[R] A) : (a : R[X]) → A)
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) :
      A)
    (0 : A)

Tactic:
rw [map_sub, aeval_X, aeval_C, sub_self]

Premises used: map_sub, sub_self, Polynomial.aeval_C, Polynomial.aeval_X
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : Nontrivial R
rw : IsAlgebraic.{u, v} R (A := A) ((algebraMap R A : (a : R) → A) 1 : A)
⊢ IsAlgebraic.{u, v} R (A := A) 1

Tactic:
rw [← map_one (algebraMap R A)]

Premises used: Algebra.algebraMap, map_one
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : Nontrivial R
⊢ IsAlgebraic.{u, v} R (A := A) ((algebraMap R A : (a : R) → A) 1 : A)

Tactic:
isAlgebraic_algebraMap 1

Premises used: isAlgebraic_algebraMap, OfNat.ofNat
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : Nontrivial R
⊢ IsAlgebraic.{u, v} R (A := A) ((algebraMap R A : (a : R) → A) 1 : A)

Tactic:
exact isAlgebraic_algebraMap 1

Premises used: isAlgebraic_algebraMap, OfNat.ofNat
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : Nontrivial R
n : ℕ
rw : IsAlgebraic.{u, v} R (A := A) ((algebraMap R A : (a : R) → A) (↑n : R) : A)
rw₁ : R →+* A
⊢ IsAlgebraic.{u, v} R (A := A) (↑n : A)

Tactic:
rw [← map_natCast (_ : R →+* A) n]

Premises used: map_natCast
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : Nontrivial R
n : ℕ
⊢ IsAlgebraic.{u, v} R (A := A) ((algebraMap R A : (a : R) → A) (↑n : R) : A)

Tactic:
isAlgebraic_algebraMap (Nat.cast n)

Premises used: Nat.cast, 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
inst_3 : Nontrivial R
n : ℤ
rw : IsAlgebraic.{u, v} R (A := A) ((algebraMap R A : (a : R) → A) (↑n : R) : A)
⊢ IsAlgebraic.{u, v} R (A := A) (↑n : A)

Tactic:
rw [← map_intCast (algebraMap R A)]

Premises used: Algebra.algebraMap, map_intCast
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : Nontrivial R
n : ℤ
⊢ IsAlgebraic.{u, v} R (A := A) ((algebraMap R A : (a : R) → A) (↑n : R) : A)

Tactic:
isAlgebraic_algebraMap (Int.cast n)

Premises used: Int.cast, 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
inst_3 : Nontrivial R
n : ℤ
⊢ IsAlgebraic.{u, v} R (A := A) ((algebraMap R A : (a : R) → A) (↑n : R) : A)

Tactic:
exact isAlgebraic_algebraMap (Int.cast n)

Premises used: Int.cast, isAlgebraic_algebraMap
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
R : Type u
A : Type v
inst : DivisionRing A
inst_1 : Field R
inst_2 : Algebra R A
n : ℚ
rw : IsAlgebraic.{u, v} R (A := A) ((algebraMap R A : (a : R) → A) (↑n : R) : A)
⊢ IsAlgebraic.{u, v} R (A := A) (↑n : A)

Tactic:
rw [← map_ratCast (algebraMap R A)]

Premises used: map_ratCast, Algebra.algebraMap
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
R : Type u
A : Type v
inst : DivisionRing A
inst_1 : Field R
inst_2 : Algebra R A
n : ℚ
⊢ IsAlgebraic.{u, v} R (A := A) ((algebraMap R A : (a : R) → A) (↑n : R) : A)

Tactic:
isAlgebraic_algebraMap (Rat.cast n)

Premises used: Rat.cast, isAlgebraic_algebraMap
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
R : Type u
A : Type v
inst : DivisionRing A
inst_1 : Field R
inst_2 : Algebra R A
n : ℚ
⊢ IsAlgebraic.{u, v} R (A := A) ((algebraMap R A : (a : R) → A) (↑n : R) : A)

Tactic:
exact isAlgebraic_algebraMap (Rat.cast n)

Premises used: Rat.cast, isAlgebraic_algebraMap
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Field A
inst_2 : Algebra R A
p : R[X]
x : A
hx : x ∈ p.rootSet A
⊢ IsAlgebraic R x

Tactic:
⟨p, ne_zero_of_mem_rootSet hx, aeval_eq_zero_of_mem_rootSet hx⟩

Premises used: IsAlgebraic, Polynomial.aeval_eq_zero_of_mem_rootSet, Polynomial.ne_zero_of_mem_rootSet, And.intro, Exists.intro
-- 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 : Nontrivial R
M : Submonoid R
inst_4 : IsLocalization M S
x : S
inl : IsAlgebraic.{u, u_1} R (A := S) 0
inr : ∀ (hx : x ≠ 0), IsAlgebraic R x
⊢ IsAlgebraic R x

Tactic:
obtain rfl | hx := eq_or_ne x 0

Premises used: eq_or_ne, OfNat.ofNat, 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 : Nontrivial R
M : Submonoid R
inst_4 : IsLocalization M S
⊢ IsAlgebraic.{u, u_1} R (A := S) 0

Tactic:
isAlgebraic_zero

Premises used: isAlgebraic_zero
-- 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 : Nontrivial R
M : Submonoid R
inst_4 : IsLocalization M S
⊢ IsAlgebraic.{u, u_1} R (A := S) 0

Tactic:
exact isAlgebraic_zero

Premises used: isAlgebraic_zero
-- 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 : Nontrivial R
M : Submonoid R
inst_4 : IsLocalization M S
x : S
hx : x ≠ 0
inr :
  ∀ (r : R) (m : ↥M)
    (h :
      HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (↑(r, m).2 : R) : S) =
        (algebraMap R S : (a : R) → S) (r, m).1),
    IsAlgebraic R x
⊢ IsAlgebraic R x

Tactic:
have ⟨⟨r, m⟩, h⟩ := surj M x
-- 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 : Nontrivial R
M : Submonoid R
inst_4 : IsLocalization M S
x : S
hx : x ≠ 0
r : R
m : ↥M
h : HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (↑(r, m).2 : R) : S) = (algebraMap R S : (a : R) → S) (r, m).1
⊢ Eq.{u_1 + 1} (α := S)
    ((aeval x : (a : R[X]) → S)
        (HSub.hSub (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (↑m : R) : R[X]) X)
          ((C : (a : R) → R[X]) r : R[X])) :
      S)
    (0 : S)

Tactic:
simpa [sub_eq_zero, mul_comm x] using h

Premises used: sub_eq_zero, mul_comm
-- 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 : Nontrivial R
M : Submonoid R
inst_4 : IsLocalization M S
x : S
hx : x ≠ 0
r : R
m : ↥M
h : HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (↑(r, m).2 : R) : S) = (algebraMap R S : (a : R) → S) (r, m).1
inr :
  ∀
    (eq :
      HSub.hSub (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (↑m : R) : R[X]) X)
          ((C : (a : R) → R[X]) r : R[X]) =
        0),
    x = 0
⊢ IsAlgebraic R x

Tactic:
refine ⟨C m.1 * X - C r, fun eq ↦ hx ?_, by simpa [sub_eq_zero, mul_comm x] using 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
inst_3 : Nontrivial R
M : Submonoid R
inst_4 : IsLocalization M S
x : S
hx : x ≠ 0
r : R
m : ↥M
h : x = mk' S (r, m).1 (r, m).2
eq :
  HSub.hSub (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (↑m : R) : R[X]) X)
      ((C : (a : R) → R[X]) r : R[X]) =
    0
⊢ r = 0

Tactic:
simpa using congr(coeff $eq 0)
-- 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 : Nontrivial R
M : Submonoid R
inst_4 : IsLocalization M S
x : S
hx : x ≠ 0
r : R
m : ↥M
h : HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (↑(r, m).2 : R) : S) = (algebraMap R S : (a : R) → S) (r, m).1
eq :
  HSub.hSub (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (↑m : R) : R[X]) X)
      ((C : (a : R) → R[X]) r : R[X]) =
    0
inr :
  ∀ (h : x = mk' S (r, m).1 (r, m).2)
    (eq :
      HSub.hSub (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (↑m : R) : R[X]) X)
          ((C : (a : R) → R[X]) r : R[X]) =
        0),
    x = 0
inr₁ :
  ∀ (h : x = mk' S (0, m).1 (0, m).2)
    (eq :
      HSub.hSub (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (↑m : R) : R[X]) X)
          ((C : (a : R) → R[X]) r : R[X]) =
        0),
    x = 0
inr₂ inr₃ inr₄ inr₅ :
  ∀ (h : x = 0)
    (eq :
      HSub.hSub (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (↑m : R) : R[X]) X)
          ((C : (a : R) → R[X]) r : R[X]) =
        0),
    x = 0
⊢ x = 0

Tactic:
rwa [← eq_mk'_iff_mul_eq, show r = 0 by simpa using congr(coeff $eq 0), mk'_zero] at h

Premises used: IsLocalization.mk'_zero, IsLocalization.eq_mk'_iff_mul_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
inst_4 : Algebra R S
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
a : S
h : IsAlgebraic R a
f : R[X]
hf₁ : f ≠ 0
hf₂ : Eq.{u_1 + 1} (α := S) ((aeval a : (a : R[X]) → S) f : S) (0 : S)
rw : Eq.{v + 1} (α := A) ((algebraMap S A : (a : S) → A) ((aeval a : (a : R[X]) → S) f : S) : A) (0 : A)
rw₁ : Eq.{v + 1} (α := A) ((algebraMap S A : (a : S) → A) 0 : A) (0 : A)
rw₂ rw₃ : Eq.{v + 1} (α := A) 0 0
⊢ Eq.{v + 1} (α := A) (((aeval ((algebraMap S A : (a : S) → A) a) : R[X] →ₐ[R] A) : (a : R[X]) → A) f : A) (0 : A)

Tactic:
rw [aeval_algebraMap_apply, hf₂, map_zero]

Premises used: map_zero, Polynomial.aeval_algebraMap_apply
-- 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
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)
rw₃ rw₄ : Eq.{u_2 + 1} (α := B) 0 0
⊢ Eq.{u_2 + 1} (α := B) (((aeval ((f : (a : A) → B) a) : R[X] →ₐ[R] B) : (a : R[X]) → B) p : B) (0 : B)

Tactic:
rw [aeval_algHom, f.comp_apply, ha, map_zero]

Premises used: AlgHom.comp_apply, map_zero, Polynomial.aeval_algHom
-- 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)
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)
rwa₁ : Eq.{u_2 + 1} (α := B) ((f.comp (aeval a) : (a : R[X]) → B) p : B) (0 : B)
rwa₂ rwa₃ rwa₄ rwa₅ :
  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)

Tactic:
rwa [map_zero, ← f.comp_apply, ← aeval_algHom]

Premises used: AlgHom.comp_apply, map_zero, Polynomial.aeval_algHom
-- 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 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))
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)
⊢ IsAlgebraic.{u_1, u_2} S (A := B) ((g : (a : A) → B) a : B)

Tactic:
obtain ⟨p, h1, h2⟩ := halg