awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.LinearDisjoint
Goal:
F : Type u
inst : Field F
A : Type v
inst_1 : Field A
B : Type w
inst_2 : Field B
inst_3 : Algebra F A
inst_4 : Algebra F B
H : IsField (A ⊗[F] B)
K : Type u_1
inst_5 : Field K
inst_6 : Algebra F K
fa : A →ₐ[F] K
fb : B →ₐ[F] K
⊢ IsField.{u_1} (↥fa.fieldRange.toSubalgebra ⊗[F] ↥fb.fieldRange.toSubalgebra)

Tactic:
exact Algebra.TensorProduct.congr (AlgEquiv.ofInjective fa fa.injective)
    (AlgEquiv.ofInjective fb fb.injective) |>.symm.toMulEquiv.isField H

Premises used: AlgEquiv.symm, AlgEquiv.toMulEquiv, RingHom.injective, AlgHom.toRingHom, AlgEquiv.ofInjective, MulEquiv.isField, Algebra.TensorProduct.congr
-- Module: Mathlib.FieldTheory.LinearDisjoint
Goal:
F : Type u
inst : Field F
A : Type v
inst_1 : Field A
B : Type w
inst_2 : Field B
inst_3 : Algebra F A
inst_4 : Algebra F B
inst_5 : IsDomain (A ⊗[F] B)
⊢ ∃ (K : Type (max v w)) (x : Field K) (x_1 : Algebra F K) (fa : A →ₐ[F] K) (fb : B →ₐ[F] K),
    fa.fieldRange.LinearDisjoint ↥fb.fieldRange

Tactic:
have ⟨K, inst1, inst2, fa, fb, _, _, H⟩ :=
    Subalgebra.LinearDisjoint.exists_field_of_isDomain_of_injective F A B
      (RingHom.injective _) (RingHom.injective _)
  ⟨K, inst1, inst2, fa, fb, linearDisjoint_iff'.2 H⟩

Premises used: Iff.mpr, _private.0.IntermediateField.LinearDisjoint.exists_field_of_isDomain.match_1, Algebra.algebraMap, IntermediateField.linearDisjoint_iff', Membership.mem, Exists, Subalgebra.LinearDisjoint.exists_field_of_isDomain_of_injective, Subtype, RingHom.injective, AlgHom.fieldRange, Exists.intro, IntermediateField.LinearDisjoint
-- Module: Mathlib.FieldTheory.LinearDisjoint
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type u_1
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : IsDomain (E ⊗[F] K)
halg : Algebra.IsAlgebraic F E ∨ Algebra.IsAlgebraic F K
L : Type (max v u_1)
w : Field L
w_1 : Algebra F L
fa : E →ₐ[F] L
fb : K →ₐ[F] L
hfa : Function.Injective (α := E) (β := L) (⇑fa : (a : E) → L)
hfb : Function.Injective (α := K) (β := L) (⇑fb : (a : K) → L)
H : fa.range.LinearDisjoint fb.range
rwa :
  ∀ (halg : Algebra.IsAlgebraic F ↥fa.range ∨ Algebra.IsAlgebraic F K) (fb : K →ₐ[F] L)
    (hfa : Function.Injective (α := E) (β := L) (⇑fa : (a : E) → L))
    (hfb : Function.Injective (α := K) (β := L) (⇑fb : (a : K) → L)) (H : fa.range.LinearDisjoint fb.range),
    Algebra.IsAlgebraic F ↥fa.fieldRange ∨ Algebra.IsAlgebraic F ↥fb.fieldRange
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀ (fb : K →ₐ[F] L) (halg : Algebra.IsAlgebraic F ↥fa.range ∨ Algebra.IsAlgebraic F ↥fb.range)
    (hfa : Function.Injective (α := E) (β := L) (⇑fa : (a : E) → L))
    (hfb : Function.Injective (α := K) (β := L) (⇑fb : (a : K) → L)) (H : fa.range.LinearDisjoint fb.range),
    Algebra.IsAlgebraic F ↥fa.fieldRange ∨ Algebra.IsAlgebraic F ↥fb.fieldRange
⊢ Algebra.IsAlgebraic F ↥fa.fieldRange ∨ Algebra.IsAlgebraic F ↥fb.fieldRange

