-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lex.lean
theorem map_le [DecidableEq α] [LT α] [DecidableLT α] [DecidableEq β] [LT β] [DecidableLT β]
    [Std.Irrefl (· < · : α → α → Prop)]
    [Std.Asymm (· < · : α → α → Prop)]
    [Std.Antisymm (¬ · < · : α → α → Prop)]
    [Std.Irrefl (· < · : β → β → Prop)]
    [Std.Asymm (· < · : β → β → Prop)]
    [Std.Antisymm (¬ · < · : β → β → Prop)]
    {l₁ l₂ : List α} {f : α → β} (w : ∀ x y, x < y → f x < f y) (h : l₁ ≤ l₂) :
    map f l₁ ≤ map f l₂

Proof state:
case inr.intro.intro.intro.intro.h.refine_1
α : Type u_1
β : Type u_2
inst✝¹¹ : DecidableEq α
inst✝¹⁰ : LT α
inst✝⁹ : DecidableLT α
inst✝⁸ : DecidableEq β
inst✝⁷ : LT β
inst✝⁶ : DecidableLT β
inst✝⁵ : Std.Irrefl fun x1 x2 => x1 < x2
inst✝⁴ : Std.Asymm fun x1 x2 => x1 < x2
inst✝³ : Std.Antisymm fun x1 x2 => ¬x1 < x2
inst✝² : Std.Irrefl fun x1 x2 => x1 < x2
inst✝¹ : Std.Asymm fun x1 x2 => x1 < x2
inst✝ : Std.Antisymm fun x1 x2 => ¬x1 < x2
l₁ l₂ : List α
f : α → β
w : ∀ (x y : α), x < y → f x < f y
i : Nat
h₁ : i < l₁.length
h₂ : i < l₂.length
w₁ : ∀ (j : Nat) (hj : j < i), l₁[j] = l₂[j]
w₂ : l₁[i] < l₂[i]
⊢ ∀ (j : Nat) (hj : j < i), (map f l₁)[j] = (map f l₂)[j]

Tactic:
simp +contextual [w₁]

Result:
no goals

Proof state:
case inl.h
α : Type u_1
β : Type u_2
inst✝¹¹ : DecidableEq α
inst✝¹⁰ : LT α
inst✝⁹ : DecidableLT α
inst✝⁸ : DecidableEq β
inst✝⁷ : LT β
inst✝⁶ : DecidableLT β
inst✝⁵ : Std.Irrefl fun x1 x2 => x1 < x2
inst✝⁴ : Std.Asymm fun x1 x2 => x1 < x2
inst✝³ : Std.Antisymm fun x1 x2 => ¬x1 < x2
inst✝² : Std.Irrefl fun x1 x2 => x1 < x2
inst✝¹ : Std.Asymm fun x1 x2 => x1 < x2
inst✝ : Std.Antisymm fun x1 x2 => ¬x1 < x2
l₁ l₂ : List α
f : α → β
w : ∀ (x y : α), x < y → f x < f y
h : l₁ = take l₁.length l₂
⊢ map f (take l₁.length l₂) = take (map f (take l₁.length l₂)).length (map f l₂)

Tactic:
simp

Result:
no goals

Proof state:
case inr.intro.intro.intro.intro.h.refine_2
α : Type u_1
β : Type u_2
inst✝¹¹ : DecidableEq α
inst✝¹⁰ : LT α
inst✝⁹ : DecidableLT α
inst✝⁸ : DecidableEq β
inst✝⁷ : LT β
inst✝⁶ : DecidableLT β
inst✝⁵ : Std.Irrefl fun x1 x2 => x1 < x2
inst✝⁴ : Std.Asymm fun x1 x2 => x1 < x2
inst✝³ : Std.Antisymm fun x1 x2 => ¬x1 < x2
inst✝² : Std.Irrefl fun x1 x2 => x1 < x2
inst✝¹ : Std.Asymm fun x1 x2 => x1 < x2
inst✝ : Std.Antisymm fun x1 x2 => ¬x1 < x2
l₁ l₂ : List α
f : α → β
w : ∀ (x y : α), x < y → f x < f y
i : Nat
h₁ : i < l₁.length
h₂ : i < l₂.length
w₁ : ∀ (j : Nat) (hj : j < i), l₁[j] = l₂[j]
w₂ : l₁[i] < l₂[i]
⊢ (map f l₁)[i] < (map f l₂)[i]

Tactic:
simpa using w _ _ w₂

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹¹ : DecidableEq α
inst✝¹⁰ : LT α
inst✝⁹ : DecidableLT α
inst✝⁸ : DecidableEq β
inst✝⁷ : LT β
inst✝⁶ : DecidableLT β
inst✝⁵ : Std.Irrefl fun x1 x2 => x1 < x2
inst✝⁴ : Std.Asymm fun x1 x2 => x1 < x2
inst✝³ : Std.Antisymm fun x1 x2 => ¬x1 < x2
inst✝² : Std.Irrefl fun x1 x2 => x1 < x2
inst✝¹ : Std.Asymm fun x1 x2 => x1 < x2
inst✝ : Std.Antisymm fun x1 x2 => ¬x1 < x2
l₁ l₂ : List α
f : α → β
w : ∀ (x y : α), x < y → f x < f y
h : l₁ ≤ l₂
⊢ map f l₁ ≤ map f l₂

Tactic:
rw [List.le_iff_exists] at h ⊢

