awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
s : S
h : Transcendental R s
refine_1 refine_1₁ refine_1₂ refine_1₃ :
  Transcendental R (↑(Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) R[s] x) s ⋯) : S)
⊢ Transcendental R (A := ↥R[s]) (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) R[s] x) s ⋯)

Tactic:
rwa [Subalgebra.transcendental_iff_transcendental_val]

Premises used: Subalgebra.transcendental_iff_transcendental_val
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
s : S
h : Transcendental R s
refine_2 :
  LE.le (α := Subalgebra R ↥R[s]) ⊤
    (AlgHom.range (aeval (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) R[s] x) s ⋯)))
⊢ Function.Surjective.{u_1 + 1, u_2 + 1} (α := R[X]) (β := ↥R[s])
    (⇑(aeval (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) R[s] x) s ⋯)) : (a : R[X]) → ↥R[s])

Tactic:
rw [← AlgHom.range_eq_top, _root_.eq_top_iff]

Premises used: eq_top_iff, AlgHom.range_eq_top
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
s : S
h : Transcendental R s
t : S
ht : Membership.mem (γ := Subalgebra R S) R[s] t
h_1 :
  Membership.mem (γ := Subalgebra R ↥R[s]) ⊤
    (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) R[s] x) t ht)
refine_2 :
  ∀ (r : R[X]) (ht : Membership.mem (α := S) (γ := Subalgebra R S) R[s] ((aeval s : (a : R[X]) → S) r : S)),
    Membership.mem.{u_2, u_2} (α := ↥R[s]) (γ := Subalgebra R ↥R[s]) ⊤
        (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) R[s] x) ((aeval s : (a : R[X]) → S) r) ht :
          ↥R[s]) →
      Membership.mem (α := ↥R[s]) (γ := Subalgebra R ↥R[s])
        (AlgHom.range (aeval (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) R[s] x) s ⋯)))
        (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) R[s] x) ((aeval s : (a : R[X]) → S) r) ht :
          ↥R[s])
⊢ Membership.mem (γ := Subalgebra R ↥R[s])
    (AlgHom.range (aeval (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) R[s] x) s ⋯)))
    (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) R[s] x) t ht)

Tactic:
obtain ⟨r, rfl⟩ := adjoin_mem_exists_aeval _ _ ht

Premises used: Algebra.adjoin_mem_exists_aeval, rfl
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
s : S
h : Transcendental R s
r : R[X]
ht : Membership.mem (α := S) (γ := Subalgebra R S) R[s] ((aeval s : (a : R[X]) → S) r : S)
h_1 :
  Membership.mem.{u_2, u_2} (α := ↥R[s]) (γ := Subalgebra R ↥R[s]) ⊤
    (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) R[s] x) ((aeval s : (a : R[X]) → S) r) ht :
      ↥R[s])
a :
  Eq.{u_2 + 1} (α := S)
    ((↑((AlgHom.toRingHom (aeval (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) R[s] x) s ⋯)) :
              (a : R[X]) → ↥R[s])
            r) :
        S) :
      S)
    ((↑(Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) R[s] x) ((aeval s : (a : R[X]) → S) r) ht) :
        S) :
      S)
⊢ Eq.{u_2 + 1} (α := ↥R[s])
    ((AlgHom.toRingHom (aeval (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) R[s] x) s ⋯)) :
          (a : R[X]) → ↥R[s])
        r :
      ↥R[s])
    (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) R[s] x) ((aeval s : (a : R[X]) → S) r) ht :
      ↥R[s])

Tactic:
ext
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
s : S
h : Transcendental R s
r : R[X]
ht : Membership.mem (α := S) (γ := Subalgebra R S) R[s] ((aeval s : (a : R[X]) → S) r : S)
h_1 :
  Membership.mem.{u_2, u_2} (α := ↥R[s]) (γ := Subalgebra R ↥R[s]) ⊤
    (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) R[s] x) ((aeval s : (a : R[X]) → S) r) ht :
      ↥R[s])
