awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.JordanHolder (goal)
Goal:
X : Type u
inst : Lattice X
inst_1 : JordanHolderLattice X
s : CompositionSeries X
⊢ List.IsChain (fun (x1 x2 : X) ↦ x1 < x2)
    (toList (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      s)
have simp_rw : ∀ (i : ℕ) (_hi : i + 1 < (toList (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2}) s).length),
  s.toFun (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2})
      (⟨i, sorry⟩ : 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}) ⟨i + 1, sorry⟩
Tactic: simp_rw [List.isChain_iff_getElem, s.toList_getElem]
-- Lean 4 proof step from Mathlib.Order.JordanHolder (goal)
Goal:
X : Type u
inst : Lattice X
inst_1 : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
h : ∀ (x : X), x ∈ s₁ ↔ x ∈ s₂
⊢ s₁ = s₂
have apply : (toList (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      s₁).toFinset =
  (toList (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      s₂).toFinset
Tactic: apply toList_injective <|
    (List.perm_of_nodup_nodup_toFinset_eq s₁.toList_nodup s₂.toList_nodup _).eq_of_pairwise'
    s₁.toList_sorted.pairwise s₂.toList_sorted.pairwise
-- Lean 4 proof step from Mathlib.Order.JordanHolder (goal)
Goal:
X : Type u
inst : Lattice X
inst_1 : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
h : ∀ (x : X), x ∈ s₁ ↔ x ∈ s₂
⊢ s₁ = s₂
have apply : (toList (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      s₁).toFinset =
  (toList (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      s₂).toFinset
Tactic: classical
  apply toList_injective <|
    (List.perm_of_nodup_nodup_toFinset_eq s₁.toList_nodup s₂.toList_nodup _).eq_of_pairwise'
    s₁.toList_sorted.pairwise s₂.toList_sorted.pairwise
  simpa only [Finset.ext_iff, List.mem_toFinset, RelSeries.mem_toList]
-- Lean 4 proof step from Mathlib.Order.JordanHolder (goal)
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
⊢ x ∈
    eraseLast (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      s
have 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
Tactic: rcases hxs with ⟨i, rfl⟩
Cleared hypotheses: x, hx, hxs
-- Lean 4 proof step from Mathlib.Order.JordanHolder (goal)
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
| (s.length (r :=
        {x : X × X |
          match (motive := X × X → Prop) x with
          | (x, y) => @IsMaximal _ inst _ x y}) -
      1).succ
have rw : s.length (r :=
  {x : X × X |
    match (motive := X × X → Prop) x with
    | (x, y) => @IsMaximal _ inst _ x y})
Tactic: rw [← Nat.succ_sub (length_pos_of_nontrivial ⟨_, ⟨i, rfl⟩, _, s.last_mem, hx⟩),
      Nat.add_one_sub_one]
-- Lean 4 proof step from Mathlib.Order.JordanHolder (goal)
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
have conv_rhs : (↑i : ℕ) <
  s.length (r :=
    {x : X × X |
      match (motive := X × X → Prop) x with
      | (x, y) => @IsMaximal _ inst _ x y})
Tactic: conv_rhs => rw [← Nat.succ_sub (length_pos_of_nontrivial ⟨_, ⟨i, rfl⟩, _, s.last_mem, hx⟩),
      Nat.add_one_sub_one]
-- Lean 4 proof step from Mathlib.Order.JordanHolder (hypothesis)
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
⊢ 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
have hi : (↑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)
-- Lean 4 proof step from Mathlib.Order.JordanHolder (goal)
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})
⊢ 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
have 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 : ℕ), sorry⟩)
    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: simp only [RelSeries.mem_def, eraseLast]
-- Lean 4 proof step from Mathlib.Order.JordanHolder (goal)
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})
⊢ 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}))
have 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 : ℕ), sorry⟩)
    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
-- Lean 4 proof step from Mathlib.Order.JordanHolder (goal)
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}))
⊢ 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}))
have 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 : ℕ), sorry⟩)
    x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.JordanHolder (hypothesis)
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)
⊢ (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}))
have hi : (↑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
-- Lean 4 proof step from Mathlib.Order.JordanHolder (goal)
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})
⊢ @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)
have 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,
        sorry⟩ :
      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: rw [last_eraseLast, last]
-- Lean 4 proof step from Mathlib.Order.JordanHolder (hypothesis)
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})
⊢ @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}))))
have this : 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,
            sorry⟩ :
          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,
            sorry⟩ :
          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⟩
