awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.LinearDisjoint (goal)
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
⊢ Algebra.IsAlgebraic F ↥fa.fieldRange ∨ Algebra.IsAlgebraic F ↥fb.fieldRange
have 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
Tactic: rwa [(AlgEquiv.ofInjective fa hfa).isAlgebraic_iff,
          (AlgEquiv.ofInjective fb hfb).isAlgebraic_iff] at halg
Cleared hypotheses: halg, fb, hfa, hfb, H
-- Lean 4 proof step from Mathlib.FieldTheory.LinearDisjoint (goal)
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
⊢ 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)
have 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)
Tactic: rw [linearDisjoint_iff'] at h₁
Cleared hypotheses: h₁, h₂, x
-- Lean 4 proof step from Mathlib.FieldTheory.LinearDisjoint (goal)
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)
have refine : A.toSubalgebra ⊔ B.toSubalgebra = ⊤
Tactic: refine h₁.trace_algebraMap ?_ x
-- Lean 4 proof step from Mathlib.FieldTheory.LinearDisjoint (goal)
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
⊢ 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)
have 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)
Tactic: rw [linearDisjoint_iff'] at h₁
Cleared hypotheses: h₁, h₂, x
-- Lean 4 proof step from Mathlib.FieldTheory.LinearDisjoint (goal)
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)
have refine : A.toSubalgebra ⊔ B.toSubalgebra = ⊤
Tactic: refine h₁.norm_algebraMap ?_ x
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Basic (goal)
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
⊢ 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)
have rw : (WellFounded.min (r := fun (p q : A[X]) ↦ p.degree < q.degree) sorry
    (fun (x_1 : A[X]) ↦ x_1.Monic ∧ eval₂ (algebraMap A B) x x_1 = 0) hx).Monic
Tactic: rw [dif_pos hx]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Basic (goal)
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
⊢ Eq (α := A[X]) (minpoly.{u_1, u_3} A (B := B') ((f : (a : B) → B') x : B')) (minpoly A x)
have 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) sorry
      (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) sorry
      (fun (x_1 : A[X]) ↦ x_1.Monic ∧ eval₂ (algebraMap A B) x x_1 = 0) hx
  else 0)
Tactic: simp_rw [minpoly, isIntegral_algHom_iff _ hf, ← Polynomial.aeval_def, aeval_algHom,
    AlgHom.comp_apply, _root_.map_eq_zero_iff f hf]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Basic (goal)
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)
⊢ Eq (α := A[X]) (minpoly.{u_1, u_3} A (B := B') ((f : (a : B) → B') x : B')) (minpoly A x)
have 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) sorry
      (fun (x_1 : A[X]) ↦ x_1.Monic ∧ eval₂ (algebraMap A B') ((f : (a : B) → B') x) x_1 = 0) sorry
  else 0)
  (if hx : IsIntegral A x then
    WellFounded.min (r := fun (p q : A[X]) ↦ p.degree < q.degree) sorry
      (fun (x_1 : A[X]) ↦ x_1.Monic ∧ eval₂ (algebraMap A B) x x_1 = 0) hx
  else 0)
Tactic: simp_rw [minpoly, isIntegral_algHom_iff _ hf, ← Polynomial.aeval_def, aeval_algHom,
    AlgHom.comp_apply, _root_.map_eq_zero_iff f hf]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Basic (goal)
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)
⊢ Eq (α := A[X]) (minpoly.{u_1, u_3} A (B := B') ((f : (a : B) → B') x : B')) (minpoly A x)
have 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) sorry
      (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'))
      sorry
  else 0)
  (if h : IsIntegral A x then
    WellFounded.min (r := fun (p q : A[X]) ↦ p.degree < q.degree) sorry
      (fun (x_1 : A[X]) ↦ x_1.Monic ∧ Eq.{u_2 + 1} (α := B) ((aeval x : (a : A[X]) → B) x_1 : B) (0 : B)) sorry
  else 0)
Tactic: simp_rw [minpoly, isIntegral_algHom_iff _ hf, ← Polynomial.aeval_def, aeval_algHom,
    AlgHom.comp_apply, _root_.map_eq_zero_iff f hf]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Basic (goal)
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)
⊢ Eq (α := A[X]) (minpoly.{u_1, u_3} A (B := B') ((f : (a : B) → B') x : B')) (minpoly A x)
have 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) sorry
      (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')) sorry
  else 0)
  (if h : IsIntegral A x then
    WellFounded.min (r := fun (p q : A[X]) ↦ p.degree < q.degree) sorry
      (fun (x_1 : A[X]) ↦ x_1.Monic ∧ Eq.{u_2 + 1} (α := B) ((aeval x : (a : A[X]) → B) x_1 : B) (0 : B)) sorry
  else 0)
