awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
l : List α
inst : Preorder α
⊢ l.SortedLT ↔
    ∀ ⦃i j : ℕ⦄ ⦃hi : i < l.length⦄ ⦃hj : j < l.length⦄,
      i < j →
        getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i hi <
          getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l j hj

Tactic:
⟨fun h _ _ _ _ hij => h.strictMono_get hij, fun h => StrictMono.sortedLT <| fun _ _ => (h ·)⟩

Premises used: StrictMono.sortedLT, List.SortedLT.strictMono_get, Iff.intro
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
l : List α
inst : Preorder α
⊢ l.SortedGT ↔
    ∀ ⦃i j : ℕ⦄ ⦃hi : i < l.length⦄ ⦃hj : j < l.length⦄,
      j < i →
        getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i hi <
          getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l j hj

Tactic:
⟨fun h _ _ _ _ hij => h.strictAnti_get hij, fun h => StrictAnti.sortedGT <| fun _ _ => (h ·)⟩

Premises used: List.SortedGT.strictAnti_get, Iff.intro, StrictAnti.sortedGT
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
inst : Preorder α
l : List α
h : l.SortedLT
⊢ l.SortedLE

Tactic:
h.strictMono_get.monotone.sortedLE

Premises used: StrictMono.monotone, List.SortedLT.strictMono_get, Monotone.sortedLE
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
inst : Preorder α
l : List α
h : l.SortedGT
⊢ l.SortedGE

Tactic:
h.strictAnti_get.antitone.sortedGE

Premises used: List.SortedGT.strictAnti_get, Antitone.sortedGE, StrictAnti.antitone
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
l : List α
inst : Preorder α
h : l.SortedLT
⊢ l.Nodup

Tactic:
h.strictMono_get.injective.nodup

Premises used: StrictMono.injective, List.SortedLT.strictMono_get, Function.Injective.nodup
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
l : List α
inst : Preorder α
h : l.SortedGT
⊢ l.Nodup

Tactic:
h.strictAnti_get.injective.nodup

Premises used: List.SortedGT.strictAnti_get, StrictAnti.injective, Function.Injective.nodup
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
inst : Preorder α
a : α
n : ℕ
⊢ (replicate n a).SortedLE

Tactic:
(pairwise_replicate.mpr (Or.inr le_rfl)).sortedLE

Premises used: Iff.mpr, le_rfl, List.Pairwise.sortedLE, List.pairwise_replicate, Or.inr
-- Module: Mathlib.Data.List.Sort
Goal:
n : ℕ
⊢ ∀ ⦃i j : ℕ⦄ ⦃hi : i < (finRange n).length⦄ ⦃hj : j < (finRange n).length⦄,
    i < j →
      getElem (valid := fun (as : List (Fin n)) (i : ℕ) ↦ i < as.length) (finRange n) i hi <
        getElem (valid := fun (as : List (Fin n)) (i : ℕ) ↦ i < as.length) (finRange n) j hj

Tactic:
simp
-- Module: Mathlib.Data.List.Sort
Goal:
n : ℕ
⊢ (range n).SortedLT

Tactic:
pairwise_lt_range.sortedLT

Premises used: List.pairwise_lt_range, List.Pairwise.sortedLT
-- Module: Mathlib.Data.List.Sort
Goal:
n : ℕ
⊢ (range n).SortedLE

Tactic:
(sortedLT_range n).sortedLE

