awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Goal:
A : Type u_1
B : Type u_6
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain A
inst_4 : IsIntegrallyClosed A
inst_5 : IsDomain B
inst_6 : IsIntegrallyClosed B
inst_7 : Module.Finite A B
inst_8 : IsTorsionFree A B
x : B
this_1 : FiniteDimensional.{u_1, u_6} (FractionRing A) (FractionRing B)
hx : ¬x = 0
K : Type u_1 := FractionRing A
L : Type u_6 := FractionRing B
E : Type u_6 := AlgebraicClosure L
this :
  IsIntegral A
    (HMul.hMul (α := L) (β := L) (((algebraMap B L : (a : B) → L) x)⁻¹ : L)
      (((algebraMap A L : A →+* L) : (a : A) → L) ((intNorm A B : (a : B) → A) x) : L))
y : B
hy :
  (algebraMap B L : (a : B) → L) y =
    HMul.hMul (α := L) (β := L) (((algebraMap B L : (a : B) → L) x)⁻¹ : L)
      (((algebraMap A L : A →+* L) : (a : A) → L) ((intNorm A B : (a : B) → A) x) : L)
a :
  Eq (α := L) ((algebraMap B L : (a : B) → L) ((algebraMap A B : (a : A) → B) ((intNorm A B : (a : B) → A) x : A)) : L)
    ((algebraMap B L : (a : B) → L) (x * y) : L)
⊢ (algebraMap A B : (a : A) → B) ((intNorm A B : (a : B) → A) x : A) = x * y

Tactic:
apply FaithfulSMul.algebraMap_injective B L

Premises used: FaithfulSMul.algebraMap_injective
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Goal:
A : Type u_1
B : Type u_6
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain A
inst_4 : IsIntegrallyClosed A
inst_5 : IsDomain B
inst_6 : IsIntegrallyClosed B
inst_7 : Module.Finite A B
inst_8 : IsTorsionFree A B
x : B
this_1 : FiniteDimensional.{u_1, u_6} (FractionRing A) (FractionRing B)
hx : ¬x = 0
K : Type u_1 := FractionRing A
L : Type u_6 := FractionRing B
E : Type u_6 := AlgebraicClosure L
this :
  IsIntegral A
    (HMul.hMul (α := L) (β := L) (((algebraMap B L : (a : B) → L) x)⁻¹ : L)
      (((algebraMap A L : A →+* L) : (a : A) → L) ((intNorm A B : (a : B) → A) x) : L))
y : B
hy :
  (algebraMap B L : (a : B) → L) y =
    HMul.hMul (α := L) (β := L) (((algebraMap B L : (a : B) → L) x)⁻¹ : L)
      (((algebraMap A L : A →+* L) : (a : A) → L) ((intNorm A B : (a : B) → A) x) : L)
a : Ne (α := L) ((algebraMap B L : (a : B) → L) x : L) (0 : L)
⊢ Eq (α := L) ((algebraMap B L : (a : B) → L) ((algebraMap A B : (a : A) → B) ((intNorm A B : (a : B) → A) x : A)) : L)
    ((algebraMap B L : (a : B) → L) (x * y) : L)

Tactic:
rw [← algebraMap_apply, map_mul, hy, mul_inv_cancel_left₀]

Premises used: mul_inv_cancel_left₀, map_mul, IsScalarTower.algebraMap_apply
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Goal:
A : Type u_1
B : Type u_6
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain A
inst_4 : IsIntegrallyClosed A
inst_5 : IsDomain B
inst_6 : IsIntegrallyClosed B
inst_7 : Module.Finite A B
inst_8 : IsTorsionFree A B
x : B
this_1 : FiniteDimensional.{u_1, u_6} (FractionRing A) (FractionRing B)
hx : ¬x = 0
K : Type u_1 := FractionRing A
L : Type u_6 := FractionRing B
E : Type u_6 := AlgebraicClosure L
this :
  IsIntegral A
    (HMul.hMul (α := L) (β := L) (((algebraMap B L : (a : B) → L) x)⁻¹ : L)
      (((algebraMap A L : A →+* L) : (a : A) → L) ((intNorm A B : (a : B) → A) x) : L))
