-- Mathlib/Data/List/Sort.lean
theorem map_insertionSort (f : α → β) (l : List α) (hl : ∀ a ∈ l, ∀ b ∈ l, a ≼ b ↔ f a ≼ f b) :
    (l.insertionSort r).map f = (l.map f).insertionSort s

Proof state:
case cons
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : DecidableRel r
inst✝ : DecidableRel s
f : α → β
x : α
xs : List α
ih : (∀ a ∈ xs, ∀ b ∈ xs, r a b ↔ s (f a) (f b)) → map f (insertionSort r xs) = insertionSort s (map f xs)
hl :
  ((r x x ↔ s (f x) (f x)) ∧ ∀ x_1 ∈ xs, r x x_1 ↔ s (f x) (f x_1)) ∧
    (∀ x_1 ∈ xs, r x_1 x ↔ s (f x_1) (f x)) ∧ ∀ x ∈ xs, ∀ x_2 ∈ xs, r x x_2 ↔ s (f x) (f x_2)
⊢ map f (orderedInsert r x (insertionSort r xs)) = orderedInsert s (f x) (insertionSort s (map f xs))

Tactic:
rw [List.map_orderedInsert _ s, ih hl.2.2]

Result:
case cons.hl₁
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : DecidableRel r
inst✝ : DecidableRel s
f : α → β
x : α
xs : List α
ih : (∀ a ∈ xs, ∀ b ∈ xs, r a b ↔ s (f a) (f b)) → map f (insertionSort r xs) = insertionSort s (map f xs)
hl :
  ((r x x ↔ s (f x) (f x)) ∧ ∀ x_1 ∈ xs, r x x_1 ↔ s (f x) (f x_1)) ∧
    (∀ x_1 ∈ xs, r x_1 x ↔ s (f x_1) (f x)) ∧ ∀ x ∈ xs, ∀ x_2 ∈ xs, r x x_2 ↔ s (f x) (f x_2)
⊢ ∀ a ∈ insertionSort r xs, r a x ↔ s (f a) (f x)

case cons.hl₂
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : DecidableRel r
inst✝ : DecidableRel s
f : α → β
x : α
xs : List α
ih : (∀ a ∈ xs, ∀ b ∈ xs, r a b ↔ s (f a) (f b)) → map f (insertionSort r xs) = insertionSort s (map f xs)
hl :
  ((r x x ↔ s (f x) (f x)) ∧ ∀ x_1 ∈ xs, r x x_1 ↔ s (f x) (f x_1)) ∧
    (∀ x_1 ∈ xs, r x_1 x ↔ s (f x_1) (f x)) ∧ ∀ x ∈ xs, ∀ x_2 ∈ xs, r x x_2 ↔ s (f x) (f x_2)
⊢ ∀ a ∈ insertionSort r xs, r x a ↔ s (f x) (f a)

Proof state:
case cons.hl₁
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : DecidableRel r
inst✝ : DecidableRel s
f : α → β
x : α
xs : List α
ih : (∀ a ∈ xs, ∀ b ∈ xs, r a b ↔ s (f a) (f b)) → map f (insertionSort r xs) = insertionSort s (map f xs)
hl :
  ((r x x ↔ s (f x) (f x)) ∧ ∀ x_1 ∈ xs, r x x_1 ↔ s (f x) (f x_1)) ∧
    (∀ x_1 ∈ xs, r x_1 x ↔ s (f x_1) (f x)) ∧ ∀ x ∈ xs, ∀ x_2 ∈ xs, r x x_2 ↔ s (f x) (f x_2)
⊢ ∀ a ∈ insertionSort r xs, r a x ↔ s (f a) (f x)

Tactic:
simpa only [mem_insertionSort] using hl.2.1

Result:
no goals

Proof state:
case nil
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : DecidableRel r
inst✝ : DecidableRel s
f : α → β
hl : ∀ a ∈ [], ∀ b ∈ [], r a b ↔ s (f a) (f b)
⊢ map f (insertionSort r []) = insertionSort s (map f [])

Tactic:
simp

