-- Mathlib/Order/Height.lean
theorem chainHeight_image (f : α → β) (hf : ∀ {x y}, x < y ↔ f x < f y) (s : Set α) :
    (f '' s).chainHeight = s.chainHeight

Proof state:
case a.cons
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
f : α → β
hf : ∀ {x y : α}, x < y ↔ f x < f y
s : Set α
x : β
xs : List β
hx : xs ∈ (f '' s).subchain → ∃ l' ∈ s.subchain, map f l' = xs
h : x :: xs ∈ (f '' s).subchain
⊢ ∃ l' ∈ s.subchain, map f l' = x :: xs

Tactic:
rw [cons_mem_subchain_iff] at h

Result:
case a.cons
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
f : α → β
hf : ∀ {x y : α}, x < y ↔ f x < f y
s : Set α
x : β
xs : List β
hx : xs ∈ (f '' s).subchain → ∃ l' ∈ s.subchain, map f l' = xs
h : x ∈ f '' s ∧ xs ∈ (f '' s).subchain ∧ ∀ b ∈ xs.head?, x < b
⊢ ∃ l' ∈ s.subchain, map f l' = x :: xs

Proof state:
case a
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
f : α → β
hf : ∀ {x y : α}, x < y ↔ f x < f y
s : Set α
⊢ ∀ l ∈ (f '' s).subchain, ∃ l' ∈ s.subchain, map f l' = l

Tactic:
intro l

Result:
case a
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
f : α → β
hf : ∀ {x y : α}, x < y ↔ f x < f y
s : Set α
l : List β
⊢ l ∈ (f '' s).subchain → ∃ l' ∈ s.subchain, map f l' = l