y : B
hy :
  (algebraMap B L : (a : B) → L) y =
    HMul.hMul (α := L) (β := L) (((algebraMap B L : (a : B) → L) x)⁻¹ : L)
      (((algebraMap A L : A →+* L) : (a : A) → L) ((intNorm A B : (a : B) → A) x) : L)
⊢ Ne (α := L) ((algebraMap B L : (a : B) → L) x : L) (0 : L)

Tactic:
(map_ne_zero_iff _ (FaithfulSMul.algebraMap_injective B L)).mpr hx

Premises used: Iff.mpr, FaithfulSMul.algebraMap_injective, map_ne_zero_iff
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Goal:
A : Type u_1
B : Type u_6
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain A
inst_4 : IsIntegrallyClosed A
inst_5 : IsDomain B
inst_6 : IsIntegrallyClosed B
inst_7 : Module.Finite A B
inst_8 : IsTorsionFree A B
x : B
this_1 : FiniteDimensional.{u_1, u_6} (FractionRing A) (FractionRing B)
hx : ¬x = 0
K : Type u_1 := FractionRing A
L : Type u_6 := FractionRing B
E : Type u_6 := AlgebraicClosure L
this :
  IsIntegral A
    (HMul.hMul (α := L) (β := L) (((algebraMap B L : (a : B) → L) x)⁻¹ : L)
      (((algebraMap A L : A →+* L) : (a : A) → L) ((intNorm A B : (a : B) → A) x) : L))
y : B
hy :
  (algebraMap B L : (a : B) → L) y =
    HMul.hMul (α := L) (β := L) (((algebraMap B L : (a : B) → L) x)⁻¹ : L)
      (((algebraMap A L : A →+* L) : (a : A) → L) ((intNorm A B : (a : B) → A) x) : L)
⊢ Ne (α := L) ((algebraMap B L : (a : B) → L) x : L) (0 : L)

Tactic:
exact (map_ne_zero_iff _ (FaithfulSMul.algebraMap_injective B L)).mpr hx

Premises used: Iff.mpr, FaithfulSMul.algebraMap_injective, map_ne_zero_iff
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Goal:
A : Type u_1
B : Type u_6
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain A
inst_4 : IsIntegrallyClosed A
inst_5 : IsDomain B
inst_6 : IsIntegrallyClosed B
inst_7 : Module.Finite A B
inst_8 : IsTorsionFree A B
x : B
this : FiniteDimensional.{u_1, u_6} (FractionRing A) (FractionRing B)
hx : ¬x = 0
K : Type u_1 := FractionRing A
L : Type u_6 := FractionRing B
E : Type u_6 := AlgebraicClosure L
neg :
  IsIntegral A
    (HMul.hMul (α := L) (β := L) (((algebraMap B L : (a : B) → L) x)⁻¹ : L)
      (((algebraMap A L : A →+* L) : (a : A) → L) ((intNorm A B : (a : B) → A) x) : L))
⊢ x ∣ (algebraMap A B : (a : A) → B) ((intNorm A B : (a : B) → A) x : A)