Tactic:
rwa [(AlgEquiv.ofInjective fa hfa).isAlgebraic_iff,
          (AlgEquiv.ofInjective fb hfb).isAlgebraic_iff] at halg

Premises used: AlgEquiv.isAlgebraic_iff, AlgEquiv.ofInjective
-- Module: Mathlib.FieldTheory.LinearDisjoint
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A : IntermediateField F E
L : Type w
inst_3 : Field L
inst_4 : Algebra F L
inst_5 : Algebra L E
inst_6 : IsScalarTower F L E
H : A.LinearDisjoint L
halg : Algebra.IsAlgebraic.{u, v} F ↥A ∨ Algebra.IsAlgebraic F L
⊢ IsField (TensorProduct.{u, v, w} F (↥A) L)

Tactic:
have := H.isDomain
  Algebra.TensorProduct.isField_of_isAlgebraic F A L halg

Premises used: Set.Mem, Membership.mem, Subtype, Algebra.TensorProduct.isField_of_isAlgebraic, IntermediateField.LinearDisjoint.isDomain
-- Module: Mathlib.FieldTheory.LinearDisjoint
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A : Type u_1
B : Type u_2
inst_3 : Field A
inst_4 : Algebra F A
inst_5 : Field B
inst_6 : Algebra F B
fa : A →ₐ[F] E
fb : B →ₐ[F] E
H : fa.fieldRange.LinearDisjoint ↥fb.fieldRange
halg : Algebra.IsAlgebraic F A ∨ Algebra.IsAlgebraic F B
⊢ IsField (A ⊗[F] B)

Tactic:
have := H.isDomain'
  Algebra.TensorProduct.isField_of_isAlgebraic F A B halg

Premises used: Algebra.TensorProduct.isField_of_isAlgebraic, IntermediateField.LinearDisjoint.isDomain'
-- Module: Mathlib.FieldTheory.LinearDisjoint
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A : IntermediateField F E
L : Type w
inst_3 : Field L
inst_4 : Algebra F L
inst_5 : Algebra L E
inst_6 : IsScalarTower F L E
H : A.LinearDisjoint L
E' : Type u_1
inst_7 : Field E'
inst_8 : Algebra F E'
B : IntermediateField F E'
L' : Type u_2
inst_9 : Field L'
inst_10 : Algebra F L'
inst_11 : Algebra L' E'
inst_12 : IsScalarTower F L' E'
f1 : AlgEquiv.{u, v, u_1} F ↥A ↥B
f2 : L ≃ₐ[F] L'
halg : Algebra.IsAlgebraic.{u, v} F ↥A ∨ Algebra.IsAlgebraic F L
⊢ B.LinearDisjoint L'

Tactic:
.of_isField ((Algebra.TensorProduct.congr f1 f2).symm.toMulEquiv.isField
    (H.isField_of_isAlgebraic halg))

Premises used: AlgEquiv.symm, AlgEquiv.toMulEquiv, MulEquiv.isField, Algebra.TensorProduct.congr, IntermediateField.LinearDisjoint.of_isField, IntermediateField.LinearDisjoint.isField_of_isAlgebraic
-- Module: Mathlib.FieldTheory.LinearDisjoint
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A B : IntermediateField F E
inst_3 : FiniteDimensional F E
h₁ : A.LinearDisjoint ↥B
h₂ : A ⊔ B = ⊤
x : ↥B
rw :
  ∀ (h₁ : A.LinearDisjoint B.toSubalgebra) (h₂ : A ⊔ B = ⊤) (x : ↥B),
    Eq (α := ↥A) ((Algebra.trace (↥A) E : (a : E) → ↥A) ((algebraMap (↥B) E : (a : ↥B) → E) x) : ↥A)
      ((algebraMap F ↥A : (a : F) → ↥A) ((Algebra.trace F ↥B : (a : ↥B) → F) x) : ↥A)
⊢ Eq (α := ↥A) ((Algebra.trace (↥A) E : (a : E) → ↥A) ((algebraMap (↥B) E : (a : ↥B) → E) x) : ↥A)
    ((algebraMap F ↥A : (a : F) → ↥A) ((Algebra.trace F ↥B : (a : ↥B) → F) x) : ↥A)