Proof state:
case a.cons.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
f : α → β
hf : ∀ {x y : α}, x < y ↔ f x < f y
s : Set α
x : α
hx' : x ∈ s
l' : List α
h₃ : l' ∈ s.subchain
hx : map f l' ∈ (f '' s).subchain → ∃ l'_1 ∈ s.subchain, map f l'_1 = map f l'
h₁ : map f l' ∈ (f '' s).subchain
h₂ : ∀ b ∈ (map f l').head?, f x < b
⊢ ∃ l'_1 ∈ s.subchain, map f l'_1 = f x :: map f l'

Tactic:
refine ⟨x::l', Set.cons_mem_subchain_iff.mpr ⟨hx', h₃, ?_⟩, rfl⟩

Result:
case a.cons.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
f : α → β
hf : ∀ {x y : α}, x < y ↔ f x < f y
s : Set α
x : α
hx' : x ∈ s
l' : List α
h₃ : l' ∈ s.subchain
hx : map f l' ∈ (f '' s).subchain → ∃ l'_1 ∈ s.subchain, map f l'_1 = map f l'
h₁ : map f l' ∈ (f '' s).subchain
h₂ : ∀ b ∈ (map f l').head?, f x < b
⊢ ∀ b ∈ l'.head?, x < b

Proof state:
case a.cons
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
f : α → β
hf : ∀ {x y : α}, x < y ↔ f x < f y
s : Set α
x : β
xs : List β
hx : xs ∈ (f '' s).subchain → ∃ l' ∈ s.subchain, map f l' = xs
⊢ x :: xs ∈ (f '' s).subchain → ∃ l' ∈ s.subchain, map f l' = x :: xs

Tactic:
intro h

Result:
case a.cons
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
f : α → β
hf : ∀ {x y : α}, x < y ↔ f x < f y
s : Set α
x : β
xs : List β
hx : xs ∈ (f '' s).subchain → ∃ l' ∈ s.subchain, map f l' = xs
h : x :: xs ∈ (f '' s).subchain
⊢ ∃ l' ∈ s.subchain, map f l' = x :: xs

Proof state:
case a.refine_2.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
f : α → β
hf : ∀ {x y : α}, x < y ↔ f x < f y
s : Set α
l : List α
hl : l ∈ s.subchain
a : α
ha : a ∈ l
e : f a ∈ map f l
⊢ f a ∈ f '' s

Tactic:
exact Set.mem_image_of_mem _ (hl.2 _ ha)

Result:
no goals

Proof state:
case a
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
f : α → β
hf : ∀ {x y : α}, x < y ↔ f x < f y
s : Set α
l : List α
hl : l ∈ s.subchain
⊢ ∃ l' ∈ (f '' s).subchain, l.length = l'.length

Tactic:
refine ⟨l.map f, ⟨?_, ?_⟩, ?_⟩

Result:
case a.refine_1
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
f : α → β
hf : ∀ {x y : α}, x < y ↔ f x < f y
s : Set α
l : List α
hl : l ∈ s.subchain
⊢ Chain' (fun x1 x2 => x1 < x2) (map f l)

case a.refine_2
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
f : α → β
hf : ∀ {x y : α}, x < y ↔ f x < f y
s : Set α
l : List α
hl : l ∈ s.subchain
⊢ ∀ i ∈ map f l, i ∈ f '' s

case a.refine_3
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
f : α → β
hf : ∀ {x y : α}, x < y ↔ f x < f y
s : Set α
l : List α
hl : l ∈ s.subchain
⊢ l.length = (map f l).length

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
f : α → β
hf : ∀ {x y : α}, x < y ↔ f x < f y
s : Set α
this : ∀ l ∈ (f '' s).subchain, ∃ l' ∈ s.subchain, map f l' = l
⊢ ∀ l ∈ (f '' s).subchain, ∃ l' ∈ s.subchain, l.length = l'.length

Tactic:
intro l hl

Result:
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
f : α → β
hf : ∀ {x y : α}, x < y ↔ f x < f y
s : Set α
this : ∀ l ∈ (f '' s).subchain, ∃ l' ∈ s.subchain, map f l' = l
l : List β
hl : l ∈ (f '' s).subchain
⊢ ∃ l' ∈ s.subchain, l.length = l'.length

Proof state:
case a.refine_1
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
f : α → β
hf : ∀ {x y : α}, x < y ↔ f x < f y
s : Set α
l : List α
hl : l ∈ s.subchain
⊢ Chain' (fun x1 x2 => x1 < x2) (map f l)

Tactic:
simp_rw [chain'_map, ← hf]

Result:
case a.refine_1
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
f : α → β
hf : ∀ {x y : α}, x < y ↔ f x < f y
s : Set α
l : List α
hl : l ∈ s.subchain
⊢ Chain' (fun a b => a < b) l

Proof state:
case a
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
f : α → β
hf : ∀ {x y : α}, x < y ↔ f x < f y
s : Set α
⊢ ∀ l ∈ (f '' s).subchain, ∃ l' ∈ s.subchain, l.length = l'.length

Tactic:
suffices ∀ l ∈ (f '' s).subchain, ∃ l' ∈ s.subchain, map f l' = l by
  intro l hl
  obtain ⟨l', h₁, rfl⟩ := this l hl
  exact ⟨l', h₁, length_map _ _⟩

Result:
case a
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
f : α → β
hf : ∀ {x y : α}, x < y ↔ f x < f y
s : Set α
⊢ ∀ l ∈ (f '' s).subchain, ∃ l' ∈ s.subchain, map f l' = l

Proof state:
case a.refine_2
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
f : α → β
hf : ∀ {x y : α}, x < y ↔ f x < f y
s : Set α
l : List α
hl : l ∈ s.subchain
i✝ : β
e : i✝ ∈ map f l
⊢ i✝ ∈ f '' s

Tactic:
obtain ⟨a, ha, rfl⟩ := mem_map.mp e

Result:
case a.refine_2.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
f : α → β
hf : ∀ {x y : α}, x < y ↔ f x < f y
s : Set α
l : List α
hl : l ∈ s.subchain
a : α
ha : a ∈ l
e : f a ∈ map f l
⊢ f a ∈ f '' s