awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.JordanHolder
Goal:
X : Type u
inst : Lattice X
inst_1 : JordanHolderLattice X
s : CompositionSeries X
x : X
hx : x ∈ s
⊢ head (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      s ≤
    x

Tactic:
let ⟨_i, hi⟩ := Set.mem_range.2 hx
  hi ▸ head_le _

Premises used: Iff.mpr, Set.mem_range, Eq.rec, LE.le, _private.0.CompositionSeries.le_last_of_mem.match_1, RelSeries.head, CompositionSeries.head_le
-- Module: Mathlib.Order.JordanHolder
Goal:
X : Type u
inst : Lattice X
inst_1 : JordanHolderLattice X
s : CompositionSeries 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}) ≤
    last (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      s

Tactic:
simp [eraseLast, last, s.strictMono.le_iff_le, Fin.le_iff_val_le_val]

Premises used: RelSeries.last, RelSeries.eraseLast, CompositionSeries.strictMono, StrictMono.le_iff_le, Fin.le_iff_val_le_val
-- Module: Mathlib.Order.JordanHolder
Goal:
X : Type u
inst : Lattice X
inst_1 : JordanHolderLattice X
s : CompositionSeries X
x : X
hx :
  x ≠
    last (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      s
hxs : x ∈ s
rcases :
  ∀
    (i :
      Fin
        (s.length (r :=
            {x : X × X |
              match (motive := X × X → Prop) x with
              | (x, y) => @IsMaximal _ inst _ x y}) +
          1))
    (hx :
      s.toFun (r :=
          {x : X × X |
            match (motive := X × X → Prop) x with
            | (x, y) => @IsMaximal _ inst _ x y})
          i ≠
        last (r :=
          {x : X × X |
            match (motive := X × X → Prop) x with
            | (x, y) => @IsMaximal _ inst _ x y})
          s),
    s.toFun (r :=
        {x : X × X |
          match (motive := X × X → Prop) x with
          | (x, y) => @IsMaximal _ inst _ x y})
        i ∈
      eraseLast (r :=
        {x : X × X |
          match (motive := X × X → Prop) x with
          | (x, y) => @IsMaximal _ inst _ x y})
        s
⊢ x ∈
    eraseLast (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      s

Tactic:
rcases hxs with ⟨i, rfl⟩

Premises used: rfl
-- Module: Mathlib.Order.JordanHolder
Goal:
X : Type u
inst : Lattice X
inst_1 : JordanHolderLattice X
s : CompositionSeries X
i :
  Fin
    (s.length (r :=
        {x : X × X |
          match (motive := X × X → Prop) x with
          | (x, y) => @IsMaximal _ inst _ x y}) +
      1)
hx :
  s.toFun (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      i ≠
    last (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      s
rw :
  s.length (r :=
    {x : X × X |
      match (motive := X × X → Prop) x with
      | (x, y) => @IsMaximal _ inst _ x y})
| (s.length (r :=
        {x : X × X |
          match (motive := X × X → Prop) x with
          | (x, y) => @IsMaximal _ inst _ x y}) -
      1).succ

Tactic:
rw [← Nat.succ_sub (length_pos_of_nontrivial ⟨_, ⟨i, rfl⟩, _, s.last_mem, hx⟩),
      Nat.add_one_sub_one]

Premises used: Nat.add_one_sub_one, RelSeries.last_mem, RelSeries.length_pos_of_nontrivial, Nat.succ_sub, And.intro, Exists.intro, rfl
-- Module: Mathlib.Order.JordanHolder
Goal:
X : Type u
inst : Lattice X
inst_1 : JordanHolderLattice X
s : CompositionSeries X
i :
  Fin
    (s.length (r :=
        {x : X × X |
          match (motive := X × X → Prop) x with
          | (x, y) => @IsMaximal _ inst _ x y}) +
      1)
hx :
  s.toFun (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      i ≠
    last (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      s
conv_rhs :
  (↑i : ℕ) <
    s.length (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
⊢ (↑i : ℕ) <
    (s.length (r :=
          {x : X × X |
            match (motive := X × X → Prop) x with
            | (x, y) => @IsMaximal _ inst _ x y}) -
        1).succ

Tactic:
conv_rhs => rw [← Nat.succ_sub (length_pos_of_nontrivial ⟨_, ⟨i, rfl⟩, _, s.last_mem, hx⟩),
      Nat.add_one_sub_one]

Premises used: Nat.add_one_sub_one, RelSeries.last_mem, RelSeries.length_pos_of_nontrivial, Nat.succ_sub, And.intro, Exists.intro, rfl
-- Module: Mathlib.Order.JordanHolder
Goal:
X : Type u
inst : Lattice X
inst_1 : JordanHolderLattice X
s : CompositionSeries X
i :
  Fin
    (s.length (r :=
        {x : X × X |
          match (motive := X × X → Prop) x with
          | (x, y) => @IsMaximal _ inst _ x y}) +
      1)
hx :
  s.toFun (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      i ≠
    last (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      s
⊢ (↑i : ℕ) ≠
    s.length (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})

Tactic:
simpa [last, s.inj, Fin.ext_iff] using hx

Premises used: Fin.ext_iff, RelSeries.last, CompositionSeries.inj
-- Module: Mathlib.Order.JordanHolder
Goal:
X : Type u
inst : Lattice X
inst_1 : JordanHolderLattice X
s : CompositionSeries X
i :
  Fin
    (s.length (r :=
        {x : X × X |
          match (motive := X × X → Prop) x with
          | (x, y) => @IsMaximal _ inst _ x y}) +
      1)
hx :
  s.toFun (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      i ≠
    last (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      s
⊢ (↑i : ℕ) <
    s.length (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})

Tactic:
exact lt_of_le_of_ne (Nat.le_of_lt_succ i.2) (by simpa [last, s.inj, Fin.ext_iff] using hx)

Premises used: Fin.isLt, Nat.le_of_lt_succ, lt_of_le_of_ne
-- Module: Mathlib.Order.JordanHolder
Goal:
X : Type u
inst : Lattice X
inst_1 : JordanHolderLattice X
s : CompositionSeries X
i :
  Fin
    (s.length (r :=
        {x : X × X |
          match (motive := X × X → Prop) x with
          | (x, y) => @IsMaximal _ inst _ x y}) +
      1)
hx :
  s.toFun (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      i ≠
    last (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      s
⊢ (↑i : ℕ) <
    (s.length (r :=
          {x : X × X |
            match (motive := X × X → Prop) x with
            | (x, y) => @IsMaximal _ inst _ x y}) -
        1).succ

Tactic:
have hi : (i : ℕ) < (s.length - 1).succ := by
    conv_rhs => rw [← Nat.succ_sub (length_pos_of_nontrivial ⟨_, ⟨i, rfl⟩, _, s.last_mem, hx⟩),
      Nat.add_one_sub_one]
    exact lt_of_le_of_ne (Nat.le_of_lt_succ i.2) (by simpa [last, s.inj, Fin.ext_iff] using hx)
-- Module: Mathlib.Order.JordanHolder
Goal:
X : Type u
inst : Lattice X
inst_1 : JordanHolderLattice X
s : CompositionSeries X
i :
  Fin
    (s.length (r :=
        {x : X × X |
          match (motive := X × X → Prop) x with
          | (x, y) => @IsMaximal _ inst _ x y}) +
      1)
hx :
  s.toFun (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      i ≠
    last (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      s
hi :
  (↑i : ℕ) <
    (s.length (r :=
          {x : X × X |
            match (motive := X × X → Prop) x with
            | (x, y) => @IsMaximal _ inst _ x y}) -
        1).succ
⊢ (eraseLast (r :=
          {x : X × X |
            match (motive := X × X → Prop) x with
            | (x, y) => @IsMaximal _ inst _ x y})
          s).toFun
      (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      (⟨(↑i : ℕ), hi⟩ :
        Fin
          ((eraseLast (r :=
                  {x : X × X |
                    match (motive := X × X → Prop) x with
                    | (x, y) => @IsMaximal _ inst _ x y})
                  s).length
              (r :=
              {x : X × X |
                match (motive := X × X → Prop) x with
                | (x, y) => @IsMaximal _ inst _ x y}) +
            1)) =
    s.toFun (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      i

Tactic:
simp
-- Module: Mathlib.Order.JordanHolder
Goal:
X : Type u
inst : Lattice X
inst_1 : JordanHolderLattice X
s : CompositionSeries X
i :
  Fin
    (s.length (r :=
        {x : X × X |
          match (motive := X × X → Prop) x with
          | (x, y) => @IsMaximal _ inst _ x y}) +
      1)
hx :
  s.toFun (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      i ≠
    last (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      s
hi :
  (↑i : ℕ) <
    (s.length (r :=
          {x : X × X |
            match (motive := X × X → Prop) x with
            | (x, y) => @IsMaximal _ inst _ x y}) -
        1).succ
⊢ s.toFun (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      i ∈
    eraseLast (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      s

Tactic:
exact ⟨⟨↑i, hi⟩, by simp⟩
-- Module: Mathlib.Order.JordanHolder
Goal:
X : Type u
inst : Lattice X
inst_1 : JordanHolderLattice X
s : CompositionSeries X
x : X
h :
  0 <
    s.length (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
simp :
  Membership.mem (γ := Set X)
      (range fun (i : Fin (s.length (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2}) - 1 + 1)) ↦
        s.toFun (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2}) ⟨(↑i : ℕ), ⋯⟩)
      x ↔
    x ≠ last (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2}) s ∧
      x ∈ range (s.toFun (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2}))
⊢ x ∈
      eraseLast (r :=
        {x : X × X |
          match (motive := X × X → Prop) x with
          | (x, y) => @IsMaximal _ inst _ x y})
        s ↔
    x ≠
        last (r :=
          {x : X × X |
            match (motive := X × X → Prop) x with
            | (x, y) => @IsMaximal _ inst _ x y})
          s ∧
      x ∈ s

Tactic:
simp only [RelSeries.mem_def, eraseLast]

Premises used: RelSeries.eraseLast, RelSeries.mem_def
-- Module: Mathlib.Order.JordanHolder
Goal:
X : Type u
inst : Lattice X
inst_1 : JordanHolderLattice X
s : CompositionSeries X
x : X
h :
  0 <
    s.length (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
mp :
  Membership.mem (γ := Set X)
      (range fun (i : Fin (s.length (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2}) - 1 + 1)) ↦
        s.toFun (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2}) ⟨(↑i : ℕ), ⋯⟩)
      x →
    x ≠ last (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2}) s ∧
      x ∈ range (s.toFun (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2}))
mpr :
  x ≠ last (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2}) s ∧
      x ∈ range (s.toFun (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2})) →
    Membership.mem (γ := Set X)
      (range fun (i : Fin (s.length (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2}) - 1 + 1)) ↦
        s.toFun (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2}) ⟨(↑i : ℕ), ⋯⟩)
      x
⊢ Membership.mem (γ := Set X)
      (range fun (i : Fin (s.length (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2}) - 1 + 1)) ↦
        s.toFun (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2}) ⟨(↑i : ℕ), ⋯⟩)
      x ↔
    x ≠ last (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2}) s ∧
      x ∈ range (s.toFun (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2}))

Tactic:
constructor
-- Module: Mathlib.Order.JordanHolder
Goal:
X : Type u
inst : Lattice X
inst_1 : JordanHolderLattice X
s : CompositionSeries X
h :
  0 <
    s.length (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
i : Fin (s.length (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2}) - 1 + 1)
⊢ (↑i : ℕ) <
    s.length (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})

Tactic:
lia
-- Module: Mathlib.Order.JordanHolder
Goal:
X : Type u
inst : Lattice X
inst_1 : JordanHolderLattice X
s : CompositionSeries X
h :
  0 <
    s.length (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
i : Fin (s.length (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2}) - 1 + 1)
⊢ (↑i : ℕ) <
    s.length (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})

Tactic:
have hi : (i : ℕ) < s.length := by lia
-- Module: Mathlib.Order.JordanHolder
Goal:
X : Type u
inst : Lattice X
inst_1 : JordanHolderLattice X
s : CompositionSeries X
h :
  0 <
    s.length (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
i : Fin (s.length (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2}) - 1 + 1)
hi :
  (↑i : ℕ) <
    s.length (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
⊢ (fun (i : Fin (s.length (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2}) - 1 + 1)) ↦
          s.toFun (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2}) ⟨(↑i : ℕ), ⋯⟩)
        i ≠
      last (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2}) s ∧
    (fun (i : Fin (s.length (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2}) - 1 + 1)) ↦
          s.toFun (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2}) ⟨(↑i : ℕ), ⋯⟩)
        i ∈
      range (s.toFun (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2}))

