-- 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:
classical
  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