-- 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:
α : 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]
⊢ i < (map f l₂).length

Tactic:
simpa using h₂

Result:
no goals

Proof state:
case inr.intro.intro.intro.intro
α : 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₁ = 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:
right

Result:
case inr.intro.intro.intro.intro.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
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]
⊢ ∃ 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 inr.intro.intro.intro.intro.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
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]
⊢ ∃ 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:
refine ⟨i, by simpa using h₁, by simpa using h₂, ?_, ?_⟩

Result:
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]

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]

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₁ = 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]

Tactic:
obtain (h | ⟨i, h₁, h₂, w₁, w₂⟩) := h

Result:
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]

case inr.intro.intro.intro.intro
α : 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₁ = 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:
α : 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]
⊢ i < (map f l₁).length

Tactic:
simpa using h₁

Result:
no goals