-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lex/Lemmas.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₂ : Array α} {f : α → β} (w : ∀ x y, x < y → f x < f y) (h : l₁ ≤ l₂) :
    map f l₁ ≤ map f l₂

Proof state:
case mk
α : 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₂ : Array α
f : α → β
w : ∀ (x y : α), x < y → f x < f y
toList✝ : List α
h : { toList := toList✝ } ≤ l₂
⊢ map f { toList := toList✝ } ≤ map f l₂

Tactic:
cases l₂

Result:
case mk.mk
α : 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
f : α → β
w : ∀ (x y : α), x < y → f x < f y
toList✝¹ toList✝ : List α
h : { toList := toList✝¹ } ≤ { toList := toList✝ }
⊢ map f { toList := toList✝¹ } ≤ map f { toList := toList✝ }

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₂ : Array α
f : α → β
w : ∀ (x y : α), x < y → f x < f y
h : l₁ ≤ l₂
⊢ map f l₁ ≤ map f l₂

Tactic:
cases l₁

Result:
case mk
α : 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₂ : Array α
f : α → β
w : ∀ (x y : α), x < y → f x < f y
toList✝ : List α
h : { toList := toList✝ } ≤ l₂
⊢ map f { toList := toList✝ } ≤ map f l₂

Proof state:
case mk.mk
α : 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
f : α → β
w : ∀ (x y : α), x < y → f x < f y
toList✝¹ toList✝ : List α
h : { toList := toList✝¹ } ≤ { toList := toList✝ }
⊢ map f { toList := toList✝¹ } ≤ map f { toList := toList✝ }

Tactic:
simpa using List.map_le w h

Result:
no goals