Tactic:
simp [last, Fin.ext_iff, ne_of_lt hi, -Set.mem_range, Set.mem_range_self]

Premises used: Set.mem_range_self, Set.mem_range, Fin.ext_iff, RelSeries.last, ne_of_lt
-- Module: Mathlib.Order.JordanHolder
Goal:
X : Type u
inst : Lattice X
inst_1 : JordanHolderLattice X
s : CompositionSeries X
x : X
h_1 :
  0 <
    s.length (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
h :
  x ≠ last (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2}) s ∧
    x ∈ range (s.toFun (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2}))
⊢ Membership.mem (γ := Set X)
    (range fun (i : Fin (s.length (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2}) - 1 + 1)) ↦
      s.toFun (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2}) ⟨(↑i : ℕ), ⋯⟩)
    x

Tactic:
mem_eraseLast_of_ne_of_mem h.1 h.2

Premises used: Set.Mem, And.right, And.left, CompositionSeries.mem_eraseLast_of_ne_of_mem
-- Module: Mathlib.Order.JordanHolder
Goal:
X : Type u
inst : Lattice X
inst_1 : JordanHolderLattice X
s : CompositionSeries X
x : X
h_1 :
  0 <
    s.length (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
h :
  x ≠ last (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2}) s ∧
    x ∈ range (s.toFun (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2}))