Tactic:
rw [linearDisjoint_iff'] at h₁

Premises used: IntermediateField.linearDisjoint_iff'
-- Module: Mathlib.FieldTheory.LinearDisjoint
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A B : IntermediateField F E
inst_3 : FiniteDimensional F E
h₁ : A.LinearDisjoint B.toSubalgebra
h₂ : A ⊔ B = ⊤
x : ↥B
⊢ Eq (α := ↥A) ((Algebra.trace (↥A) E : (a : E) → ↥A) ((algebraMap (↥B) E : (a : ↥B) → E) x) : ↥A)
    ((algebraMap F ↥A : (a : F) → ↥A) ((Algebra.trace F ↥B : (a : ↥B) → F) x) : ↥A)

Tactic:
h₁.trace_algebraMap ?_ x

Premises used: Set.Mem, Subalgebra.LinearDisjoint.trace_algebraMap
-- Module: Mathlib.FieldTheory.LinearDisjoint
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A B : IntermediateField F E
inst_3 : FiniteDimensional F E
h₁ : A.LinearDisjoint B.toSubalgebra
h₂ : A ⊔ B = ⊤
x : ↥B
refine : A.toSubalgebra ⊔ B.toSubalgebra = ⊤
⊢ Eq (α := ↥A) ((Algebra.trace (↥A) E : (a : E) → ↥A) ((algebraMap (↥B) E : (a : ↥B) → E) x) : ↥A)
    ((algebraMap F ↥A : (a : F) → ↥A) ((Algebra.trace F ↥B : (a : ↥B) → F) x) : ↥A)

Tactic:
refine h₁.trace_algebraMap ?_ x

Premises used: Subalgebra.LinearDisjoint.trace_algebraMap
-- Module: Mathlib.FieldTheory.LinearDisjoint
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A B : IntermediateField F E
inst_3 : FiniteDimensional F E
h₁ : A.LinearDisjoint B.toSubalgebra
h₂ : A ⊔ B = ⊤
x : ↥B
⊢ A.toSubalgebra ⊔ B.toSubalgebra = ⊤

Tactic:
simpa [sup_toSubalgebra_of_isAlgebraic_right] using congr_arg toSubalgebra h₂

Premises used: congr_arg, IntermediateField.sup_toSubalgebra_of_isAlgebraic_right, IntermediateField.toSubalgebra
-- Module: Mathlib.FieldTheory.LinearDisjoint
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A B : IntermediateField F E
inst_3 : FiniteDimensional F E
h₁ : A.LinearDisjoint ↥B
h₂ : A ⊔ B = ⊤
x : ↥B
rw :
  ∀ (h₁ : A.LinearDisjoint B.toSubalgebra) (h₂ : A ⊔ B = ⊤) (x : ↥B),
    Eq (α := ↥A) ((Algebra.norm ↥A : (a : E) → ↥A) ((algebraMap (↥B) E : (a : ↥B) → E) x) : ↥A)
      ((algebraMap F ↥A : (a : F) → ↥A) ((Algebra.norm F : (a : ↥B) → F) x) : ↥A)
⊢ Eq (α := ↥A) ((Algebra.norm ↥A : (a : E) → ↥A) ((algebraMap (↥B) E : (a : ↥B) → E) x) : ↥A)
    ((algebraMap F ↥A : (a : F) → ↥A) ((Algebra.norm F : (a : ↥B) → F) x) : ↥A)

Tactic:
rw [linearDisjoint_iff'] at h₁

Premises used: IntermediateField.linearDisjoint_iff'
-- Module: Mathlib.FieldTheory.LinearDisjoint
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A B : IntermediateField F E
inst_3 : FiniteDimensional F E
h₁ : A.LinearDisjoint B.toSubalgebra
h₂ : A ⊔ B = ⊤
x : ↥B
⊢ Eq (α := ↥A) ((Algebra.norm ↥A : (a : E) → ↥A) ((algebraMap (↥B) E : (a : ↥B) → E) x) : ↥A)
    ((algebraMap F ↥A : (a : F) → ↥A) ((Algebra.norm F : (a : ↥B) → F) x) : ↥A)

Tactic:
h₁.norm_algebraMap ?_ x

Premises used: Set.Mem, Subalgebra.LinearDisjoint.norm_algebraMap
-- Module: Mathlib.FieldTheory.LinearDisjoint
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A B : IntermediateField F E
inst_3 : FiniteDimensional F E
h₁ : A.LinearDisjoint B.toSubalgebra
h₂ : A ⊔ B = ⊤
x : ↥B
refine : A.toSubalgebra ⊔ B.toSubalgebra = ⊤
⊢ Eq (α := ↥A) ((Algebra.norm ↥A : (a : E) → ↥A) ((algebraMap (↥B) E : (a : ↥B) → E) x) : ↥A)
    ((algebraMap F ↥A : (a : F) → ↥A) ((Algebra.norm F : (a : ↥B) → F) x) : ↥A)

Tactic:
refine h₁.norm_algebraMap ?_ x

Premises used: Subalgebra.LinearDisjoint.norm_algebraMap
-- Module: Mathlib.FieldTheory.Minpoly.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
hx : IsIntegral A x
rw :
  (WellFounded.min (r := fun (p q : A[X]) ↦ p.degree < q.degree) ⋯
      (fun (x_1 : A[X]) ↦ x_1.Monic ∧ eval₂ (algebraMap A B) x x_1 = 0) hx).Monic
⊢ Monic.{u_1} (R := A)
    (if hx : IsIntegral A x then
      WellFounded.min (r := fun (p q : A[X]) ↦ p.degree < q.degree) ⋯
        (fun (x_1 : A[X]) ↦ x_1.Monic ∧ eval₂ (algebraMap A B) x x_1 = 0) hx
    else 0)

Tactic:
rw [dif_pos hx]

Premises used: dif_pos
-- Module: Mathlib.FieldTheory.Minpoly.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
hx : IsIntegral A x
⊢ (WellFounded.min (r := fun (p q : A[X]) ↦ p.degree < q.degree) ⋯
      (fun (x_1 : A[X]) ↦ x_1.Monic ∧ eval₂ (algebraMap A B) x x_1 = 0) hx).Monic

Tactic:
(degree_lt_wf.min_mem _ hx).1

Premises used: WellFounded.min_mem, Polynomial.degree_lt_wf, And.left
-- Module: Mathlib.FieldTheory.Minpoly.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
hx : IsIntegral A x
⊢ (WellFounded.min (r := fun (p q : A[X]) ↦ p.degree < q.degree) ⋯
      (fun (x_1 : A[X]) ↦ x_1.Monic ∧ eval₂ (algebraMap A B) x x_1 = 0) hx).Monic

Tactic:
exact (degree_lt_wf.min_mem _ hx).1

Premises used: WellFounded.min_mem, Polynomial.degree_lt_wf, And.left
-- Module: Mathlib.FieldTheory.Minpoly.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
inst_3 : Nontrivial A
hx : IsIntegral A x
⊢ Ne (α := A[X]) (minpoly A x) 0

Tactic:
(monic hx).ne_zero

Premises used: minpoly.monic, Polynomial.Monic.ne_zero
-- Module: Mathlib.FieldTheory.Minpoly.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
hx : ¬IsIntegral A x
⊢ Eq (α := A[X]) (minpoly A x) 0

Tactic:
dif_neg hx

Premises used: dif_neg, minpoly
-- Module: Mathlib.FieldTheory.Minpoly.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
inst_3 : Nontrivial A
⊢ Ne (α := A[X]) (minpoly A x) 0 ↔ IsIntegral A x

Tactic:
⟨fun h => of_not_not <| eq_zero.mt h, ne_zero⟩

Premises used: Function.mt, minpoly.eq_zero, Iff.intro, of_not_not, minpoly.ne_zero
-- Module: Mathlib.FieldTheory.Minpoly.Basic
Goal:
A : Type u_1
B : Type u_2
B' : Type u_3
inst : CommRing A
inst_1 : Ring B
inst_2 : Ring B'
inst_3 : Algebra A B
inst_4 : Algebra A B'
f : B →ₐ[A] B'
hf : Injective.{u_2 + 1, u_3 + 1} (α := B) (β := B') (⇑f : (a : B) → B')
x : B
simp_rw :
  Eq.{u_1 + 1} (α := A[X])
    (if hx : IsIntegral.{u_1, u_3} A (A := B') ((f : (a : B) → B') x : B') then
      WellFounded.min (r := fun (p q : A[X]) ↦ p.degree < q.degree) ⋯
        (fun (x_1 : A[X]) ↦ x_1.Monic ∧ eval₂ (algebraMap A B') ((f : (a : B) → B') x) x_1 = 0) hx
    else 0)
    (if hx : IsIntegral A x then
      WellFounded.min (r := fun (p q : A[X]) ↦ p.degree < q.degree) ⋯
        (fun (x_1 : A[X]) ↦ x_1.Monic ∧ eval₂ (algebraMap A B) x x_1 = 0) hx
    else 0)
simp_rw₁ :
  Eq.{u_1 + 1} (α := A[X])
    (if h : IsIntegral A x then
      WellFounded.min (r := fun (p q : A[X]) ↦ p.degree < q.degree) ⋯
        (fun (x_1 : A[X]) ↦ x_1.Monic ∧ eval₂ (algebraMap A B') ((f : (a : B) → B') x) x_1 = 0) ⋯
    else 0)
    (if hx : IsIntegral A x then
      WellFounded.min (r := fun (p q : A[X]) ↦ p.degree < q.degree) ⋯
        (fun (x_1 : A[X]) ↦ x_1.Monic ∧ eval₂ (algebraMap A B) x x_1 = 0) hx
    else 0)
