awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegralRestrict (goal)
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)
⊢ x ∣ (algebraMap A B : (a : A) → B) ((intNorm A B : (a : B) → A) x : A)
have pos : ∀ (hx : x = 0), x ∣ (algebraMap A B : (a : A) → B) ((intNorm A B : (a : B) → A) x : A)
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegralRestrict (goal)
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)
pos : ∀ (hx : x = 0), x ∣ (algebraMap A B : (a : A) → B) ((intNorm A B : (a : B) → A) x : A)
⊢ x ∣ (algebraMap A B : (a : A) → B) ((intNorm A B : (a : B) → A) x : A)
have neg : ∀ (hx : ¬x = 0), x ∣ (algebraMap A B : (a : A) → B) ((intNorm A B : (a : B) → A) x : A)
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegralRestrict (goal)
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))
⊢ x ∣ (algebraMap A B : (a : A) → B) ((intNorm A B : (a : B) → A) x : A)
have obtain : ∀ (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)),
  x ∣ (algebraMap A B : (a : A) → B) ((intNorm A B : (a : B) → A) x : A)
Tactic: obtain ⟨y, hy⟩ := IsIntegrallyClosed.isIntegral_iff.mp <|
      _root_.IsIntegral.tower_top (A := B) this
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegralRestrict (goal)
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)
⊢ x ∣ (algebraMap A B : (a : A) → B) ((intNorm A B : (a : B) → A) x : A)
have refine : (algebraMap A B : (a : A) → B) ((intNorm A B : (a : B) → A) x : A) = x * y
Tactic: refine ⟨y, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegralRestrict (goal)
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)
⊢ (algebraMap A B : (a : A) → B) ((intNorm A B : (a : B) → A) x : A) = x * y
have 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)
Tactic: apply FaithfulSMul.algebraMap_injective B L
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegralRestrict (goal)
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)
⊢ 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)
have a : Ne (α := L) ((algebraMap B L : (a : B) → L) x : L) (0 : L)
Tactic: rw [← algebraMap_apply, map_mul, hy, mul_inv_cancel_left₀]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegralRestrict (goal)
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
⊢ x ∣ (algebraMap A B : (a : A) → B) ((intNorm A B : (a : B) → A) x : A)
have 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))
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
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegralRestrict (goal)
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
⊢ 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))
have 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))
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)]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegralRestrict (goal)
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))
⊢ 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))
have 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)
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)]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegralRestrict (hypothesis)
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
⊢ 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))
have this₁ : IsTorsionFree B E
Tactic: have := IsTorsionFree.trans_faithfulSMul B L E
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegralRestrict (goal)
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
    (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))
have 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)
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₀]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegralRestrict (goal)
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)
⊢ 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))
have neg₁ : Ne (α := E) ((algebraMap B E : (a : B) → E) x : E) (0 : E)
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₀]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegralRestrict (goal)
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)
have neg : IsIntegral A (A := E) ((algebraMap B E : (a : B) → E) x : E)
Tactic: refine IsIntegral.mul (IsIntegral.pow ?_ _)
        (IsIntegral.pow (IsIntegral.multiset_prod (fun a ha ↦ ⟨minpoly A x, minpoly.monic
          (IsIntegral.isIntegral x), ?_⟩)) _)
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegralRestrict (goal)
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)
⊢ 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)
have 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
Tactic: refine IsIntegral.mul (IsIntegral.pow ?_ _)
        (IsIntegral.pow (IsIntegral.multiset_prod (fun a ha ↦ ⟨minpoly A x, minpoly.monic
          (IsIntegral.isIntegral x), ?_⟩)) _)
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegralRestrict (hypothesis)
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)
⊢ eval₂ (algebraMap A E) a (minpoly A x) = 0
have ha₁ : a ∈ aroots (minpoly K (B := L) ((algebraMap B L : (a : B) → L) x : L)) E
Tactic: replace ha := Multiset.erase_subset _ _ ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegralRestrict (goal)
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
⊢ eval₂ (algebraMap A E) a (minpoly A x) = 0
have neg : Eq.{u_6 + 1} (α := E) ((aeval a : (a : K[X]) → E) (map (algebraMap A K) (minpoly A x)) : E) (0 : E)
Tactic: suffices (aeval a) ((minpoly A x).map (algebraMap A K)) = 0 by simpa
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegralRestrict (goal)
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.{u_6 + 1} (α := E) ((aeval a : (a : K[X]) → E) (map (algebraMap A K) (minpoly A x)) : E) (0 : E)
have 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)
Tactic: rw [← minpoly.isIntegrallyClosed_eq_field_fractions K L (IsIntegral.isIntegral x)]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegralRestrict (hypothesis)
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.{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)
have 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)
Tactic: simp only [mem_roots', ne_eq, Polynomial.map_eq_zero, IsRoot.def, eval_map_algebraMap] at ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegralRestrict (goal)
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
⊢ 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)
have 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)
Tactic: simp only [mem_roots', ne_eq, Polynomial.map_eq_zero, IsRoot.def, eval_map_algebraMap]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegralRestrict (goal)
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)
have neg : 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: refine ⟨minpoly.ne_zero (IsIntegral.isIntegral _), ?_⟩