awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Iterate
Goal:
α : Type u_1
inst : Preorder α
f g : α → α
h : Commute f g
hf : StrictMono f
hg : Monotone g
x : α
hx : f x < g x
n : ℕ
hn : 0 < n
⊢ f^[n] x < g^[n] x

Tactic:
@iterate_pos_lt_of_map_lt αᵒᵈ _ g f h.symm hg.dual hf.dual x hx n hn

Premises used: Function.Commute.iterate_pos_lt_of_map_lt, Monotone.dual, StrictMono.dual, OrderDual, Function.Commute.symm
-- Module: Mathlib.Order.Iterate
Goal:
α : Type u_1
inst : LinearOrder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : StrictMono g
x : α
n : ℕ
hn : 0 < n
inl : ∀ (H : f x < g x), f^[n] x < g^[n] x ↔ f x < g x
inr : ∀ (H : f x = g x), f^[n] x < g^[n] x ↔ f x < g x
inr₁ : ∀ (H : g x < f x), f^[n] x < g^[n] x ↔ f x < g x
⊢ f^[n] x < g^[n] x ↔ f x < g x

Tactic:
rcases lt_trichotomy (f x) (g x) with (H | H | H)

Premises used: lt_trichotomy
-- Module: Mathlib.Order.Iterate
Goal:
α : Type u_1
inst : LinearOrder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : StrictMono g
x : α
n : ℕ
hn : 0 < n
H : f x < g x
⊢ f^[n] x < g^[n] x ↔ f x < g x

Tactic:
simp only [*, iterate_pos_lt_of_map_lt]

Premises used: Function.Commute.iterate_pos_lt_of_map_lt
-- Module: Mathlib.Order.Iterate
Goal:
α : Type u_1
inst : LinearOrder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : StrictMono g
x : α
n : ℕ
hn : 0 < n
H : f x = g x
⊢ f^[n] x < g^[n] x ↔ f x < g x

Tactic:
simp only [*, h.iterate_eq_of_map_eq, lt_irrefl]

Premises used: lt_irrefl, Function.Commute.iterate_eq_of_map_eq
-- Module: Mathlib.Order.Iterate
Goal:
α : Type u_1
inst : LinearOrder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : StrictMono g
x : α
n : ℕ
hn : 0 < n
H : g x < f x
⊢ f^[n] x < g^[n] x ↔ f x < g x