⊢ Eq.{u_2 + 1} (α := S)
    ((↑((AlgHom.toRingHom (aeval (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) R[s] x) s ⋯)) :
              (a : R[X]) → ↥R[s])
            r) :
        S) :
      S)
    ((↑(Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) R[s] x) ((aeval s : (a : R[X]) → S) r) ht) :
        S) :
      S)

Tactic:
simp
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
s : S
h : Transcendental R s
r : R[X]
ht : Membership.mem (α := S) (γ := Subalgebra R S) R[s] ((aeval s : (a : R[X]) → S) r : S)
h_1 :
  Membership.mem.{u_2, u_2} (α := ↥R[s]) (γ := Subalgebra R ↥R[s]) ⊤
    (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) R[s] x) ((aeval s : (a : R[X]) → S) r) ht :
      ↥R[s])
⊢ Membership.mem (α := ↥R[s]) (γ := Subalgebra R ↥R[s])
    (AlgHom.range (aeval (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) R[s] x) s ⋯)))
    (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) R[s] x) ((aeval s : (a : R[X]) → S) r) ht :
      ↥R[s])

Tactic:
exact ⟨r, by ext; simp⟩
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
s : S
h : Transcendental R s
⊢ Eq (α := RingHom.{u_1, u_2} R[X] ↥R[s]) (↑(algEquivOfTranscendental R s h) : R[X] →+* ↥R[s])
    (↑(aeval (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) R[s] x) s ⋯)) : R[X] →+* ↥R[s])

Tactic:
rfl

Premises used: AlgEquiv.ofBijective, MonoidHomClass.toMonoidHom, Polynomial.algEquivOfTranscendental, RingHomClass.toRingHom, Polynomial.aeval, Polynomial.eval₂AlgHom, rfl
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
s : S
h : Transcendental R s
f : R[X]
⊢ Eq.{u_2 + 1} (α := ↥R[s]) ((algEquivOfTranscendental R s h : (a : R[X]) → ↥R[s]) f : ↥R[s])
    ((aeval (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) R[s] x) s ⋯) : (a : R[X]) → ↥R[s]) f :
      ↥R[s])

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
s : S
h : Transcendental R s
⊢ Eq.{u_2 + 1} (α := ↥R[s]) ((algEquivOfTranscendental R s h : (a : R[X]) → ↥R[s]) X : ↥R[s])
    (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) R[s] x) s ⋯ : ↥R[s])

Tactic:
simp
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
s : S
h : Transcendental R s
f : R[X]
a :
  Eq.{u_2 + 1} (α := ↥R[s])
    (((algEquivOfTranscendental R s h).toEquiv : (a : R[X]) → ↥R[s])
        (((algEquivOfTranscendental R s h).symm : (a : ↥R[s]) → R[X])
          ((aeval (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) R[s] x) s ⋯) :
              (a : R[X]) → ↥R[s])
            f)) :
      ↥R[s])
    (((algEquivOfTranscendental R s h).toEquiv : (a : R[X]) → ↥R[s]) f : ↥R[s])
⊢ ((algEquivOfTranscendental R s h).symm : (a : ↥R[s]) → R[X])
      ((aeval (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) R[s] x) s ⋯) : (a : R[X]) → ↥R[s])
        f) =
    f

Tactic:
apply (algEquivOfTranscendental R s h).toEquiv.injective

Premises used: Polynomial.algEquivOfTranscendental, Equiv.injective, AlgEquiv.toEquiv
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
s : S
h : Transcendental R s
f : R[X]
⊢ Eq.{u_2 + 1} (α := ↥R[s])
    (((algEquivOfTranscendental R s h).toEquiv : (a : R[X]) → ↥R[s])
        (((algEquivOfTranscendental R s h).symm : (a : ↥R[s]) → R[X])
          ((aeval (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) R[s] x) s ⋯) :
              (a : R[X]) → ↥R[s])
            f)) :
      ↥R[s])
    (((algEquivOfTranscendental R s h).toEquiv : (a : R[X]) → ↥R[s]) f : ↥R[s])