Tactic:
suffices IsIntegral A ((algebraMap B L x)⁻¹ * (algebraMap A L (intNorm A B x))) by
    obtain ⟨y, hy⟩ := IsIntegrallyClosed.isIntegral_iff.mp <|
      _root_.IsIntegral.tower_top (A := B) this
    refine ⟨y, ?_⟩
    apply FaithfulSMul.algebraMap_injective B L
    rw [← algebraMap_apply, map_mul, hy, mul_inv_cancel_left₀]
    exact (map_ne_zero_iff _ (FaithfulSMul.algebraMap_injective B L)).mpr hx
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Goal:
A : Type u_1
B : Type u_6
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain A
inst_4 : IsIntegrallyClosed A
inst_5 : IsDomain B
inst_6 : IsIntegrallyClosed B
inst_7 : Module.Finite A B
inst_8 : IsTorsionFree A B
x : B
this : FiniteDimensional.{u_1, u_6} (FractionRing A) (FractionRing B)
hx : ¬x = 0
K : Type u_1 := FractionRing A
L : Type u_6 := FractionRing B
E : Type u_6 := AlgebraicClosure L
neg :
  IsIntegral A
    (HMul.hMul (α := E) (((algebraMap B E : (a : B) → E) x)⁻¹ : E)
      (HMul.hMul (α := E) ((algebraMap B E : (a : B) → E) x : E)
          ((aroots (minpoly K (B := L) ((algebraMap B L : (a : B) → L) x : L)) E).erase
              ((algebraMap B E : (a : B) → E) x)).prod ^
        finrank (↥K⟮((algebraMap B L : (a : B) → L) x : L)⟯) L))
neg₁ :
  Membership.mem (α := E) (aroots (minpoly K (B := L) ((algebraMap B L : (a : B) → L) x : L)) E)
    ((algebraMap B E : (a : B) → E) x : E)
⊢ IsIntegral A
    (HMul.hMul (α := L) (β := L) (((algebraMap B L : (a : B) → L) x)⁻¹ : L)
      (((algebraMap A L : A →+* L) : (a : A) → L) ((intNorm A B : (a : B) → A) x) : L))

Tactic:
rw [← isIntegral_algHom_iff (toAlgHom A L E)
    (FaithfulSMul.algebraMap_injective L E), coe_toAlgHom', map_mul, map_inv₀,
    algebraMap_apply A K L, algebraMap_intNorm (L := L), ← algebraMap_apply, ← algebraMap_apply,
    norm_eq_prod_roots _ (IsAlgClosed.splits _), ← Multiset.prod_erase
    (a := algebraMap B E x)]

Premises used: IsScalarTower.coe_toAlgHom', Algebra.algebraMap_intNorm, IsScalarTower.toAlgHom, isIntegral_algHom_iff, map_inv₀, map_mul, FaithfulSMul.algebraMap_injective, Multiset.prod_erase, IsAlgClosed.splits, Algebra.norm_eq_prod_roots, IsScalarTower.algebraMap_apply
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Goal:
A : Type u_1
B : Type u_6
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain A
inst_4 : IsIntegrallyClosed A
inst_5 : IsDomain B
inst_6 : IsIntegrallyClosed B
inst_7 : Module.Finite A B
inst_8 : IsTorsionFree A B
x : B
this : FiniteDimensional.{u_1, u_6} (FractionRing A) (FractionRing B)
hx : ¬x = 0
K : Type u_1 := FractionRing A
L : Type u_6 := FractionRing B
E : Type u_6 := AlgebraicClosure L
⊢ IsTorsionFree B E

Tactic:
have := IsTorsionFree.trans_faithfulSMul B L E
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Goal:
A : Type u_1
B : Type u_6
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain A
inst_4 : IsIntegrallyClosed A
inst_5 : IsDomain B
inst_6 : IsIntegrallyClosed B
inst_7 : Module.Finite A B
inst_8 : IsTorsionFree A B
x : B
this_1 : FiniteDimensional.{u_1, u_6} (FractionRing A) (FractionRing B)
hx : ¬x = 0
K : Type u_1 := FractionRing A
L : Type u_6 := FractionRing B
E : Type u_6 := AlgebraicClosure L
this : IsTorsionFree B E
neg :
  IsIntegral A
    (HPow.hPow (α := E) ((algebraMap B E : (a : B) → E) x : E)
        (finrank (↥K⟮((algebraMap B L : (a : B) → L) x : L)⟯) L - 1) *
      ((aroots (minpoly K (B := L) ((algebraMap B L : (a : B) → L) x : L)) E).erase
            ((algebraMap B E : (a : B) → E) x)).prod ^
        finrank (↥K⟮((algebraMap B L : (a : B) → L) x : L)⟯) L)