⊢ Membership.mem (γ := Set X)
    (range fun (i : Fin (s.length (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2}) - 1 + 1)) ↦
      s.toFun (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2}) ⟨(↑i : ℕ), ⋯⟩)
    x

Tactic:
exact mem_eraseLast_of_ne_of_mem h.1 h.2

Premises used: And.right, And.left, CompositionSeries.mem_eraseLast_of_ne_of_mem
-- Module: Mathlib.Order.JordanHolder
Goal:
X : Type u
inst : Lattice X
inst_1 : JordanHolderLattice X
s : CompositionSeries X
x : X
h :
  0 <
    s.length (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
hx :
  x ∈
    eraseLast (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      s
⊢ x <
    last (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      s

Tactic:
lt_of_le_of_ne (le_last_of_mem ((mem_eraseLast h).1 hx).2) ((mem_eraseLast h).1 hx).1

Premises used: And.right, And.left, CompositionSeries.mem_eraseLast, Iff.mp, CompositionSeries.le_last_of_mem, lt_of_le_of_ne
-- Module: Mathlib.Order.JordanHolder
Goal:
X : Type u
inst : Lattice X
inst_1 : JordanHolderLattice X
s : CompositionSeries X
h :
  0 <
    s.length (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
rw :
  @IsMaximal _ inst _
    (s.toFun (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      (⟨s.length (r :=
              {x : X × X |
                match (motive := X × X → Prop) x with
                | (x, y) => @IsMaximal _ inst _ x y}).pred,
          ⋯⟩ :
        Fin
          (s.length (r :=
              {x : X × X |
                match (motive := X × X → Prop) x with
                | (x, y) => @IsMaximal _ inst _ x y}) +
            1)))
    (s.toFun (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      (Fin.last
        (s.length (r :=
          {x : X × X |
            match (motive := X × X → Prop) x with
            | (x, y) => @IsMaximal _ inst _ x y}))))
⊢ @IsMaximal _ inst _
    ((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}))
    (last (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      s)

Tactic:
rw [last_eraseLast, last]

Premises used: RelSeries.last, RelSeries.last_eraseLast
-- Module: Mathlib.Order.JordanHolder
Goal:
X : Type u
inst : Lattice X
inst_1 : JordanHolderLattice X
s : CompositionSeries X
h :
  0 <
    s.length (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
⊢ s.length (r :=
        {x : X × X |
          match (motive := X × X → Prop) x with
          | (x, y) => @IsMaximal _ inst _ x y}) -
      1 <
    s.length (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})

Tactic:
lia
-- Module: Mathlib.Order.JordanHolder
Goal:
X : Type u
inst : Lattice X
inst_1 : JordanHolderLattice X
s : CompositionSeries X
h :
  0 <
    s.length (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
⊢ Membership.mem (γ := SetRel X X)
    {x : X × X |
      match (motive := X × X → Prop) x with
      | (x, y) => @IsMaximal _ inst _ x y}
    (s.toFun (r :=
        {x : X × X |
          match (motive := X × X → Prop) x with
          | (x, y) => @IsMaximal _ inst _ x y})
        (⟨s.length (r :=
                  {x : X × X |
                    match (motive := X × X → Prop) x with
                    | (x, y) => @IsMaximal _ inst _ x y}) -
                1,
              ⋯⟩ :
            Fin
              (s.length (r :=
                {x : X × X |
                  match (motive := X × X → Prop) x with
                  | (x, y) => @IsMaximal _ inst _ x y}))).castSucc,
      s.toFun (r :=
        {x : X × X |
          match (motive := X × X → Prop) x with
          | (x, y) => @IsMaximal _ inst _ x y})
        (⟨s.length (r :=
                  {x : X × X |
                    match (motive := X × X → Prop) x with
                    | (x, y) => @IsMaximal _ inst _ x y}) -
                1,
              ⋯⟩ :
            Fin
              (s.length (r :=
                {x : X × X |
                  match (motive := X × X → Prop) x with
                  | (x, y) => @IsMaximal _ inst _ x y}))).succ)

Tactic:
have := s.step ⟨s.length - 1, by lia⟩
-- Module: Mathlib.Order.JordanHolder
Goal:
X : Type u
inst : Lattice X
inst_1 : JordanHolderLattice X
s : CompositionSeries X
h :
  0 <
    s.length (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
this :
  @IsMaximal _ inst _
    (s.toFun (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2})
      (⟨s.length (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2}) - 1, ⋯⟩ :
        Fin (s.length (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2}) + 1)))
    (s.toFun (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2})
      ⟨s.length (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2}) - 1 + 1, ⋯⟩)
⊢ @IsMaximal _ inst _
    (s.toFun (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2})
      (⟨s.length (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2}) - 1, ⋯⟩ :
        Fin (s.length (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2}) + 1)))
    (s.toFun (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2})
      ⟨s.length (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2}) - 1 + 1, ⋯⟩)