Tactic:
simp
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
s : S
h : Transcendental R s
a :
  Eq.{u_2 + 1} (α := ↥R[s])
    (((algEquivOfTranscendental R s h).toEquiv : (a : R[X]) → ↥R[s])
        (((algEquivOfTranscendental R s h).symm : (a : ↥R[s]) → R[X])
          (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) R[s] x) s ⋯)) :
      ↥R[s])
    (((algEquivOfTranscendental R s h).toEquiv : (a : R[X]) → ↥R[s]) X : ↥R[s])
⊢ Eq.{u_1 + 1} (α := R[X])
    (((algEquivOfTranscendental R s h).symm : (a : ↥R[s]) → R[X])
        (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) R[s] x) s ⋯) :
      R[X])
    (X : R[X])

Tactic:
apply (algEquivOfTranscendental R s h).toEquiv.injective

Premises used: Polynomial.algEquivOfTranscendental, Equiv.injective, AlgEquiv.toEquiv
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
s : S
h : Transcendental R s
⊢ Eq.{u_2 + 1} (α := ↥R[s])
    (((algEquivOfTranscendental R s h).toEquiv : (a : R[X]) → ↥R[s])
        (((algEquivOfTranscendental R s h).symm : (a : ↥R[s]) → R[X])
          (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) R[s] x) s ⋯)) :
      ↥R[s])
    (((algEquivOfTranscendental R s h).toEquiv : (a : R[X]) → ↥R[s]) X : ↥R[s])

Tactic:
simp
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
inst_3 : UniqueFactorizationMonoid R
s : S
h : Transcendental R s
⊢ UniqueFactorizationMonoid.{u_2} ↥R[s]

Tactic:
(algEquivOfTranscendental R s h).toMulEquiv.uniqueFactorizationMonoid inferInstance