neg₁ : Ne (α := E) ((algebraMap B E : (a : B) → E) x : E) (0 : E)
⊢ IsIntegral A
    (HMul.hMul (α := E) (((algebraMap B E : (a : B) → E) x)⁻¹ : E)
      (HMul.hMul (α := E) ((algebraMap B E : (a : B) → E) x : E)
          ((aroots (minpoly K (B := L) ((algebraMap B L : (a : B) → L) x : L)) E).erase
              ((algebraMap B E : (a : B) → E) x)).prod ^
        finrank (↥K⟮((algebraMap B L : (a : B) → L) x : L)⟯) L))

Tactic:
rw [mul_pow, ← mul_pow_sub_one (Nat.pos_iff_ne_zero.1 Module.finrank_pos) (algebraMap B E x),
      mul_assoc, inv_mul_cancel_left₀]

Premises used: Algebra.algebraMap, Nat.pos_iff_ne_zero, inv_mul_cancel_left₀, mul_assoc, mul_pow_sub_one, Iff.mp, mul_pow, DFunLike.coe, Module.finrank_pos
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Goal:
A : Type u_1
B : Type u_6
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain A
inst_4 : IsIntegrallyClosed A
inst_5 : IsDomain B
inst_6 : IsIntegrallyClosed B
inst_7 : Module.Finite A B
inst_8 : IsTorsionFree A B
x : B
this_1 : FiniteDimensional.{u_1, u_6} (FractionRing A) (FractionRing B)
hx : ¬x = 0
K : Type u_1 := FractionRing A
L : Type u_6 := FractionRing B
E : Type u_6 := AlgebraicClosure L
this : IsTorsionFree B E
⊢ IsIntegral A
    (HPow.hPow (α := E) ((algebraMap B E : (a : B) → E) x : E)
        (finrank (↥K⟮((algebraMap B L : (a : B) → L) x : L)⟯) L - 1) *
      ((aroots (minpoly K (B := L) ((algebraMap B L : (a : B) → L) x : L)) E).erase
            ((algebraMap B E : (a : B) → E) x)).prod ^
        finrank (↥K⟮((algebraMap B L : (a : B) → L) x : L)⟯) L)

Tactic:
IsIntegral.mul (IsIntegral.pow ?_ _)
        (IsIntegral.pow (IsIntegral.multiset_prod (fun a ha ↦ ⟨minpoly A x, minpoly.monic
          (IsIntegral.isIntegral x), ?_⟩)) _)

Premises used: Algebra.IsIntegral.isIntegral, minpoly.monic, IsIntegral.mul, IsIntegral.pow, IsIntegral.multiset_prod, minpoly, And.intro, Exists.intro
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Goal:
A : Type u_1
B : Type u_6
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain A
inst_4 : IsIntegrallyClosed A
inst_5 : IsDomain B
inst_6 : IsIntegrallyClosed B
inst_7 : Module.Finite A B
inst_8 : IsTorsionFree A B
x : B
this_1 : FiniteDimensional.{u_1, u_6} (FractionRing A) (FractionRing B)
hx : ¬x = 0
K : Type u_1 := FractionRing A
L : Type u_6 := FractionRing B
E : Type u_6 := AlgebraicClosure L
this : IsTorsionFree B E
neg : IsIntegral A (A := E) ((algebraMap B E : (a : B) → E) x : E)
neg₁ :
  ∀ (a : E)
    (ha :
      a ∈
        (aroots (minpoly K (B := L) ((algebraMap B L : (a : B) → L) x : L)) E).erase
          ((algebraMap B E : (a : B) → E) x)),
    eval₂ (algebraMap A E) a (minpoly A x) = 0
