-- Lean 4 proof step from Mathlib.Order.NonemptyFiniteChains (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : PartialOrder X
inst_1 : PartialOrder Y
s : NonemptyFiniteChains X
f : X →o Y
a : X
ha' : a ∈ s.finset
ha :
  Membership.mem.{u_2, u_2} (α := Y) (γ := Finset Y) (Finset.image (⇑f : (a : X) → Y) s.finset)
    ((f : (a : X) → Y) a : Y)
b : X
hb' : b ∈ s.finset
hb :
  Membership.mem.{u_2, u_2} (α := Y) (γ := Finset Y) (Finset.image (⇑f : (a : X) → Y) s.finset)
    ((f : (a : X) → Y) b : Y)
inl :
  ∀ (h : Subtype.mk (p := fun (x : X) ↦ x ∈ s.finset) a ha' ≤ Subtype.mk (p := fun (x : X) ↦ x ∈ s.finset) b hb'),
    LE.le.{u_2} (α := ↥(Finset.image (⇑f : (a : X) → Y) s.finset))
        (Subtype.mk (p := fun (x : Y) ↦ Membership.mem (γ := Finset Y) (Finset.image (⇑f : (a : X) → Y) s.finset) x)
            ((f : (a : X) → Y) a) ha :
          ↥(Finset.image (⇑f : (a : X) → Y) s.finset))
        (Subtype.mk (p := fun (x : Y) ↦ Membership.mem (γ := Finset Y) (Finset.image (⇑f : (a : X) → Y) s.finset) x)
            ((f : (a : X) → Y) b) hb :
          ↥(Finset.image (⇑f : (a : X) → Y) s.finset)) ∨
      LE.le.{u_2} (α := ↥(Finset.image (⇑f : (a : X) → Y) s.finset))
        (Subtype.mk (p := fun (x : Y) ↦ Membership.mem (γ := Finset Y) (Finset.image (⇑f : (a : X) → Y) s.finset) x)
            ((f : (a : X) → Y) b) hb :
          ↥(Finset.image (⇑f : (a : X) → Y) s.finset))
        (Subtype.mk (p := fun (x : Y) ↦ Membership.mem (γ := Finset Y) (Finset.image (⇑f : (a : X) → Y) s.finset) x)
            ((f : (a : X) → Y) a) ha :
          ↥(Finset.image (⇑f : (a : X) → Y) s.finset))
⊢ LE.le.{u_2} (α := ↥(Finset.image (⇑f : (a : X) → Y) s.finset))
      (Subtype.mk (p := fun (x : Y) ↦ Membership.mem (γ := Finset Y) (Finset.image (⇑f : (a : X) → Y) s.finset) x)
          ((f : (a : X) → Y) a) ha :
        ↥(Finset.image (⇑f : (a : X) → Y) s.finset))
      (Subtype.mk (p := fun (x : Y) ↦ Membership.mem (γ := Finset Y) (Finset.image (⇑f : (a : X) → Y) s.finset) x)
          ((f : (a : X) → Y) b) hb :
        ↥(Finset.image (⇑f : (a : X) → Y) s.finset)) ∨
    LE.le.{u_2} (α := ↥(Finset.image (⇑f : (a : X) → Y) s.finset))
      (Subtype.mk (p := fun (x : Y) ↦ Membership.mem (γ := Finset Y) (Finset.image (⇑f : (a : X) → Y) s.finset) x)
          ((f : (a : X) → Y) b) hb :
        ↥(Finset.image (⇑f : (a : X) → Y) s.finset))
      (Subtype.mk (p := fun (x : Y) ↦ Membership.mem (γ := Finset Y) (Finset.image (⇑f : (a : X) → Y) s.finset) x)
          ((f : (a : X) → Y) a) ha :
        ↥(Finset.image (⇑f : (a : X) → Y) s.finset))
have inr : ∀ (h : Subtype.mk (p := fun (x : X) ↦ x ∈ s.finset) b hb' ≤ Subtype.mk (p := fun (x : X) ↦ x ∈ s.finset) a ha'),
  LE.le.{u_2} (α := ↥(Finset.image (⇑f : (a : X) → Y) s.finset))
      (Subtype.mk (p := fun (x : Y) ↦ Membership.mem (γ := Finset Y) (Finset.image (⇑f : (a : X) → Y) s.finset) x)
          ((f : (a : X) → Y) a) ha :
        ↥(Finset.image (⇑f : (a : X) → Y) s.finset))
      (Subtype.mk (p := fun (x : Y) ↦ Membership.mem (γ := Finset Y) (Finset.image (⇑f : (a : X) → Y) s.finset) x)
          ((f : (a : X) → Y) b) hb :
        ↥(Finset.image (⇑f : (a : X) → Y) s.finset)) ∨
    LE.le.{u_2} (α := ↥(Finset.image (⇑f : (a : X) → Y) s.finset))
      (Subtype.mk (p := fun (x : Y) ↦ Membership.mem (γ := Finset Y) (Finset.image (⇑f : (a : X) → Y) s.finset) x)
          ((f : (a : X) → Y) b) hb :
        ↥(Finset.image (⇑f : (a : X) → Y) s.finset))
      (Subtype.mk (p := fun (x : Y) ↦ Membership.mem (γ := Finset Y) (Finset.image (⇑f : (a : X) → Y) s.finset) x)
          ((f : (a : X) → Y) a) ha :
        ↥(Finset.image (⇑f : (a : X) → Y) s.finset))
Tactic: obtain h | h := s.comparable ⟨_, ha'⟩ ⟨_, hb'⟩