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

case a
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t : Set α
l : List α
a : α
f : α → β
hf : ∀ {x y : α}, x < y ↔ f x < f y
s : Set α
⊢ ∀ (l : List α), l ∈ subchain s → ∃ l', l' ∈ subchain (f '' s) ∧ length l = length l'
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t : Set α
l : List α
a : α
f : α → β
hf : ∀ {x y : α}, x < y ↔ f x < f y
s : Set α
⊢ chainHeight (f '' s) = chainHeight s
apply le_antisymm <;> rw [chainHeight_le_chainHeight_iff]
case a
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t : Set α
l : List α
a : α
f : α → β
hf : ∀ {x y : α}, x < y ↔ f x < f y
s : Set α
⊢ ∀ (l : List β), l ∈ subchain (f '' s) → ∃ l', l' ∈ subchain s ∧ map f l' = l
case a
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t : Set α
l : List α
a : α
f : α → β
hf : ∀ {x y : α}, x < y ↔ f x < f y
s : Set α
⊢ ∀ (l : List β), l ∈ subchain (f '' s) → ∃ l', l' ∈ subchain s ∧ length l = length l'
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 _ _⟩
case a
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t : Set α
l✝ : List α
a : α
f : α → β
hf : ∀ {x y : α}, x < y ↔ f x < f y
s : Set α
l : List β
⊢ l ∈ subchain (f '' s) → ∃ l', l' ∈ subchain s ∧ map f l' = l
case a
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t : Set α
l : List α
a : α
f : α → β
hf : ∀ {x y : α}, x < y ↔ f x < f y
s : Set α
⊢ ∀ (l : List β), l ∈ subchain (f '' s) → ∃ l', l' ∈ subchain s ∧ map f l' = l
intro l
case a.nil
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t : Set α
l : List α
a : α
f : α → β
hf : ∀ {x y : α}, x < y ↔ f x < f y
s : Set α
⊢ [] ∈ subchain (f '' s) → ∃ l', l' ∈ subchain s ∧ map f l' = []

