-- 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
hc :
  ∀ α' ∈ (Polynomial.map (ιEE'.comp ιFE) f).roots,
    ∀ β' ∈ (Polynomial.map (ιEE'.comp ιFE) g).roots,
      -HSub.hSub (β := (Polynomial.map ιFE g).SplittingField) α'
              ((ιEE' : (a : E) → (Polynomial.map ιFE g).SplittingField) α : (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) ≠
        (ιEE'.comp ιFE : (a : F) → (Polynomial.map ιFE g).SplittingField) c
γ : E := α + c • β
let let₁ let₂ let₃ : Membership.mem (γ := IntermediateField F E) F⟮γ⟯ β
let₄ : ∀ (map_g_ne_zero : Polynomial.map ιFE g ≠ 0), Membership.mem (γ := IntermediateField F E) F⟮γ⟯ β
let₅ :
  let h :=
    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), Membership.mem (γ := IntermediateField F E) F⟮γ⟯ β
⊢ Membership.mem (γ := IntermediateField F E) F⟮γ⟯ β
have let₆ : let p :=
  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) sorry) :
            (↥F⟮γ⟯)[X])
          X)))
    (Polynomial.map (algebraMap F ↥F⟮γ⟯) g);
let h :=
  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),
  Polynomial.map (algebraMap (↥F⟮γ⟯) E) p =
    HMul.hMul (α := E[X]) ((C : (a : E) → E[X]) h.leadingCoeff : E[X])
      (HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) β : E[X]))
Tactic: classical
  let p := EuclideanDomain.gcd ((f.map (algebraMap F F⟮γ⟯)).comp
    (C (AdjoinSimple.gen F γ) - (C ↑c : F⟮γ⟯[X]) * X)) (g.map (algebraMap F F⟮γ⟯))
  let h := EuclideanDomain.gcd ((f.map ιFE).comp (C γ - C (ιFE c) * X)) (g.map ιFE)
  have map_g_ne_zero : g.map ιFE ≠ 0 := map_ne_zero (minpoly.ne_zero hβ)
  have h_ne_zero : h ≠ 0 :=
    mt EuclideanDomain.gcd_eq_zero_iff.mp (not_and.mpr fun _ => map_g_ne_zero)
  suffices p_linear : p.map (algebraMap F⟮γ⟯ E) = C h.leadingCoeff * (X - C β) by
    have finale : β = algebraMap F⟮γ⟯ E (-p.coeff 0 / p.coeff 1) := by
      simp [map_div₀, map_neg, ← coeff_map, ← coeff_map, p_linear,
        mul_sub, coeff_C, mul_div_cancel_left₀ β (mt leadingCoeff_eq_zero.mp h_ne_zero)]
    rw [finale]
    exact Subtype.mem (-p.coeff 0 / p.coeff 1)
  have h_sep : h.Separable := separable_gcd_right _ (.map (Algebra.IsSeparable.isSeparable F β))
  have h_root : h.eval β = 0 := by
    apply eval_gcd_eq_zero
    · rw [eval_comp, eval_sub, eval_mul, eval_C, eval_C, eval_X, eval_map_algebraMap, ←
        Algebra.smul_def, add_sub_cancel_right, minpoly.aeval]
    · rw [eval_map_algebraMap, minpoly.aeval]
  have h_splits : Splits (h.map ιEE') := by
    rw [← Polynomial.gcd_map]
    exact (SplittingField.splits _).of_dvd (map_ne_zero map_g_ne_zero)
      (EuclideanDomain.gcd_dvd_right _ _)
  have h_roots : ∀ x ∈ (h.map ιEE').roots, x = ιEE' β := by
    intro x hx
    rw [mem_roots_map h_ne_zero] at hx
    specialize hc (ιEE' γ - ιEE' (ιFE c) * x) (by
      have f_root := root_left_of_root_gcd hx
      rw [eval₂_comp, eval₂_sub, eval₂_mul, eval₂_C, eval₂_C, eval₂_X, eval₂_map] at f_root
      exact (mem_roots_map (minpoly.ne_zero hα)).mpr f_root)
    specialize hc x (by
      rw [mem_roots_map (minpoly.ne_zero hβ), ← eval₂_map]
      exact root_right_of_root_gcd hx)
    by_contra a
    apply hc
    apply (div_eq_iff (sub_ne_zero.mpr a)).mpr
    simp only [γ, Algebra.smul_def, map_add, map_mul, RingHom.comp_apply]
    ring
  rw [← eq_X_sub_C_of_separable_of_root_eq h_sep h_root h_splits h_roots]
  trans EuclideanDomain.gcd (?_ : E[X]) (?_ : E[X])
  · dsimp only [γ]
    convert! (gcd_map (algebraMap F⟮γ⟯ E)).symm
  · simp only [map_comp, Polynomial.map_map, ← IsScalarTower.algebraMap_eq, Polynomial.map_sub,
      map_C, AdjoinSimple.algebraMap_gen, Polynomial.map_mul, map_X]
    congr