-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : Infinite F
E : Type u_2
inst_2 : Field E
α β : E
inst_3 : Algebra F E
inst_4 : Algebra.IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* (Polynomial.map ιFE g).SplittingField := algebraMap E (Polynomial.map ιFE g).SplittingField
c : F
γ : E := α + c • β
p : (↥F⟮γ⟯)[X] :=
  EuclideanDomain.gcd
    (comp (Polynomial.map (algebraMap F ↥F⟮γ⟯) f)
      (HSub.hSub (α := (↥F⟮γ⟯)[X]) ((C : (a : ↥F⟮γ⟯) → (↥F⟮γ⟯)[X]) (AdjoinSimple.gen F γ) : (↥F⟮γ⟯)[X])
        (HMul.hMul (α := (↥F⟮γ⟯)[X]) (β := (↥F⟮γ⟯)[X])
          ((C : (a : ↥F⟮γ⟯) → (↥F⟮γ⟯)[X])
              (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) F⟮γ⟯ x)
                ((algebraMap F E : (a : F) → E) c) ⋯) :
            (↥F⟮γ⟯)[X])
          X)))
    (Polynomial.map (algebraMap F ↥F⟮γ⟯) g)
h : E[X] :=
  EuclideanDomain.gcd
    ((Polynomial.map ιFE f).comp
      (HSub.hSub (α := E[X]) ((C : (a : E) → E[X]) γ : E[X])
        (HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) ((ιFE : (a : F) → E) c) : E[X]) X)))
    (Polynomial.map ιFE g)
map_g_ne_zero : Polynomial.map ιFE g ≠ 0
h_ne_zero : h ≠ 0
h_sep : h.Separable
h_root : eval β h = 0
h_splits : (Polynomial.map ιEE' h).Splits
x : (Polynomial.map ιFE g).SplittingField
hx : eval₂ ιEE' x h = 0
hc :
  -HSub.hSub (β := (Polynomial.map ιFE g).SplittingField)
          (HSub.hSub (α := (Polynomial.map ιFE g).SplittingField)
            ((ιEE' : (a : E) → (Polynomial.map ιFE g).SplittingField) γ : (Polynomial.map ιFE g).SplittingField)
            (HMul.hMul (α := (Polynomial.map ιFE g).SplittingField)
              ((ιEE' : (a : E) → (Polynomial.map ιFE g).SplittingField) ((ιFE : (a : F) → E) c) :
                (Polynomial.map ιFE g).SplittingField)
              x))
          ((ιEE' : (a : E) → (Polynomial.map ιFE g).SplittingField) α : (Polynomial.map ιFE g).SplittingField) /
      HSub.hSub (β := (Polynomial.map ιFE g).SplittingField) x
        ((ιEE' : (a : E) → (Polynomial.map ιFE g).SplittingField) β : (Polynomial.map ιFE g).SplittingField) ≠
    (ιEE'.comp ιFE : (a : F) → (Polynomial.map ιFE g).SplittingField) c
a : ¬x = (ιEE' : (a : E) → (Polynomial.map ιFE g).SplittingField) β
⊢ -HSub.hSub (β := (Polynomial.map ιFE g).SplittingField)
        (HSub.hSub (α := (Polynomial.map ιFE g).SplittingField)
          ((ιEE' : (a : E) → (Polynomial.map ιFE g).SplittingField) γ : (Polynomial.map ιFE g).SplittingField)
          (HMul.hMul (α := (Polynomial.map ιFE g).SplittingField)
            ((ιEE' : (a : E) → (Polynomial.map ιFE g).SplittingField) ((ιFE : (a : F) → E) c) :
              (Polynomial.map ιFE g).SplittingField)
            x))
        ((ιEE' : (a : E) → (Polynomial.map ιFE g).SplittingField) α : (Polynomial.map ιFE g).SplittingField) =
    HMul.hMul (α := (Polynomial.map ιFE g).SplittingField)
      ((ιEE'.comp ιFE : (a : F) → (Polynomial.map ιFE g).SplittingField) c : (Polynomial.map ιFE g).SplittingField)
      (HSub.hSub (β := (Polynomial.map ιFE g).SplittingField) x
        ((ιEE' : (a : E) → (Polynomial.map ιFE g).SplittingField) β : (Polynomial.map ιFE g).SplittingField))
have simp : -HSub.hSub (β := (Polynomial.map ιFE g).SplittingField)
      (HAdd.hAdd (α := (Polynomial.map ιFE g).SplittingField)
          ((ιEE' : (a : E) → (Polynomial.map ιFE g).SplittingField) α : (Polynomial.map ιFE g).SplittingField)
          (HMul.hMul (α := (Polynomial.map ιFE g).SplittingField) (β := (Polynomial.map ιFE g).SplittingField)
            ((ιEE' : (a : E) → (Polynomial.map ιFE g).SplittingField) ((algebraMap F E : (a : F) → E) c) :
              (Polynomial.map ιFE g).SplittingField)
            ((ιEE' : (a : E) → (Polynomial.map ιFE g).SplittingField) β : (Polynomial.map ιFE g).SplittingField)) -
        HMul.hMul (α := (Polynomial.map ιFE g).SplittingField)
          ((ιEE' : (a : E) → (Polynomial.map ιFE g).SplittingField) ((ιFE : (a : F) → E) c) :
            (Polynomial.map ιFE g).SplittingField)
          x)
      ((ιEE' : (a : E) → (Polynomial.map ιFE g).SplittingField) α : (Polynomial.map ιFE g).SplittingField) =
  HMul.hMul (α := (Polynomial.map ιFE g).SplittingField)
    ((ιEE' : (a : E) → (Polynomial.map ιFE g).SplittingField) ((ιFE : (a : F) → E) c) :
      (Polynomial.map ιFE g).SplittingField)
    (HSub.hSub (β := (Polynomial.map ιFE g).SplittingField) x
      ((ιEE' : (a : E) → (Polynomial.map ιFE g).SplittingField) β : (Polynomial.map ιFE g).SplittingField))
Tactic: simp only [γ, Algebra.smul_def, map_add, map_mul, RingHom.comp_apply]