Premises used: inferInstance, AlgEquiv.toMulEquiv, Polynomial.algEquivOfTranscendental, MulEquiv.uniqueFactorizationMonoid
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
A : Type u_3
inst_1 : CommRing S
inst_2 : NoZeroDivisors S
inst_3 : Algebra R S
alg : Algebra.IsAlgebraic R S
inst_4 : Ring A
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : IsScalarTower R S A
inj : Injective.{u_1 + 1, u_3 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
⊢ Injective.{u_2 + 1, u_3 + 1} (α := S) (β := A) (⇑(algebraMap S A) : (a : S) → A)

Tactic:
(injective_iff_map_eq_zero _).mpr fun s eq ↦ of_not_not fun ne ↦ ?_

Premises used: Iff.mpr, injective_iff_map_eq_zero, of_not_not
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
A : Type u_3
inst_1 : CommRing S
inst_2 : NoZeroDivisors S
inst_3 : Algebra R S
alg : Algebra.IsAlgebraic R S
inst_4 : Ring A
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : IsScalarTower R S A
inj : Injective.{u_1 + 1, u_3 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
refine : ∀ (s : S) (eq : Eq.{u_3 + 1} (α := A) ((algebraMap S A : (a : S) → A) s : A) (0 : A)) (ne : ¬s = 0), False
⊢ Injective.{u_2 + 1, u_3 + 1} (α := S) (β := A) (⇑(algebraMap S A) : (a : S) → A)

Tactic:
refine (injective_iff_map_eq_zero _).mpr fun s eq ↦ of_not_not fun ne ↦ ?_

Premises used: Iff.mpr, injective_iff_map_eq_zero, of_not_not
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
A : Type u_3
inst_1 : CommRing S
inst_2 : NoZeroDivisors S
inst_3 : Algebra R S
alg : Algebra.IsAlgebraic R S
inst_4 : Ring A
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : IsScalarTower R S A
inj : Injective.{u_1 + 1, u_3 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
s : S
eq : Eq.{u_3 + 1} (α := A) ((algebraMap S A : (a : S) → A) s : A) (0 : A)
ne : ¬s = 0
have : ∀ (r : R) (ne : r ≠ 0) (dvd : s ∣ (algebraMap R S : (a : R) → S) r), False
⊢ False

Tactic:
have ⟨r, ne, dvd⟩ := (alg.1 s).exists_nonzero_dvd (mem_nonZeroDivisors_of_ne_zero ne)
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
A : Type u_3
inst_1 : CommRing S
inst_2 : NoZeroDivisors S
inst_3 : Algebra R S
alg : Algebra.IsAlgebraic R S
inst_4 : Ring A
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : IsScalarTower R S A
inj : Injective.{u_1 + 1, u_3 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
s : S
eq : Eq.{u_3 + 1} (α := A) ((algebraMap S A : (a : S) → A) s : A) (0 : A)
ne_1 : ¬s = 0
r : R
ne : r ≠ 0
dvd : s ∣ (algebraMap R S : (a : R) → S) r
⊢ False

Tactic:
ne (inj <| map_zero (algebraMap R A) ▸ zero_dvd_iff.mp ?_)

Premises used: Algebra.algebraMap, zero_dvd_iff, Eq.rec, map_zero, Iff.mp, Eq.symm
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
A : Type u_3
inst_1 : CommRing S
inst_2 : NoZeroDivisors S
inst_3 : Algebra R S
alg : Algebra.IsAlgebraic R S
inst_4 : Ring A
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : IsScalarTower R S A
inj : Injective.{u_1 + 1, u_3 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
s : S
eq : Eq.{u_3 + 1} (α := A) ((algebraMap S A : (a : S) → A) s : A) (0 : A)
ne_1 : ¬s = 0
r : R
ne : r ≠ 0
dvd : s ∣ (algebraMap R S : (a : R) → S) r
refine : Dvd.dvd.{u_3} (α := A) (0 : A) ((algebraMap R A : (a : R) → A) r : A)
⊢ False

Tactic:
refine ne (inj <| map_zero (algebraMap R A) ▸ zero_dvd_iff.mp ?_)

Premises used: Algebra.algebraMap, zero_dvd_iff, Eq.rec, map_zero, Iff.mp, Eq.symm
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
A : Type u_3
inst_1 : CommRing S
inst_2 : NoZeroDivisors S
inst_3 : Algebra R S
alg : Algebra.IsAlgebraic R S
inst_4 : Ring A
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : IsScalarTower R S A
inj : Injective.{u_1 + 1, u_3 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
s : S
eq : Eq.{u_3 + 1} (α := A) ((algebraMap S A : (a : S) → A) s : A) (0 : A)
ne_1 : ¬s = 0
r : R
ne : r ≠ 0
dvd : s ∣ (algebraMap R S : (a : R) → S) r
simp_rw : Dvd.dvd.{u_3} (α := A) ((algebraMap S A : (a : S) → A) s : A) ((algebraMap R A : (a : R) → A) r : A)
simp_rw₁ :
  Dvd.dvd.{u_3} (α := A) ((algebraMap S A : (a : S) → A) s : A)
    ((algebraMap S A : (a : S) → A) ((algebraMap R S : (a : R) → S) r : S) : A)
⊢ Dvd.dvd.{u_3} (α := A) (0 : A) ((algebraMap R A : (a : R) → A) r : A)

Tactic:
simp_rw [← eq, IsScalarTower.algebraMap_apply R S A, map_dvd (algebraMap S A) dvd]

Premises used: Algebra.algebraMap, map_dvd, IsScalarTower.algebraMap_apply
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
A : Type u_3
inst_1 : CommRing S
inst_2 : NoZeroDivisors S
inst_3 : Algebra R S
alg : Algebra.IsAlgebraic R S
inst_4 : Ring A
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : IsScalarTower R S A
inst_8 : FaithfulSMul R A
rw :
  Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A) →
    Function.Injective.{u_2 + 1, u_3 + 1} (α := S) (β := A) (⇑(algebraMap S A) : (a : S) → A)
⊢ FaithfulSMul S A

Tactic:
rw [faithfulSMul_iff_algebraMap_injective] at *

Premises used: faithfulSMul_iff_algebraMap_injective
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
A : Type u_3
inst_1 : CommRing S
inst_2 : NoZeroDivisors S
inst_3 : Algebra R S
alg : Algebra.IsAlgebraic R S
inst_4 : Ring A
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : IsScalarTower R S A
inst_8 : Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
⊢ Function.Injective.{u_2 + 1, u_3 + 1} (α := S) (β := A) (⇑(algebraMap S A) : (a : S) → A)

Tactic:
injective_tower_top S ‹_›

Premises used: Algebra.IsAlgebraic.injective_tower_top
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
A : Type u_3
inst_1 : CommRing S
inst_2 : NoZeroDivisors S
inst_3 : Algebra R S
alg : Algebra.IsAlgebraic R S
inst_4 : Ring A
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : IsScalarTower R S A
inst_8 : Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
⊢ Function.Injective.{u_2 + 1, u_3 + 1} (α := S) (β := A) (⇑(algebraMap S A) : (a : S) → A)

Tactic:
exact injective_tower_top S ‹_›

Premises used: Algebra.IsAlgebraic.injective_tower_top
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x : L
p : K[X]
aeval_ne : Ne.{u_2 + 1} (α := L) ((aeval x : (a : K[X]) → L) p.divX : L) (0 : L)
rw :
  (aeval x : (a : K[X]) → L) p =
    HAdd.hAdd (β := L) (HMul.hMul (α := L) ((aeval x : (a : K[X]) → L) p.divX : L) x)
      ((algebraMap K L : (a : K) → L) (p.coeff 0) : L)
rw₁ : Ne.{u_2 + 1} (α := L) ((aeval x : (a : K[X]) → L) p.divX : L) (0 : L)
⊢ x⁻¹ =
    HDiv.hDiv (α := L) ((aeval x : (a : K[X]) → L) p.divX : L)
      (HSub.hSub (α := L) (β := L) ((aeval x : (a : K[X]) → L) p : L) ((algebraMap K L : (a : K) → L) (p.coeff 0) : L))

Tactic:
rw [inv_eq_iff_eq_inv, inv_div, eq_comm, div_eq_iff, sub_eq_iff_eq_add, mul_comm]

Premises used: eq_comm, div_eq_iff, sub_eq_iff_eq_add, mul_comm, inv_div, inv_eq_iff_eq_inv
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x : L
p : K[X]
aeval_ne : Ne.{u_2 + 1} (α := L) ((aeval x : (a : K[X]) → L) p.divX : L) (0 : L)
rw : ((aeval x : (a : K[X]) → L) (HAdd.hAdd (β := K[X]) (p.divX * X) ((C : (a : K) → K[X]) (p.coeff 0) : K[X])) : L)
| ((aeval x : (a : K[X]) → L) p : L)

Tactic:
rw [← divX_mul_X_add p]

Premises used: Polynomial.divX_mul_X_add
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x : L
p : K[X]
aeval_ne : Ne.{u_2 + 1} (α := L) ((aeval x : (a : K[X]) → L) p.divX : L) (0 : L)
conv_lhs :
  (aeval x : (a : K[X]) → L) (HAdd.hAdd (β := K[X]) (p.divX * X) ((C : (a : K) → K[X]) (p.coeff 0) : K[X])) =
    HAdd.hAdd (β := L) (HMul.hMul (α := L) ((aeval x : (a : K[X]) → L) p.divX : L) x)
      ((algebraMap K L : (a : K) → L) (p.coeff 0) : L)
⊢ (aeval x : (a : K[X]) → L) p =
    HAdd.hAdd (β := L) (HMul.hMul (α := L) ((aeval x : (a : K[X]) → L) p.divX : L) x)
      ((algebraMap K L : (a : K) → L) (p.coeff 0) : L)

Tactic:
conv_lhs => rw [← divX_mul_X_add p]

Premises used: Polynomial.divX_mul_X_add
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x : L
p : K[X]
aeval_ne : Ne.{u_2 + 1} (α := L) ((aeval x : (a : K[X]) → L) p.divX : L) (0 : L)
rw :
  HAdd.hAdd (α := L) (β := L) ((aeval x : (a : K[X]) → L) (p.divX * X) : L)
      ((aeval x : (a : K[X]) → L) ((C : (a : K) → K[X]) (p.coeff 0) : K[X]) : L) =
    HAdd.hAdd (β := L) (HMul.hMul (α := L) ((aeval x : (a : K[X]) → L) p.divX : L) x)
      ((algebraMap K L : (a : K) → L) (p.coeff 0) : L)
rw₁ :
  HAdd.hAdd (β := L)
      (HMul.hMul (α := L) (β := L) ((aeval x : (a : K[X]) → L) p.divX : L) ((aeval x : (a : K[X]) → L) X : L))
      ((aeval x : (a : K[X]) → L) ((C : (a : K) → K[X]) (p.coeff 0) : K[X]) : L) =
    HAdd.hAdd (β := L) (HMul.hMul (α := L) ((aeval x : (a : K[X]) → L) p.divX : L) x)
      ((algebraMap K L : (a : K) → L) (p.coeff 0) : L)
rw₂ :
  HAdd.hAdd (β := L) (HMul.hMul (α := L) ((aeval x : (a : K[X]) → L) p.divX : L) x)
      ((aeval x : (a : K[X]) → L) ((C : (a : K) → K[X]) (p.coeff 0) : K[X]) : L) =
    HAdd.hAdd (β := L) (HMul.hMul (α := L) ((aeval x : (a : K[X]) → L) p.divX : L) x)
      ((algebraMap K L : (a : K) → L) (p.coeff 0) : L)
rw₃ rw₄ :
  HAdd.hAdd (β := L) (HMul.hMul (α := L) ((aeval x : (a : K[X]) → L) p.divX : L) x)
      ((algebraMap K L : (a : K) → L) (p.coeff 0) : L) =
    HAdd.hAdd (β := L) (HMul.hMul (α := L) ((aeval x : (a : K[X]) → L) p.divX : L) x)
      ((algebraMap K L : (a : K) → L) (p.coeff 0) : L)
⊢ (aeval x : (a : K[X]) → L) (HAdd.hAdd (β := K[X]) (p.divX * X) ((C : (a : K) → K[X]) (p.coeff 0) : K[X])) =
    HAdd.hAdd (β := L) (HMul.hMul (α := L) ((aeval x : (a : K[X]) → L) p.divX : L) x)
      ((algebraMap K L : (a : K) → L) (p.coeff 0) : L)

Tactic:
rw [map_add, map_mul, aeval_X, aeval_C]

Premises used: map_add, map_mul, Polynomial.aeval_C, Polynomial.aeval_X
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x : L
p : K[X]
aeval_ne : Ne.{u_2 + 1} (α := L) ((aeval x : (a : K[X]) → L) p.divX : L) (0 : L)
⊢ Ne.{u_2 + 1} (α := L) ((aeval x : (a : K[X]) → L) p.divX : L) (0 : L)

Tactic:
aeval_ne
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x : L
p : K[X]
aeval_ne : Ne.{u_2 + 1} (α := L) ((aeval x : (a : K[X]) → L) p.divX : L) (0 : L)
⊢ Ne.{u_2 + 1} (α := L) ((aeval x : (a : K[X]) → L) p.divX : L) (0 : L)

Tactic:
exact aeval_ne
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x : L
p : K[X]
aeval_eq : Eq.{u_2 + 1} (α := L) ((aeval x : (a : K[X]) → L) p : L) (0 : L)
coeff_zero_ne : p.coeff 0 ≠ 0
⊢ x⁻¹ =
    HDiv.hDiv (α := L) ((aeval x : (a : K[X]) → L) p.divX : L)
      (HSub.hSub (α := L) (β := L) ((aeval x : (a : K[X]) → L) p : L) ((algebraMap K L : (a : K) → L) (p.coeff 0) : L))

Tactic:
inv_eq_of_aeval_divX_ne_zero (p := p) (L := L)
      (mt (fun h => (algebraMap K L).injective ?_) coeff_zero_ne)

Premises used: Algebra.algebraMap, mt, RingHom.injective, inv_eq_of_aeval_divX_ne_zero
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x : L
p : K[X]
aeval_eq : Eq.{u_2 + 1} (α := L) ((aeval x : (a : K[X]) → L) p : L) (0 : L)
coeff_zero_ne : p.coeff 0 ≠ 0
h :
  -HDiv.hDiv (α := L) (β := L) ((aeval x : (a : K[X]) → L) p.divX : L)
        ((algebraMap K L : (a : K) → L) (p.coeff 0) : L) =
    HDiv.hDiv (α := L) ((aeval x : (a : K[X]) → L) p.divX : L)
      (HSub.hSub (α := L) (β := L) ((aeval x : (a : K[X]) → L) p : L) ((algebraMap K L : (a : K) → L) (p.coeff 0) : L))
convert_2 :
  ∀ (h : Eq.{u_2 + 1} (α := L) ((aeval x : (a : K[X]) → L) p.divX : L) (0 : L)),
    Eq.{u_2 + 1} (α := L) (((algebraMap K L : K →+* L) : (a : K) → L) (p.coeff 0) : L)
      (((algebraMap K L : K →+* L) : (a : K) → L) 0 : L)
⊢ x⁻¹ =
    -HDiv.hDiv (α := L) (β := L) ((aeval x : (a : K[X]) → L) p.divX : L)
        ((algebraMap K L : (a : K) → L) (p.coeff 0) : L)

Tactic:
convert!
    inv_eq_of_aeval_divX_ne_zero (p := p) (L := L)
      (mt (fun h => (algebraMap K L).injective ?_) coeff_zero_ne) using 1

Premises used: Algebra.algebraMap, mt, RingHom.injective, inv_eq_of_aeval_divX_ne_zero
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x : L
p : K[X]
aeval_eq : Eq.{u_2 + 1} (α := L) ((aeval x : (a : K[X]) → L) p : L) (0 : L)
coeff_zero_ne : p.coeff 0 ≠ 0
h :
  -HDiv.hDiv (α := L) (β := L) ((aeval x : (a : K[X]) → L) p.divX : L)
        ((algebraMap K L : (a : K) → L) (p.coeff 0) : L) =
    HDiv.hDiv (α := L) ((aeval x : (a : K[X]) → L) p.divX : L)
      (HSub.hSub (α := L) (β := L) (0 : L) ((algebraMap K L : (a : K) → L) (p.coeff 0) : L))
h₁ :
  -HDiv.hDiv (α := L) (β := L) ((aeval x : (a : K[X]) → L) p.divX : L)
        ((algebraMap K L : (a : K) → L) (p.coeff 0) : L) =
    HDiv.hDiv (α := L) (β := L) ((aeval x : (a : K[X]) → L) p.divX : L)
      (-(algebraMap K L : (a : K) → L) (p.coeff 0) : L)
h₂ h₃ :
  -HDiv.hDiv (α := L) (β := L) ((aeval x : (a : K[X]) → L) p.divX : L)
        ((algebraMap K L : (a : K) → L) (p.coeff 0) : L) =
    -HDiv.hDiv (α := L) (β := L) ((aeval x : (a : K[X]) → L) p.divX : L)
        ((algebraMap K L : (a : K) → L) (p.coeff 0) : L)
⊢ -HDiv.hDiv (α := L) (β := L) ((aeval x : (a : K[X]) → L) p.divX : L)
        ((algebraMap K L : (a : K) → L) (p.coeff 0) : L) =
    HDiv.hDiv (α := L) ((aeval x : (a : K[X]) → L) p.divX : L)
      (HSub.hSub (α := L) (β := L) ((aeval x : (a : K[X]) → L) p : L) ((algebraMap K L : (a : K) → L) (p.coeff 0) : L))

Tactic:
rw [aeval_eq, zero_sub, div_neg]

Premises used: div_neg, zero_sub