Tactic:
simp only [lt_asymm H, lt_asymm (h.symm.iterate_pos_lt_of_map_lt' hg hf H hn)]

Premises used: Function.Commute.iterate_pos_lt_of_map_lt', lt_asymm, Function.Commute.symm
-- Module: Mathlib.Order.Iterate
Goal:
α : Type u_1
inst : LinearOrder α
f g : α → α
h : Commute f g
hf : StrictMono f
hg : Monotone g
x : α
n : ℕ
hn : 0 < n
⊢ f^[n] x < g^[n] x ↔ f x < g x

Tactic:
@iterate_pos_lt_iff_map_lt αᵒᵈ _ _ _ h.symm hg.dual hf.dual x n hn

Premises used: Function.Commute.iterate_pos_lt_iff_map_lt, Monotone.dual, StrictMono.dual, OrderDual, Function.Commute.symm
-- Module: Mathlib.Order.Iterate
Goal:
α : Type u_1
inst : LinearOrder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : StrictMono g
x : α
n : ℕ
hn : 0 < n
⊢ f^[n] x ≤ g^[n] x ↔ f x ≤ g x

Tactic:
simpa only [not_lt] using not_congr (h.symm.iterate_pos_lt_iff_map_lt' hg hf hn)

Premises used: Function.Commute.iterate_pos_lt_iff_map_lt', not_lt, Function.Commute.symm, not_congr
-- Module: Mathlib.Order.Iterate
Goal:
α : Type u_1
inst : LinearOrder α
f g : α → α
h : Commute f g
hf : StrictMono f
hg : Monotone g
x : α
n : ℕ
hn : 0 < n
⊢ f^[n] x ≤ g^[n] x ↔ f x ≤ g x

Tactic:
simpa only [not_lt] using not_congr (h.symm.iterate_pos_lt_iff_map_lt hg hf hn)

Premises used: Function.Commute.iterate_pos_lt_iff_map_lt, not_lt, Function.Commute.symm, not_congr
-- Module: Mathlib.Order.Iterate
Goal:
α : Type u_1
inst : LinearOrder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : StrictMono g
x : α
n : ℕ
hn : 0 < n
⊢ f^[n] x = g^[n] x ↔ f x = g x

Tactic:
simp only [le_antisymm_iff, h.iterate_pos_le_iff_map_le hf hg hn,
    h.symm.iterate_pos_le_iff_map_le' hg hf hn]

Premises used: Function.Commute.iterate_pos_le_iff_map_le', le_antisymm_iff, Function.Commute.iterate_pos_le_iff_map_le, Function.Commute.symm
-- Module: Mathlib.Order.Iterate
Goal:
α : Type u_1
inst : Preorder α
f : α → α
x : α
hf : Monotone f
hx : x ≤ f x
n : ℕ
rw : f^[n] x ≤ f^[n] (f x)
⊢ f^[n] x ≤ f^[n + 1] x

Tactic:
rw [iterate_succ_apply]

Premises used: Function.iterate_succ_apply
-- Module: Mathlib.Order.Iterate
Goal:
α : Type u_1
inst : Preorder α
f : α → α
x : α
hf : Monotone f
hx : x ≤ f x
n : ℕ
⊢ f^[n] x ≤ f^[n] (f x)

Tactic:
hf.iterate n hx

Premises used: Monotone.iterate
-- Module: Mathlib.Order.Iterate
Goal:
α : Type u_1
inst : Preorder α
f : α → α
x : α
hf : Monotone f
hx : x ≤ f x
n : ℕ
⊢ f^[n] x ≤ f^[n] (f x)

Tactic:
exact hf.iterate n hx

Premises used: Monotone.iterate
-- Module: Mathlib.Order.Iterate
Goal:
α : Type u_1
inst : Preorder α
f : α → α
x : α
hf : Monotone f
hx : f x ≤ x
⊢ Antitone.{0, u_1} (β := α) fun (n : ℕ) ↦ f^[n] x

Tactic:
hf.dual.monotone_iterate_of_le_map hx

Premises used: Monotone.monotone_iterate_of_le_map, Antitone, Monotone.dual, OrderDual
-- Module: Mathlib.Order.Iterate
Goal:
α : Type u_1
inst : Preorder α
f : α → α
x : α
hf : StrictMono f
hx : x < f x
n : ℕ
rw : f^[n] x < f^[n] (f x)
⊢ f^[n] x < f^[n + 1] x

Tactic:
rw [iterate_succ_apply]

Premises used: Function.iterate_succ_apply
-- Module: Mathlib.Order.Iterate
Goal:
α : Type u_1
inst : Preorder α
f : α → α
x : α
hf : StrictMono f
hx : x < f x
n : ℕ
⊢ f^[n] x < f^[n] (f x)

Tactic:
hf.iterate n hx

Premises used: StrictMono.iterate
-- Module: Mathlib.Order.Iterate
Goal:
α : Type u_1
inst : Preorder α
f : α → α
x : α
hf : StrictMono f
hx : x < f x
n : ℕ
⊢ f^[n] x < f^[n] (f x)

Tactic:
exact hf.iterate n hx

Premises used: StrictMono.iterate
-- Module: Mathlib.Order.Iterate
Goal:
α : Type u_1
inst : Preorder α
f : α → α
x : α
hf : StrictMono f
hx : f x < x
⊢ StrictAnti.{0, u_1} (β := α) fun (n : ℕ) ↦ f^[n] x

Tactic:
hf.dual.strictMono_iterate_of_lt_map hx

Premises used: StrictAnti, StrictMono.dual, StrictMono.strictMono_iterate_of_lt_map, OrderDual
-- Module: Mathlib.Order.JordanHolder
Goal:
X : Type u
inst : Lattice X
inst_1 : JordanHolderLattice X
x y : X
hxz : @IsMaximal _ inst _ x (x ⊔ y)
hyz : @IsMaximal _ inst _ y (x ⊔ y)
rw : @IsMaximal _ inst _ (y ⊓ x) y
⊢ @IsMaximal _ inst _ (x ⊓ y) y

Tactic:
rw [inf_comm]

Premises used: inf_comm
-- Module: Mathlib.Order.JordanHolder
Goal:
X : Type u
inst : Lattice X
inst_1 : JordanHolderLattice X
x y : X
hxz : @IsMaximal _ inst _ x (x ⊔ y)
hyz : @IsMaximal _ inst _ y (x ⊔ y)
⊢ @IsMaximal _ inst _ x (y ⊔ x)

Tactic:
rw [sup_comm] at hxz hyz

Premises used: sup_comm
-- Module: Mathlib.Order.JordanHolder
Goal:
X : Type u
inst : Lattice X
inst_1 : JordanHolderLattice X
x y : X
hxz : @IsMaximal _ inst _ x (x ⊔ y)
hyz : @IsMaximal _ inst _ y (x ⊔ y)
hxz₁ : @IsMaximal _ inst _ x (y ⊔ x)
⊢ @IsMaximal _ inst _ y (y ⊔ x)

Tactic:
rw [sup_comm] at hxz hyz

Premises used: sup_comm
-- Module: Mathlib.Order.JordanHolder
Goal:
X : Type u
inst : Lattice X
inst_1 : JordanHolderLattice X
x y : X
hxz : @IsMaximal _ inst _ x (y ⊔ x)
hyz : @IsMaximal _ inst _ y (y ⊔ x)
⊢ @IsMaximal _ inst _ (y ⊓ x) y

Tactic:
isMaximal_inf_left_of_isMaximal_sup hyz hxz

Premises used: JordanHolderLattice.isMaximal_inf_left_of_isMaximal_sup
-- Module: Mathlib.Order.JordanHolder
Goal:
X : Type u
inst : Lattice X
inst_1 : JordanHolderLattice X
x y : X
hxz : @IsMaximal _ inst _ x (y ⊔ x)
hyz : @IsMaximal _ inst _ y (y ⊔ x)
⊢ @IsMaximal _ inst _ (y ⊓ x) y

Tactic:
exact isMaximal_inf_left_of_isMaximal_sup hyz hxz

Premises used: JordanHolderLattice.isMaximal_inf_left_of_isMaximal_sup
-- Module: Mathlib.Order.JordanHolder
Goal:
X : Type u
inst : Lattice X
inst_1 : JordanHolderLattice X
x b a y : X
ha : x ⊓ y = a
hxy : x ≠ y
hxb : @IsMaximal _ inst _ x b
hyb : @IsMaximal _ inst _ y b
⊢ x ⊔ y = b

Tactic:
have hb : x ⊔ y = b := sup_eq_of_isMaximal hxb hyb hxy
-- Module: Mathlib.Order.JordanHolder
Goal:
X : Type u
inst : Lattice X
inst_1 : JordanHolderLattice X
x b a y : X
ha : x ⊓ y = a
hxy : x ≠ y
hxb : @IsMaximal _ inst _ x b
hyb : @IsMaximal _ inst _ y b
hb : x ⊔ y = b
substs : ∀ (hxb : @IsMaximal _ inst _ x (x ⊔ y)) (hyb : @IsMaximal _ inst _ y (x ⊔ y)), @IsMaximal _ inst _ (x ⊓ y) y
⊢ @IsMaximal _ inst _ a y

Tactic:
substs a b
-- Module: Mathlib.Order.JordanHolder
Goal:
X : Type u
inst : Lattice X
inst_1 : JordanHolderLattice X
x y : X
hxy : x ≠ y
hxb : @IsMaximal _ inst _ x (x ⊔ y)
hyb : @IsMaximal _ inst _ y (x ⊔ y)
⊢ @IsMaximal _ inst _ (x ⊓ y) y

Tactic:
isMaximal_inf_right_of_isMaximal_sup hxb hyb

Premises used: JordanHolderLattice.isMaximal_inf_right_of_isMaximal_sup
-- Module: Mathlib.Order.JordanHolder
Goal:
X : Type u
inst : Lattice X
inst_1 : JordanHolderLattice X
x y : X
hxy : x ≠ y
hxb : @IsMaximal _ inst _ x (x ⊔ y)
hyb : @IsMaximal _ inst _ y (x ⊔ y)
⊢ @IsMaximal _ inst _ (x ⊓ y) y

Tactic:
exact isMaximal_inf_right_of_isMaximal_sup hxb hyb

Premises used: JordanHolderLattice.isMaximal_inf_right_of_isMaximal_sup
-- Module: Mathlib.Order.JordanHolder
Goal:
X : Type u
inst : Lattice X
inst_1 : JordanHolderLattice X
x y a b : X
hm : @IsMaximal _ inst _ x a
ha : x ⊔ y = a
hb : x ⊓ y = b
substs : ∀ (hm : @IsMaximal _ inst _ x (x ⊔ y)), @Iso _ inst _ (x, x ⊔ y) (x ⊓ y, y)
⊢ @Iso _ inst _ (x, a) (b, y)

Tactic:
substs a b
-- Module: Mathlib.Order.JordanHolder
Goal:
X : Type u
inst : Lattice X
inst_1 : JordanHolderLattice X
x y : X
hm : @IsMaximal _ inst _ x (x ⊔ y)
⊢ @Iso _ inst _ (x, x ⊔ y) (x ⊓ y, y)

Tactic:
second_iso hm

Premises used: JordanHolderLattice.second_iso
-- Module: Mathlib.Order.JordanHolder
Goal:
X : Type u
inst : Lattice X
inst_1 : JordanHolderLattice X
x y : X
hm : @IsMaximal _ inst _ x (x ⊔ y)
⊢ @Iso _ inst _ (x, x ⊔ y) (x ⊓ y, y)

Tactic:
exact second_iso hm

Premises used: JordanHolderLattice.second_iso
-- Module: Mathlib.Order.JordanHolder
Goal:
X : Type u
inst : Lattice X
inst_1 : JordanHolderLattice X
x y : X
h : @IsMaximal _ inst _ x y
⊢ @Iso _ inst _ (x, y) (x, y)

Tactic:
second_iso_of_eq h (sup_eq_right.2 (le_of_lt (lt_of_isMaximal h)))
    (inf_eq_left.2 (le_of_lt (lt_of_isMaximal h)))

Premises used: Iff.mpr, le_of_lt, JordanHolderLattice.lt_of_isMaximal, JordanHolderLattice.second_iso_of_eq, sup_eq_right, inf_eq_left
-- 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}))
⊢ s.toFun (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      i.castSucc <
    s.toFun (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      i.succ

Tactic:
lt_of_isMaximal (s.step _)

Premises used: JordanHolderLattice.lt_of_isMaximal, RelSeries.step
-- Module: Mathlib.Order.JordanHolder
Goal:
X : Type u
inst : Lattice X
inst_1 : JordanHolderLattice X
s : CompositionSeries X
⊢ StrictMono
    (s.toFun (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y}))

Tactic:
Fin.strictMono_iff_lt_succ.2 s.lt_succ

Premises used: Iff.mpr, CompositionSeries.lt_succ, Fin.strictMono_iff_lt_succ
-- Module: Mathlib.Order.JordanHolder
Goal:
X : Type u
inst : Lattice X
inst_1 : JordanHolderLattice X
s : CompositionSeries X
⊢ Function.Injective
    (s.toFun (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y}))

Tactic:
s.strictMono.injective

Premises used: StrictMono.injective, CompositionSeries.strictMono
-- Module: Mathlib.Order.JordanHolder
Goal:
X : Type u
inst : Lattice X
inst_1 : JordanHolderLattice X
s : CompositionSeries X
i j :
  Fin
    s.length (r :=
        {x : X × X |
          match (motive := X × X → Prop) x with
          | (x, y) => @IsMaximal _ inst _ x y}).succ
⊢ s.toFun (r :=
        {x : X × X |
          match (motive := X × X → Prop) x with
          | (x, y) => @IsMaximal _ inst _ x y})
        i =
      s.toFun (r :=
        {x : X × X |
          match (motive := X × X → Prop) x with
          | (x, y) => @IsMaximal _ inst _ x y})
        j ↔
    i = j

Tactic:
s.injective.eq_iff

Premises used: Function.Injective.eq_iff, CompositionSeries.injective
-- Module: Mathlib.Order.JordanHolder
Goal:
X : Type u
inst : Lattice X
inst_1 : JordanHolderLattice X
s : CompositionSeries X
x y : X
hx : x ∈ s
hy : y ∈ 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 ∈
        s),
    s.toFun (r :=
          {x : X × X |
            match (motive := X × X → Prop) x with
            | (x, y) => @IsMaximal _ inst _ x y})
          i ≤
        y ∨
      y ≤
        s.toFun (r :=
          {x : X × X |
            match (motive := X × X → Prop) x with
            | (x, y) => @IsMaximal _ inst _ x y})
          i