⊢ IsIntegral A
    (HPow.hPow (α := E) ((algebraMap B E : (a : B) → E) x : E)
        (finrank (↥K⟮((algebraMap B L : (a : B) → L) x : L)⟯) L - 1) *
      ((aroots (minpoly K (B := L) ((algebraMap B L : (a : B) → L) x : L)) E).erase
            ((algebraMap B E : (a : B) → E) x)).prod ^
        finrank (↥K⟮((algebraMap B L : (a : B) → L) x : L)⟯) L)

Tactic:
refine IsIntegral.mul (IsIntegral.pow ?_ _)
        (IsIntegral.pow (IsIntegral.multiset_prod (fun a ha ↦ ⟨minpoly A x, minpoly.monic
          (IsIntegral.isIntegral x), ?_⟩)) _)

Premises used: Algebra.IsIntegral.isIntegral, minpoly.monic, IsIntegral.mul, IsIntegral.pow, IsIntegral.multiset_prod, minpoly, And.intro, Exists.intro
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Goal:
A : Type u_1
B : Type u_6
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain A
inst_4 : IsIntegrallyClosed A
inst_5 : IsDomain B
inst_6 : IsIntegrallyClosed B
inst_7 : Module.Finite A B
inst_8 : IsTorsionFree A B
x : B
this_1 : FiniteDimensional.{u_1, u_6} (FractionRing A) (FractionRing B)
hx : ¬x = 0
K : Type u_1 := FractionRing A
L : Type u_6 := FractionRing B
E : Type u_6 := AlgebraicClosure L
this : IsTorsionFree B E
⊢ IsIntegral A (A := E) ((algebraMap B E : (a : B) → E) x : E)

Tactic:
(isIntegral_algebraMap_iff (isTorsionFree_iff_algebraMap_injective.1 this)).mpr
          (IsIntegral.isIntegral x)

Premises used: Iff.mpr, Algebra.IsIntegral.isIntegral, Module.isTorsionFree_iff_algebraMap_injective, isIntegral_algebraMap_iff, Iff.mp
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Goal:
A : Type u_1
B : Type u_6
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain A
inst_4 : IsIntegrallyClosed A
inst_5 : IsDomain B
inst_6 : IsIntegrallyClosed B
inst_7 : Module.Finite A B
inst_8 : IsTorsionFree A B
x : B
this_1 : FiniteDimensional.{u_1, u_6} (FractionRing A) (FractionRing B)
hx : ¬x = 0
K : Type u_1 := FractionRing A
L : Type u_6 := FractionRing B
E : Type u_6 := AlgebraicClosure L
this : IsTorsionFree B E
⊢ IsIntegral A (A := E) ((algebraMap B E : (a : B) → E) x : E)

Tactic:
exact (isIntegral_algebraMap_iff (isTorsionFree_iff_algebraMap_injective.1 this)).mpr
          (IsIntegral.isIntegral x)

Premises used: Iff.mpr, Algebra.IsIntegral.isIntegral, Module.isTorsionFree_iff_algebraMap_injective, isIntegral_algebraMap_iff, Iff.mp
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Goal:
A : Type u_1
B : Type u_6
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain A
inst_4 : IsIntegrallyClosed A
inst_5 : IsDomain B
inst_6 : IsIntegrallyClosed B
inst_7 : Module.Finite A B
inst_8 : IsTorsionFree A B
x : B
this_1 : FiniteDimensional.{u_1, u_6} (FractionRing A) (FractionRing B)
hx : ¬x = 0
K : Type u_1 := FractionRing A
L : Type u_6 := FractionRing B
E : Type u_6 := AlgebraicClosure L
this : IsTorsionFree B E
a : E
ha : a ∈ (aroots (minpoly K (B := L) ((algebraMap B L : (a : B) → L) x : L)) E).erase ((algebraMap B E : (a : B) → E) x)
⊢ a ∈ aroots (minpoly K (B := L) ((algebraMap B L : (a : B) → L) x : L)) E