case a.cons
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t : Set α
l : List α
a : α
f : α → β
hf : ∀ {x y : α}, x < y ↔ f x < f y
s : Set α
x : β
xs : List β
hx : xs ∈ subchain (f '' s) → ∃ l', l' ∈ subchain s ∧ map f l' = xs
⊢ x :: xs ∈ subchain (f '' s) → ∃ l', l' ∈ subchain s ∧ map f l' = x :: xs
case a
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t : Set α
l✝ : List α
a : α
f : α → β
hf : ∀ {x y : α}, x < y ↔ f x < f y
s : Set α
l : List β
⊢ l ∈ subchain (f '' s) → ∃ l', l' ∈ subchain s ∧ map f l' = l
induction' l with x xs hx
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t : Set α
l✝ : List α
a : α
f : α → β
hf : ∀ {x y : α}, x < y ↔ f x < f y
s : Set α
this : ∀ (l : List β), l ∈ subchain (f '' s) → ∃ l', l' ∈ subchain s ∧ map f l' = l
l : List β
hl : l ∈ subchain (f '' s)
⊢ ∃ l', l' ∈ subchain s ∧ length l = length l'
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t : Set α
l : List α
a : α
f : α → β
hf : ∀ {x y : α}, x < y ↔ f x < f y
s : Set α
this : ∀ (l : List β), l ∈ subchain (f '' s) → ∃ l', l' ∈ subchain s ∧ map f l' = l
⊢ ∀ (l : List β), l ∈ subchain (f '' s) → ∃ l', l' ∈ subchain s ∧ length l = length l'
intro l hl
case intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t : Set α
l : List α
a : α
f : α → β
hf : ∀ {x y : α}, x < y ↔ f x < f y
s : Set α
this : ∀ (l : List β), l ∈ subchain (f '' s) → ∃ l', l' ∈ subchain s ∧ map f l' = l
l' : List α
h₁ : l' ∈ subchain s
hl : map f l' ∈ subchain (f '' s)
⊢ ∃ l'_1, l'_1 ∈ subchain s ∧ length (map f l') = length l'_1
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t : Set α
l✝ : List α
a : α
f : α → β
hf : ∀ {x y : α}, x < y ↔ f x < f y
s : Set α
this : ∀ (l : List β), l ∈ subchain (f '' s) → ∃ l', l' ∈ subchain s ∧ map f l' = l
l : List β
hl : l ∈ subchain (f '' s)
⊢ ∃ l', l' ∈ subchain s ∧ length l = length l'
obtain ⟨l', h₁, rfl⟩ := this l hl
no goals
case intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t : Set α
l : List α
a : α
f : α → β
hf : ∀ {x y : α}, x < y ↔ f x < f y
s : Set α
this : ∀ (l : List β), l ∈ subchain (f '' s) → ∃ l', l' ∈ subchain s ∧ map f l' = l
l' : List α
h₁ : l' ∈ subchain s
hl : map f l' ∈ subchain (f '' s)
⊢ ∃ l'_1, l'_1 ∈ subchain s ∧ length (map f l') = length l'_1
exact ⟨l', h₁, length_map _ _⟩
no goals
case a.nil
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t : Set α
l : List α
a : α
f : α → β
hf : ∀ {x y : α}, x < y ↔ f x < f y
s : Set α
⊢ [] ∈ subchain (f '' s) → ∃ l', l' ∈ subchain s ∧ map f l' = []
exact fun _ ↦ ⟨nil, ⟨trivial, fun x h ↦ (not_mem_nil x h).elim⟩, rfl⟩
case a.cons
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t : Set α
l : List α
a : α
f : α → β
hf : ∀ {x y : α}, x < y ↔ f x < f y
s : Set α
x : β
xs : List β
hx : xs ∈ subchain (f '' s) → ∃ l', l' ∈ subchain s ∧ map f l' = xs
h : x :: xs ∈ subchain (f '' s)
⊢ ∃ l', l' ∈ subchain s ∧ map f l' = x :: xs
case a.cons
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t : Set α
l : List α
a : α
f : α → β
hf : ∀ {x y : α}, x < y ↔ f x < f y
s : Set α
x : β
xs : List β
hx : xs ∈ subchain (f '' s) → ∃ l', l' ∈ subchain s ∧ map f l' = xs
⊢ x :: xs ∈ subchain (f '' s) → ∃ l', l' ∈ subchain s ∧ map f l' = x :: xs
intro h
case a.cons
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t : Set α
l : List α
a : α
f : α → β
hf : ∀ {x y : α}, x < y ↔ f x < f y
s : Set α
x : β
xs : List β
hx : xs ∈ subchain (f '' s) → ∃ l', l' ∈ subchain s ∧ map f l' = xs
h : x ∈ f '' s ∧ xs ∈ subchain (f '' s) ∧ ∀ (b : β), b ∈ head? xs → x < b
⊢ ∃ l', l' ∈ subchain s ∧ map f l' = x :: xs
case a.cons
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t : Set α
l : List α
a : α
f : α → β
hf : ∀ {x y : α}, x < y ↔ f x < f y
s : Set α
x : β
xs : List β
hx : xs ∈ subchain (f '' s) → ∃ l', l' ∈ subchain s ∧ map f l' = xs
h : x :: xs ∈ subchain (f '' s)
⊢ ∃ l', l' ∈ subchain s ∧ map f l' = x :: xs
rw [cons_mem_subchain_iff] at h
case a.cons.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t : Set α
l : List α
a : α
f : α → β
hf : ∀ {x y : α}, x < y ↔ f x < f y
s : Set α
xs : List β
hx : xs ∈ subchain (f '' s) → ∃ l', l' ∈ subchain s ∧ map f l' = xs
x : α
hx' : x ∈ s
h₁ : xs ∈ subchain (f '' s)
h₂ : ∀ (b : β), b ∈ head? xs → f x < b
⊢ ∃ l', l' ∈ subchain s ∧ map f l' = f x :: xs
case a.cons
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t : Set α
l : List α
a : α
f : α → β
hf : ∀ {x y : α}, x < y ↔ f x < f y
s : Set α
x : β
xs : List β
hx : xs ∈ subchain (f '' s) → ∃ l', l' ∈ subchain s ∧ map f l' = xs
h : x ∈ f '' s ∧ xs ∈ subchain (f '' s) ∧ ∀ (b : β), b ∈ head? xs → x < b
⊢ ∃ l', l' ∈ subchain s ∧ map f l' = x :: xs
obtain ⟨⟨x, hx', rfl⟩, h₁, h₂⟩ := h
case a.cons.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t : Set α
l : List α
a : α
f : α → β
hf : ∀ {x y : α}, x < y ↔ f x < f y
s : Set α
x : α
hx' : x ∈ s
l' : List α
h₃ : l' ∈ subchain s
hx : map f l' ∈ subchain (f '' s) → ∃ l'_1, l'_1 ∈ subchain s ∧ map f l'_1 = map f l'
h₁ : map f l' ∈ subchain (f '' s)
h₂ : ∀ (b : β), b ∈ head? (map f l') → f x < b
⊢ ∃ l'_1, l'_1 ∈ subchain s ∧ map f l'_1 = f x :: map f l'
case a.cons.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t : Set α
l : List α
a : α
f : α → β
hf : ∀ {x y : α}, x < y ↔ f x < f y
s : Set α
xs : List β
hx : xs ∈ subchain (f '' s) → ∃ l', l' ∈ subchain s ∧ map f l' = xs
x : α
hx' : x ∈ s
h₁ : xs ∈ subchain (f '' s)
h₂ : ∀ (b : β), b ∈ head? xs → f x < b
⊢ ∃ l', l' ∈ subchain s ∧ map f l' = f x :: xs
obtain ⟨l', h₃, rfl⟩ := hx h₁
case a.cons.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t : Set α
l : List α
a : α
f : α → β
hf : ∀ {x y : α}, x < y ↔ f x < f y
s : Set α
x : α
hx' : x ∈ s
l' : List α
h₃ : l' ∈ subchain s
hx : map f l' ∈ subchain (f '' s) → ∃ l'_1, l'_1 ∈ subchain s ∧ map f l'_1 = map f l'
h₁ : map f l' ∈ subchain (f '' s)
h₂ : ∀ (b : β), b ∈ head? (map f l') → f x < b
⊢ ∀ (b : α), b ∈ head? l' → x < b
case a.cons.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t : Set α
l : List α
a : α
f : α → β
hf : ∀ {x y : α}, x < y ↔ f x < f y
s : Set α
x : α
hx' : x ∈ s
l' : List α
h₃ : l' ∈ subchain s
hx : map f l' ∈ subchain (f '' s) → ∃ l'_1, l'_1 ∈ subchain s ∧ map f l'_1 = map f l'
h₁ : map f l' ∈ subchain (f '' s)
h₂ : ∀ (b : β), b ∈ head? (map f l') → f x < b
⊢ ∃ l'_1, l'_1 ∈ subchain s ∧ map f l'_1 = f x :: map f l'
refine' ⟨x::l', Set.cons_mem_subchain_iff.mpr ⟨hx', h₃, _⟩, rfl⟩
case a.cons.intro.intro.intro.intro.intro.intro.nil
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t : Set α
l : List α
a : α
f : α → β
hf : ∀ {x y : α}, x < y ↔ f x < f y
s : Set α
x : α
hx' : x ∈ s
h₃ : [] ∈ subchain s
hx : map f [] ∈ subchain (f '' s) → ∃ l', l' ∈ subchain s ∧ map f l' = map f []
h₁ : map f [] ∈ subchain (f '' s)
h₂ : ∀ (b : β), b ∈ head? (map f []) → f x < b
⊢ ∀ (b : α), b ∈ head? [] → x < b

case a.cons.intro.intro.intro.intro.intro.intro.cons
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t : Set α
l : List α
a : α
f : α → β
hf : ∀ {x y : α}, x < y ↔ f x < f y
s : Set α
x : α
hx' : x ∈ s
head✝ : α
tail✝ : List α
h₃ : head✝ :: tail✝ ∈ subchain s
hx : map f (head✝ :: tail✝) ∈ subchain (f '' s) → ∃ l', l' ∈ subchain s ∧ map f l' = map f (head✝ :: tail✝)
h₁ : map f (head✝ :: tail✝) ∈ subchain (f '' s)
h₂ : ∀ (b : β), b ∈ head? (map f (head✝ :: tail✝)) → f x < b
⊢ ∀ (b : α), b ∈ head? (head✝ :: tail✝) → x < b
case a.cons.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t : Set α
l : List α
a : α
f : α → β
hf : ∀ {x y : α}, x < y ↔ f x < f y
s : Set α
x : α
hx' : x ∈ s
l' : List α
h₃ : l' ∈ subchain s
hx : map f l' ∈ subchain (f '' s) → ∃ l'_1, l'_1 ∈ subchain s ∧ map f l'_1 = map f l'
h₁ : map f l' ∈ subchain (f '' s)
h₂ : ∀ (b : β), b ∈ head? (map f l') → f x < b
⊢ ∀ (b : α), b ∈ head? l' → x < b
cases l'
no goals
case a.cons.intro.intro.intro.intro.intro.intro.nil
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t : Set α
l : List α
a : α
f : α → β
hf : ∀ {x y : α}, x < y ↔ f x < f y
s : Set α
x : α
hx' : x ∈ s
h₃ : [] ∈ subchain s
hx : map f [] ∈ subchain (f '' s) → ∃ l', l' ∈ subchain s ∧ map f l' = map f []
h₁ : map f [] ∈ subchain (f '' s)
h₂ : ∀ (b : β), b ∈ head? (map f []) → f x < b
⊢ ∀ (b : α), b ∈ head? [] → x < b
simp
no goals
case a.cons.intro.intro.intro.intro.intro.intro.cons
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t : Set α
l : List α
a : α
f : α → β
hf : ∀ {x y : α}, x < y ↔ f x < f y
s : Set α
x : α
hx' : x ∈ s
head✝ : α
tail✝ : List α
h₃ : head✝ :: tail✝ ∈ subchain s
hx : map f (head✝ :: tail✝) ∈ subchain (f '' s) → ∃ l', l' ∈ subchain s ∧ map f l' = map f (head✝ :: tail✝)
h₁ : map f (head✝ :: tail✝) ∈ subchain (f '' s)
h₂ : ∀ (b : β), b ∈ head? (map f (head✝ :: tail✝)) → f x < b
⊢ ∀ (b : α), b ∈ head? (head✝ :: tail✝) → x < b
simpa [← hf] using h₂
case a
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t : Set α
l✝ : List α
a : α
f : α → β
hf : ∀ {x y : α}, x < y ↔ f x < f y
s : Set α
l : List α
hl : l ∈ subchain s
⊢ ∃ l', l' ∈ subchain (f '' s) ∧ length l = length l'
case a
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t : Set α
l : List α
a : α
f : α → β
hf : ∀ {x y : α}, x < y ↔ f x < f y
s : Set α
⊢ ∀ (l : List α), l ∈ subchain s → ∃ l', l' ∈ subchain (f '' s) ∧ length l = length l'
intro l hl
case a.refine'_1
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t : Set α
l✝ : List α
a : α
f : α → β
hf : ∀ {x y : α}, x < y ↔ f x < f y
s : Set α
l : List α
hl : l ∈ subchain s
⊢ Chain' (fun x x_1 => x < x_1) (map f l)

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

case a.refine'_3
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t : Set α
l✝ : List α
a : α
f : α → β
hf : ∀ {x y : α}, x < y ↔ f x < f y
s : Set α
l : List α
hl : l ∈ subchain s
⊢ length l = length (map f l)
case a
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t : Set α
l✝ : List α
a : α
f : α → β
hf : ∀ {x y : α}, x < y ↔ f x < f y
s : Set α
l : List α
hl : l ∈ subchain s
⊢ ∃ l', l' ∈ subchain (f '' s) ∧ length l = length l'
refine' ⟨l.map f, ⟨_, _⟩, _⟩
case a.refine'_1
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t : Set α
l✝ : List α
a : α
f : α → β
hf : ∀ {x y : α}, x < y ↔ f x < f y
s : Set α
l : List α
hl : l ∈ subchain s
⊢ Chain' (fun a b => a < b) l
case a.refine'_1
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t : Set α
l✝ : List α
a : α
f : α → β
hf : ∀ {x y : α}, x < y ↔ f x < f y
s : Set α
l : List α
hl : l ∈ subchain s
⊢ Chain' (fun x x_1 => x < x_1) (map f l)
simp_rw [chain'_map, ← hf]
no goals
case a.refine'_1
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t : Set α
l✝ : List α
a : α
f : α → β
hf : ∀ {x y : α}, x < y ↔ f x < f y
s : Set α
l : List α
hl : l ∈ subchain s
⊢ Chain' (fun a b => a < b) l
exact hl.1
case a.refine'_2
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t : Set α
l✝ : List α
a : α
f : α → β
hf : ∀ {x y : α}, x < y ↔ f x < f y
s : Set α
l : List α
hl : l ∈ subchain s
i✝ : β
e : i✝ ∈ map f l
⊢ i✝ ∈ f '' s
case a.refine'_2
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t : Set α
l✝ : List α
a : α
f : α → β
hf : ∀ {x y : α}, x < y ↔ f x < f y
s : Set α
l : List α
hl : l ∈ subchain s
⊢ ∀ (i : β), i ∈ map f l → i ∈ f '' s
intro _ e
case a.refine'_2.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t : Set α
l✝ : List α
a✝ : α
f : α → β
hf : ∀ {x y : α}, x < y ↔ f x < f y
s : Set α
l : List α
hl : l ∈ subchain s
a : α
ha : a ∈ l
e : f a ∈ map f l
⊢ f a ∈ f '' s
case a.refine'_2
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t : Set α
l✝ : List α
a : α
f : α → β
hf : ∀ {x y : α}, x < y ↔ f x < f y
s : Set α
l : List α
hl : l ∈ subchain s
i✝ : β
e : i✝ ∈ map f l
⊢ i✝ ∈ f '' s
obtain ⟨a, ha, rfl⟩ := mem_map.mp e
no goals
case a.refine'_2.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t : Set α
l✝ : List α
a✝ : α
f : α → β
hf : ∀ {x y : α}, x < y ↔ f x < f y
s : Set α
l : List α
hl : l ∈ subchain s
a : α
ha : a ∈ l
e : f a ∈ map f l
⊢ f a ∈ f '' s
exact Set.mem_image_of_mem _ (hl.2 _ ha)
no goals
case a.refine'_3
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t : Set α
l✝ : List α
a : α
f : α → β
hf : ∀ {x y : α}, x < y ↔ f x < f y
s : Set α
l : List α
hl : l ∈ subchain s
⊢ length l = length (map f l)
rw [length_map]