⊢ x ≤ y ∨ y ≤ x

Tactic:
rcases Set.mem_range.1 hx with ⟨i, rfl⟩

Premises used: Set.mem_range, Iff.mp, rfl
-- Module: Mathlib.Order.JordanHolder
Goal:
X : Type u
inst : Lattice X
inst_1 : JordanHolderLattice X
s : CompositionSeries X
y : X
hy : y ∈ s
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 ∈
    s
rcases :
  ∀
    (j :
      Fin
        (s.length (r :=
            {x : X × X |
              match (motive := X × X → Prop) x with
              | (x, y) => @IsMaximal _ inst _ x y}) +
          1))
    (hy :
      s.toFun (r :=
          {x : X × X |
            match (motive := X × X → Prop) x with
            | (x, y) => @IsMaximal _ inst _ x y})
          j ∈
        s),
    s.toFun (r :=
          {x : X × X |
            match (motive := X × X → Prop) x with
            | (x, y) => @IsMaximal _ inst _ x y})
          i ≤
        s.toFun (r :=
          {x : X × X |
            match (motive := X × X → Prop) x with
            | (x, y) => @IsMaximal _ inst _ x y})
          j ∨
      s.toFun (r :=
          {x : X × X |
            match (motive := X × X → Prop) x with
            | (x, y) => @IsMaximal _ inst _ x y})
          j ≤
        s.toFun (r :=
          {x : X × X |
            match (motive := X × X → Prop) x with
            | (x, y) => @IsMaximal _ inst _ x y})
          i