Tactic:
replace ha := Multiset.erase_subset _ _ ha
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Goal:
A : Type u_1
B : Type u_6
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain A
inst_4 : IsIntegrallyClosed A
inst_5 : IsDomain B
inst_6 : IsIntegrallyClosed B
inst_7 : Module.Finite A B
inst_8 : IsTorsionFree A B
x : B
this_1 : FiniteDimensional.{u_1, u_6} (FractionRing A) (FractionRing B)
hx : ¬x = 0
K : Type u_1 := FractionRing A
L : Type u_6 := FractionRing B
E : Type u_6 := AlgebraicClosure L
this_2 : IsTorsionFree B E
a : E
ha : a ∈ aroots (minpoly K (B := L) ((algebraMap B L : (a : B) → L) x : L)) E
this : Eq.{u_6 + 1} (α := E) ((aeval a : (a : K[X]) → E) (map (algebraMap A K) (minpoly A x)) : E) (0 : E)
⊢ eval₂ (algebraMap A E) a (minpoly A x) = 0

Tactic:
simpa
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Goal:
A : Type u_1
B : Type u_6
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain A
inst_4 : IsIntegrallyClosed A
inst_5 : IsDomain B
inst_6 : IsIntegrallyClosed B
inst_7 : Module.Finite A B
inst_8 : IsTorsionFree A B
x : B
this_1 : FiniteDimensional.{u_1, u_6} (FractionRing A) (FractionRing B)
hx : ¬x = 0
K : Type u_1 := FractionRing A
L : Type u_6 := FractionRing B
E : Type u_6 := AlgebraicClosure L
this : IsTorsionFree B E
a : E
ha : a ∈ aroots (minpoly K (B := L) ((algebraMap B L : (a : B) → L) x : L)) E
neg : Eq.{u_6 + 1} (α := E) ((aeval a : (a : K[X]) → E) (map (algebraMap A K) (minpoly A x)) : E) (0 : E)
⊢ eval₂ (algebraMap A E) a (minpoly A x) = 0

Tactic:
suffices (aeval a) ((minpoly A x).map (algebraMap A K)) = 0 by simpa
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Goal:
A : Type u_1
B : Type u_6
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain A
inst_4 : IsIntegrallyClosed A
inst_5 : IsDomain B
inst_6 : IsIntegrallyClosed B
inst_7 : Module.Finite A B
inst_8 : IsTorsionFree A B
x : B
this_1 : FiniteDimensional.{u_1, u_6} (FractionRing A) (FractionRing B)
hx : ¬x = 0
K : Type u_1 := FractionRing A
L : Type u_6 := FractionRing B
E : Type u_6 := AlgebraicClosure L
this : IsTorsionFree B E
a : E
ha : a ∈ aroots (minpoly K (B := L) ((algebraMap B L : (a : B) → L) x : L)) E
neg :
  Eq.{u_6 + 1} (α := E) ((aeval a : (a : K[X]) → E) (minpoly K (B := L) ((algebraMap B L : (a : B) → L) x : L)) : E)
    (0 : E)
⊢ Eq.{u_6 + 1} (α := E) ((aeval a : (a : K[X]) → E) (map (algebraMap A K) (minpoly A x)) : E) (0 : E)

Tactic:
rw [← minpoly.isIntegrallyClosed_eq_field_fractions K L (IsIntegral.isIntegral x)]

Premises used: Algebra.IsIntegral.isIntegral, minpoly.isIntegrallyClosed_eq_field_fractions
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Goal:
A : Type u_1
B : Type u_6
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain A
inst_4 : IsIntegrallyClosed A
inst_5 : IsDomain B
inst_6 : IsIntegrallyClosed B
inst_7 : Module.Finite A B
inst_8 : IsTorsionFree A B
x : B
this_1 : FiniteDimensional.{u_1, u_6} (FractionRing A) (FractionRing B)
hx : ¬x = 0
K : Type u_1 := FractionRing A
L : Type u_6 := FractionRing B
E : Type u_6 := AlgebraicClosure L
this : IsTorsionFree B E
a : E
ha : a ∈ aroots (minpoly K (B := L) ((algebraMap B L : (a : B) → L) x : L)) E
⊢ ¬Eq (α := K[X]) (minpoly K (B := L) ((algebraMap B L : (a : B) → L) x : L)) 0 ∧
    Eq.{u_6 + 1} (α := E) ((aeval a : (a : K[X]) → E) (minpoly K (B := L) ((algebraMap B L : (a : B) → L) x : L)) : E)
      (0 : E)