Premises used: List.SortedLT.sortedLE, List.sortedLT_range
-- Module: Mathlib.Data.List.Sort
Goal:
a b s : ℕ
hs : s ≠ 0
⊢ (range' a b s).SortedLT

Tactic:
(pairwise_lt_range' _ (Nat.pos_of_ne_zero hs)).sortedLT

Premises used: List.pairwise_lt_range', Nat.pos_of_ne_zero, List.Pairwise.sortedLT
-- Module: Mathlib.Data.List.Sort
Goal:
a b s : ℕ
hs : s ≠ 0
⊢ (range' a b s).SortedLE

Tactic:
(sortedLT_range' a b hs).sortedLE

Premises used: List.sortedLT_range', List.SortedLT.sortedLE
-- Module: Mathlib.Data.List.Sort
Goal:
a b s : ℕ
⊢ (range' a b s).SortedLE

Tactic:
(pairwise_le_range' _).sortedLE

Premises used: List.pairwise_le_range', List.Pairwise.sortedLE
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
inst : Preorder α
n : ℕ
f : Fin n → α
⊢ (ofFn f).SortedLE ↔ Monotone f

Tactic:
simp only [sortedLE_iff_monotone_get, Monotone, Fin.forall_iff,
    length_ofFn, get_ofFn, Fin.cast_mk, Fin.mk_le_mk]

Premises used: Fin.mk_le_mk, List.get_ofFn, Monotone, List.length_ofFn, Fin.forall_iff, Fin.cast_mk, List.sortedLE_iff_monotone_get
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
inst : Preorder α
n : ℕ
f : Fin n → α
⊢ (ofFn f).SortedGE ↔ Antitone f

Tactic:
simp only [sortedGE_iff_antitone_get, Antitone, Fin.forall_iff,
    length_ofFn, get_ofFn, Fin.cast_mk, Fin.mk_le_mk]

Premises used: Fin.mk_le_mk, List.get_ofFn, List.length_ofFn, Antitone, Fin.forall_iff, Fin.cast_mk, List.sortedGE_iff_antitone_get
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
inst : Preorder α
n : ℕ
f : Fin n → α
⊢ (ofFn f).SortedLT ↔ StrictMono f

Tactic:
simp only [sortedLT_iff_strictMono_get, StrictMono, Fin.forall_iff,
    length_ofFn, get_ofFn, Fin.cast_mk, Fin.mk_lt_mk]

Premises used: List.get_ofFn, StrictMono, Fin.mk_lt_mk, List.length_ofFn, List.sortedLT_iff_strictMono_get, Fin.forall_iff, Fin.cast_mk
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
inst : Preorder α
n : ℕ
f : Fin n → α
⊢ (ofFn f).SortedGT ↔ StrictAnti f

Tactic:
simp only [sortedGT_iff_strictAnti_get, StrictAnti, Fin.forall_iff,
    length_ofFn, get_ofFn, Fin.cast_mk, Fin.mk_lt_mk]

Premises used: List.get_ofFn, Fin.mk_lt_mk, List.length_ofFn, List.sortedGT_iff_strictAnti_get, Fin.forall_iff, StrictAnti, Fin.cast_mk
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
l : List α
inst : Preorder α
⊢ l.reverse.SortedLE ↔ l.SortedGE

Tactic:
grind
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
l : List α
inst : Preorder α
⊢ l.reverse.SortedGE ↔ l.SortedLE

Tactic:
grind
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
l : List α
inst : Preorder α
⊢ l.reverse.SortedLT ↔ l.SortedGT

Tactic:
grind
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
l : List α
inst : Preorder α
⊢ l.reverse.SortedGT ↔ l.SortedLT

Tactic:
grind
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
inst : Preorder α
l : List αᵒᵈ
⊢ SortedLE (α := α) (map (⇑OrderDual.ofDual : (a : αᵒᵈ) → α) l) ↔ l.SortedGE

Tactic:
grind [OrderDual.ofDual_le_ofDual]

Premises used: OrderDual.ofDual_le_ofDual
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
inst : Preorder α
l : List αᵒᵈ
⊢ SortedGE (α := α) (map (⇑OrderDual.ofDual : (a : αᵒᵈ) → α) l) ↔ l.SortedLE

Tactic:
grind [OrderDual.ofDual_le_ofDual]

Premises used: OrderDual.ofDual_le_ofDual
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
inst : Preorder α
l : List αᵒᵈ
⊢ SortedLT (α := α) (map (⇑OrderDual.ofDual : (a : αᵒᵈ) → α) l) ↔ l.SortedGT

Tactic:
grind [OrderDual.ofDual_lt_ofDual]

Premises used: OrderDual.ofDual_lt_ofDual
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
inst : Preorder α
l : List αᵒᵈ
⊢ SortedGT (α := α) (map (⇑OrderDual.ofDual : (a : αᵒᵈ) → α) l) ↔ l.SortedLT

Tactic:
grind [OrderDual.ofDual_lt_ofDual]

Premises used: OrderDual.ofDual_lt_ofDual
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
inst : Preorder α
l : List α
⊢ SortedLE (α := αᵒᵈ) (map (⇑OrderDual.toDual : (a : α) → αᵒᵈ) l) ↔ l.SortedGE

Tactic:
grind [OrderDual.toDual_le_toDual]

Premises used: OrderDual.toDual_le_toDual
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
inst : Preorder α
l : List α
⊢ SortedGE (α := αᵒᵈ) (map (⇑OrderDual.toDual : (a : α) → αᵒᵈ) l) ↔ l.SortedLE

Tactic:
grind [OrderDual.toDual_le_toDual]

Premises used: OrderDual.toDual_le_toDual
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
inst : Preorder α
l : List α
⊢ SortedLT (α := αᵒᵈ) (map (⇑OrderDual.toDual : (a : α) → αᵒᵈ) l) ↔ l.SortedGT

Tactic:
grind [OrderDual.toDual_lt_toDual]

Premises used: OrderDual.toDual_lt_toDual
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
inst : Preorder α
l : List αᵒᵈ
⊢ SortedGT (α := αᵒᵈᵒᵈ) (map (⇑OrderDual.toDual : (a : αᵒᵈ) → αᵒᵈᵒᵈ) l) ↔ l.SortedLT

Tactic:
grind [OrderDual.toDual_lt_toDual]

Premises used: OrderDual.toDual_lt_toDual
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
inst : PartialOrder α
l : List α
h₁ : l.SortedLE
h₂ : l.Nodup
⊢ l.SortedLT

Tactic:
(h₁.monotone_get.strictMono_of_injective h₂.injective_get).sortedLT

Premises used: List.SortedLE.monotone_get, StrictMono.sortedLT, Monotone.strictMono_of_injective, List.Nodup.injective_get
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
inst : PartialOrder α
l : List α
h₁ : l.SortedGE
h₂ : l.Nodup
⊢ l.SortedGT

Tactic:
(h₁.antitone_get.strictAnti_of_injective h₂.injective_get).sortedGT

Premises used: Antitone.strictAnti_of_injective, List.SortedGE.antitone_get, StrictAnti.sortedGT, List.Nodup.injective_get
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
l : List α
inst : PartialOrder α
⊢ l.SortedLT ↔ l.Nodup ∧ l.SortedLE

Tactic:
⟨fun h => ⟨h.nodup, h.sortedLE⟩, fun h => h.2.sortedLT_of_nodup h.1⟩

Premises used: List.SortedLT.nodup, And.right, And.left, And.intro, Iff.intro, List.SortedLE.sortedLT_of_nodup, List.SortedLT.sortedLE
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
l : List α
inst : PartialOrder α
⊢ l.SortedGT ↔ l.Nodup ∧ l.SortedGE

Tactic:
⟨fun h => ⟨h.nodup, h.sortedGE⟩, fun h => h.2.sortedGT_of_nodup h.1⟩

Premises used: List.SortedGT.nodup, List.SortedGT.sortedGE, And.right, And.left, And.intro, Iff.intro, List.SortedGE.sortedGT_of_nodup
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
inst : PartialOrder α
l₁ l₂ : List α
hl₁ : l₁.SortedLE
hl₂ : l₂.SortedLE
⊢ ∀ (hl₁₂ : l₁ ~ l₂), l₁ = l₂

Tactic:
Perm.eq_of_pairwise' hl₁.pairwise hl₂.pairwise

Premises used: List.SortedLE.pairwise, List.Perm.eq_of_pairwise'
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
inst : PartialOrder α
l₁ l₂ : List α
hl₁ : l₁.SortedGE
hl₂ : l₂.SortedGE
⊢ ∀ (hl₁₂ : l₁ ~ l₂), l₁ = l₂

Tactic:
Perm.eq_of_pairwise' hl₁.pairwise hl₂.pairwise

Premises used: List.SortedGE.pairwise, List.Perm.eq_of_pairwise'
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
inst : PartialOrder α
l₁ l₂ : List α
hl₁₂ : l₁ ⊆ l₂
hl₁₂' : l₂ ⊆ l₁
h₁ : l₁.SortedLT
h₂ : l₂.SortedLT
⊢ l₁ = l₂

Tactic:
hl₁₂.antisymm_of_pairwise h₁.pairwise h₂.pairwise hl₁₂'

Premises used: List.SortedLT.pairwise, List.Subset.antisymm_of_pairwise
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
inst : PartialOrder α
l₁ l₂ : List α
hl₁₂ : l₁ ⊆ l₂
hl₁₂' : l₂ ⊆ l₁
h₁ : l₁.SortedGT
h₂ : l₂.SortedGT
⊢ l₁ = l₂

Tactic:
hl₁₂.antisymm_of_pairwise h₁.pairwise h₂.pairwise hl₁₂'

Premises used: List.Subset.antisymm_of_pairwise, List.SortedGT.pairwise
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
inst : PartialOrder α
l₁ l₂ : List α
h₁ : l₁.SortedLT
h₂ : l₂.SortedLT
⊢ ∀ (h : ∀ (a : α), a ∈ l₁ ↔ a ∈ l₂), l₁ = l₂

Tactic:
h₁.pairwise.eq_of_mem_iff h₂.pairwise

Premises used: List.SortedLT.pairwise, List.Pairwise.eq_of_mem_iff
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
inst : PartialOrder α
l₁ l₂ : List α
h₁ : l₁.SortedGT
h₂ : l₂.SortedGT
h : ∀ (a : α), a ∈ l₁ ↔ a ∈ l₂
⊢ l₁ = l₂

Tactic:
h₁.pairwise.eq_of_mem_iff h₂.pairwise h

Premises used: List.Pairwise.eq_of_mem_iff, List.SortedGT.pairwise
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
inst : PartialOrder α
l₁ l₂ : List α
hp : l₁ ~ l₂
hl₁ : l₁.SortedLE
hl₂ : l₂.SortedGE
⊢ l₁ = l₂.reverse

Tactic:
(perm_reverse.mpr hp).eq_of_sortedLE hl₁ hl₂.reverse

Premises used: Iff.mpr, List.SortedGE.reverse, List.perm_reverse, List.Perm.eq_of_sortedLE
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
inst : PartialOrder α
l₁ l₂ : List α
h : ∀ (a : α), a ∈ l₁ ↔ a ∈ l₂
hl₁ : l₁.SortedLT
hl₂ : l₂.SortedGT
⊢ ∀ (a : α), a ∈ l₁ ↔ a ∈ l₂.reverse

Tactic:
simpa using h
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
inst : PartialOrder α
l₁ l₂ : List α
h : ∀ (a : α), a ∈ l₁ ↔ a ∈ l₂
hl₁ : l₁.SortedGT
hl₂ : l₂.SortedLT
⊢ ∀ (a : α), a ∈ l₁ ↔ a ∈ l₂.reverse

Tactic:
simpa using h
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
inst : PartialOrder α
l₁ l₂ : List α
hp : l₁ <+~ l₂
hl₁ : l₁.SortedLE
hl₂ : l₂.SortedLE
⊢ l₁ <+ l₂

Tactic:
sublist_of_subperm_of_pairwise hp hl₁.pairwise hl₂.pairwise

Premises used: List.sublist_of_subperm_of_pairwise, List.SortedLE.pairwise
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
inst : PartialOrder α
l₁ l₂ : List α
hp : l₁ <+~ l₂
hl₁ : l₁.SortedGE
hl₂ : l₂.SortedGE
⊢ l₁ <+ l₂

Tactic:
sublist_of_subperm_of_pairwise hp hl₁.pairwise hl₂.pairwise

Premises used: List.sublist_of_subperm_of_pairwise, List.SortedGE.pairwise
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
l : List α
inst : LinearOrder α
⊢ (l.mergeSort fun (x1 x2 : α) ↦ decide (x1 ≤ x2)).SortedLE

Tactic:
(pairwise_mergeSort' _ _).sortedLE

Premises used: List.Pairwise.sortedLE, List.pairwise_mergeSort'
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
l : List α
inst : LinearOrder α
⊢ (l.mergeSort fun (x1 x2 : α) ↦ decide (x1 ≥ x2)).SortedGE

Tactic:
(pairwise_mergeSort' _ _).sortedGE

Premises used: List.Pairwise.sortedGE, List.pairwise_mergeSort'
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
l : List α
inst : LinearOrder α
⊢ (insertionSort (fun (x1 x2 : α) ↦ x1 ≤ x2) l).SortedLE

Tactic:
(pairwise_insertionSort _ _).sortedLE

Premises used: List.pairwise_insertionSort, List.Pairwise.sortedLE
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
l : List α
inst : LinearOrder α
⊢ (insertionSort (fun (x1 x2 : α) ↦ x1 ≥ x2) l).SortedGE

Tactic:
(pairwise_insertionSort _ _).sortedGE

Premises used: List.Pairwise.sortedGE, List.pairwise_insertionSort
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
l : List α
inst : LinearOrder α
hl : l.SortedLT
i j : ℕ
hi : i < l.length
hj : j < l.length
⊢ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i hi ≤
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l j hj ↔
    i ≤ j

Tactic:
hl.strictMono_get.le_iff_le

Premises used: List.SortedLT.strictMono_get, StrictMono.le_iff_le
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
l : List α
inst : LinearOrder α
hl : l.SortedGT
i j : ℕ
hi : i < l.length
hj : j < l.length
⊢ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i hi ≤
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l j hj ↔
    j ≤ i

Tactic:
hl.strictAnti_get.le_iff_ge

Premises used: List.SortedGT.strictAnti_get, StrictAnti.le_iff_ge
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
l : List α
inst : LinearOrder α
hl : l.SortedLT
i j : ℕ
hi : i < l.length
hj : j < l.length
⊢ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i hi <
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l j hj ↔
    i < j

Tactic:
hl.strictMono_get.lt_iff_lt

Premises used: StrictMono.lt_iff_lt, List.SortedLT.strictMono_get
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
l : List α
inst : LinearOrder α
hl : l.SortedGT
i j : ℕ
hi : i < l.length
hj : j < l.length
⊢ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i hi <
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l j hj ↔
    j < i

Tactic:
hl.strictAnti_get.lt_iff_gt

Premises used: List.SortedGT.strictAnti_get, StrictAnti.lt_iff_gt
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
β : Type u_2
ra : α → α → Prop
rb : β → β → Prop
e : ra ↪r rb
l : List α
⊢ List.Pairwise rb (map (⇑e : (a : α) → β) l) ↔ List.Pairwise ra l

Tactic:
simp [pairwise_map, e.map_rel_iff]

Premises used: List.pairwise_map, RelEmbedding.map_rel_iff
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
β : Type u_2
ra : α → α → Prop
rb : β → β → Prop
e : ra ↪r rb
l : List α
⊢ List.Pairwise (Function.swap (φ := fun (a a_1 : β) ↦ Prop) rb) (map (⇑e : (a : α) → β) l) ↔
    List.Pairwise (Function.swap (φ := fun (a a_1 : α) ↦ Prop) ra) l

Tactic:
simp [pairwise_map, e.map_rel_iff]

Premises used: List.pairwise_map, RelEmbedding.map_rel_iff
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
β : Type u_2
ra : α → α → Prop
rb : β → β → Prop
e : ra ≃r rb
l : List α
⊢ List.Pairwise rb (List.map (⇑e : (a : α) → β) l) ↔ List.Pairwise ra l

Tactic:
e.toRelEmbedding.pairwise_listMap

Premises used: RelEmbedding.pairwise_listMap, RelIso.toRelEmbedding
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
β : Type u_2
ra : α → α → Prop
rb : β → β → Prop
e : ra ≃r rb
l : List α
⊢ List.Pairwise (Function.swap (φ := fun (a a_1 : β) ↦ Prop) rb) (List.map (⇑e : (a : α) → β) l) ↔
    List.Pairwise (Function.swap (φ := fun (a a_1 : α) ↦ Prop) ra) l

Tactic:
e.toRelEmbedding.pairwise_swap_listMap

Premises used: RelEmbedding.pairwise_swap_listMap, RelIso.toRelEmbedding
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
e : α ↪o β
l : List α
simp_rw :
  List.Pairwise (fun (x1 x2 : β) ↦ x1 ≤ x2) (map (⇑e : (a : α) → β) l) ↔ List.Pairwise (fun (x1 x2 : α) ↦ x1 ≤ x2) l
⊢ SortedLE.{u_2} (α := β) (map (⇑e : (a : α) → β) l) ↔ l.SortedLE

Tactic:
simp_rw [sortedLE_iff_pairwise, e.pairwise_listMap]

Premises used: List.sortedLE_iff_pairwise, RelEmbedding.pairwise_listMap
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
e : α ↪o β
l : List α
simp_rw :
  List.Pairwise (fun (x1 x2 : β) ↦ x1 < x2) (map (⇑e : (a : α) → β) l) ↔ List.Pairwise (fun (x1 x2 : α) ↦ x1 < x2) l
⊢ SortedLT.{u_2} (α := β) (map (⇑e : (a : α) → β) l) ↔ l.SortedLT

Tactic:
simp_rw [sortedLT_iff_pairwise]

Premises used: List.sortedLT_iff_pairwise
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
e : α ↪o β
l : List α
⊢ List.Pairwise (fun (x1 x2 : β) ↦ x1 < x2) (map (⇑e : (a : α) → β) l) ↔ List.Pairwise (fun (x1 x2 : α) ↦ x1 < x2) l

Tactic:
e.ltEmbedding.pairwise_listMap

Premises used: RelEmbedding.pairwise_listMap, OrderEmbedding.ltEmbedding
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
e : α ↪o β
l : List α
⊢ List.Pairwise (fun (x1 x2 : β) ↦ x1 < x2) (map (⇑e : (a : α) → β) l) ↔ List.Pairwise (fun (x1 x2 : α) ↦ x1 < x2) l

Tactic:
exact e.ltEmbedding.pairwise_listMap

Premises used: RelEmbedding.pairwise_listMap, OrderEmbedding.ltEmbedding
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
e : α ↪o β
l : List α
simp_rw : SortedLE.{u_2} (α := β) (reverse (map (⇑e : (a : α) → β) l)) ↔ l.reverse.SortedLE
simp_rw₁ : SortedLE.{u_2} (α := β) (map (⇑e : (a : α) → β) l.reverse) ↔ l.reverse.SortedLE
⊢ SortedGE.{u_2} (α := β) (map (⇑e : (a : α) → β) l) ↔ l.SortedGE

Tactic:
simp_rw [← sortedLE_reverse, ← map_reverse, sortedLE_listMap]

Premises used: List.map_reverse, OrderEmbedding.sortedLE_listMap, List.sortedLE_reverse
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
e : α ↪o β
l : List α
simp_rw : SortedLT.{u_2} (α := β) (reverse (map (⇑e : (a : α) → β) l)) ↔ l.reverse.SortedLT
simp_rw₁ : SortedLT.{u_2} (α := β) (map (⇑e : (a : α) → β) l.reverse) ↔ l.reverse.SortedLT
⊢ SortedGT.{u_2} (α := β) (map (⇑e : (a : α) → β) l) ↔ l.SortedGT

Tactic:
simp_rw [← sortedLT_reverse, ← map_reverse, sortedLT_listMap]

Premises used: OrderEmbedding.sortedLT_listMap, List.map_reverse, List.sortedLT_reverse
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
e : α ≃o β
l : List α
⊢ List.SortedLT.{u_2} (α := β) (List.map (⇑e : (a : α) → β) l) ↔ l.SortedLT

Tactic:
e.toOrderEmbedding.sortedLT_listMap

Premises used: OrderIso.toOrderEmbedding, OrderEmbedding.sortedLT_listMap
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
e : α ≃o β
l : List α
⊢ List.SortedGT.{u_2} (α := β) (List.map (⇑e : (a : α) → β) l) ↔ l.SortedGT

Tactic:
e.toOrderEmbedding.sortedGT_listMap

Premises used: OrderIso.toOrderEmbedding, OrderEmbedding.sortedGT_listMap
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
l : List α
hf : StrictMono f
⊢ (List.map f l).SortedLE ↔ l.SortedLE

Tactic:
(OrderEmbedding.ofStrictMono f hf).sortedLE_listMap

Premises used: OrderEmbedding.ofStrictMono, OrderEmbedding.sortedLE_listMap
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
l : List α
hf : StrictMono f
⊢ (List.map f l).SortedGE ↔ l.SortedGE

Tactic:
(OrderEmbedding.ofStrictMono f hf).sortedGE_listMap

Premises used: OrderEmbedding.sortedGE_listMap, OrderEmbedding.ofStrictMono
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
l : List α
hf : StrictMono f
⊢ (List.map f l).SortedLT ↔ l.SortedLT

Tactic:
(OrderEmbedding.ofStrictMono f hf).sortedLT_listMap

Premises used: OrderEmbedding.sortedLT_listMap, OrderEmbedding.ofStrictMono
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
l : List α
hf : StrictMono f
⊢ (List.map f l).SortedGT ↔ l.SortedGT

Tactic:
(OrderEmbedding.ofStrictMono f hf).sortedGT_listMap

Premises used: OrderEmbedding.ofStrictMono, OrderEmbedding.sortedGT_listMap
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
l : List α
hf : StrictAnti f
⊢ (map f l).SortedLE ↔ l.SortedGE

Tactic:
grind [hf.le_iff_ge]

Premises used: StrictAnti.le_iff_ge
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
l : List α
hf : StrictAnti f
⊢ (map f l).SortedGE ↔ l.SortedLE

Tactic:
grind [hf.le_iff_ge]

Premises used: StrictAnti.le_iff_ge
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
l : List α
hf : StrictAnti f
⊢ (map f l).SortedLT ↔ l.SortedGT

Tactic:
grind [hf.lt_iff_gt]

Premises used: StrictAnti.lt_iff_gt
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
l : List α
hf : StrictAnti f
⊢ (map f l).SortedGT ↔ l.SortedLT

Tactic:
grind [hf.lt_iff_gt]

Premises used: StrictAnti.lt_iff_gt
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
r : α → α → Bool
⊢ splitBy r [] = []

Tactic:
rfl

Premises used: List.splitBy, rfl
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
r : α → α → Bool
a : α
g : List α
gs : List (List α)
⊢ splitBy.loop r [] a g gs = gs.reverse ++ splitBy.loop r [] a g []

Tactic:
simp [splitBy.loop]

Premises used: List.splitBy.loop
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH : ∀ {a : α} {g : List α} (gs : List (List α)), splitBy.loop r l a g gs = gs.reverse ++ splitBy.loop r l a g []
a : α
g : List α
gs : List (List α)
cons :
  (match (motive := Bool → List (List α)) r a b with
    | true => splitBy.loop r l b (a :: g) gs
    | false => splitBy.loop r l b [] ((a :: g).reverse :: gs)) =
    HAppend.hAppend (β := List (List α)) gs.reverse
      (match (motive := Bool → List (List α)) r a b with
        | true => splitBy.loop r l b (a :: g) []
        | false => splitBy.loop r l b [] [(a :: g).reverse] :
        List (List α))
⊢ splitBy.loop r (b :: l) a g gs = gs.reverse ++ splitBy.loop r (b :: l) a g []

Tactic:
simp_rw [splitBy.loop]

Premises used: List.splitBy.loop
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH : ∀ {a : α} {g : List α} (gs : List (List α)), splitBy.loop r l a g gs = gs.reverse ++ splitBy.loop r l a g []
a : α
g : List α
gs : List (List α)
h_1 : ∀ (x : Bool), r a b = true → splitBy.loop r l b (a :: g) gs = gs.reverse ++ splitBy.loop r l b (a :: g) []
h_2 :
  ∀ (x : Bool),
    r a b = false →
      splitBy.loop r l b [] ((a :: g).reverse :: gs) = gs.reverse ++ splitBy.loop r l b [] [(a :: g).reverse]
⊢ (match (motive := Bool → List (List α)) r a b with
    | true => splitBy.loop r l b (a :: g) gs
    | false => splitBy.loop r l b [] ((a :: g).reverse :: gs)) =
    HAppend.hAppend (β := List (List α)) gs.reverse
      (match (motive := Bool → List (List α)) r a b with
        | true => splitBy.loop r l b (a :: g) []
        | false => splitBy.loop r l b [] [(a :: g).reverse] :
        List (List α))

Tactic:
split
-- Module: Mathlib.Data.List.SplitBy
Goal:
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH : ∀ {a : α} {g : List α} (gs : List (List α)), splitBy.loop r l a g gs = gs.reverse ++ splitBy.loop r l a g []
a : α
g : List α
gs : List (List α)
x : Bool
heq : r a b = true
h_1 h_1₁ : gs.reverse ++ splitBy.loop r l b (a :: g) [] = gs.reverse ++ splitBy.loop r l b (a :: g) []
⊢ splitBy.loop r l b (a :: g) gs = gs.reverse ++ splitBy.loop r l b (a :: g) []

Tactic:
rw [IH]