simp_rw₂ :
  Eq.{u_1 + 1} (α := A[X])
    (if h : IsIntegral A x then
      WellFounded.min (r := fun (p q : A[X]) ↦ p.degree < q.degree) ⋯
        (fun (x_1 : A[X]) ↦
          x_1.Monic ∧
            Eq.{u_3 + 1} (α := B') (((aeval ((f : (a : B) → B') x) : A[X] →ₐ[A] B') : (a : A[X]) → B') x_1 : B')
              (0 : B'))
        ⋯
    else 0)
    (if h : IsIntegral A x then
      WellFounded.min (r := fun (p q : A[X]) ↦ p.degree < q.degree) ⋯
        (fun (x_1 : A[X]) ↦ x_1.Monic ∧ Eq.{u_2 + 1} (α := B) ((aeval x : (a : A[X]) → B) x_1 : B) (0 : B)) ⋯
    else 0)
simp_rw₃ :
  Eq.{u_1 + 1} (α := A[X])
    (if h : IsIntegral A x then
      WellFounded.min (r := fun (p q : A[X]) ↦ p.degree < q.degree) ⋯
        (fun (x_1 : A[X]) ↦ x_1.Monic ∧ Eq.{u_3 + 1} (α := B') ((f.comp (aeval x) : (a : A[X]) → B') x_1 : B') (0 : B'))
        ⋯
    else 0)
    (if h : IsIntegral A x then
      WellFounded.min (r := fun (p q : A[X]) ↦ p.degree < q.degree) ⋯
        (fun (x_1 : A[X]) ↦ x_1.Monic ∧ Eq.{u_2 + 1} (α := B) ((aeval x : (a : A[X]) → B) x_1 : B) (0 : B)) ⋯
    else 0)
