A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x✝¹ : B
f : B →ₐ[A] B'
hf : Injective ↑f
x : B
x✝ : IsIntegral A x
⊢ WellFounded.min (_ : WellFounded fun p q => degree p < degree q)
      (fun x_1 => Monic x_1 ∧ eval₂ (algebraMap A ((fun x => B') x)) (↑f x) x_1 = 0) (_ : IsIntegral A (↑f x)) =
    WellFounded.min (_ : WellFounded fun p q => degree p < degree q)
      (fun x_1 => Monic x_1 ∧ eval₂ (algebraMap A B) x x_1 = 0) x✝
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x✝ : B
f : B →ₐ[A] B'
hf : Injective ↑f
x : B
⊢ minpoly A (↑f x) = minpoly A x
refine' dif_ctx_congr (isIntegral_algHom_iff _ hf) (fun _ => _) fun _ => rfl
no goals
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x✝¹ : B
f : B →ₐ[A] B'
hf : Injective ↑f
x : B
x✝ : IsIntegral A x
⊢ WellFounded.min (_ : WellFounded fun p q => degree p < degree q)
      (fun x_1 => Monic x_1 ∧ eval₂ (algebraMap A ((fun x => B') x)) (↑f x) x_1 = 0) (_ : IsIntegral A (↑f x)) =
    WellFounded.min (_ : WellFounded fun p q => degree p < degree q)
      (fun x_1 => Monic x_1 ∧ eval₂ (algebraMap A B) x x_1 = 0) x✝
simp_rw [← Polynomial.aeval_def, aeval_algHom, AlgHom.comp_apply, _root_.map_eq_zero_iff f hf]