⊢ s.toFun (r :=
        {x : X × X |
          match (motive := X × X → Prop) x with
          | (x, y) => @IsMaximal _ inst _ x y})
        i ≤
      y ∨
    y ≤
      s.toFun (r :=
        {x : X × X |
          match (motive := X × X → Prop) x with
          | (x, y) => @IsMaximal _ inst _ x y})
        i

Tactic:
rcases Set.mem_range.1 hy with ⟨j, rfl⟩

Premises used: Set.mem_range, Iff.mp, 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 ∈
    s
j :
  Fin
    (s.length (r :=
        {x : X × X |
          match (motive := X × X → Prop) x with
          | (x, y) => @IsMaximal _ inst _ x y}) +
      1)
hy :
  s.toFun (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      j ∈
    s
rw : i ≤ j ∨ j ≤ i
⊢ s.toFun (r :=
        {x : X × X |
          match (motive := X × X → Prop) x with
          | (x, y) => @IsMaximal _ inst _ x y})
        i ≤
      s.toFun (r :=
        {x : X × X |
          match (motive := X × X → Prop) x with
          | (x, y) => @IsMaximal _ inst _ x y})
        j ∨
    s.toFun (r :=
        {x : X × X |
          match (motive := X × X → Prop) x with
          | (x, y) => @IsMaximal _ inst _ x y})
        j ≤
      s.toFun (r :=
        {x : X × X |
          match (motive := X × X → Prop) x with
          | (x, y) => @IsMaximal _ inst _ x y})
        i

Tactic:
rw [s.strictMono.le_iff_le, s.strictMono.le_iff_le]

Premises used: CompositionSeries.strictMono, StrictMono.le_iff_le
-- 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 ∈
    s
j :
  Fin
    (s.length (r :=
        {x : X × X |
          match (motive := X × X → Prop) x with
          | (x, y) => @IsMaximal _ inst _ x y}) +
      1)
hy :
  s.toFun (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      j ∈
    s
⊢ i ≤ j ∨ j ≤ i

Tactic:
le_total i j

Premises used: le_total
-- 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 ∈
    s
j :
  Fin
    (s.length (r :=
        {x : X × X |
          match (motive := X × X → Prop) x with
          | (x, y) => @IsMaximal _ inst _ x y}) +
      1)
hy :
  s.toFun (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      j ∈
    s
⊢ i ≤ j ∨ j ≤ i

Tactic:
exact le_total i j

Premises used: le_total
-- Module: Mathlib.Order.JordanHolder
Goal:
X : Type u
inst : Lattice X
inst_1 : JordanHolderLattice X
s : CompositionSeries X
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, ⋯⟩ : 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, ⋯⟩
⊢ 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)

Tactic:
simp_rw [List.isChain_iff_getElem, s.toList_getElem]

Premises used: List.isChain_iff_getElem, RelSeries.toList_getElem
-- Module: Mathlib.Order.JordanHolder
Goal:
X : Type u
inst : Lattice X
inst_1 : JordanHolderLattice X
s : CompositionSeries X
⊢ ∀ (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, ⋯⟩ : 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, ⋯⟩

Tactic:
fun _ _ => s.strictMono (Nat.lt_succ_self _)

Premises used: Fin.mk, Nat.lt_succ_self, Fin.val, CompositionSeries.strictMono, List.isChain_iff_getElem._proof_2, RelSeries.toList_getElem._proof_1
-- Module: Mathlib.Order.JordanHolder
Goal:
X : Type u
inst : Lattice X
inst_1 : JordanHolderLattice X
s : CompositionSeries X
⊢ ∀ (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, ⋯⟩ : 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, ⋯⟩

Tactic:
exact fun _ _ => s.strictMono (Nat.lt_succ_self _)

Premises used: CompositionSeries.strictMono
-- Module: Mathlib.Order.JordanHolder
Goal:
X : Type u
inst : Lattice X
inst_1 : JordanHolderLattice X
s : CompositionSeries X
⊢ (toList (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      s).Nodup

Tactic:
s.toList_sorted.nodup

Premises used: List.SortedLT.nodup, CompositionSeries.toList_sorted
-- Module: Mathlib.Order.JordanHolder
Goal:
X : Type u
inst : Lattice X
inst_1 : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
h : ∀ (x : X), x ∈ s₁ ↔ x ∈ s₂
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
⊢ s₁ = s₂

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

Premises used: List.perm_of_nodup_nodup_toFinset_eq, List.SortedLT.pairwise, List.Perm.eq_of_pairwise', RelSeries.toList_injective, CompositionSeries.toList_sorted, CompositionSeries.toList_nodup
-- Module: Mathlib.Order.JordanHolder
Goal:
X : Type u
inst : Lattice X
inst_1 : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
h : ∀ (x : X), x ∈ s₁ ↔ x ∈ s₂
⊢ (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:
simpa only [Finset.ext_iff, List.mem_toFinset, RelSeries.mem_toList]

Premises used: List.mem_toFinset, RelSeries.mem_toList, Finset.ext_iff
-- Module: Mathlib.Order.JordanHolder
Goal:
X : Type u
inst : Lattice X
inst_1 : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
h : ∀ (x : X), x ∈ s₁ ↔ x ∈ s₂
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
⊢ s₁ = s₂

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]

Premises used: List.mem_toFinset, RelSeries.mem_toList, Finset.ext_iff, RelSeries.toList_injective
-- 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)
⊢ 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

Tactic:
s.strictMono.monotone (Fin.le_last _)

Premises used: StrictMono.monotone, RelSeries.last, CompositionSeries.strictMono, Fin.le_last
-- Module: Mathlib.Order.JordanHolder
Goal:
X : Type u
inst : Lattice X
inst_1 : JordanHolderLattice X
s : CompositionSeries X
x : X
hx : x ∈ s
⊢ x ≤
    last (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      s

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

Premises used: Iff.mpr, CompositionSeries.le_last, Set.mem_range, RelSeries.last, Eq.rec, LE.le, _private.0.CompositionSeries.le_last_of_mem.match_1
-- 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)
⊢ head (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

Tactic:
s.strictMono.monotone (Fin.zero_le _)

Premises used: StrictMono.monotone, Fin.zero_le, CompositionSeries.strictMono, RelSeries.head