Tactic:
this
-- Module: Mathlib.Order.JordanHolder
Goal:
X : Type u
inst : Lattice X
inst_1 : JordanHolderLattice X
s : CompositionSeries X
h :
  0 <
    s.length (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
this :
  @IsMaximal _ inst _
    (s.toFun (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2})
      (⟨s.length (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2}) - 1, ⋯⟩ :
        Fin (s.length (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2}) + 1)))
    (s.toFun (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2})
      ⟨s.length (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2}) - 1 + 1, ⋯⟩)
h₁ :
  (↑(Fin.last
          (s.length (r :=
            {x : X × X |
              match (motive := X × X → Prop) x with
              | (x, y) => @IsMaximal _ inst _ x y}))) :
      ℕ) =
    s.length (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2}) - 1 + 1
⊢ @IsMaximal _ inst _
    (s.toFun (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      (⟨s.length (r :=
              {x : X × X |
                match (motive := X × X → Prop) x with
                | (x, y) => @IsMaximal _ inst _ x y}).pred,
          ⋯⟩ :
        Fin
          (s.length (r :=
              {x : X × X |
                match (motive := X × X → Prop) x with
                | (x, y) => @IsMaximal _ inst _ x y}) +
            1)))
    (s.toFun (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      (Fin.last
        (s.length (r :=
          {x : X × X |
            match (motive := X × X → Prop) x with
            | (x, y) => @IsMaximal _ inst _ x y}))))

Tactic:
convert! this using 3