-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u
inst : Field F
K : Type v
inst_1 : Field K
i : F →+* K
f : F[X]
sep : f.Separable
sp : (map i f).Splits
obtain :
  ∀ (s : Multiset K)
    (h :
      map i f =
        HMul.hMul (α := K[X]) (β := K[X]) ((C : (a : K) → K[X]) (map i f).leadingCoeff : K[X])
          (Multiset.prod
              (Multiset.map (fun (x : K) ↦ HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) x : K[X])) s) :
            K[X])),
    ∃ (s : Finset K),
      map i f =
        HMul.hMul (α := K[X]) (β := K[X]) ((C : (a : K) → K[X]) ((i : (a : F) → K) f.leadingCoeff) : K[X])
          (∏ a ∈ s, HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]) : K[X])
h :
  ∀ (s : Multiset K)
    (h :
      map i f =
        HMul.hMul (α := K[X]) (β := K[X]) ((C : (a : K) → K[X]) (map i f).leadingCoeff : K[X])
          (Multiset.prod
              (Multiset.map (fun (x : K) ↦ HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) x : K[X])) s) :
            K[X])),
    map i f =
      HMul.hMul (α := K[X]) (β := K[X]) ((C : (a : K) → K[X]) ((i : (a : F) → K) f.leadingCoeff) : K[X])
        (∏ a ∈ s.toFinset, HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]) : K[X])
h₁ :
  ∀ (s : Multiset K)
    (h :
      map i f =
        HMul.hMul (α := K[X]) (β := K[X]) ((C : (a : K) → K[X]) (map i f).leadingCoeff : K[X])
          (Multiset.prod
              (Multiset.map (fun (x : K) ↦ HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) x : K[X])) s) :
            K[X])),
    s.Nodup
h₂ :
  ∀ (s : Multiset K)
    (h :
      map i f =
        HMul.hMul (α := K[X]) (β := K[X]) ((C : (a : K) → K[X]) (map i f).leadingCoeff : K[X])
          (Multiset.prod
              (Multiset.map (fun (x : K) ↦ HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) x : K[X])) s) :
            K[X])),
    Separable (R := K)
      (Multiset.prod
        (Multiset.map (fun (a : K) ↦ HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])) s))
h₃ :
  ∀ (s : Multiset K)
    (h :
      map i f =
        HMul.hMul (α := K[X]) (β := K[X]) ((C : (a : K) → K[X]) (map i f).leadingCoeff : K[X])
          (Multiset.prod
              (Multiset.map (fun (x : K) ↦ HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) x : K[X])) s) :
            K[X])),
    (HMul.hMul (α := K[X]) (β := K[X]) ((C : (a : K) → K[X]) (map i f).leadingCoeff : K[X])
        (Multiset.prod
            (Multiset.map (fun (a : K) ↦ HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])) s) :
          K[X])).Separable
h₄ :
  (s : Multiset K) →
    (h :
        map i f =
          HMul.hMul (α := K[X]) (β := K[X]) ((C : (a : K) → K[X]) (map i f).leadingCoeff : K[X])
            (Multiset.prod
                (Multiset.map (fun (x : K) ↦ HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) x : K[X])) s) :
              K[X])) →
      K[X]
h₅ :
  ∀ (s : Multiset K)
    (h :
      map i f =
        HMul.hMul (α := K[X]) (β := K[X]) ((C : (a : K) → K[X]) (map i f).leadingCoeff : K[X])
          (Multiset.prod
              (Multiset.map (fun (x : K) ↦ HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) x : K[X])) s) :
            K[X])),
    (map i f).Separable
⊢ ∃ (s : Finset K),
    map i f =
      HMul.hMul (α := K[X]) (β := K[X]) ((C : (a : K) → K[X]) ((i : (a : F) → K) f.leadingCoeff) : K[X])
        (∏ a ∈ s, HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]) : K[X])

Tactic:
classical
  obtain ⟨s, h⟩ := splits_iff_exists_multiset.1 sp
  use s.toFinset
  rw [h, Finset.prod_eq_multiset_prod, ← Multiset.toFinset_eq, leadingCoeff_map]
  apply nodup_of_separable_prod
  apply Separable.of_mul_right
  rw [← h]
  exact sep.map

Premises used: Polynomial.splits_iff_exists_multiset, Polynomial.Separable.map, Finset.prod_eq_multiset_prod, Iff.mp, Polynomial.nodup_of_separable_prod, Multiset.toFinset_eq, Polynomial.leadingCoeff_map, Polynomial.Separable.of_mul_right