simp_rw₄ :
  Eq.{u_1 + 1} (α := A[X])
    (if h : IsIntegral A x then
      WellFounded.min (r := fun (p q : A[X]) ↦ p.degree < q.degree) ⋯
        (fun (x_1 : A[X]) ↦
          x_1.Monic ∧ Eq.{u_3 + 1} (α := B') ((f : (a : B) → B') ((aeval x : (a : A[X]) → B) x_1 : B) : B') (0 : B'))
        ⋯
    else 0)
    (if h : IsIntegral A x then
      WellFounded.min (r := fun (p q : A[X]) ↦ p.degree < q.degree) ⋯
        (fun (x_1 : A[X]) ↦ x_1.Monic ∧ Eq.{u_2 + 1} (α := B) ((aeval x : (a : A[X]) → B) x_1 : B) (0 : B)) ⋯
    else 0)
⊢ Eq (α := A[X]) (minpoly.{u_1, u_3} A (B := B') ((f : (a : B) → B') x : B')) (minpoly A x)

Tactic:
simp_rw [minpoly, isIntegral_algHom_iff _ hf, ← Polynomial.aeval_def, aeval_algHom,
    AlgHom.comp_apply, _root_.map_eq_zero_iff f hf]

Premises used: isIntegral_algHom_iff, AlgHom.comp_apply, Polynomial.aeval_def, minpoly, map_eq_zero_iff, Polynomial.aeval_algHom
-- Module: Mathlib.FieldTheory.Minpoly.Basic
Goal:
A : Type u_1
B' : Type u_3
inst : CommRing A
inst_1 : Ring B'
inst_2 : Algebra A B'
B : Type u_4
inst_3 : CommRing B
inst_4 : Algebra A B
inst_5 : Algebra B B'
inst_6 : IsScalarTower A B B'
h : Injective.{u_4 + 1, u_3 + 1} (α := B) (β := B') (⇑(algebraMap B B') : (a : B) → B')
x : B
⊢ Eq (α := A[X]) (minpoly.{u_1, u_3} A (B := B') ((algebraMap B B' : (a : B) → B') x : B')) (minpoly A x)

Tactic:
algHom_eq (IsScalarTower.toAlgHom A B B') h x

Premises used: IsScalarTower.toAlgHom, minpoly.algHom_eq
-- Module: Mathlib.FieldTheory.Minpoly.Basic
Goal:
A : Type u_1
B : Type u_2
B' : Type u_3
inst : CommRing A
inst_1 : Ring B
inst_2 : Ring B'
inst_3 : Algebra A B
inst_4 : Algebra A B'
f : B ≃ₐ[A] B'
x : B
⊢ Eq (α := A[X]) (minpoly.{u_1, u_3} A (B := B') ((f : (a : B) → B') x : B')) (minpoly A x)

Tactic:
algHom_eq (f : B →ₐ[A] B') f.injective x

Premises used: AlgEquiv.toAlgHom, minpoly.algHom_eq, AlgEquiv.injective
-- Module: Mathlib.FieldTheory.Minpoly.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
delta :
  Eq.{u_2 + 1} (α := B)
    ((Polynomial.aeval x : (a : A[X]) → B)
        (if hx : IsIntegral A x then
          WellFounded.min (r := fun (p q : A[X]) ↦ p.degree < q.degree) ⋯
            (fun (x_1 : A[X]) ↦ x_1.Monic ∧ eval₂ (algebraMap A B) x x_1 = 0) hx
        else 0) :
      B)
    (0 : B)
⊢ Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) (minpoly A x) : B) (0 : B)

Tactic:
delta minpoly

Premises used: minpoly
-- Module: Mathlib.FieldTheory.Minpoly.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
pos :
  ∀ (hx : IsIntegral A x),
    Eq.{u_2 + 1} (α := B)
      ((Polynomial.aeval x : (a : A[X]) → B)
          (WellFounded.min (r := fun (p q : A[X]) ↦ p.degree < q.degree) ⋯
            (fun (x_1 : A[X]) ↦ x_1.Monic ∧ eval₂ (algebraMap A B) x x_1 = 0) hx) :
        B)
      (0 : B)
neg : ∀ (hx : ¬IsIntegral A x), Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) 0 : B) (0 : B)
⊢ Eq.{u_2 + 1} (α := B)
    ((Polynomial.aeval x : (a : A[X]) → B)
        (if hx : IsIntegral A x then
          WellFounded.min (r := fun (p q : A[X]) ↦ p.degree < q.degree) ⋯
            (fun (x_1 : A[X]) ↦ x_1.Monic ∧ eval₂ (algebraMap A B) x x_1 = 0) hx
        else 0) :
      B)
    (0 : B)