Tactic:
simp only [mem_roots', ne_eq, Polynomial.map_eq_zero, IsRoot.def, eval_map_algebraMap] at ha

Premises used: Polynomial.IsRoot.def, ne_eq, Polynomial.mem_roots', Polynomial.eval_map_algebraMap, Polynomial.map_eq_zero
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Goal:
A : Type u_1
B : Type u_6
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain A
inst_4 : IsIntegrallyClosed A
inst_5 : IsDomain B
inst_6 : IsIntegrallyClosed B
inst_7 : Module.Finite A B
inst_8 : IsTorsionFree A B
x : B
this_1 : FiniteDimensional.{u_1, u_6} (FractionRing A) (FractionRing B)
hx : ¬x = 0
K : Type u_1 := FractionRing A
L : Type u_6 := FractionRing B
E : Type u_6 := AlgebraicClosure L
this : IsTorsionFree B E
a : E
ha :
  ¬Eq (α := K[X]) (minpoly K (B := L) ((algebraMap B L : (a : B) → L) x : L)) 0 ∧
    Eq.{u_6 + 1} (α := E) ((aeval a : (a : K[X]) → E) (minpoly K (B := L) ((algebraMap B L : (a : B) → L) x : L)) : E)
      (0 : E)
⊢ Eq.{u_6 + 1} (α := E) ((aeval a : (a : K[X]) → E) (minpoly K (B := L) ((algebraMap B L : (a : B) → L) x : L)) : E)
    (0 : E)

Tactic:
ha.2

Premises used: And.right
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Goal:
A : Type u_1
B : Type u_6
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain A
inst_4 : IsIntegrallyClosed A
inst_5 : IsDomain B
inst_6 : IsIntegrallyClosed B
inst_7 : Module.Finite A B
inst_8 : IsTorsionFree A B
x : B
this_1 : FiniteDimensional.{u_1, u_6} (FractionRing A) (FractionRing B)
hx : ¬x = 0
K : Type u_1 := FractionRing A
L : Type u_6 := FractionRing B
E : Type u_6 := AlgebraicClosure L
this : IsTorsionFree B E
a : E
ha :
  ¬Eq (α := K[X]) (minpoly K (B := L) ((algebraMap B L : (a : B) → L) x : L)) 0 ∧
    Eq.{u_6 + 1} (α := E) ((aeval a : (a : K[X]) → E) (minpoly K (B := L) ((algebraMap B L : (a : B) → L) x : L)) : E)
      (0 : E)
⊢ Eq.{u_6 + 1} (α := E) ((aeval a : (a : K[X]) → E) (minpoly K (B := L) ((algebraMap B L : (a : B) → L) x : L)) : E)
    (0 : E)

Tactic:
exact ha.2

Premises used: And.right
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Goal:
A : Type u_1
B : Type u_6
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain A
inst_4 : IsIntegrallyClosed A
inst_5 : IsDomain B
inst_6 : IsIntegrallyClosed B
inst_7 : Module.Finite A B
inst_8 : IsTorsionFree A B
x : B
this_1 : FiniteDimensional.{u_1, u_6} (FractionRing A) (FractionRing B)
hx : ¬x = 0
K : Type u_1 := FractionRing A
L : Type u_6 := FractionRing B
E : Type u_6 := AlgebraicClosure L
this : IsTorsionFree B E
⊢ Ne (α := E) ((algebraMap B E : (a : B) → E) x : E) (0 : E)

Tactic:
(map_ne_zero_iff _ (FaithfulSMul.algebraMap_injective B E)).mpr hx

Premises used: Iff.mpr, FaithfulSMul.algebraMap_injective, map_ne_zero_iff
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Goal:
A : Type u_1
B : Type u_6
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain A
inst_4 : IsIntegrallyClosed A
inst_5 : IsDomain B
inst_6 : IsIntegrallyClosed B
inst_7 : Module.Finite A B
inst_8 : IsTorsionFree A B
x : B
this_1 : FiniteDimensional.{u_1, u_6} (FractionRing A) (FractionRing B)
hx : ¬x = 0
K : Type u_1 := FractionRing A
L : Type u_6 := FractionRing B
E : Type u_6 := AlgebraicClosure L
this : IsTorsionFree B E
⊢ Ne (α := E) ((algebraMap B E : (a : B) → E) x : E) (0 : E)

Tactic:
exact (map_ne_zero_iff _ (FaithfulSMul.algebraMap_injective B E)).mpr hx

Premises used: Iff.mpr, FaithfulSMul.algebraMap_injective, map_ne_zero_iff
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Goal:
A : Type u_1
B : Type u_6
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain A
inst_4 : IsIntegrallyClosed A
inst_5 : IsDomain B
inst_6 : IsIntegrallyClosed B
inst_7 : Module.Finite A B
inst_8 : IsTorsionFree A B
x : B
this : FiniteDimensional.{u_1, u_6} (FractionRing A) (FractionRing B)
hx : ¬x = 0
K : Type u_1 := FractionRing A
L : Type u_6 := FractionRing B
E : Type u_6 := AlgebraicClosure L
neg :
  ¬Eq (α := K[X]) (minpoly K (B := L) ((algebraMap B L : (a : B) → L) x : L)) 0 ∧
    Eq.{u_6 + 1} (α := E)
      (((aeval ((algebraMap B E : (a : B) → E) x) : K[X] →ₐ[K] E) : (a : K[X]) → E)
          (minpoly K (B := L) ((algebraMap B L : (a : B) → L) x : L)) :
        E)
      (0 : E)
⊢ Membership.mem (α := E) (aroots (minpoly K (B := L) ((algebraMap B L : (a : B) → L) x : L)) E)
    ((algebraMap B E : (a : B) → E) x : E)

Tactic:
simp only [mem_roots', ne_eq, Polynomial.map_eq_zero, IsRoot.def, eval_map_algebraMap]

Premises used: Polynomial.IsRoot.def, ne_eq, Polynomial.mem_roots', Polynomial.eval_map_algebraMap, Polynomial.map_eq_zero
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Goal:
A : Type u_1
B : Type u_6
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain A
inst_4 : IsIntegrallyClosed A
inst_5 : IsDomain B
inst_6 : IsIntegrallyClosed B
inst_7 : Module.Finite A B
inst_8 : IsTorsionFree A B
x : B
this : FiniteDimensional.{u_1, u_6} (FractionRing A) (FractionRing B)
hx : ¬x = 0
K : Type u_1 := FractionRing A
L : Type u_6 := FractionRing B
E : Type u_6 := AlgebraicClosure L
⊢ ¬Eq (α := K[X]) (minpoly K (B := L) ((algebraMap B L : (a : B) → L) x : L)) 0 ∧
    Eq.{u_6 + 1} (α := E)
      (((aeval ((algebraMap B E : (a : B) → E) x) : K[X] →ₐ[K] E) : (a : K[X]) → E)
          (minpoly K (B := L) ((algebraMap B L : (a : B) → L) x : L)) :
        E)
      (0 : E)

Tactic:
⟨minpoly.ne_zero (IsIntegral.isIntegral _), ?_⟩

Premises used: Algebra.IsIntegral.isIntegral, And.intro, minpoly.ne_zero