-- Lean 4 proof step from Mathlib.Combinatorics.Colex (goal)
Goal:
α : Type u_1
inst : PartialOrder α
s t u : Finset α
a : α
hst :
  LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))
htu :
  LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) u : Colex (Finset α))
has : a ∈ s
hat : a ∉ t
let let₁ let₂ : ∃ b ∈ u, b ∉ s ∧ a ≤ b
let₃ :
  let s' := {b ∈ s | b ∉ t ∧ a ≤ b};
  ∀ (b : α) (hb : b ∈ s') (hbmax : ∀ ⦃y : α⦄, (fun (x : α) ↦ x ∈ s') y → b ≤ y → y ≤ b), ∃ b ∈ u, b ∉ s ∧ a ≤ b
let₄ :
  ∀ (b : α) (hb : b ∈ s ∧ b ∉ t ∧ a ≤ b) (hbmax : ∀ ⦃y : α⦄, y ∈ s → y ∉ t → a ≤ y → b ≤ y → y ≤ b),
    ∃ b ∈ u, b ∉ s ∧ a ≤ b
let₅ :
  ∀ (b : α) (hb : b ∈ s ∧ b ∉ t ∧ a ≤ b) (hbmax : ∀ ⦃y : α⦄, y ∈ s → y ∉ t → a ≤ y → b ≤ y → y ≤ b) (c : α)
    (hct :
      Membership.mem (γ := Finset α)
        ((ofColex : (a : Colex (Finset α)) → Finset α)
            ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α)) :
          Finset α)
        c)
    (hcs :
      c ∉
        ((ofColex : (a : Colex (Finset α)) → Finset α)
            ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α)) :
          Finset α))
    (hbc : b ≤ c), ∃ b ∈ u, b ∉ s ∧ a ≤ b
pos :
  ∀ (b : α) (hb : b ∈ s ∧ b ∉ t ∧ a ≤ b) (hbmax : ∀ ⦃y : α⦄, y ∈ s → y ∉ t → a ≤ y → b ≤ y → y ≤ b) (c : α)
    (hct :
      Membership.mem (γ := Finset α)
        ((ofColex : (a : Colex (Finset α)) → Finset α)
            ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α)) :
          Finset α)
        c)
    (hcs :
      c ∉
        ((ofColex : (a : Colex (Finset α)) → Finset α)
            ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α)) :
          Finset α))
    (hbc : b ≤ c) (hcu : c ∈ u), ∃ b ∈ u, b ∉ s ∧ a ≤ b
neg neg₁ :
  ∀ (b : α) (hb : b ∈ s ∧ b ∉ t ∧ a ≤ b) (hbmax : ∀ ⦃y : α⦄, y ∈ s → y ∉ t → a ≤ y → b ≤ y → y ≤ b) (c : α)
    (hct :
      Membership.mem (γ := Finset α)
        ((ofColex : (a : Colex (Finset α)) → Finset α)
            ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α)) :
          Finset α)
        c)
    (hcs :
      c ∉
        ((ofColex : (a : Colex (Finset α)) → Finset α)
            ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α)) :
          Finset α))
    (hbc : b ≤ c) (hcu : c ∉ u), ∃ b ∈ u, b ∉ s ∧ a ≤ b
⊢ ∃ b ∈ u, b ∉ s ∧ a ≤ b
have neg₂ : ∀ (b : α) (hb : b ∈ s ∧ b ∉ t ∧ a ≤ b) (hbmax : ∀ ⦃y : α⦄, y ∈ s → y ∉ t → a ≤ y → b ≤ y → y ≤ b) (c : α)
  (hct :
    Membership.mem (γ := Finset α)
      ((ofColex : (a : Colex (Finset α)) → Finset α)
          ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α)) :
        Finset α)
      c)
  (hcs :
    c ∉
      ((ofColex : (a : Colex (Finset α)) → Finset α)
          ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α)) :
        Finset α))
  (hbc : b ≤ c) (hcu : c ∉ u) (d : α)
  (hdu :
    Membership.mem (γ := Finset α)
      ((ofColex : (a : Colex (Finset α)) → Finset α)
          ((toColex : (a : Finset α) → Colex (Finset α)) u : Colex (Finset α)) :
        Finset α)
      d)
  (hdt :
    d ∉
      ((ofColex : (a : Colex (Finset α)) → Finset α)
          ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α)) :
        Finset α))
  (hcd : c ≤ d), ∃ b ∈ u, b ∉ s ∧ a ≤ b
Tactic: classical
  let s' : Finset α := {b ∈ s | b ∉ t ∧ a ≤ b}
  have ⟨b, hb, hbmax⟩ := s'.exists_maximal ⟨a, by simp [s', has, hat]⟩
  simp only [s', mem_filter, and_imp] at hb hbmax
  have ⟨c, hct, hcs, hbc⟩ := hst hb.1 hb.2.1
  by_cases hcu : c ∈ u
  · exact ⟨c, hcu, hcs, hb.2.2.trans hbc⟩
  have ⟨d, hdu, hdt, hcd⟩ := htu hct hcu
  have had : a ≤ d := hb.2.2.trans <| hbc.trans hcd
  refine ⟨d, hdu, fun hds ↦ not_lt_iff_le_imp_ge.2 (hbmax hds hdt had) ?_, had⟩
  exact hbc.trans_lt <| hcd.lt_of_ne <| ne_of_mem_of_not_mem hct hdt