Tactic:
split_ifs with hx
-- Module: Mathlib.FieldTheory.Minpoly.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
hx : IsIntegral A x
⊢ Eq.{u_2 + 1} (α := B)
    ((Polynomial.aeval x : (a : A[X]) → B)
        (WellFounded.min (r := fun (p q : A[X]) ↦ p.degree < q.degree) ⋯
          (fun (x_1 : A[X]) ↦ x_1.Monic ∧ eval₂ (algebraMap A B) x x_1 = 0) hx) :
      B)
    (0 : B)

Tactic:
(degree_lt_wf.min_mem _ hx).2

Premises used: WellFounded.min_mem, Polynomial.degree_lt_wf, MonoidHomClass.toMonoidHom, And.right, RingHomClass.toRingHom
-- Module: Mathlib.FieldTheory.Minpoly.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
hx : IsIntegral A x
⊢ Eq.{u_2 + 1} (α := B)
    ((Polynomial.aeval x : (a : A[X]) → B)
        (WellFounded.min (r := fun (p q : A[X]) ↦ p.degree < q.degree) ⋯
          (fun (x_1 : A[X]) ↦ x_1.Monic ∧ eval₂ (algebraMap A B) x x_1 = 0) hx) :
      B)
    (0 : B)

Tactic:
exact (degree_lt_wf.min_mem _ hx).2