Tactic: simp_rw [minpoly, isIntegral_algHom_iff _ hf, ← Polynomial.aeval_def, aeval_algHom,
    AlgHom.comp_apply, _root_.map_eq_zero_iff f hf]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Basic (goal)
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)
⊢ Eq (α := A[X]) (minpoly.{u_1, u_3} A (B := B') ((f : (a : B) → B') x : B')) (minpoly A x)
have 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) sorry
      (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'))
      sorry
  else 0)
  (if h : IsIntegral A x then
    WellFounded.min (r := fun (p q : A[X]) ↦ p.degree < q.degree) sorry
      (fun (x_1 : A[X]) ↦ x_1.Monic ∧ Eq.{u_2 + 1} (α := B) ((aeval x : (a : A[X]) → B) x_1 : B) (0 : B)) sorry
  else 0)
Tactic: simp_rw [minpoly, isIntegral_algHom_iff _ hf, ← Polynomial.aeval_def, aeval_algHom,
    AlgHom.comp_apply, _root_.map_eq_zero_iff f hf]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Basic (goal)
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
⊢ Eq (α := A[X]) (minpoly.{u_1, u_3} A (B := B') ((f : (a : B) → B') x : B')) (minpoly A x)
have 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) sorry
      (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) sorry
      (fun (x_1 : A[X]) ↦ x_1.Monic ∧ eval₂ (algebraMap A B) x x_1 = 0) hx
  else 0)
Tactic: classical
  simp_rw [minpoly, isIntegral_algHom_iff _ hf, ← Polynomial.aeval_def, aeval_algHom,
    AlgHom.comp_apply, _root_.map_eq_zero_iff f hf]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Basic (goal)
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)
⊢ Eq (α := A[X]) (minpoly.{u_1, u_3} A (B := B') ((f : (a : B) → B') x : B')) (minpoly A x)
have 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) sorry
      (fun (x_1 : A[X]) ↦ x_1.Monic ∧ eval₂ (algebraMap A B') ((f : (a : B) → B') x) x_1 = 0) sorry
  else 0)
  (if hx : IsIntegral A x then
    WellFounded.min (r := fun (p q : A[X]) ↦ p.degree < q.degree) sorry
      (fun (x_1 : A[X]) ↦ x_1.Monic ∧ eval₂ (algebraMap A B) x x_1 = 0) hx
  else 0)
Tactic: classical
  simp_rw [minpoly, isIntegral_algHom_iff _ hf, ← Polynomial.aeval_def, aeval_algHom,
    AlgHom.comp_apply, _root_.map_eq_zero_iff f hf]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Basic (goal)
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)
⊢ Eq (α := A[X]) (minpoly.{u_1, u_3} A (B := B') ((f : (a : B) → B') x : B')) (minpoly A x)
have 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) sorry
      (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'))
      sorry
  else 0)
  (if h : IsIntegral A x then
    WellFounded.min (r := fun (p q : A[X]) ↦ p.degree < q.degree) sorry
      (fun (x_1 : A[X]) ↦ x_1.Monic ∧ Eq.{u_2 + 1} (α := B) ((aeval x : (a : A[X]) → B) x_1 : B) (0 : B)) sorry
  else 0)
Tactic: classical
  simp_rw [minpoly, isIntegral_algHom_iff _ hf, ← Polynomial.aeval_def, aeval_algHom,
    AlgHom.comp_apply, _root_.map_eq_zero_iff f hf]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Basic (goal)
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)
⊢ Eq (α := A[X]) (minpoly.{u_1, u_3} A (B := B') ((f : (a : B) → B') x : B')) (minpoly A x)
have 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) sorry
      (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')) sorry
  else 0)
  (if h : IsIntegral A x then
    WellFounded.min (r := fun (p q : A[X]) ↦ p.degree < q.degree) sorry
      (fun (x_1 : A[X]) ↦ x_1.Monic ∧ Eq.{u_2 + 1} (α := B) ((aeval x : (a : A[X]) → B) x_1 : B) (0 : B)) sorry
  else 0)
Tactic: classical
  simp_rw [minpoly, isIntegral_algHom_iff _ hf, ← Polynomial.aeval_def, aeval_algHom,
    AlgHom.comp_apply, _root_.map_eq_zero_iff f hf]