-- Lean 4 proof step from Mathlib.Order.JordanHolder (hypothesis)
Goal:
X : Type u
inst : Lattice X
inst_1 : JordanHolderLattice X
n : ℕ
ih :
  ∀ (s : CompositionSeries X) (x : X)
    (hm :
      @IsMaximal _ inst _ x
        (last (r :=
          {x : X × X |
            match (motive := X × X → Prop) x with
            | (x, y) => @IsMaximal _ inst _ x y})
          s))
    (hb :
      head (r :=
          {x : X × X |
            match (motive := X × X → Prop) x with
            | (x, y) => @IsMaximal _ inst _ x y})
          s ≤
        x)
    (hn :
      s.length (r :=
          {x : X × X |
            match (motive := X × X → Prop) x with
            | (x, y) => @IsMaximal _ inst _ x y}) =
        n),
    ∃ (t : CompositionSeries X),
      head (r :=
            {x : X × X |
              match (motive := X × X → Prop) x with
              | (x, y) => @IsMaximal _ inst _ x y})
            t =
          head (r :=
            {x : X × X |
              match (motive := X × X → Prop) x with
              | (x, y) => @IsMaximal _ inst _ x y})
            s ∧
        t.length (r :=
                {x : X × X |
                  match (motive := X × X → Prop) x with
                  | (x, y) => @IsMaximal _ inst _ x y}) +
              1 =
            n ∧
          ∃ (htx :
            last (r :=
                {x : X × X |
                  match (motive := X × X → Prop) x with
                  | (x, y) => @IsMaximal _ inst _ x y})
                t =
              x),
            s.Equivalent
              (snoc (r :=
                {x : X × X |
                  match (motive := X × X → Prop) x with
                  | (x, y) => @IsMaximal _ inst _ x y})
                t
                (last (r :=
                  {x : X × X |
                    match (motive := X × X → Prop) x with
                    | (x, y) => @IsMaximal _ inst _ x y})
                  s)
                ⋯)
s : CompositionSeries X
x : X
hm :
  @IsMaximal _ inst _ x
    (last (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      s)
hb :
  head (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      s ≤
    x
hn :
  s.length (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y}) =
    n + 1
h0s :
  0 <
    s.length (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
hetx :
  ¬(eraseLast (r :=
            {x : X × X |
              match (motive := X × X → Prop) x with
              | (x, y) => @IsMaximal _ inst _ x y})
            s).last
        (r :=
        {x : X × X |
          match (motive := X × X → Prop) x with
          | (x, y) => @IsMaximal _ inst _ x y}) =
      x
⊢ ∃ (t : CompositionSeries X),
    head (r :=
          {x : X × X |
            match (motive := X × X → Prop) x with
            | (x, y) => @IsMaximal _ inst _ x y})
          t =
        head (r :=
          {x : X × X |
            match (motive := X × X → Prop) x with
            | (x, y) => @IsMaximal _ inst _ x y})
          s ∧
      t.length (r :=
              {x : X × X |
                match (motive := X × X → Prop) x with
                | (x, y) => @IsMaximal _ inst _ x y}) +
            1 =
          n + 1 ∧
        ∃ (htx :
          last (r :=
              {x : X × X |
                match (motive := X × X → Prop) x with
                | (x, y) => @IsMaximal _ inst _ x y})
              t =
            x),
          s.Equivalent
            (snoc (r :=
              {x : X × X |
                match (motive := X × X → Prop) x with
                | (x, y) => @IsMaximal _ inst _ x y})
              t
              (last (r :=
                {x : X × X |
                  match (motive := X × X → Prop) x with
                  | (x, y) => @IsMaximal _ inst _ x y})
                s)
              ⋯)
have imxs : @IsMaximal _ inst _
  (x ⊓
    (eraseLast (r :=
          {x : X × X |
            match (motive := X × X → Prop) x with
            | (x, y) => @IsMaximal _ inst _ x y})
          s).last
      (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y}))
  ((eraseLast (r :=
        {x : X × X |
          match (motive := X × X → Prop) x with
          | (x, y) => @IsMaximal _ inst _ x y})
        s).last
    (r :=
    {x : X × X |
      match (motive := X × X → Prop) x with
      | (x, y) => @IsMaximal _ inst _ x y}))
Tactic: have imxs : IsMaximal (x ⊓ s.eraseLast.last) s.eraseLast.last :=
        isMaximal_of_eq_inf x s.last rfl (Ne.symm hetx) hm (isMaximal_eraseLast_last h0s)