Premises used: WellFounded.min_mem, Polynomial.degree_lt_wf, And.right
-- Module: Mathlib.FieldTheory.Minpoly.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
hx : ¬IsIntegral A x
⊢ Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) 0 : B) (0 : B)

Tactic:
aeval_zero _

Premises used: Polynomial.aeval_zero
-- Module: Mathlib.FieldTheory.Minpoly.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
hx : ¬IsIntegral A x
⊢ Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) 0 : B) (0 : B)

Tactic:
exact aeval_zero _

Premises used: Polynomial.aeval_zero
-- Module: Mathlib.FieldTheory.Minpoly.Basic
Goal:
A : Type u_1
B : Type u_2
B' : Type u_3
inst : CommRing A
inst_1 : Ring B
inst_2 : Ring B'
inst_3 : Algebra A B
inst_4 : Algebra A B'
f : B →ₐ[A] B'
x : B
rw : Eq.{u_3 + 1} (α := B') ((f.comp (Polynomial.aeval x) : (a : A[X]) → B') (minpoly A x) : B') (0 : B')
rw₁ :
  Eq.{u_3 + 1} (α := B')
    (Function.comp.{u_1 + 1, u_2 + 1, u_3 + 1} (α := A[X]) (β := B) (⇑f : (a : B) → B')
      (⇑(Polynomial.aeval x) : (a : A[X]) → B) (minpoly A x))
    0
rw₂ :
  Eq.{u_3 + 1} (α := B') ((f : (a : B) → B') ((Polynomial.aeval x : (a : A[X]) → B) (minpoly A x) : B) : B') (0 : B')
rw₃ : Eq.{u_3 + 1} (α := B') ((f : (a : B) → B') 0 : B') (0 : B')
rw₄ rw₅ : Eq.{u_3 + 1} (α := B') 0 0
⊢ Eq.{u_3 + 1} (α := B')
    (((Polynomial.aeval ((f : (a : B) → B') x) : A[X] →ₐ[A] B') : (a : A[X]) → B') (minpoly A x) : B') (0 : B')

Tactic:
rw [Polynomial.aeval_algHom, AlgHom.coe_comp, comp_apply, aeval, map_zero]

Premises used: map_zero, minpoly.aeval, AlgHom.coe_comp, Function.comp_apply, Polynomial.aeval_algHom
-- Module: Mathlib.FieldTheory.Minpoly.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
inst_3 : Nontrivial B
h : Eq (α := A[X]) (minpoly A x) 1
⊢ False

Tactic:
(one_ne_zero : (1 : B) ≠ 0) ?_

Premises used: one_ne_zero
-- Module: Mathlib.FieldTheory.Minpoly.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
inst_3 : Nontrivial B
h : Eq (α := A[X]) (minpoly A x) 1
refine : Eq.{u_2 + 1} (α := B) 1 0
⊢ False

Tactic:
refine (one_ne_zero : (1 : B) ≠ 0) ?_

Premises used: one_ne_zero
-- Module: Mathlib.FieldTheory.Minpoly.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
inst_3 : Nontrivial B
h : Eq (α := A[X]) (minpoly A x) 1
⊢ Eq.{u_2 + 1} (α := B) 1 0

Tactic:
simpa using congr_arg (Polynomial.aeval x) h

Premises used: congr_arg, Polynomial.aeval, DFunLike.coe
-- Module: Mathlib.FieldTheory.Minpoly.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
inst_3 : Nontrivial B
R : Type u_4
inst_4 : Semiring R
inst_5 : Nontrivial R
f : A →+* R
pos : ∀ (hx : IsIntegral A x), map f (minpoly A x) ≠ 1
neg : ∀ (hx : ¬IsIntegral A x), map f (minpoly A x) ≠ 1
⊢ map f (minpoly A x) ≠ 1

Tactic:
by_cases hx : IsIntegral A x

Premises used: IsIntegral
-- Module: Mathlib.FieldTheory.Minpoly.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
inst_3 : Nontrivial B
R : Type u_4
inst_4 : Semiring R
inst_5 : Nontrivial R
f : A →+* R
hx : IsIntegral A x
⊢ map f (minpoly A x) ≠ 1

Tactic:
mt ((monic hx).eq_one_of_map_eq_one f) (ne_one A x)

Premises used: minpoly.monic, minpoly.ne_one, mt, Polynomial.Monic.eq_one_of_map_eq_one
-- Module: Mathlib.FieldTheory.Minpoly.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
inst_3 : Nontrivial B
R : Type u_4
inst_4 : Semiring R
inst_5 : Nontrivial R
f : A →+* R
hx : IsIntegral A x
⊢ map f (minpoly A x) ≠ 1

Tactic:
exact mt ((monic hx).eq_one_of_map_eq_one f) (ne_one A x)

Premises used: minpoly.monic, minpoly.ne_one, mt, Polynomial.Monic.eq_one_of_map_eq_one
-- Module: Mathlib.FieldTheory.Minpoly.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
inst_3 : Nontrivial B
R : Type u_4
inst_4 : Semiring R
inst_5 : Nontrivial R
f : A →+* R
hx : ¬IsIntegral A x
neg : Ne.{u_4 + 1} (α := R[X]) 0 1
⊢ map f (minpoly A x) ≠ 1

Tactic:
rw [eq_zero hx, Polynomial.map_zero]

Premises used: minpoly.eq_zero, Polynomial.map_zero
-- Module: Mathlib.FieldTheory.Minpoly.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
inst_3 : Nontrivial B
R : Type u_4
inst_4 : Semiring R
inst_5 : Nontrivial R
f : A →+* R
hx : ¬IsIntegral A x
⊢ Ne.{u_4 + 1} (α := R[X]) 0 1

Tactic:
zero_ne_one

Premises used: zero_ne_one
-- Module: Mathlib.FieldTheory.Minpoly.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
inst_3 : Nontrivial B
R : Type u_4
inst_4 : Semiring R
inst_5 : Nontrivial R
f : A →+* R
hx : ¬IsIntegral A x
⊢ Ne.{u_4 + 1} (α := R[X]) 0 1

Tactic:
exact zero_ne_one

Premises used: zero_ne_one
-- Module: Mathlib.FieldTheory.Minpoly.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
inst_3 : Nontrivial B
⊢ Nontrivial A

Tactic:
haveI : Nontrivial A := (algebraMap A B).domain_nontrivial
-- Module: Mathlib.FieldTheory.Minpoly.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
inst_3 : Nontrivial B
this : Nontrivial A
pos : ∀ (hx : IsIntegral A x), ¬IsUnit (M := A[X]) (minpoly A x)
neg : ∀ (hx : ¬IsIntegral A x), ¬IsUnit (M := A[X]) (minpoly A x)
⊢ ¬IsUnit (M := A[X]) (minpoly A x)

Tactic:
by_cases hx : IsIntegral A x

Premises used: IsIntegral
-- Module: Mathlib.FieldTheory.Minpoly.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
inst_3 : Nontrivial B
this : Nontrivial A
hx : IsIntegral A x
⊢ ¬IsUnit (M := A[X]) (minpoly A x)

Tactic:
mt (monic hx).eq_one_of_isUnit (ne_one A x)

Premises used: minpoly.monic, minpoly.ne_one, mt, Polynomial.Monic.eq_one_of_isUnit