-- Lean 4 proof step from Mathlib.Order.JordanHolder (goal)
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 |
        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}))))
have 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
Tactic: convert! this using 3
-- Lean 4 proof step from Mathlib.Order.JordanHolder (goal)
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 =
    (eraseLast (r :=
          {x : X × X |
            match (motive := X × X → Prop) x with
            | (x, y) => @IsMaximal _ inst _ x y})
          s).snoc
      (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)
      ⋯
have h₁ : ∀ (x : X),
  x ∈ s ↔
    x ∈
      (eraseLast (r :=
            {x : X × X |
              match (motive := X × X → Prop) x with
              | (x, y) => @IsMaximal _ inst _ x y})
            s).snoc
        (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)
        sorry
Tactic: ext x
-- Lean 4 proof step from Mathlib.Order.JordanHolder (goal)
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})
x : X
⊢ x ∈ s ↔
    x ∈
      (eraseLast (r :=
            {x : X × X |
              match (motive := X × X → Prop) x with
              | (x, y) => @IsMaximal _ inst _ x y})
            s).snoc
        (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)
        ⋯
have h₁ : x ∈ s ↔
  ¬x = last (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2}) s ∧ x ∈ s ∨
    x = last (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2}) s
Tactic: simp only [mem_snoc, mem_eraseLast h, ne_eq]
-- Lean 4 proof step from Mathlib.Order.JordanHolder (goal)
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})
x : X
⊢ x ∈ s ↔
    ¬x = last (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2}) s ∧ x ∈ s ∨
      x = last (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2}) s
have pos : ∀
  (h :
    x =
      last (r :=
        {x : X × X |
          match (motive := X × X → Prop) x with
          | (x, y) => @IsMaximal _ inst _ x y})
        s),
  x ∈ s ↔
    ¬x = last (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2}) s ∧ x ∈ s ∨
      x = last (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2}) s
Tactic: by_cases h : x = s.last
-- Lean 4 proof step from Mathlib.Order.JordanHolder (goal)
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})
x : X
pos :
  ∀
    (h :
      x =
        last (r :=
          {x : X × X |
            match (motive := X × X → Prop) x with
            | (x, y) => @IsMaximal _ inst _ x y})
          s),
    x ∈ s ↔
      ¬x = last (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2}) s ∧ x ∈ s ∨
        x = last (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2}) s
⊢ x ∈ s ↔
    ¬x = last (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2}) s ∧ x ∈ s ∨
      x = last (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2}) s
have neg : ∀
  (h :
    ¬x =
        last (r :=
          {x : X × X |
            match (motive := X × X → Prop) x with
            | (x, y) => @IsMaximal _ inst _ x y})
          s),
  x ∈ s ↔
    ¬x = last (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2}) s ∧ x ∈ s ∨
      x = last (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2}) s
Tactic: by_cases h : x = s.last
-- Lean 4 proof step from Mathlib.Order.JordanHolder (hypothesis)
Goal:
X : Type u
inst : Lattice X
inst_1 : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
hb :
  head (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      s₁ =
    head (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      s₂
ht :
  last (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})
      s₂
hs₁ :
  s₁.length (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y}) =
    0
⊢ s₂.length (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y}) =
    0
have this : Eq (α :=
  Fin
    (s₂.length (r :=
        {x : X × X |
          match (motive := X × X → Prop) x with
          | (x, y) => @IsMaximal _ inst _ x y}) +
      1))
  (Fin.last
    (s₂.length (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})))
  0
Tactic: have : Fin.last s₂.length = (0 : Fin s₂.length.succ) :=
    s₂.injective (hb.symm.trans ((congr_arg s₁ (Fin.ext (by simp [hs₁]))).trans ht)).symm
-- Lean 4 proof step from Mathlib.Order.JordanHolder (hypothesis)
Goal:
X : Type u
inst : Lattice X
inst_1 : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
hb :
  head (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      s₁ =
    head (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      s₂
ht :
  last (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})
      s₂
hs₁0 :
  s₁.length (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y}) =
    0
⊢ s₁ = s₂
have this : ∀ (x : X),
  x ∈ s₁ ↔
    x =
      last (r :=
        {x : X × X |
          match (motive := X × X → Prop) x with
          | (x, y) => @IsMaximal _ inst _ x y})
        s₁
Tactic: have : ∀ x, x ∈ s₁ ↔ x = s₁.last := fun x =>
    ⟨fun hx =>  subsingleton_of_length_eq_zero hs₁0 hx s₁.last_mem, fun hx => hx.symm ▸ s₁.last_mem⟩