-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Morse (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDomain S
G : Type u_3
inst_4 : Group G
inst_5 : MulSemiringAction G S
inst_6 : SMulCommClass G R S
f : R[X]
inst_7 : DecidableEq (↑(f.rootSet S) : Type u_2)
hf : Splits (map (algebraMap R S) f)
p : Ideal S
inst_8 : p.IsPrime
hp : (f.rootSet S).ncard ≤ Set.ncard.{u_2} (α := S ⧸ p) (f.rootSet (S ⧸ p)) + 1
g : G
hg : Membership.mem (γ := Subgroup G) (Ideal.inertia G p) g
pos :
  ∀ (hfp : Eq.{u_2 + 1} (α := (S ⧸ p)[X]) (map (algebraMap R (S ⧸ p)) f) 0),
    Eq.{u_2 + 1} (α := Equiv.Perm (↑(f.rootSet S) : Type u_2))
        ((MulAction.toPermHom G (↑(f.rootSet S) : Type u_2) : (a : G) → Equiv.Perm (↑(f.rootSet S) : Type u_2)) g :
          Equiv.Perm (↑(f.rootSet S) : Type u_2))
        (1 : Equiv.Perm (↑(f.rootSet S) : Type u_2)) ∨
      Equiv.Perm.IsSwap.{u_2} (α := (↑(f.rootSet S) : Type u_2))
        ((MulAction.toPermHom G (↑(f.rootSet S) : Type u_2) : (a : G) → Equiv.Perm (↑(f.rootSet S) : Type u_2)) g)
neg neg₁ :
  ∀ (hfp : ¬Eq.{u_2 + 1} (α := (S ⧸ p)[X]) (map (algebraMap R (S ⧸ p)) f) 0),
    Eq.{u_2 + 1} (α := Equiv.Perm (↑(f.rootSet S) : Type u_2))
        ((MulAction.toPermHom G (↑(f.rootSet S) : Type u_2) : (a : G) → Equiv.Perm (↑(f.rootSet S) : Type u_2)) g :
          Equiv.Perm (↑(f.rootSet S) : Type u_2))
        (1 : Equiv.Perm (↑(f.rootSet S) : Type u_2)) ∨
      Equiv.Perm.IsSwap.{u_2} (α := (↑(f.rootSet S) : Type u_2))
        ((MulAction.toPermHom G (↑(f.rootSet S) : Type u_2) : (a : G) → Equiv.Perm (↑(f.rootSet S) : Type u_2)) g)
neg₂ :
  ∀ (hfp : ¬Eq.{u_2 + 1} (α := (S ⧸ p)[X]) (map (algebraMap R (S ⧸ p)) f) 0),
    Eq.{u_2 + 1} (α := Equiv.Perm (↑(f.rootSet S) : Type u_2))
        ((MulAction.toPermHom G (↑(f.rootSet S) : Type u_2) : (a : G) → Equiv.Perm (↑(f.rootSet S) : Type u_2)) g :
          Equiv.Perm (↑(f.rootSet S) : Type u_2))
        (1 : Equiv.Perm (↑(f.rootSet S) : Type u_2)) ∨
      Equiv.Perm.IsSwap.{u_2} (α := (↑(f.rootSet S) : Type u_2))
        ((MulAction.toPermHom G (↑(f.rootSet S) : Type u_2) : (a : G) → Equiv.Perm (↑(f.rootSet S) : Type u_2)) g)
⊢ Eq.{u_2 + 1} (α := Equiv.Perm (↑(f.rootSet S) : Type u_2))
      ((MulAction.toPermHom G (↑(f.rootSet S) : Type u_2) : (a : G) → Equiv.Perm (↑(f.rootSet S) : Type u_2)) g :
        Equiv.Perm (↑(f.rootSet S) : Type u_2))
      (1 : Equiv.Perm (↑(f.rootSet S) : Type u_2)) ∨
    Equiv.Perm.IsSwap.{u_2} (α := (↑(f.rootSet S) : Type u_2))
      ((MulAction.toPermHom G (↑(f.rootSet S) : Type u_2) : (a : G) → Equiv.Perm (↑(f.rootSet S) : Type u_2)) g)
have neg₃ : ∀ (hfp : ¬Eq.{u_2 + 1} (α := (S ⧸ p)[X]) (map (algebraMap R (S ⧸ p)) f) 0),
  let π : S →ₐ[R] S ⧸ p := Ideal.Quotient.mkₐ R p;
  ∀
    (hp :
      ∀ a ∈ f.rootSet S,
        ∀ b ∈ f.rootSet S,
          ∀ c ∈ f.rootSet S,
            ∀ d ∈ f.rootSet S,
              Eq (α := S ⧸ p) ((π : (a : S) → S ⧸ p) a : S ⧸ p) ((π : (a : S) → S ⧸ p) b : S ⧸ p) →
                Eq (α := S ⧸ p) ((π : (a : S) → S ⧸ p) c : S ⧸ p) ((π : (a : S) → S ⧸ p) d : S ⧸ p) →
                  a ≠ b → c ≠ d → Eq (α := Set S) {a, b} {c, d}),
    Eq.{u_2 + 1} (α := Equiv.Perm (↑(f.rootSet S) : Type u_2))
        ((MulAction.toPermHom G (↑(f.rootSet S) : Type u_2) : (a : G) → Equiv.Perm (↑(f.rootSet S) : Type u_2)) g :
          Equiv.Perm (↑(f.rootSet S) : Type u_2))
        (1 : Equiv.Perm (↑(f.rootSet S) : Type u_2)) ∨
      Equiv.Perm.IsSwap.{u_2} (α := (↑(f.rootSet S) : Type u_2))
        ((MulAction.toPermHom G (↑(f.rootSet S) : Type u_2) : (a : G) → Equiv.Perm (↑(f.rootSet S) : Type u_2)) g)
Tactic: classical
  by_cases hfp : f.map (algebraMap R (S ⧸ p)) = 0
  · rw [rootSet_def f (S ⧸ p), aroots_def, hfp, roots_zero, Multiset.toFinset_zero,
      Finset.coe_empty, Set.ncard_empty, zero_add, Set.ncard_le_one_iff_subsingleton,
      ← Set.subsingleton_coe] at hp
    exact Or.inl (Subsingleton.elim _ _)
  let π : S →ₐ[R] S ⧸ p := Ideal.Quotient.mkₐ R p
  rw [← hf.image_rootSet_of_map_ne_zero π hfp, Set.ncard_le_ncard_image_add_one_iff] at hp
  have hπ (x : S) : π (g • x) = π x := (Ideal.Quotient.mk_eq_mk_iff_sub_mem (g • x) x).mpr (hg x)
  rw [or_iff_not_imp_left, Equiv.ext_iff, not_forall]
  rintro ⟨x, hx : g • x ≠ x⟩
  refine ⟨g • x, x, hx, ?_⟩
  ext z
  simp only [Equiv.swap_apply_def, MulAction.toPermHom_apply, MulAction.toPerm_apply]
  split_ifs with hz hz'
  · subst hz
    have key := hp (g • g • x) (g • g • x).2 (g • x) (g • x).2 (g • x) (g • x).2 x x.2
      (by simp [hπ]) (by simp [hπ]) (by simpa [← rootSet.coe_smul]) (by simpa [← rootSet.coe_smul])
    grind [rootSet.coe_smul]
  · simp [hz']
  · grind [rootSet.coe_smul, SetLike.coe_eq_coe]
Cleared hypotheses: hp