-- Mathlib/Data/List/Sort.lean
theorem map_orderedInsert (f : α → β) (l : List α) (x : α)
    (hl₁ : ∀ a ∈ l, a ≼ x ↔ f a ≼ f x) (hl₂ : ∀ a ∈ l, x ≼ a ↔ f x ≼ f a) :
    (l.orderedInsert r x).map f = (l.map f).orderedInsert s (f x)

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

Tactic:
rw [List.forall_mem_cons] at hl₁ hl₂

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

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

Tactic:
simp

Result:
no goals

Proof state:
case neg
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : DecidableRel r
inst✝ : DecidableRel s
f : α → β
x✝ x : α
xs : List α
ih :
  (∀ a ∈ xs, r a x✝ ↔ s (f a) (f x✝)) →
    (∀ a ∈ xs, r x✝ a ↔ s (f x✝) (f a)) → map f (orderedInsert r x✝ xs) = orderedInsert s (f x✝) (map f xs)
hl₁ : (r x x✝ ↔ s (f x) (f x✝)) ∧ ∀ x ∈ xs, r x x✝ ↔ s (f x) (f x✝)
hl₂ : (r x✝ x ↔ s (f x✝) (f x)) ∧ ∀ x ∈ xs, r x✝ x ↔ s (f x✝) (f x)
h✝ : ¬r x✝ x
⊢ map f (x :: orderedInsert r x✝ xs) = f x :: orderedInsert s (f x✝) (map f xs)

Tactic:
rw [List.map, ih (fun _ ha => hl₁.2 _ ha) (fun _ ha => hl₂.2 _ ha)]

Result:
no goals

Proof state:
case pos
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : DecidableRel r
inst✝ : DecidableRel s
f : α → β
x✝ x : α
xs : List α
ih :
  (∀ a ∈ xs, r a x✝ ↔ s (f a) (f x✝)) →
    (∀ a ∈ xs, r x✝ a ↔ s (f x✝) (f a)) → map f (orderedInsert r x✝ xs) = orderedInsert s (f x✝) (map f xs)
hl₁ : (r x x✝ ↔ s (f x) (f x✝)) ∧ ∀ x ∈ xs, r x x✝ ↔ s (f x) (f x✝)
hl₂ : (r x✝ x ↔ s (f x✝) (f x)) ∧ ∀ x ∈ xs, r x✝ x ↔ s (f x✝) (f x)
h✝ : r x✝ x
⊢ map f (x✝ :: x :: xs) = f x✝ :: f x :: map f xs

Tactic:
rw [List.map, List.map]

Result:
no goals

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

Tactic:
simp only [List.map, List.orderedInsert, ← hl₁.1, ← hl₂.1]

Result:
case cons
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : DecidableRel r
inst✝ : DecidableRel s
f : α → β
x✝ x : α
xs : List α
ih :
  (∀ a ∈ xs, r a x✝ ↔ s (f a) (f x✝)) →
    (∀ a ∈ xs, r x✝ a ↔ s (f x✝) (f a)) → map f (orderedInsert r x✝ xs) = orderedInsert s (f x✝) (map f xs)
hl₁ : (r x x✝ ↔ s (f x) (f x✝)) ∧ ∀ x ∈ xs, r x x✝ ↔ s (f x) (f x✝)
hl₂ : (r x✝ x ↔ s (f x✝) (f x)) ∧ ∀ x ∈ xs, r x✝ x ↔ s (f x✝) (f x)
⊢ map f (if r x✝ x then x✝ :: x :: xs else x :: orderedInsert r x✝ xs) =
    if r x✝ x then f x✝ :: f x :: map f xs else f x :: orderedInsert s (f x✝) (map f xs)

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

Tactic:
split_ifs

Result:
case pos
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : DecidableRel r
inst✝ : DecidableRel s
f : α → β
x✝ x : α
xs : List α
ih :
  (∀ a ∈ xs, r a x✝ ↔ s (f a) (f x✝)) →
    (∀ a ∈ xs, r x✝ a ↔ s (f x✝) (f a)) → map f (orderedInsert r x✝ xs) = orderedInsert s (f x✝) (map f xs)
hl₁ : (r x x✝ ↔ s (f x) (f x✝)) ∧ ∀ x ∈ xs, r x x✝ ↔ s (f x) (f x✝)
hl₂ : (r x✝ x ↔ s (f x✝) (f x)) ∧ ∀ x ∈ xs, r x✝ x ↔ s (f x✝) (f x)
h✝ : r x✝ x
⊢ map f (x✝ :: x :: xs) = f x✝ :: f x :: map f xs

case neg
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : DecidableRel r
inst✝ : DecidableRel s
f : α → β
x✝ x : α
xs : List α
ih :
  (∀ a ∈ xs, r a x✝ ↔ s (f a) (f x✝)) →
    (∀ a ∈ xs, r x✝ a ↔ s (f x✝) (f a)) → map f (orderedInsert r x✝ xs) = orderedInsert s (f x✝) (map f xs)
hl₁ : (r x x✝ ↔ s (f x) (f x✝)) ∧ ∀ x ∈ xs, r x x✝ ↔ s (f x) (f x✝)
hl₂ : (r x✝ x ↔ s (f x✝) (f x)) ∧ ∀ x ∈ xs, r x✝ x ↔ s (f x✝) (f x)
h✝ : ¬r x✝ x
⊢ map f (x :: orderedInsert r x✝ xs) = f x :: orderedInsert s (f x✝) (map f xs)