Result:
no goals

Proof state:
case cons.hl₂
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : DecidableRel r
inst✝ : DecidableRel s
f : α → β
x : α
xs : List α
ih : (∀ a ∈ xs, ∀ b ∈ xs, r a b ↔ s (f a) (f b)) → map f (insertionSort r xs) = insertionSort s (map f xs)
hl :
  ((r x x ↔ s (f x) (f x)) ∧ ∀ x_1 ∈ xs, r x x_1 ↔ s (f x) (f x_1)) ∧
    (∀ x_1 ∈ xs, r x_1 x ↔ s (f x_1) (f x)) ∧ ∀ x ∈ xs, ∀ x_2 ∈ xs, r x x_2 ↔ s (f x) (f x_2)
⊢ ∀ a ∈ insertionSort r xs, r x a ↔ s (f x) (f a)

Tactic:
simpa only [mem_insertionSort] using hl.1.2

Result:
no goals

Proof state:
case cons
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : DecidableRel r
inst✝ : DecidableRel s
f : α → β
x : α
xs : List α
ih : (∀ a ∈ xs, ∀ b ∈ xs, r a b ↔ s (f a) (f b)) → map f (insertionSort r xs) = insertionSort s (map f xs)
hl :
  ((r x x ↔ s (f x) (f x)) ∧ ∀ x_1 ∈ xs, r x x_1 ↔ s (f x) (f x_1)) ∧
    (∀ x_1 ∈ xs, r x_1 x ↔ s (f x_1) (f x)) ∧ ∀ x ∈ xs, ∀ x_2 ∈ xs, r x x_2 ↔ s (f x) (f x_2)
⊢ map f (insertionSort r (x :: xs)) = insertionSort s (map f (x :: xs))

Tactic:
simp_rw [List.map, List.insertionSort]

Result:
case cons
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : DecidableRel r
inst✝ : DecidableRel s
f : α → β
x : α
xs : List α
ih : (∀ a ∈ xs, ∀ b ∈ xs, r a b ↔ s (f a) (f b)) → map f (insertionSort r xs) = insertionSort s (map f xs)
hl :
  ((r x x ↔ s (f x) (f x)) ∧ ∀ x_1 ∈ xs, r x x_1 ↔ s (f x) (f x_1)) ∧
    (∀ x_1 ∈ xs, r x_1 x ↔ s (f x_1) (f x)) ∧ ∀ x ∈ xs, ∀ x_2 ∈ xs, r x x_2 ↔ s (f x) (f x_2)
⊢ map f (orderedInsert r x (insertionSort r xs)) = orderedInsert s (f x) (insertionSort s (map f xs))

Proof state:
case cons
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : DecidableRel r
inst✝ : DecidableRel s
f : α → β
x : α
xs : List α
ih : (∀ a ∈ xs, ∀ b ∈ xs, r a b ↔ s (f a) (f b)) → map f (insertionSort r xs) = insertionSort s (map f xs)
hl : ∀ a ∈ x :: xs, ∀ b ∈ x :: xs, r a b ↔ s (f a) (f b)
⊢ map f (insertionSort r (x :: xs)) = insertionSort s (map f (x :: xs))

Tactic:
simp_rw [List.forall_mem_cons, forall_and] at hl

Result:
case cons
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : DecidableRel r
inst✝ : DecidableRel s
f : α → β
x : α
xs : List α
ih : (∀ a ∈ xs, ∀ b ∈ xs, r a b ↔ s (f a) (f b)) → map f (insertionSort r xs) = insertionSort s (map f xs)
hl :
  ((r x x ↔ s (f x) (f x)) ∧ ∀ x_1 ∈ xs, r x x_1 ↔ s (f x) (f x_1)) ∧
    (∀ x_1 ∈ xs, r x_1 x ↔ s (f x_1) (f x)) ∧ ∀ x ∈ xs, ∀ x_2 ∈ xs, r x x_2 ↔ s (f x) (f x_2)
⊢ map f (insertionSort r (x :: xs)) = insertionSort s (map f (x :: xs))