Result:
α : Type u_1
β : Type u_2
inst✝¹¹ : DecidableEq α
inst✝¹⁰ : LT α
inst✝⁹ : DecidableLT α
inst✝⁸ : DecidableEq β
inst✝⁷ : LT β
inst✝⁶ : DecidableLT β
inst✝⁵ : Std.Irrefl fun x1 x2 => x1 < x2
inst✝⁴ : Std.Asymm fun x1 x2 => x1 < x2
inst✝³ : Std.Antisymm fun x1 x2 => ¬x1 < x2
inst✝² : Std.Irrefl fun x1 x2 => x1 < x2
inst✝¹ : Std.Asymm fun x1 x2 => x1 < x2
inst✝ : Std.Antisymm fun x1 x2 => ¬x1 < x2
l₁ l₂ : List α
f : α → β
w : ∀ (x y : α), x < y → f x < f y
h : l₁ = take l₁.length l₂ ∨ ∃ i h₁ h₂, (∀ (j : Nat) (hj : j < i), l₁[j] = l₂[j]) ∧ l₁[i] < l₂[i]
⊢ map f l₁ = take (map f l₁).length (map f l₂) ∨
    ∃ i h₁ h₂, (∀ (j : Nat) (hj : j < i), (map f l₁)[j] = (map f l₂)[j]) ∧ (map f l₁)[i] < (map f l₂)[i]

Proof state:
case inl
α : Type u_1
β : Type u_2
inst✝¹¹ : DecidableEq α
inst✝¹⁰ : LT α
inst✝⁹ : DecidableLT α
inst✝⁸ : DecidableEq β
inst✝⁷ : LT β
inst✝⁶ : DecidableLT β
inst✝⁵ : Std.Irrefl fun x1 x2 => x1 < x2
inst✝⁴ : Std.Asymm fun x1 x2 => x1 < x2
inst✝³ : Std.Antisymm fun x1 x2 => ¬x1 < x2
inst✝² : Std.Irrefl fun x1 x2 => x1 < x2
inst✝¹ : Std.Asymm fun x1 x2 => x1 < x2
inst✝ : Std.Antisymm fun x1 x2 => ¬x1 < x2
l₁ l₂ : List α
f : α → β
w : ∀ (x y : α), x < y → f x < f y
h : l₁ = take l₁.length l₂
⊢ map f l₁ = take (map f l₁).length (map f l₂) ∨
    ∃ i h₁ h₂, (∀ (j : Nat) (hj : j < i), (map f l₁)[j] = (map f l₂)[j]) ∧ (map f l₁)[i] < (map f l₂)[i]

Tactic:
left

Result:
case inl.h
α : Type u_1
β : Type u_2
inst✝¹¹ : DecidableEq α
inst✝¹⁰ : LT α
inst✝⁹ : DecidableLT α
inst✝⁸ : DecidableEq β
inst✝⁷ : LT β
inst✝⁶ : DecidableLT β
inst✝⁵ : Std.Irrefl fun x1 x2 => x1 < x2
inst✝⁴ : Std.Asymm fun x1 x2 => x1 < x2
inst✝³ : Std.Antisymm fun x1 x2 => ¬x1 < x2
inst✝² : Std.Irrefl fun x1 x2 => x1 < x2
inst✝¹ : Std.Asymm fun x1 x2 => x1 < x2
inst✝ : Std.Antisymm fun x1 x2 => ¬x1 < x2
l₁ l₂ : List α
f : α → β
w : ∀ (x y : α), x < y → f x < f y
h : l₁ = take l₁.length l₂
⊢ map f l₁ = take (map f l₁).length (map f l₂)

Proof state:
case inl.h
α : Type u_1
β : Type u_2
inst✝¹¹ : DecidableEq α
inst✝¹⁰ : LT α
inst✝⁹ : DecidableLT α
inst✝⁸ : DecidableEq β
inst✝⁷ : LT β
inst✝⁶ : DecidableLT β
inst✝⁵ : Std.Irrefl fun x1 x2 => x1 < x2
inst✝⁴ : Std.Asymm fun x1 x2 => x1 < x2
inst✝³ : Std.Antisymm fun x1 x2 => ¬x1 < x2
inst✝² : Std.Irrefl fun x1 x2 => x1 < x2
inst✝¹ : Std.Asymm fun x1 x2 => x1 < x2
inst✝ : Std.Antisymm fun x1 x2 => ¬x1 < x2
l₁ l₂ : List α
f : α → β
w : ∀ (x y : α), x < y → f x < f y
h : l₁ = take l₁.length l₂
⊢ map f l₁ = take (map f l₁).length (map f l₂)

Tactic:
rw [h]

Result:
case inl.h
α : Type u_1
β : Type u_2
inst✝¹¹ : DecidableEq α
inst✝¹⁰ : LT α
inst✝⁹ : DecidableLT α
inst✝⁸ : DecidableEq β
inst✝⁷ : LT β
inst✝⁶ : DecidableLT β
inst✝⁵ : Std.Irrefl fun x1 x2 => x1 < x2
inst✝⁴ : Std.Asymm fun x1 x2 => x1 < x2
inst✝³ : Std.Antisymm fun x1 x2 => ¬x1 < x2
inst✝² : Std.Irrefl fun x1 x2 => x1 < x2
inst✝¹ : Std.Asymm fun x1 x2 => x1 < x2
inst✝ : Std.Antisymm fun x1 x2 => ¬x1 < x2
l₁ l₂ : List α
f : α → β
w : ∀ (x y : α), x < y → f x < f y
h : l₁ = take l₁.length l₂
⊢ map f (take l₁.length l₂) = take (map f (take l₁.length l₂)).length (map f l₂)