[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r r' : α → α → Prop
f : β → α
s t : Set α
x y : α
⊢ WellFoundedOn s r ↔ WellFounded fun a b => r a b ∧ a ∈ s ∧ b ∈ s
[PROOFSTEP]
have f : RelEmbedding (fun (a : s) (b : s) => r a b) fun a b : α => r a b ∧ a ∈ s ∧ b ∈ s :=
  ⟨⟨(↑), Subtype.coe_injective⟩, by simp⟩
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r r' : α → α → Prop
f : β → α
s t : Set α
x y : α
⊢ ∀ {a b : ↑s},
    r (↑{ toFun := Subtype.val, inj' := (_ : Function.Injective fun a => ↑a) } a)
          (↑{ toFun := Subtype.val, inj' := (_ : Function.Injective fun a => ↑a) } b) ∧
        ↑{ toFun := Subtype.val, inj' := (_ : Function.Injective fun a => ↑a) } a ∈ s ∧
          ↑{ toFun := Subtype.val, inj' := (_ : Function.Injective fun a => ↑a) } b ∈ s ↔
      r ↑a ↑b
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r r' : α → α → Prop
f✝ : β → α
s t : Set α
x y : α
f : (fun a b => r ↑a ↑b) ↪r fun a b => r a b ∧ a ∈ s ∧ b ∈ s
⊢ WellFoundedOn s r ↔ WellFounded fun a b => r a b ∧ a ∈ s ∧ b ∈ s
[PROOFSTEP]
refine' ⟨fun h => _, f.wellFounded⟩
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r r' : α → α → Prop
f✝ : β → α
s t : Set α
x y : α
f : (fun a b => r ↑a ↑b) ↪r fun a b => r a b ∧ a ∈ s ∧ b ∈ s
h : WellFoundedOn s r
⊢ WellFounded fun a b => r a b ∧ a ∈ s ∧ b ∈ s
[PROOFSTEP]
rw [WellFounded.wellFounded_iff_has_min]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r r' : α → α → Prop
f✝ : β → α
s t : Set α
x y : α
f : (fun a b => r ↑a ↑b) ↪r fun a b => r a b ∧ a ∈ s ∧ b ∈ s
h : WellFoundedOn s r
⊢ ∀ (s_1 : Set α), Set.Nonempty s_1 → ∃ m, m ∈ s_1 ∧ ∀ (x : α), x ∈ s_1 → ¬(r x m ∧ x ∈ s ∧ m ∈ s)
[PROOFSTEP]
intro t ht
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r r' : α → α → Prop
f✝ : β → α
s t✝ : Set α
x y : α
f : (fun a b => r ↑a ↑b) ↪r fun a b => r a b ∧ a ∈ s ∧ b ∈ s
h : WellFoundedOn s r
t : Set α
ht : Set.Nonempty t
⊢ ∃ m, m ∈ t ∧ ∀ (x : α), x ∈ t → ¬(r x m ∧ x ∈ s ∧ m ∈ s)
[PROOFSTEP]
by_cases hst : (s ∩ t).Nonempty
[GOAL]
case pos
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r r' : α → α → Prop
f✝ : β → α
s t✝ : Set α
x y : α
f : (fun a b => r ↑a ↑b) ↪r fun a b => r a b ∧ a ∈ s ∧ b ∈ s
h : WellFoundedOn s r
t : Set α
ht : Set.Nonempty t
hst : Set.Nonempty (s ∩ t)
⊢ ∃ m, m ∈ t ∧ ∀ (x : α), x ∈ t → ¬(r x m ∧ x ∈ s ∧ m ∈ s)
[PROOFSTEP]
rw [← Subtype.preimage_coe_nonempty] at hst 
[GOAL]
case pos
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r r' : α → α → Prop
f✝ : β → α
s t✝ : Set α
x y : α
f : (fun a b => r ↑a ↑b) ↪r fun a b => r a b ∧ a ∈ s ∧ b ∈ s
h : WellFoundedOn s r
t : Set α
ht : Set.Nonempty t
hst : Set.Nonempty (Subtype.val ⁻¹' t)
⊢ ∃ m, m ∈ t ∧ ∀ (x : α), x ∈ t → ¬(r x m ∧ x ∈ s ∧ m ∈ s)
[PROOFSTEP]
rcases h.has_min (Subtype.val ⁻¹' t) hst with ⟨⟨m, ms⟩, mt, hm⟩
[GOAL]
case pos.intro.mk.intro
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r r' : α → α → Prop
f✝ : β → α
s t✝ : Set α
x y : α
f : (fun a b => r ↑a ↑b) ↪r fun a b => r a b ∧ a ∈ s ∧ b ∈ s
h : WellFoundedOn s r
t : Set α
ht : Set.Nonempty t
hst : Set.Nonempty (Subtype.val ⁻¹' t)
m : α
ms : m ∈ s
mt : { val := m, property := ms } ∈ Subtype.val ⁻¹' t
hm : ∀ (x : ↑s), x ∈ Subtype.val ⁻¹' t → ¬r ↑x ↑{ val := m, property := ms }
⊢ ∃ m, m ∈ t ∧ ∀ (x : α), x ∈ t → ¬(r x m ∧ x ∈ s ∧ m ∈ s)
[PROOFSTEP]
exact ⟨m, mt, fun x xt ⟨xm, xs, _⟩ => hm ⟨x, xs⟩ xt xm⟩
[GOAL]
case neg
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r r' : α → α → Prop
f✝ : β → α
s t✝ : Set α
x y : α
f : (fun a b => r ↑a ↑b) ↪r fun a b => r a b ∧ a ∈ s ∧ b ∈ s
h : WellFoundedOn s r
t : Set α
ht : Set.Nonempty t
hst : ¬Set.Nonempty (s ∩ t)
⊢ ∃ m, m ∈ t ∧ ∀ (x : α), x ∈ t → ¬(r x m ∧ x ∈ s ∧ m ∈ s)
[PROOFSTEP]
rcases ht with ⟨m, mt⟩
[GOAL]
case neg.intro
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r r' : α → α → Prop
f✝ : β → α
s t✝ : Set α
x y : α
f : (fun a b => r ↑a ↑b) ↪r fun a b => r a b ∧ a ∈ s ∧ b ∈ s
h : WellFoundedOn s r
t : Set α
hst : ¬Set.Nonempty (s ∩ t)
m : α
mt : m ∈ t
⊢ ∃ m, m ∈ t ∧ ∀ (x : α), x ∈ t → ¬(r x m ∧ x ∈ s ∧ m ∈ s)
[PROOFSTEP]
exact ⟨m, mt, fun x _ ⟨_, _, ms⟩ => hst ⟨m, ⟨ms, mt⟩⟩⟩
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r r' : α → α → Prop
f : β → α
s t : Set α
x y : α
⊢ WellFoundedOn univ r ↔ WellFounded r
[PROOFSTEP]
simp [wellFoundedOn_iff]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r r' : α → α → Prop
f : β → α
s t : Set α
x y : α
⊢ WellFoundedOn (range f) r ↔ WellFounded (r on f)
[PROOFSTEP]
let f' : β → range f := fun c => ⟨f c, c, rfl⟩
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r r' : α → α → Prop
f : β → α
s t : Set α
x y : α
f' : β → ↑(range f) := fun c => { val := f c, property := (_ : ∃ y, f y = f c) }
⊢ WellFoundedOn (range f) r ↔ WellFounded (r on f)
[PROOFSTEP]
refine' ⟨fun h => (InvImage.wf f' h).mono fun c c' => id, fun h => ⟨_⟩⟩
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r r' : α → α → Prop
f : β → α
s t : Set α
x y : α
f' : β → ↑(range f) := fun c => { val := f c, property := (_ : ∃ y, f y = f c) }
h : WellFounded (r on f)
⊢ ∀ (a : ↑(range f)), Acc (fun a b => r ↑a ↑b) a
[PROOFSTEP]
rintro ⟨_, c, rfl⟩
[GOAL]
case mk.intro
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r r' : α → α → Prop
f : β → α
s t : Set α
x y : α
f' : β → ↑(range f) := fun c => { val := f c, property := (_ : ∃ y, f y = f c) }
h : WellFounded (r on f)
c : β
⊢ Acc (fun a b => r ↑a ↑b) { val := f c, property := (_ : ∃ y, f y = f c) }
[PROOFSTEP]
refine' Acc.of_downward_closed f' _ _ _
[GOAL]
case mk.intro.refine'_1
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r r' : α → α → Prop
f : β → α
s t : Set α
x y : α
f' : β → ↑(range f) := fun c => { val := f c, property := (_ : ∃ y, f y = f c) }
h : WellFounded (r on f)
c : β
⊢ ∀ {a : β} {b : ↑(range f)}, r ↑b ↑(f' a) → ∃ c, f' c = b
[PROOFSTEP]
rintro _ ⟨_, c', rfl⟩ -
[GOAL]
case mk.intro.refine'_1.mk.intro
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r r' : α → α → Prop
f : β → α
s t : Set α
x y : α
f' : β → ↑(range f) := fun c => { val := f c, property := (_ : ∃ y, f y = f c) }
h : WellFounded (r on f)
c a✝ c' : β
⊢ ∃ c, f' c = { val := f c', property := (_ : ∃ y, f y = f c') }
[PROOFSTEP]
exact ⟨c', rfl⟩
[GOAL]
case mk.intro.refine'_2
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r r' : α → α → Prop
f : β → α
s t : Set α
x y : α
f' : β → ↑(range f) := fun c => { val := f c, property := (_ : ∃ y, f y = f c) }
h : WellFounded (r on f)
c : β
⊢ Acc (InvImage (fun a b => r ↑a ↑b) f') c
[PROOFSTEP]
exact h.apply _
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r r' : α → α → Prop
f : β → α
s✝ t : Set α
x y : α
s : Set β
⊢ WellFoundedOn (f '' s) r ↔ WellFoundedOn s (r on f)
[PROOFSTEP]
rw [image_eq_range]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r r' : α → α → Prop
f : β → α
s✝ t : Set α
x y : α
s : Set β
⊢ WellFoundedOn (range fun x => f ↑x) r ↔ WellFoundedOn s (r on f)
[PROOFSTEP]
exact wellFoundedOn_range
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r r' : α → α → Prop
f : β → α
s t : Set α
x y : α
hs : WellFoundedOn s r
hx : x ∈ s
P : α → Prop
hP : ∀ (y : α), y ∈ s → (∀ (z : α), z ∈ s → r z y → P z) → P y
⊢ P x
[PROOFSTEP]
let Q : s → Prop := fun y => P y
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r r' : α → α → Prop
f : β → α
s t : Set α
x y : α
hs : WellFoundedOn s r
hx : x ∈ s
P : α → Prop
hP : ∀ (y : α), y ∈ s → (∀ (z : α), z ∈ s → r z y → P z) → P y
Q : ↑s → Prop := fun y => P ↑y
⊢ P x
[PROOFSTEP]
change Q ⟨x, hx⟩
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r r' : α → α → Prop
f : β → α
s t : Set α
x y : α
hs : WellFoundedOn s r
hx : x ∈ s
P : α → Prop
hP : ∀ (y : α), y ∈ s → (∀ (z : α), z ∈ s → r z y → P z) → P y
Q : ↑s → Prop := fun y => P ↑y
⊢ Q { val := x, property := hx }
[PROOFSTEP]
refine' WellFounded.induction hs ⟨x, hx⟩ _
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r r' : α → α → Prop
f : β → α
s t : Set α
x y : α
hs : WellFoundedOn s r
hx : x ∈ s
P : α → Prop
hP : ∀ (y : α), y ∈ s → (∀ (z : α), z ∈ s → r z y → P z) → P y
Q : ↑s → Prop := fun y => P ↑y
⊢ ∀ (x : ↑s), (∀ (y : ↑s), r ↑y ↑x → Q y) → Q x
[PROOFSTEP]
simpa only [Subtype.forall]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r r' : α → α → Prop
f : β → α
s t : Set α
x y : α
h : WellFoundedOn t r'
hle : r ≤ r'
hst : s ⊆ t
⊢ WellFoundedOn s r
[PROOFSTEP]
rw [wellFoundedOn_iff] at *
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r r' : α → α → Prop
f : β → α
s t : Set α
x y : α
h : WellFounded fun a b => r' a b ∧ a ∈ t ∧ b ∈ t
hle : r ≤ r'
hst : s ⊆ t
⊢ WellFounded fun a b => r a b ∧ a ∈ s ∧ b ∈ s
[PROOFSTEP]
exact Subrelation.wf (fun xy => ⟨hle _ _ xy.1, hst xy.2.1, hst xy.2.2⟩) h
[GOAL]
ι : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r✝ r' : α✝ → α✝ → Prop
f : β → α✝
s t : Set α✝
x y : α✝
α : Type u_6
r : α → α → Prop
a : α
⊢ TFAE [Acc r a, WellFoundedOn {b | ReflTransGen r b a} r, WellFoundedOn {b | TransGen r b a} r]
[PROOFSTEP]
tfae_have 1 → 2
[GOAL]
case tfae_1_to_2
ι : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r✝ r' : α✝ → α✝ → Prop
f : β → α✝
s t : Set α✝
x y : α✝
α : Type u_6
r : α → α → Prop
a : α
⊢ Acc r a → WellFoundedOn {b | ReflTransGen r b a} r
[PROOFSTEP]
refine fun h => ⟨fun b => InvImage.accessible _ ?_⟩
[GOAL]
case tfae_1_to_2
ι : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r✝ r' : α✝ → α✝ → Prop
f : β → α✝
s t : Set α✝
x y : α✝
α : Type u_6
r : α → α → Prop
a : α
h : Acc r a
b : ↑{b | ReflTransGen r b a}
⊢ Acc r ↑b
[PROOFSTEP]
rw [← acc_transGen_iff] at h ⊢
[GOAL]
case tfae_1_to_2
ι : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r✝ r' : α✝ → α✝ → Prop
f : β → α✝
s t : Set α✝
x y : α✝
α : Type u_6
r : α → α → Prop
a : α
h : Acc (TransGen r) a
b : ↑{b | ReflTransGen r b a}
⊢ Acc (TransGen r) ↑b
[PROOFSTEP]
obtain h' | h' := reflTransGen_iff_eq_or_transGen.1 b.2
[GOAL]
case tfae_1_to_2.inl
ι : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r✝ r' : α✝ → α✝ → Prop
f : β → α✝
s t : Set α✝
x y : α✝
α : Type u_6
r : α → α → Prop
a : α
h : Acc (TransGen r) a
b : ↑{b | ReflTransGen r b a}
h' : a = ↑b
⊢ Acc (TransGen r) ↑b
[PROOFSTEP]
rwa [h'] at h 
[GOAL]
case tfae_1_to_2.inr
ι : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r✝ r' : α✝ → α✝ → Prop
f : β → α✝
s t : Set α✝
x y : α✝
α : Type u_6
r : α → α → Prop
a : α
h : Acc (TransGen r) a
b : ↑{b | ReflTransGen r b a}
h' : TransGen r (↑b) a
⊢ Acc (TransGen r) ↑b
[PROOFSTEP]
exact h.inv h'
[GOAL]
ι : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r✝ r' : α✝ → α✝ → Prop
f : β → α✝
s t : Set α✝
x y : α✝
α : Type u_6
r : α → α → Prop
a : α
tfae_1_to_2 : Acc r a → WellFoundedOn {b | ReflTransGen r b a} r
⊢ TFAE [Acc r a, WellFoundedOn {b | ReflTransGen r b a} r, WellFoundedOn {b | TransGen r b a} r]
[PROOFSTEP]
tfae_have 2 → 3
[GOAL]
case tfae_2_to_3
ι : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r✝ r' : α✝ → α✝ → Prop
f : β → α✝
s t : Set α✝
x y : α✝
α : Type u_6
r : α → α → Prop
a : α
tfae_1_to_2 : Acc r a → WellFoundedOn {b | ReflTransGen r b a} r
⊢ WellFoundedOn {b | ReflTransGen r b a} r → WellFoundedOn {b | TransGen r b a} r
[PROOFSTEP]
exact fun h => h.subset fun _ => TransGen.to_reflTransGen
[GOAL]
ι : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r✝ r' : α✝ → α✝ → Prop
f : β → α✝
s t : Set α✝
x y : α✝
α : Type u_6
r : α → α → Prop
a : α
tfae_1_to_2 : Acc r a → WellFoundedOn {b | ReflTransGen r b a} r
tfae_2_to_3 : WellFoundedOn {b | ReflTransGen r b a} r → WellFoundedOn {b | TransGen r b a} r
⊢ TFAE [Acc r a, WellFoundedOn {b | ReflTransGen r b a} r, WellFoundedOn {b | TransGen r b a} r]
[PROOFSTEP]
tfae_have 3 → 1
[GOAL]
case tfae_3_to_1
ι : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r✝ r' : α✝ → α✝ → Prop
f : β → α✝
s t : Set α✝
x y : α✝
α : Type u_6
r : α → α → Prop
a : α
tfae_1_to_2 : Acc r a → WellFoundedOn {b | ReflTransGen r b a} r
tfae_2_to_3 : WellFoundedOn {b | ReflTransGen r b a} r → WellFoundedOn {b | TransGen r b a} r
⊢ WellFoundedOn {b | TransGen r b a} r → Acc r a
[PROOFSTEP]
refine fun h => Acc.intro _ (fun b hb => (h.apply ⟨b, .single hb⟩).of_fibration Subtype.val ?_)
[GOAL]
case tfae_3_to_1
ι : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r✝ r' : α✝ → α✝ → Prop
f : β → α✝
s t : Set α✝
x y : α✝
α : Type u_6
r : α → α → Prop
a : α
tfae_1_to_2 : Acc r a → WellFoundedOn {b | ReflTransGen r b a} r
tfae_2_to_3 : WellFoundedOn {b | ReflTransGen r b a} r → WellFoundedOn {b | TransGen r b a} r
h : WellFoundedOn {b | TransGen r b a} r
b : α
hb : r b a
⊢ Fibration (fun a_1 b => r ↑a_1 ↑b) r Subtype.val
[PROOFSTEP]
exact fun ⟨c, hc⟩ d h => ⟨⟨d, .head h hc⟩, h, rfl⟩
[GOAL]
ι : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r✝ r' : α✝ → α✝ → Prop
f : β → α✝
s t : Set α✝
x y : α✝
α : Type u_6
r : α → α → Prop
a : α
tfae_1_to_2 : Acc r a → WellFoundedOn {b | ReflTransGen r b a} r
tfae_2_to_3 : WellFoundedOn {b | ReflTransGen r b a} r → WellFoundedOn {b | TransGen r b a} r
tfae_3_to_1 : WellFoundedOn {b | TransGen r b a} r → Acc r a
⊢ TFAE [Acc r a, WellFoundedOn {b | ReflTransGen r b a} r, WellFoundedOn {b | TransGen r b a} r]
[PROOFSTEP]
tfae_finish
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r r' : α → α → Prop
inst✝ : IsStrictOrder α r
s t : Set α
⊢ WellFoundedOn s r ↔ ∀ (f : (fun x x_1 => x > x_1) ↪r r), ¬∀ (n : ℕ), ↑f n ∈ s
[PROOFSTEP]
simp only [wellFoundedOn_iff, RelEmbedding.wellFounded_iff_no_descending_seq, ← not_exists, ← not_nonempty_iff,
  not_iff_not]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r r' : α → α → Prop
inst✝ : IsStrictOrder α r
s t : Set α
⊢ Nonempty ((fun x x_1 => x > x_1) ↪r fun a b => r a b ∧ a ∈ s ∧ b ∈ s) ↔ ∃ x, ∀ (n : ℕ), ↑x n ∈ s
[PROOFSTEP]
constructor
[GOAL]
case mp
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r r' : α → α → Prop
inst✝ : IsStrictOrder α r
s t : Set α
⊢ Nonempty ((fun x x_1 => x > x_1) ↪r fun a b => r a b ∧ a ∈ s ∧ b ∈ s) → ∃ x, ∀ (n : ℕ), ↑x n ∈ s
[PROOFSTEP]
rintro ⟨⟨f, hf⟩⟩
[GOAL]
case mp.intro.mk
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r r' : α → α → Prop
inst✝ : IsStrictOrder α r
s t : Set α
f : ℕ ↪ α
hf : ∀ {a b : ℕ}, r (↑f a) (↑f b) ∧ ↑f a ∈ s ∧ ↑f b ∈ s ↔ a > b
⊢ ∃ x, ∀ (n : ℕ), ↑x n ∈ s
[PROOFSTEP]
have H : ∀ n, f n ∈ s := fun n => (hf.2 n.lt_succ_self).2.2
[GOAL]
case mp.intro.mk
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r r' : α → α → Prop
inst✝ : IsStrictOrder α r
s t : Set α
f : ℕ ↪ α
hf : ∀ {a b : ℕ}, r (↑f a) (↑f b) ∧ ↑f a ∈ s ∧ ↑f b ∈ s ↔ a > b
H : ∀ (n : ℕ), ↑f n ∈ s
⊢ ∃ x, ∀ (n : ℕ), ↑x n ∈ s
[PROOFSTEP]
refine' ⟨⟨f, _⟩, H⟩
[GOAL]
case mp.intro.mk
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r r' : α → α → Prop
inst✝ : IsStrictOrder α r
s t : Set α
f : ℕ ↪ α
hf : ∀ {a b : ℕ}, r (↑f a) (↑f b) ∧ ↑f a ∈ s ∧ ↑f b ∈ s ↔ a > b
H : ∀ (n : ℕ), ↑f n ∈ s
⊢ ∀ {a b : ℕ}, r (↑f a) (↑f b) ↔ a > b
[PROOFSTEP]
simpa only [H, and_true_iff] using @hf
[GOAL]
case mpr
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r r' : α → α → Prop
inst✝ : IsStrictOrder α r
s t : Set α
⊢ (∃ x, ∀ (n : ℕ), ↑x n ∈ s) → Nonempty ((fun x x_1 => x > x_1) ↪r fun a b => r a b ∧ a ∈ s ∧ b ∈ s)
[PROOFSTEP]
rintro ⟨⟨f, hf⟩, hfs : ∀ n, f n ∈ s⟩
[GOAL]
case mpr.intro.mk
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r r' : α → α → Prop
inst✝ : IsStrictOrder α r
s t : Set α
f : ℕ ↪ α
hf : ∀ {a b : ℕ}, r (↑f a) (↑f b) ↔ a > b
hfs : ∀ (n : ℕ), ↑f n ∈ s
⊢ Nonempty ((fun x x_1 => x > x_1) ↪r fun a b => r a b ∧ a ∈ s ∧ b ∈ s)
[PROOFSTEP]
refine' ⟨⟨f, _⟩⟩
[GOAL]
case mpr.intro.mk
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r r' : α → α → Prop
inst✝ : IsStrictOrder α r
s t : Set α
f : ℕ ↪ α
hf : ∀ {a b : ℕ}, r (↑f a) (↑f b) ↔ a > b
hfs : ∀ (n : ℕ), ↑f n ∈ s
⊢ ∀ {a b : ℕ}, r (↑f a) (↑f b) ∧ ↑f a ∈ s ∧ ↑f b ∈ s ↔ a > b
[PROOFSTEP]
simpa only [hfs, and_true_iff] using @hf
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r r' : α → α → Prop
inst✝ : IsStrictOrder α r
s t : Set α
hs : WellFoundedOn s r
ht : WellFoundedOn t r
⊢ WellFoundedOn (s ∪ t) r
[PROOFSTEP]
rw [wellFoundedOn_iff_no_descending_seq] at *
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r r' : α → α → Prop
inst✝ : IsStrictOrder α r
s t : Set α
hs : ∀ (f : (fun x x_1 => x > x_1) ↪r r), ¬∀ (n : ℕ), ↑f n ∈ s
ht : ∀ (f : (fun x x_1 => x > x_1) ↪r r), ¬∀ (n : ℕ), ↑f n ∈ t
⊢ ∀ (f : (fun x x_1 => x > x_1) ↪r r), ¬∀ (n : ℕ), ↑f n ∈ s ∪ t
[PROOFSTEP]
rintro f hf
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r r' : α → α → Prop
inst✝ : IsStrictOrder α r
s t : Set α
hs : ∀ (f : (fun x x_1 => x > x_1) ↪r r), ¬∀ (n : ℕ), ↑f n ∈ s
ht : ∀ (f : (fun x x_1 => x > x_1) ↪r r), ¬∀ (n : ℕ), ↑f n ∈ t
f : (fun x x_1 => x > x_1) ↪r r
hf : ∀ (n : ℕ), ↑f n ∈ s ∪ t
⊢ False
[PROOFSTEP]
rcases Nat.exists_subseq_of_forall_mem_union f hf with ⟨g, hg | hg⟩
[GOAL]
case intro.inl
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r r' : α → α → Prop
inst✝ : IsStrictOrder α r
s t : Set α
hs : ∀ (f : (fun x x_1 => x > x_1) ↪r r), ¬∀ (n : ℕ), ↑f n ∈ s
ht : ∀ (f : (fun x x_1 => x > x_1) ↪r r), ¬∀ (n : ℕ), ↑f n ∈ t
f : (fun x x_1 => x > x_1) ↪r r
hf : ∀ (n : ℕ), ↑f n ∈ s ∪ t
g : ℕ ↪o ℕ
hg : ∀ (n : ℕ), ↑f (↑g n) ∈ s
⊢ False
case intro.inr
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r r' : α → α → Prop
inst✝ : IsStrictOrder α r
s t : Set α
hs : ∀ (f : (fun x x_1 => x > x_1) ↪r r), ¬∀ (n : ℕ), ↑f n ∈ s
ht : ∀ (f : (fun x x_1 => x > x_1) ↪r r), ¬∀ (n : ℕ), ↑f n ∈ t
f : (fun x x_1 => x > x_1) ↪r r
hf : ∀ (n : ℕ), ↑f n ∈ s ∪ t
g : ℕ ↪o ℕ
hg : ∀ (n : ℕ), ↑f (↑g n) ∈ t
⊢ False
[PROOFSTEP]
exacts [hs (g.dual.ltEmbedding.trans f) hg, ht (g.dual.ltEmbedding.trans f) hg]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
inst✝ : LT α
s t : Set α
⊢ IsWf univ ↔ WellFounded fun x x_1 => x < x_1
[PROOFSTEP]
simp [IsWf, wellFoundedOn_iff]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r : α → α → Prop
r' : β → β → Prop
f : α → β
s t : Set α
a : α
hs : PartiallyWellOrderedOn s r
ht : PartiallyWellOrderedOn t r
⊢ PartiallyWellOrderedOn (s ∪ t) r
[PROOFSTEP]
rintro f hf
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r : α → α → Prop
r' : β → β → Prop
f✝ : α → β
s t : Set α
a : α
hs : PartiallyWellOrderedOn s r
ht : PartiallyWellOrderedOn t r
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s ∪ t
⊢ ∃ m n, m < n ∧ r (f m) (f n)
[PROOFSTEP]
rcases Nat.exists_subseq_of_forall_mem_union f hf with ⟨g, hgs | hgt⟩
[GOAL]
case intro.inl
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r : α → α → Prop
r' : β → β → Prop
f✝ : α → β
s t : Set α
a : α
hs : PartiallyWellOrderedOn s r
ht : PartiallyWellOrderedOn t r
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s ∪ t
g : ℕ ↪o ℕ
hgs : ∀ (n : ℕ), f (↑g n) ∈ s
⊢ ∃ m n, m < n ∧ r (f m) (f n)
[PROOFSTEP]
rcases hs _ hgs with ⟨m, n, hlt, hr⟩
[GOAL]
case intro.inl.intro.intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r : α → α → Prop
r' : β → β → Prop
f✝ : α → β
s t : Set α
a : α
hs : PartiallyWellOrderedOn s r
ht : PartiallyWellOrderedOn t r
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s ∪ t
g : ℕ ↪o ℕ
hgs : ∀ (n : ℕ), f (↑g n) ∈ s
m n : ℕ
hlt : m < n
hr : r (f (↑g m)) (f (↑g n))
⊢ ∃ m n, m < n ∧ r (f m) (f n)
[PROOFSTEP]
exact ⟨g m, g n, g.strictMono hlt, hr⟩
[GOAL]
case intro.inr
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r : α → α → Prop
r' : β → β → Prop
f✝ : α → β
s t : Set α
a : α
hs : PartiallyWellOrderedOn s r
ht : PartiallyWellOrderedOn t r
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s ∪ t
g : ℕ ↪o ℕ
hgt : ∀ (n : ℕ), f (↑g n) ∈ t
⊢ ∃ m n, m < n ∧ r (f m) (f n)
[PROOFSTEP]
rcases ht _ hgt with ⟨m, n, hlt, hr⟩
[GOAL]
case intro.inr.intro.intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r : α → α → Prop
r' : β → β → Prop
f✝ : α → β
s t : Set α
a : α
hs : PartiallyWellOrderedOn s r
ht : PartiallyWellOrderedOn t r
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s ∪ t
g : ℕ ↪o ℕ
hgt : ∀ (n : ℕ), f (↑g n) ∈ t
m n : ℕ
hlt : m < n
hr : r (f (↑g m)) (f (↑g n))
⊢ ∃ m n, m < n ∧ r (f m) (f n)
[PROOFSTEP]
exact ⟨g m, g n, g.strictMono hlt, hr⟩
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r : α → α → Prop
r' : β → β → Prop
f : α → β
s t : Set α
a : α
hs : PartiallyWellOrderedOn s r
hf : ∀ (a₁ : α), a₁ ∈ s → ∀ (a₂ : α), a₂ ∈ s → r a₁ a₂ → r' (f a₁) (f a₂)
⊢ PartiallyWellOrderedOn (f '' s) r'
[PROOFSTEP]
intro g' hg'
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r : α → α → Prop
r' : β → β → Prop
f : α → β
s t : Set α
a : α
hs : PartiallyWellOrderedOn s r
hf : ∀ (a₁ : α), a₁ ∈ s → ∀ (a₂ : α), a₂ ∈ s → r a₁ a₂ → r' (f a₁) (f a₂)
g' : ℕ → β
hg' : ∀ (n : ℕ), g' n ∈ f '' s
⊢ ∃ m n, m < n ∧ r' (g' m) (g' n)
[PROOFSTEP]
choose g hgs heq using hg'
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r : α → α → Prop
r' : β → β → Prop
f : α → β
s t : Set α
a : α
hs : PartiallyWellOrderedOn s r
hf : ∀ (a₁ : α), a₁ ∈ s → ∀ (a₂ : α), a₂ ∈ s → r a₁ a₂ → r' (f a₁) (f a₂)
g' : ℕ → β
g : ℕ → α
hgs : ∀ (n : ℕ), g n ∈ s
heq : ∀ (n : ℕ), f (g n) = g' n
⊢ ∃ m n, m < n ∧ r' (g' m) (g' n)
[PROOFSTEP]
obtain rfl : f ∘ g = g'
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r : α → α → Prop
r' : β → β → Prop
f : α → β
s t : Set α
a : α
hs : PartiallyWellOrderedOn s r
hf : ∀ (a₁ : α), a₁ ∈ s → ∀ (a₂ : α), a₂ ∈ s → r a₁ a₂ → r' (f a₁) (f a₂)
g' : ℕ → β
g : ℕ → α
hgs : ∀ (n : ℕ), g n ∈ s
heq : ∀ (n : ℕ), f (g n) = g' n
⊢ f ∘ g = g'
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r : α → α → Prop
r' : β → β → Prop
f : α → β
s t : Set α
a : α
hs : PartiallyWellOrderedOn s r
hf : ∀ (a₁ : α), a₁ ∈ s → ∀ (a₂ : α), a₂ ∈ s → r a₁ a₂ → r' (f a₁) (f a₂)
g : ℕ → α
hgs : ∀ (n : ℕ), g n ∈ s
heq : ∀ (n : ℕ), f (g n) = (f ∘ g) n
⊢ ∃ m n, m < n ∧ r' ((f ∘ g) m) ((f ∘ g) n)
[PROOFSTEP]
exact funext heq
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r : α → α → Prop
r' : β → β → Prop
f : α → β
s t : Set α
a : α
hs : PartiallyWellOrderedOn s r
hf : ∀ (a₁ : α), a₁ ∈ s → ∀ (a₂ : α), a₂ ∈ s → r a₁ a₂ → r' (f a₁) (f a₂)
g : ℕ → α
hgs : ∀ (n : ℕ), g n ∈ s
heq : ∀ (n : ℕ), f (g n) = (f ∘ g) n
⊢ ∃ m n, m < n ∧ r' ((f ∘ g) m) ((f ∘ g) n)
[PROOFSTEP]
obtain ⟨m, n, hlt, hmn⟩ := hs g hgs
[GOAL]
case intro.intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r : α → α → Prop
r' : β → β → Prop
f : α → β
s t : Set α
a : α
hs : PartiallyWellOrderedOn s r
hf : ∀ (a₁ : α), a₁ ∈ s → ∀ (a₂ : α), a₂ ∈ s → r a₁ a₂ → r' (f a₁) (f a₂)
g : ℕ → α
hgs : ∀ (n : ℕ), g n ∈ s
heq : ∀ (n : ℕ), f (g n) = (f ∘ g) n
m n : ℕ
hlt : m < n
hmn : r (g m) (g n)
⊢ ∃ m n, m < n ∧ r' ((f ∘ g) m) ((f ∘ g) n)
[PROOFSTEP]
exact ⟨m, n, hlt, hf _ (hgs m) _ (hgs n) hmn⟩
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r : α → α → Prop
r' : β → β → Prop
f : α → β
s t : Set α
a : α
ha : IsAntichain r s
hp : PartiallyWellOrderedOn s r
⊢ Set.Finite s
[PROOFSTEP]
refine' not_infinite.1 fun hi => _
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r : α → α → Prop
r' : β → β → Prop
f : α → β
s t : Set α
a : α
ha : IsAntichain r s
hp : PartiallyWellOrderedOn s r
hi : Set.Infinite s
⊢ False
[PROOFSTEP]
obtain ⟨m, n, hmn, h⟩ := hp (fun n => hi.natEmbedding _ n) fun n => (hi.natEmbedding _ n).2
[GOAL]
case intro.intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r : α → α → Prop
r' : β → β → Prop
f : α → β
s t : Set α
a : α
ha : IsAntichain r s
hp : PartiallyWellOrderedOn s r
hi : Set.Infinite s
m n : ℕ
hmn : m < n
h : r ↑(↑(Infinite.natEmbedding s hi) m) ↑(↑(Infinite.natEmbedding s hi) n)
⊢ False
[PROOFSTEP]
exact
  hmn.ne
    ((hi.natEmbedding _).injective <| Subtype.val_injective <| ha.eq (hi.natEmbedding _ m).2 (hi.natEmbedding _ n).2 h)
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r : α → α → Prop
r' : β → β → Prop
f : α → β
s t : Set α
a : α
inst✝ : IsRefl α r
hs : Set.Finite s
⊢ PartiallyWellOrderedOn s r
[PROOFSTEP]
intro f hf
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r : α → α → Prop
r' : β → β → Prop
f✝ : α → β
s t : Set α
a : α
inst✝ : IsRefl α r
hs : Set.Finite s
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
⊢ ∃ m n, m < n ∧ r (f m) (f n)
[PROOFSTEP]
obtain ⟨m, n, hmn, h⟩ := hs.exists_lt_map_eq_of_forall_mem hf
[GOAL]
case intro.intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r : α → α → Prop
r' : β → β → Prop
f✝ : α → β
s t : Set α
a : α
inst✝ : IsRefl α r
hs : Set.Finite s
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
m n : ℕ
hmn : m < n
h : f m = f n
⊢ ∃ m n, m < n ∧ r (f m) (f n)
[PROOFSTEP]
exact ⟨m, n, hmn, h.subst <| refl (f m)⟩
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r : α → α → Prop
r' : β → β → Prop
f : α → β
s t : Set α
a : α
inst✝ : IsRefl α r
⊢ PartiallyWellOrderedOn (insert a s) r ↔ PartiallyWellOrderedOn s r
[PROOFSTEP]
simp only [← singleton_union, partiallyWellOrderedOn_union, partiallyWellOrderedOn_singleton, true_and_iff]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r : α → α → Prop
r' : β → β → Prop
f : α → β
s t : Set α
a : α
inst✝¹ : IsRefl α r
inst✝ : IsSymm α r
⊢ PartiallyWellOrderedOn s r ↔ ∀ (t : Set α), t ⊆ s → IsAntichain r t → Set.Finite t
[PROOFSTEP]
refine' ⟨fun h t ht hrt => hrt.finite_of_partiallyWellOrderedOn (h.mono ht), _⟩
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r : α → α → Prop
r' : β → β → Prop
f : α → β
s t : Set α
a : α
inst✝¹ : IsRefl α r
inst✝ : IsSymm α r
⊢ (∀ (t : Set α), t ⊆ s → IsAntichain r t → Set.Finite t) → PartiallyWellOrderedOn s r
[PROOFSTEP]
rintro hs f hf
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r : α → α → Prop
r' : β → β → Prop
f✝ : α → β
s t : Set α
a : α
inst✝¹ : IsRefl α r
inst✝ : IsSymm α r
hs : ∀ (t : Set α), t ⊆ s → IsAntichain r t → Set.Finite t
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
⊢ ∃ m n, m < n ∧ r (f m) (f n)
[PROOFSTEP]
by_contra' H
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r : α → α → Prop
r' : β → β → Prop
f✝ : α → β
s t : Set α
a : α
inst✝¹ : IsRefl α r
inst✝ : IsSymm α r
hs : ∀ (t : Set α), t ⊆ s → IsAntichain r t → Set.Finite t
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
H : ∀ (m n : ℕ), m < n → ¬r (f m) (f n)
⊢ False
[PROOFSTEP]
refine' infinite_range_of_injective (fun m n hmn => _) (hs _ (range_subset_iff.2 hf) _)
[GOAL]
case refine'_1
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r : α → α → Prop
r' : β → β → Prop
f✝ : α → β
s t : Set α
a : α
inst✝¹ : IsRefl α r
inst✝ : IsSymm α r
hs : ∀ (t : Set α), t ⊆ s → IsAntichain r t → Set.Finite t
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
H : ∀ (m n : ℕ), m < n → ¬r (f m) (f n)
m n : ℕ
hmn : f m = f n
⊢ m = n
[PROOFSTEP]
obtain h | h | h := lt_trichotomy m n
[GOAL]
case refine'_1.inl
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r : α → α → Prop
r' : β → β → Prop
f✝ : α → β
s t : Set α
a : α
inst✝¹ : IsRefl α r
inst✝ : IsSymm α r
hs : ∀ (t : Set α), t ⊆ s → IsAntichain r t → Set.Finite t
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
H : ∀ (m n : ℕ), m < n → ¬r (f m) (f n)
m n : ℕ
hmn : f m = f n
h : m < n
⊢ m = n
[PROOFSTEP]
refine' (H _ _ h _).elim
[GOAL]
case refine'_1.inl
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r : α → α → Prop
r' : β → β → Prop
f✝ : α → β
s t : Set α
a : α
inst✝¹ : IsRefl α r
inst✝ : IsSymm α r
hs : ∀ (t : Set α), t ⊆ s → IsAntichain r t → Set.Finite t
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
H : ∀ (m n : ℕ), m < n → ¬r (f m) (f n)
m n : ℕ
hmn : f m = f n
h : m < n
⊢ r (f m) (f n)
[PROOFSTEP]
rw [hmn]
[GOAL]
case refine'_1.inl
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r : α → α → Prop
r' : β → β → Prop
f✝ : α → β
s t : Set α
a : α
inst✝¹ : IsRefl α r
inst✝ : IsSymm α r
hs : ∀ (t : Set α), t ⊆ s → IsAntichain r t → Set.Finite t
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
H : ∀ (m n : ℕ), m < n → ¬r (f m) (f n)
m n : ℕ
hmn : f m = f n
h : m < n
⊢ r (f n) (f n)
[PROOFSTEP]
exact refl _
[GOAL]
case refine'_1.inr.inl
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r : α → α → Prop
r' : β → β → Prop
f✝ : α → β
s t : Set α
a : α
inst✝¹ : IsRefl α r
inst✝ : IsSymm α r
hs : ∀ (t : Set α), t ⊆ s → IsAntichain r t → Set.Finite t
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
H : ∀ (m n : ℕ), m < n → ¬r (f m) (f n)
m n : ℕ
hmn : f m = f n
h : m = n
⊢ m = n
[PROOFSTEP]
exact h
[GOAL]
case refine'_1.inr.inr
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r : α → α → Prop
r' : β → β → Prop
f✝ : α → β
s t : Set α
a : α
inst✝¹ : IsRefl α r
inst✝ : IsSymm α r
hs : ∀ (t : Set α), t ⊆ s → IsAntichain r t → Set.Finite t
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
H : ∀ (m n : ℕ), m < n → ¬r (f m) (f n)
m n : ℕ
hmn : f m = f n
h : n < m
⊢ m = n
[PROOFSTEP]
refine' (H _ _ h _).elim
[GOAL]
case refine'_1.inr.inr
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r : α → α → Prop
r' : β → β → Prop
f✝ : α → β
s t : Set α
a : α
inst✝¹ : IsRefl α r
inst✝ : IsSymm α r
hs : ∀ (t : Set α), t ⊆ s → IsAntichain r t → Set.Finite t
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
H : ∀ (m n : ℕ), m < n → ¬r (f m) (f n)
m n : ℕ
hmn : f m = f n
h : n < m
⊢ r (f n) (f m)
[PROOFSTEP]
rw [hmn]
[GOAL]
case refine'_1.inr.inr
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r : α → α → Prop
r' : β → β → Prop
f✝ : α → β
s t : Set α
a : α
inst✝¹ : IsRefl α r
inst✝ : IsSymm α r
hs : ∀ (t : Set α), t ⊆ s → IsAntichain r t → Set.Finite t
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
H : ∀ (m n : ℕ), m < n → ¬r (f m) (f n)
m n : ℕ
hmn : f m = f n
h : n < m
⊢ r (f n) (f n)
[PROOFSTEP]
exact refl _
[GOAL]
case refine'_2
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r : α → α → Prop
r' : β → β → Prop
f✝ : α → β
s t : Set α
a : α
inst✝¹ : IsRefl α r
inst✝ : IsSymm α r
hs : ∀ (t : Set α), t ⊆ s → IsAntichain r t → Set.Finite t
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
H : ∀ (m n : ℕ), m < n → ¬r (f m) (f n)
⊢ IsAntichain r (range fun y => f y)
[PROOFSTEP]
rintro _ ⟨m, hm, rfl⟩ _ ⟨n, hn, rfl⟩ hmn
[GOAL]
case refine'_2.intro.refl.intro.refl
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r : α → α → Prop
r' : β → β → Prop
f✝ : α → β
s t : Set α
a : α
inst✝¹ : IsRefl α r
inst✝ : IsSymm α r
hs : ∀ (t : Set α), t ⊆ s → IsAntichain r t → Set.Finite t
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
H : ∀ (m n : ℕ), m < n → ¬r (f m) (f n)
m n : ℕ
hmn : (fun y => f y) m ≠ (fun y => f y) n
⊢ rᶜ ((fun y => f y) m) ((fun y => f y) n)
[PROOFSTEP]
obtain h | h := (ne_of_apply_ne _ hmn).lt_or_lt
[GOAL]
case refine'_2.intro.refl.intro.refl.inl
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r : α → α → Prop
r' : β → β → Prop
f✝ : α → β
s t : Set α
a : α
inst✝¹ : IsRefl α r
inst✝ : IsSymm α r
hs : ∀ (t : Set α), t ⊆ s → IsAntichain r t → Set.Finite t
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
H : ∀ (m n : ℕ), m < n → ¬r (f m) (f n)
m n : ℕ
hmn : (fun y => f y) m ≠ (fun y => f y) n
h : m < n
⊢ rᶜ ((fun y => f y) m) ((fun y => f y) n)
[PROOFSTEP]
exact H _ _ h
[GOAL]
case refine'_2.intro.refl.intro.refl.inr
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r : α → α → Prop
r' : β → β → Prop
f✝ : α → β
s t : Set α
a : α
inst✝¹ : IsRefl α r
inst✝ : IsSymm α r
hs : ∀ (t : Set α), t ⊆ s → IsAntichain r t → Set.Finite t
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
H : ∀ (m n : ℕ), m < n → ¬r (f m) (f n)
m n : ℕ
hmn : (fun y => f y) m ≠ (fun y => f y) n
h : n < m
⊢ rᶜ ((fun y => f y) m) ((fun y => f y) n)
[PROOFSTEP]
exact mt symm (H _ _ h)
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r : α → α → Prop
r' : β → β → Prop
f✝ : α → β
s t : Set α
a : α
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
h : PartiallyWellOrderedOn s r
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
⊢ ∃ g, ∀ (m n : ℕ), m ≤ n → r (f (↑g m)) (f (↑g n))
[PROOFSTEP]
obtain ⟨g, h1 | h2⟩ := exists_increasing_or_nonincreasing_subseq r f
[GOAL]
case intro.inl
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r : α → α → Prop
r' : β → β → Prop
f✝ : α → β
s t : Set α
a : α
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
h : PartiallyWellOrderedOn s r
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
g : ℕ ↪o ℕ
h1 : ∀ (m n : ℕ), m < n → r (f (↑g m)) (f (↑g n))
⊢ ∃ g, ∀ (m n : ℕ), m ≤ n → r (f (↑g m)) (f (↑g n))
[PROOFSTEP]
refine' ⟨g, fun m n hle => _⟩
[GOAL]
case intro.inl
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r : α → α → Prop
r' : β → β → Prop
f✝ : α → β
s t : Set α
a : α
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
h : PartiallyWellOrderedOn s r
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
g : ℕ ↪o ℕ
h1 : ∀ (m n : ℕ), m < n → r (f (↑g m)) (f (↑g n))
m n : ℕ
hle : m ≤ n
⊢ r (f (↑g m)) (f (↑g n))
[PROOFSTEP]
obtain hlt | rfl := hle.lt_or_eq
[GOAL]
case intro.inl.inl
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r : α → α → Prop
r' : β → β → Prop
f✝ : α → β
s t : Set α
a : α
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
h : PartiallyWellOrderedOn s r
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
g : ℕ ↪o ℕ
h1 : ∀ (m n : ℕ), m < n → r (f (↑g m)) (f (↑g n))
m n : ℕ
hle : m ≤ n
hlt : m < n
⊢ r (f (↑g m)) (f (↑g n))
case intro.inl.inr
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r : α → α → Prop
r' : β → β → Prop
f✝ : α → β
s t : Set α
a : α
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
h : PartiallyWellOrderedOn s r
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
g : ℕ ↪o ℕ
h1 : ∀ (m n : ℕ), m < n → r (f (↑g m)) (f (↑g n))
m : ℕ
hle : m ≤ m
⊢ r (f (↑g m)) (f (↑g m))
[PROOFSTEP]
exacts [h1 m n hlt, refl_of r _]
[GOAL]
case intro.inr
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r : α → α → Prop
r' : β → β → Prop
f✝ : α → β
s t : Set α
a : α
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
h : PartiallyWellOrderedOn s r
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
g : ℕ ↪o ℕ
h2 : ∀ (m n : ℕ), m < n → ¬r (f (↑g m)) (f (↑g n))
⊢ ∃ g, ∀ (m n : ℕ), m ≤ n → r (f (↑g m)) (f (↑g n))
[PROOFSTEP]
exfalso
[GOAL]
case intro.inr.h
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r : α → α → Prop
r' : β → β → Prop
f✝ : α → β
s t : Set α
a : α
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
h : PartiallyWellOrderedOn s r
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
g : ℕ ↪o ℕ
h2 : ∀ (m n : ℕ), m < n → ¬r (f (↑g m)) (f (↑g n))
⊢ False
[PROOFSTEP]
obtain ⟨m, n, hlt, hle⟩ := h (f ∘ g) fun n => hf _
[GOAL]
case intro.inr.h.intro.intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r : α → α → Prop
r' : β → β → Prop
f✝ : α → β
s t : Set α
a : α
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
h : PartiallyWellOrderedOn s r
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
g : ℕ ↪o ℕ
h2 : ∀ (m n : ℕ), m < n → ¬r (f (↑g m)) (f (↑g n))
m n : ℕ
hlt : m < n
hle : r ((f ∘ ↑g) m) ((f ∘ ↑g) n)
⊢ False
[PROOFSTEP]
exact h2 m n hlt hle
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r : α → α → Prop
r' : β → β → Prop
f : α → β
s t : Set α
a : α
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
⊢ PartiallyWellOrderedOn s r ↔ ∀ (f : ℕ → α), (∀ (n : ℕ), f n ∈ s) → ∃ g, ∀ (m n : ℕ), m ≤ n → r (f (↑g m)) (f (↑g n))
[PROOFSTEP]
constructor
[GOAL]
case mp
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r : α → α → Prop
r' : β → β → Prop
f : α → β
s t : Set α
a : α
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
⊢ PartiallyWellOrderedOn s r → ∀ (f : ℕ → α), (∀ (n : ℕ), f n ∈ s) → ∃ g, ∀ (m n : ℕ), m ≤ n → r (f (↑g m)) (f (↑g n))
[PROOFSTEP]
intro h f hf
[GOAL]
case mpr
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r : α → α → Prop
r' : β → β → Prop
f : α → β
s t : Set α
a : α
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
⊢ (∀ (f : ℕ → α), (∀ (n : ℕ), f n ∈ s) → ∃ g, ∀ (m n : ℕ), m ≤ n → r (f (↑g m)) (f (↑g n))) → PartiallyWellOrderedOn s r
[PROOFSTEP]
intro h f hf
[GOAL]
case mp
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r : α → α → Prop
r' : β → β → Prop
f✝ : α → β
s t : Set α
a : α
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
h : PartiallyWellOrderedOn s r
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
⊢ ∃ g, ∀ (m n : ℕ), m ≤ n → r (f (↑g m)) (f (↑g n))
[PROOFSTEP]
exact h.exists_monotone_subseq f hf
[GOAL]
case mpr
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r : α → α → Prop
r' : β → β → Prop
f✝ : α → β
s t : Set α
a : α
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
h : ∀ (f : ℕ → α), (∀ (n : ℕ), f n ∈ s) → ∃ g, ∀ (m n : ℕ), m ≤ n → r (f (↑g m)) (f (↑g n))
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
⊢ ∃ m n, m < n ∧ r (f m) (f n)
[PROOFSTEP]
obtain ⟨g, gmon⟩ := h f hf
[GOAL]
case mpr.intro
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r : α → α → Prop
r' : β → β → Prop
f✝ : α → β
s t : Set α
a : α
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
h : ∀ (f : ℕ → α), (∀ (n : ℕ), f n ∈ s) → ∃ g, ∀ (m n : ℕ), m ≤ n → r (f (↑g m)) (f (↑g n))
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
g : ℕ ↪o ℕ
gmon : ∀ (m n : ℕ), m ≤ n → r (f (↑g m)) (f (↑g n))
⊢ ∃ m n, m < n ∧ r (f m) (f n)
[PROOFSTEP]
exact ⟨g 0, g 1, g.lt_iff_lt.2 zero_lt_one, gmon _ _ zero_le_one⟩
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r : α → α → Prop
r' : β → β → Prop
f : α → β
s t✝ : Set α
a : α
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
t : Set β
hs : PartiallyWellOrderedOn s r
ht : PartiallyWellOrderedOn t r'
⊢ PartiallyWellOrderedOn (s ×ˢ t) fun x y => r x.fst y.fst ∧ r' x.snd y.snd
[PROOFSTEP]
intro f hf
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r : α → α → Prop
r' : β → β → Prop
f✝ : α → β
s t✝ : Set α
a : α
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
t : Set β
hs : PartiallyWellOrderedOn s r
ht : PartiallyWellOrderedOn t r'
f : ℕ → α × β
hf : ∀ (n : ℕ), f n ∈ s ×ˢ t
⊢ ∃ m n, m < n ∧ (fun x y => r x.fst y.fst ∧ r' x.snd y.snd) (f m) (f n)
[PROOFSTEP]
obtain ⟨g₁, h₁⟩ := hs.exists_monotone_subseq (Prod.fst ∘ f) fun n => (hf n).1
[GOAL]
case intro
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r : α → α → Prop
r' : β → β → Prop
f✝ : α → β
s t✝ : Set α
a : α
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
t : Set β
hs : PartiallyWellOrderedOn s r
ht : PartiallyWellOrderedOn t r'
f : ℕ → α × β
hf : ∀ (n : ℕ), f n ∈ s ×ˢ t
g₁ : ℕ ↪o ℕ
h₁ : ∀ (m n : ℕ), m ≤ n → r ((Prod.fst ∘ f) (↑g₁ m)) ((Prod.fst ∘ f) (↑g₁ n))
⊢ ∃ m n, m < n ∧ (fun x y => r x.fst y.fst ∧ r' x.snd y.snd) (f m) (f n)
[PROOFSTEP]
obtain ⟨m, n, hlt, hle⟩ := ht (Prod.snd ∘ f ∘ g₁) fun n => (hf _).2
[GOAL]
case intro.intro.intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r : α → α → Prop
r' : β → β → Prop
f✝ : α → β
s t✝ : Set α
a : α
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
t : Set β
hs : PartiallyWellOrderedOn s r
ht : PartiallyWellOrderedOn t r'
f : ℕ → α × β
hf : ∀ (n : ℕ), f n ∈ s ×ˢ t
g₁ : ℕ ↪o ℕ
h₁ : ∀ (m n : ℕ), m ≤ n → r ((Prod.fst ∘ f) (↑g₁ m)) ((Prod.fst ∘ f) (↑g₁ n))
m n : ℕ
hlt : m < n
hle : r' ((Prod.snd ∘ f ∘ ↑g₁) m) ((Prod.snd ∘ f ∘ ↑g₁) n)
⊢ ∃ m n, m < n ∧ (fun x y => r x.fst y.fst ∧ r' x.snd y.snd) (f m) (f n)
[PROOFSTEP]
exact ⟨g₁ m, g₁ n, g₁.strictMono hlt, h₁ _ _ hlt.le, hle⟩
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r : α → α → Prop
r' : β → β → Prop
f : α → β
s t : Set α
a : α
inst✝ : IsPreorder α r
h : PartiallyWellOrderedOn s r
⊢ WellFoundedOn s fun a b => r a b ∧ ¬r b a
[PROOFSTEP]
letI : Preorder α :=
  { le := r
    le_refl := refl_of r
    le_trans := fun _ _ _ => trans_of r }
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r : α → α → Prop
r' : β → β → Prop
f : α → β
s t : Set α
a : α
inst✝ : IsPreorder α r
h : PartiallyWellOrderedOn s r
this : Preorder α := Preorder.mk (_ : ∀ (a : α), r a a) (_ : ∀ (x x_1 x_2 : α), r x x_1 → r x_1 x_2 → r x x_2)
⊢ WellFoundedOn s fun a b => r a b ∧ ¬r b a
[PROOFSTEP]
change s.WellFoundedOn (· < ·)
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r : α → α → Prop
r' : β → β → Prop
f : α → β
s t : Set α
a : α
inst✝ : IsPreorder α r
h : PartiallyWellOrderedOn s r
this : Preorder α := Preorder.mk (_ : ∀ (a : α), r a a) (_ : ∀ (x x_1 x_2 : α), r x x_1 → r x_1 x_2 → r x x_2)
⊢ WellFoundedOn s fun x x_1 => x < x_1
[PROOFSTEP]
replace h : s.PartiallyWellOrderedOn (· ≤ ·) := h
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r : α → α → Prop
r' : β → β → Prop
f : α → β
s t : Set α
a : α
inst✝ : IsPreorder α r
this : Preorder α := Preorder.mk (_ : ∀ (a : α), r a a) (_ : ∀ (x x_1 x_2 : α), r x x_1 → r x_1 x_2 → r x x_2)
h : PartiallyWellOrderedOn s fun x x_1 => x ≤ x_1
⊢ WellFoundedOn s fun x x_1 => x < x_1
[PROOFSTEP]
rw [wellFoundedOn_iff_no_descending_seq]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r : α → α → Prop
r' : β → β → Prop
f : α → β
s t : Set α
a : α
inst✝ : IsPreorder α r
this : Preorder α := Preorder.mk (_ : ∀ (a : α), r a a) (_ : ∀ (x x_1 x_2 : α), r x x_1 → r x_1 x_2 → r x x_2)
h : PartiallyWellOrderedOn s fun x x_1 => x ≤ x_1
⊢ ∀ (f : (fun x x_1 => x > x_1) ↪r fun x x_1 => x < x_1), ¬∀ (n : ℕ), ↑f n ∈ s
[PROOFSTEP]
intro f hf
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r : α → α → Prop
r' : β → β → Prop
f✝ : α → β
s t : Set α
a : α
inst✝ : IsPreorder α r
this : Preorder α := Preorder.mk (_ : ∀ (a : α), r a a) (_ : ∀ (x x_1 x_2 : α), r x x_1 → r x_1 x_2 → r x x_2)
h : PartiallyWellOrderedOn s fun x x_1 => x ≤ x_1
f : (fun x x_1 => x > x_1) ↪r fun x x_1 => x < x_1
hf : ∀ (n : ℕ), ↑f n ∈ s
⊢ False
[PROOFSTEP]
obtain ⟨m, n, hlt, hle⟩ := h f hf
[GOAL]
case intro.intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r : α → α → Prop
r' : β → β → Prop
f✝ : α → β
s t : Set α
a : α
inst✝ : IsPreorder α r
this : Preorder α := Preorder.mk (_ : ∀ (a : α), r a a) (_ : ∀ (x x_1 x_2 : α), r x x_1 → r x_1 x_2 → r x x_2)
h : PartiallyWellOrderedOn s fun x x_1 => x ≤ x_1
f : (fun x x_1 => x > x_1) ↪r fun x x_1 => x < x_1
hf : ∀ (n : ℕ), ↑f n ∈ s
m n : ℕ
hlt : m < n
hle : ↑f m ≤ ↑f n
⊢ False
[PROOFSTEP]
exact (f.map_rel_iff.2 hlt).not_le hle
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
inst✝¹ : Preorder α
inst✝ : Preorder β
s t : Set α
h : IsPwo s
⊢ IsWf s
[PROOFSTEP]
simpa only [← lt_iff_le_not_le] using h.wellFoundedOn
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
inst✝¹ : Preorder α
inst✝ : Preorder β
s t : Set α
a : α
⊢ IsPwo (insert a s) ↔ IsPwo s
[PROOFSTEP]
simp only [← singleton_union, isPwo_union, isPwo_singleton, true_and_iff]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
inst✝¹ : Preorder α
inst✝ : Preorder β
s t : Set α
a : α
⊢ IsWf (insert a s) ↔ IsWf s
[PROOFSTEP]
simp only [← singleton_union, isWf_union, isWf_singleton, true_and_iff]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r : α → α → Prop
inst✝ : IsStrictOrder α r
s : Set α
a : α
⊢ WellFoundedOn (insert a s) r ↔ WellFoundedOn s r
[PROOFSTEP]
simp only [← singleton_union, wellFoundedOn_union, wellFoundedOn_singleton, true_and_iff]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
inst✝ : LinearOrder α
s : Set α
hs : IsWf s
⊢ IsPwo s
[PROOFSTEP]
intro f hf
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
inst✝ : LinearOrder α
s : Set α
hs : IsWf s
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
⊢ ∃ m n, m < n ∧ (fun x x_1 => x ≤ x_1) (f m) (f n)
[PROOFSTEP]
lift f to ℕ → s using hf
[GOAL]
case intro
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
inst✝ : LinearOrder α
s : Set α
hs : IsWf s
f : ℕ → ↑s
⊢ ∃ m n, m < n ∧ (fun x x_1 => x ≤ x_1) ((fun i => ↑(f i)) m) ((fun i => ↑(f i)) n)
[PROOFSTEP]
rcases hs.has_min (range f) (range_nonempty _) with ⟨_, ⟨m, rfl⟩, hm⟩
[GOAL]
case intro.intro.intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
inst✝ : LinearOrder α
s : Set α
hs : IsWf s
f : ℕ → ↑s
m : ℕ
hm : ∀ (x : ↑s), x ∈ range f → ¬(fun x x_1 => x < x_1) ↑x ↑(f m)
⊢ ∃ m n, m < n ∧ (fun x x_1 => x ≤ x_1) ((fun i => ↑(f i)) m) ((fun i => ↑(f i)) n)
[PROOFSTEP]
simp only [forall_range_iff, not_lt] at hm 
[GOAL]
case intro.intro.intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
inst✝ : LinearOrder α
s : Set α
hs : IsWf s
f : ℕ → ↑s
m : ℕ
hm : ∀ (i : ℕ), ↑(f m) ≤ ↑(f i)
⊢ ∃ m n, m < n ∧ (fun x x_1 => x ≤ x_1) ((fun i => ↑(f i)) m) ((fun i => ↑(f i)) n)
[PROOFSTEP]
exact ⟨m, m + 1, lt_add_one m, hm _⟩
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r : α → α → Prop
inst✝ : IsStrictOrder α r
s : Finset ι
f : ι → Set α
⊢ Set.WellFoundedOn (sup ∅ f) r ↔ ∀ (i : ι), i ∈ ∅ → Set.WellFoundedOn (f i) r
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r : α → α → Prop
inst✝ : IsStrictOrder α r
s✝ : Finset ι
f : ι → Set α
a : ι
s : Finset ι
ha : ¬a ∈ s
hs : Set.WellFoundedOn (sup s f) r ↔ ∀ (i : ι), i ∈ s → Set.WellFoundedOn (f i) r
⊢ Set.WellFoundedOn (sup (cons a s ha) f) r ↔ ∀ (i : ι), i ∈ cons a s ha → Set.WellFoundedOn (f i) r
[PROOFSTEP]
simp [-sup_set_eq_biUnion, hs]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r : α → α → Prop
s : Finset ι
f : ι → Set α
⊢ Set.PartiallyWellOrderedOn (sup ∅ f) r ↔ ∀ (i : ι), i ∈ ∅ → Set.PartiallyWellOrderedOn (f i) r
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r : α → α → Prop
s✝ : Finset ι
f : ι → Set α
a : ι
s : Finset ι
ha : ¬a ∈ s
hs : Set.PartiallyWellOrderedOn (sup s f) r ↔ ∀ (i : ι), i ∈ s → Set.PartiallyWellOrderedOn (f i) r
⊢ Set.PartiallyWellOrderedOn (sup (cons a s ha) f) r ↔ ∀ (i : ι), i ∈ cons a s ha → Set.PartiallyWellOrderedOn (f i) r
[PROOFSTEP]
simp [-sup_set_eq_biUnion, hs]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r : α → α → Prop
inst✝ : IsStrictOrder α r
s : Finset ι
f : ι → Set α
⊢ Set.WellFoundedOn (⋃ (i : ι) (_ : i ∈ s), f i) r ↔ ∀ (i : ι), i ∈ s → Set.WellFoundedOn (f i) r
[PROOFSTEP]
simpa only [Finset.sup_eq_iSup] using s.wellFoundedOn_sup
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r : α → α → Prop
s : Finset ι
f : ι → Set α
⊢ Set.PartiallyWellOrderedOn (⋃ (i : ι) (_ : i ∈ s), f i) r ↔ ∀ (i : ι), i ∈ s → Set.PartiallyWellOrderedOn (f i) r
[PROOFSTEP]
simpa only [Finset.sup_eq_iSup] using s.partiallyWellOrderedOn_sup
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
inst✝ : LinearOrder α
s t : Set α
a : α
hs : IsWf s
hsn : Set.Nonempty s
ht : IsWf t
htn : Set.Nonempty t
⊢ min (_ : IsWf (s ∪ t)) (_ : Set.Nonempty (s ∪ t)) = Min.min (min hs hsn) (min ht htn)
[PROOFSTEP]
refine'
  le_antisymm
    (le_min (IsWf.min_le_min_of_subset (subset_union_left _ _)) (IsWf.min_le_min_of_subset (subset_union_right _ _))) _
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
inst✝ : LinearOrder α
s t : Set α
a : α
hs : IsWf s
hsn : Set.Nonempty s
ht : IsWf t
htn : Set.Nonempty t
⊢ Min.min (min hs hsn) (min ht htn) ≤ min (_ : IsWf (s ∪ t)) (_ : Set.Nonempty (s ∪ t))
[PROOFSTEP]
rw [min_le_iff]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
inst✝ : LinearOrder α
s t : Set α
a : α
hs : IsWf s
hsn : Set.Nonempty s
ht : IsWf t
htn : Set.Nonempty t
⊢ min hs hsn ≤ min (_ : IsWf (s ∪ t)) (_ : Set.Nonempty (s ∪ t)) ∨
    min ht htn ≤ min (_ : IsWf (s ∪ t)) (_ : Set.Nonempty (s ∪ t))
[PROOFSTEP]
exact ((mem_union _ _ _).1 ((hs.union ht).min_mem (union_nonempty.2 (.inl hsn)))).imp (hs.min_le _) (ht.min_le _)
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r✝ r : α → α → Prop
s : Set α
f : ℕ → α
⊢ ((∀ (n : ℕ), f n ∈ s) → ∃ m n, m < n ∧ r (f m) (f n)) ↔ ¬IsBadSeq r s f
[PROOFSTEP]
simp [IsBadSeq]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r✝ r : α → α → Prop
rk : α → ℕ
s : Set α
n : ℕ
f : ℕ → α
hf : IsBadSeq r s f
⊢ { g // (∀ (m : ℕ), m < n → f m = g m) ∧ IsBadSeq r s g ∧ IsMinBadSeq r rk s n g }
[PROOFSTEP]
classical
have h : ∃ (k : ℕ) (g : ℕ → α), (∀ m, m < n → f m = g m) ∧ IsBadSeq r s g ∧ rk (g n) = k :=
  ⟨_, f, fun _ _ => rfl, hf, rfl⟩
obtain ⟨h1, h2, h3⟩ := Classical.choose_spec (Nat.find_spec h)
refine' ⟨Classical.choose (Nat.find_spec h), h1, by convert h2, fun g hg1 hg2 con => _⟩
refine' Nat.find_min h _ ⟨g, fun m mn => (h1 m mn).trans (hg1 m mn), con, rfl⟩
rwa [← h3]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r✝ r : α → α → Prop
rk : α → ℕ
s : Set α
n : ℕ
f : ℕ → α
hf : IsBadSeq r s f
⊢ { g // (∀ (m : ℕ), m < n → f m = g m) ∧ IsBadSeq r s g ∧ IsMinBadSeq r rk s n g }
[PROOFSTEP]
have h : ∃ (k : ℕ) (g : ℕ → α), (∀ m, m < n → f m = g m) ∧ IsBadSeq r s g ∧ rk (g n) = k :=
  ⟨_, f, fun _ _ => rfl, hf, rfl⟩
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r✝ r : α → α → Prop
rk : α → ℕ
s : Set α
n : ℕ
f : ℕ → α
hf : IsBadSeq r s f
h : ∃ k g, (∀ (m : ℕ), m < n → f m = g m) ∧ IsBadSeq r s g ∧ rk (g n) = k
⊢ { g // (∀ (m : ℕ), m < n → f m = g m) ∧ IsBadSeq r s g ∧ IsMinBadSeq r rk s n g }
[PROOFSTEP]
obtain ⟨h1, h2, h3⟩ := Classical.choose_spec (Nat.find_spec h)
[GOAL]
case intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r✝ r : α → α → Prop
rk : α → ℕ
s : Set α
n : ℕ
f : ℕ → α
hf : IsBadSeq r s f
h : ∃ k g, (∀ (m : ℕ), m < n → f m = g m) ∧ IsBadSeq r s g ∧ rk (g n) = k
h1 :
  ∀ (m : ℕ),
    m < n → f m = Classical.choose (_ : ∃ g, (∀ (m : ℕ), m < n → f m = g m) ∧ IsBadSeq r s g ∧ rk (g n) = Nat.find h) m
h2 : IsBadSeq r s (Classical.choose (_ : ∃ g, (∀ (m : ℕ), m < n → f m = g m) ∧ IsBadSeq r s g ∧ rk (g n) = Nat.find h))
h3 :
  rk (Classical.choose (_ : ∃ g, (∀ (m : ℕ), m < n → f m = g m) ∧ IsBadSeq r s g ∧ rk (g n) = Nat.find h) n) =
    Nat.find h
⊢ { g // (∀ (m : ℕ), m < n → f m = g m) ∧ IsBadSeq r s g ∧ IsMinBadSeq r rk s n g }
[PROOFSTEP]
refine' ⟨Classical.choose (Nat.find_spec h), h1, by convert h2, fun g hg1 hg2 con => _⟩
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r✝ r : α → α → Prop
rk : α → ℕ
s : Set α
n : ℕ
f : ℕ → α
hf : IsBadSeq r s f
h : ∃ k g, (∀ (m : ℕ), m < n → f m = g m) ∧ IsBadSeq r s g ∧ rk (g n) = k
h1 :
  ∀ (m : ℕ),
    m < n → f m = Classical.choose (_ : ∃ g, (∀ (m : ℕ), m < n → f m = g m) ∧ IsBadSeq r s g ∧ rk (g n) = Nat.find h) m
h2 : IsBadSeq r s (Classical.choose (_ : ∃ g, (∀ (m : ℕ), m < n → f m = g m) ∧ IsBadSeq r s g ∧ rk (g n) = Nat.find h))
h3 :
  rk (Classical.choose (_ : ∃ g, (∀ (m : ℕ), m < n → f m = g m) ∧ IsBadSeq r s g ∧ rk (g n) = Nat.find h) n) =
    Nat.find h
⊢ IsBadSeq r s (Classical.choose (_ : ∃ g, (∀ (m : ℕ), m < n → f m = g m) ∧ IsBadSeq r s g ∧ rk (g n) = Nat.find h))
[PROOFSTEP]
convert h2
[GOAL]
case intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r✝ r : α → α → Prop
rk : α → ℕ
s : Set α
n : ℕ
f : ℕ → α
hf : IsBadSeq r s f
h : ∃ k g, (∀ (m : ℕ), m < n → f m = g m) ∧ IsBadSeq r s g ∧ rk (g n) = k
h1 :
  ∀ (m : ℕ),
    m < n → f m = Classical.choose (_ : ∃ g, (∀ (m : ℕ), m < n → f m = g m) ∧ IsBadSeq r s g ∧ rk (g n) = Nat.find h) m
h2 : IsBadSeq r s (Classical.choose (_ : ∃ g, (∀ (m : ℕ), m < n → f m = g m) ∧ IsBadSeq r s g ∧ rk (g n) = Nat.find h))
h3 :
  rk (Classical.choose (_ : ∃ g, (∀ (m : ℕ), m < n → f m = g m) ∧ IsBadSeq r s g ∧ rk (g n) = Nat.find h) n) =
    Nat.find h
g : ℕ → α
hg1 :
  ∀ (m : ℕ),
    m < n → Classical.choose (_ : ∃ g, (∀ (m : ℕ), m < n → f m = g m) ∧ IsBadSeq r s g ∧ rk (g n) = Nat.find h) m = g m
hg2 :
  rk (g n) < rk (Classical.choose (_ : ∃ g, (∀ (m : ℕ), m < n → f m = g m) ∧ IsBadSeq r s g ∧ rk (g n) = Nat.find h) n)
con : IsBadSeq r s g
⊢ False
[PROOFSTEP]
refine' Nat.find_min h _ ⟨g, fun m mn => (h1 m mn).trans (hg1 m mn), con, rfl⟩
[GOAL]
case intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r✝ r : α → α → Prop
rk : α → ℕ
s : Set α
n : ℕ
f : ℕ → α
hf : IsBadSeq r s f
h : ∃ k g, (∀ (m : ℕ), m < n → f m = g m) ∧ IsBadSeq r s g ∧ rk (g n) = k
h1 :
  ∀ (m : ℕ),
    m < n → f m = Classical.choose (_ : ∃ g, (∀ (m : ℕ), m < n → f m = g m) ∧ IsBadSeq r s g ∧ rk (g n) = Nat.find h) m
h2 : IsBadSeq r s (Classical.choose (_ : ∃ g, (∀ (m : ℕ), m < n → f m = g m) ∧ IsBadSeq r s g ∧ rk (g n) = Nat.find h))
h3 :
  rk (Classical.choose (_ : ∃ g, (∀ (m : ℕ), m < n → f m = g m) ∧ IsBadSeq r s g ∧ rk (g n) = Nat.find h) n) =
    Nat.find h
g : ℕ → α
hg1 :
  ∀ (m : ℕ),
    m < n → Classical.choose (_ : ∃ g, (∀ (m : ℕ), m < n → f m = g m) ∧ IsBadSeq r s g ∧ rk (g n) = Nat.find h) m = g m
hg2 :
  rk (g n) < rk (Classical.choose (_ : ∃ g, (∀ (m : ℕ), m < n → f m = g m) ∧ IsBadSeq r s g ∧ rk (g n) = Nat.find h) n)
con : IsBadSeq r s g
⊢ rk (g n) < Nat.find h
[PROOFSTEP]
rwa [← h3]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r✝ r : α → α → Prop
rk : α → ℕ
s : Set α
⊢ (∃ f, IsBadSeq r s f) → ∃ f, IsBadSeq r s f ∧ ∀ (n : ℕ), IsMinBadSeq r rk s n f
[PROOFSTEP]
rintro ⟨f0, hf0 : IsBadSeq r s f0⟩
[GOAL]
case intro
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r✝ r : α → α → Prop
rk : α → ℕ
s : Set α
f0 : ℕ → α
hf0 : IsBadSeq r s f0
⊢ ∃ f, IsBadSeq r s f ∧ ∀ (n : ℕ), IsMinBadSeq r rk s n f
[PROOFSTEP]
let fs : ∀ n : ℕ, { f : ℕ → α // IsBadSeq r s f ∧ IsMinBadSeq r rk s n f } :=
  by
  refine' Nat.rec _ fun n fn => _
  · exact ⟨(minBadSeqOfBadSeq r rk s 0 f0 hf0).1, (minBadSeqOfBadSeq r rk s 0 f0 hf0).2.2⟩
  · exact ⟨(minBadSeqOfBadSeq r rk s (n + 1) fn.1 fn.2.1).1, (minBadSeqOfBadSeq r rk s (n + 1) fn.1 fn.2.1).2.2⟩
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r✝ r : α → α → Prop
rk : α → ℕ
s : Set α
f0 : ℕ → α
hf0 : IsBadSeq r s f0
⊢ (n : ℕ) → { f // IsBadSeq r s f ∧ IsMinBadSeq r rk s n f }
[PROOFSTEP]
refine' Nat.rec _ fun n fn => _
[GOAL]
case refine'_1
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r✝ r : α → α → Prop
rk : α → ℕ
s : Set α
f0 : ℕ → α
hf0 : IsBadSeq r s f0
⊢ { f // IsBadSeq r s f ∧ IsMinBadSeq r rk s Nat.zero f }
[PROOFSTEP]
exact ⟨(minBadSeqOfBadSeq r rk s 0 f0 hf0).1, (minBadSeqOfBadSeq r rk s 0 f0 hf0).2.2⟩
[GOAL]
case refine'_2
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r✝ r : α → α → Prop
rk : α → ℕ
s : Set α
f0 : ℕ → α
hf0 : IsBadSeq r s f0
n : ℕ
fn : { f // IsBadSeq r s f ∧ IsMinBadSeq r rk s n f }
⊢ { f // IsBadSeq r s f ∧ IsMinBadSeq r rk s (Nat.succ n) f }
[PROOFSTEP]
exact ⟨(minBadSeqOfBadSeq r rk s (n + 1) fn.1 fn.2.1).1, (minBadSeqOfBadSeq r rk s (n + 1) fn.1 fn.2.1).2.2⟩
[GOAL]
case intro
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r✝ r : α → α → Prop
rk : α → ℕ
s : Set α
f0 : ℕ → α
hf0 : IsBadSeq r s f0
fs : (n : ℕ) → { f // IsBadSeq r s f ∧ IsMinBadSeq r rk s n f } :=
  fun t =>
    Nat.rec
      { val := ↑(minBadSeqOfBadSeq r rk s 0 f0 hf0),
        property :=
          (_ :
            IsBadSeq r s ↑(minBadSeqOfBadSeq r rk s 0 f0 hf0) ∧
              IsMinBadSeq r rk s 0 ↑(minBadSeqOfBadSeq r rk s 0 f0 hf0)) }
      (fun n fn =>
        { val := ↑(minBadSeqOfBadSeq r rk s (n + 1) ↑fn (_ : IsBadSeq r s ↑fn)),
          property :=
            (_ :
              IsBadSeq r s ↑(minBadSeqOfBadSeq r rk s (n + 1) ↑fn (_ : IsBadSeq r s ↑fn)) ∧
                IsMinBadSeq r rk s (n + 1) ↑(minBadSeqOfBadSeq r rk s (n + 1) ↑fn (_ : IsBadSeq r s ↑fn))) })
      t
⊢ ∃ f, IsBadSeq r s f ∧ ∀ (n : ℕ), IsMinBadSeq r rk s n f
[PROOFSTEP]
have h : ∀ m n, m ≤ n → (fs m).1 m = (fs n).1 m := fun m n mn =>
  by
  obtain ⟨k, rfl⟩ := exists_add_of_le mn; clear mn
  induction' k with k ih
  · rfl
  · rw [ih,
      (minBadSeqOfBadSeq r rk s (m + k + 1) (fs (m + k)).1 (fs (m + k)).2.1).2.1 m
        (Nat.lt_succ_iff.2 (Nat.add_le_add_left k.zero_le m))]
    rfl
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r✝ r : α → α → Prop
rk : α → ℕ
s : Set α
f0 : ℕ → α
hf0 : IsBadSeq r s f0
fs : (n : ℕ) → { f // IsBadSeq r s f ∧ IsMinBadSeq r rk s n f } :=
  fun t =>
    Nat.rec
      { val := ↑(minBadSeqOfBadSeq r rk s 0 f0 hf0),
        property :=
          (_ :
            IsBadSeq r s ↑(minBadSeqOfBadSeq r rk s 0 f0 hf0) ∧
              IsMinBadSeq r rk s 0 ↑(minBadSeqOfBadSeq r rk s 0 f0 hf0)) }
      (fun n fn =>
        { val := ↑(minBadSeqOfBadSeq r rk s (n + 1) ↑fn (_ : IsBadSeq r s ↑fn)),
          property :=
            (_ :
              IsBadSeq r s ↑(minBadSeqOfBadSeq r rk s (n + 1) ↑fn (_ : IsBadSeq r s ↑fn)) ∧
                IsMinBadSeq r rk s (n + 1) ↑(minBadSeqOfBadSeq r rk s (n + 1) ↑fn (_ : IsBadSeq r s ↑fn))) })
      t
m n : ℕ
mn : m ≤ n
⊢ ↑(fs m) m = ↑(fs n) m
[PROOFSTEP]
obtain ⟨k, rfl⟩ := exists_add_of_le mn
[GOAL]
case intro
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r✝ r : α → α → Prop
rk : α → ℕ
s : Set α
f0 : ℕ → α
hf0 : IsBadSeq r s f0
fs : (n : ℕ) → { f // IsBadSeq r s f ∧ IsMinBadSeq r rk s n f } :=
  fun t =>
    Nat.rec
      { val := ↑(minBadSeqOfBadSeq r rk s 0 f0 hf0),
        property :=
          (_ :
            IsBadSeq r s ↑(minBadSeqOfBadSeq r rk s 0 f0 hf0) ∧
              IsMinBadSeq r rk s 0 ↑(minBadSeqOfBadSeq r rk s 0 f0 hf0)) }
      (fun n fn =>
        { val := ↑(minBadSeqOfBadSeq r rk s (n + 1) ↑fn (_ : IsBadSeq r s ↑fn)),
          property :=
            (_ :
              IsBadSeq r s ↑(minBadSeqOfBadSeq r rk s (n + 1) ↑fn (_ : IsBadSeq r s ↑fn)) ∧
                IsMinBadSeq r rk s (n + 1) ↑(minBadSeqOfBadSeq r rk s (n + 1) ↑fn (_ : IsBadSeq r s ↑fn))) })
      t
m k : ℕ
mn : m ≤ m + k
⊢ ↑(fs m) m = ↑(fs (m + k)) m
[PROOFSTEP]
clear mn
[GOAL]
case intro
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r✝ r : α → α → Prop
rk : α → ℕ
s : Set α
f0 : ℕ → α
hf0 : IsBadSeq r s f0
fs : (n : ℕ) → { f // IsBadSeq r s f ∧ IsMinBadSeq r rk s n f } :=
  fun t =>
    Nat.rec
      { val := ↑(minBadSeqOfBadSeq r rk s 0 f0 hf0),
        property :=
          (_ :
            IsBadSeq r s ↑(minBadSeqOfBadSeq r rk s 0 f0 hf0) ∧
              IsMinBadSeq r rk s 0 ↑(minBadSeqOfBadSeq r rk s 0 f0 hf0)) }
      (fun n fn =>
        { val := ↑(minBadSeqOfBadSeq r rk s (n + 1) ↑fn (_ : IsBadSeq r s ↑fn)),
          property :=
            (_ :
              IsBadSeq r s ↑(minBadSeqOfBadSeq r rk s (n + 1) ↑fn (_ : IsBadSeq r s ↑fn)) ∧
                IsMinBadSeq r rk s (n + 1) ↑(minBadSeqOfBadSeq r rk s (n + 1) ↑fn (_ : IsBadSeq r s ↑fn))) })
      t
m k : ℕ
⊢ ↑(fs m) m = ↑(fs (m + k)) m
[PROOFSTEP]
induction' k with k ih
[GOAL]
case intro.zero
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r✝ r : α → α → Prop
rk : α → ℕ
s : Set α
f0 : ℕ → α
hf0 : IsBadSeq r s f0
fs : (n : ℕ) → { f // IsBadSeq r s f ∧ IsMinBadSeq r rk s n f } :=
  fun t =>
    Nat.rec
      { val := ↑(minBadSeqOfBadSeq r rk s 0 f0 hf0),
        property :=
          (_ :
            IsBadSeq r s ↑(minBadSeqOfBadSeq r rk s 0 f0 hf0) ∧
              IsMinBadSeq r rk s 0 ↑(minBadSeqOfBadSeq r rk s 0 f0 hf0)) }
      (fun n fn =>
        { val := ↑(minBadSeqOfBadSeq r rk s (n + 1) ↑fn (_ : IsBadSeq r s ↑fn)),
          property :=
            (_ :
              IsBadSeq r s ↑(minBadSeqOfBadSeq r rk s (n + 1) ↑fn (_ : IsBadSeq r s ↑fn)) ∧
                IsMinBadSeq r rk s (n + 1) ↑(minBadSeqOfBadSeq r rk s (n + 1) ↑fn (_ : IsBadSeq r s ↑fn))) })
      t
m : ℕ
⊢ ↑(fs m) m = ↑(fs (m + Nat.zero)) m
[PROOFSTEP]
rfl
[GOAL]
case intro.succ
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r✝ r : α → α → Prop
rk : α → ℕ
s : Set α
f0 : ℕ → α
hf0 : IsBadSeq r s f0
fs : (n : ℕ) → { f // IsBadSeq r s f ∧ IsMinBadSeq r rk s n f } :=
  fun t =>
    Nat.rec
      { val := ↑(minBadSeqOfBadSeq r rk s 0 f0 hf0),
        property :=
          (_ :
            IsBadSeq r s ↑(minBadSeqOfBadSeq r rk s 0 f0 hf0) ∧
              IsMinBadSeq r rk s 0 ↑(minBadSeqOfBadSeq r rk s 0 f0 hf0)) }
      (fun n fn =>
        { val := ↑(minBadSeqOfBadSeq r rk s (n + 1) ↑fn (_ : IsBadSeq r s ↑fn)),
          property :=
            (_ :
              IsBadSeq r s ↑(minBadSeqOfBadSeq r rk s (n + 1) ↑fn (_ : IsBadSeq r s ↑fn)) ∧
                IsMinBadSeq r rk s (n + 1) ↑(minBadSeqOfBadSeq r rk s (n + 1) ↑fn (_ : IsBadSeq r s ↑fn))) })
      t
m k : ℕ
ih : ↑(fs m) m = ↑(fs (m + k)) m
⊢ ↑(fs m) m = ↑(fs (m + Nat.succ k)) m
[PROOFSTEP]
rw [ih,
  (minBadSeqOfBadSeq r rk s (m + k + 1) (fs (m + k)).1 (fs (m + k)).2.1).2.1 m
    (Nat.lt_succ_iff.2 (Nat.add_le_add_left k.zero_le m))]
[GOAL]
case intro.succ
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r✝ r : α → α → Prop
rk : α → ℕ
s : Set α
f0 : ℕ → α
hf0 : IsBadSeq r s f0
fs : (n : ℕ) → { f // IsBadSeq r s f ∧ IsMinBadSeq r rk s n f } :=
  fun t =>
    Nat.rec
      { val := ↑(minBadSeqOfBadSeq r rk s 0 f0 hf0),
        property :=
          (_ :
            IsBadSeq r s ↑(minBadSeqOfBadSeq r rk s 0 f0 hf0) ∧
              IsMinBadSeq r rk s 0 ↑(minBadSeqOfBadSeq r rk s 0 f0 hf0)) }
      (fun n fn =>
        { val := ↑(minBadSeqOfBadSeq r rk s (n + 1) ↑fn (_ : IsBadSeq r s ↑fn)),
          property :=
            (_ :
              IsBadSeq r s ↑(minBadSeqOfBadSeq r rk s (n + 1) ↑fn (_ : IsBadSeq r s ↑fn)) ∧
                IsMinBadSeq r rk s (n + 1) ↑(minBadSeqOfBadSeq r rk s (n + 1) ↑fn (_ : IsBadSeq r s ↑fn))) })
      t
m k : ℕ
ih : ↑(fs m) m = ↑(fs (m + k)) m
⊢ ↑(minBadSeqOfBadSeq r rk s (m + k + 1) ↑(fs (m + k)) (_ : IsBadSeq r s ↑(fs (m + k)))) m = ↑(fs (m + Nat.succ k)) m
[PROOFSTEP]
rfl
[GOAL]
case intro
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r✝ r : α → α → Prop
rk : α → ℕ
s : Set α
f0 : ℕ → α
hf0 : IsBadSeq r s f0
fs : (n : ℕ) → { f // IsBadSeq r s f ∧ IsMinBadSeq r rk s n f } :=
  fun t =>
    Nat.rec
      { val := ↑(minBadSeqOfBadSeq r rk s 0 f0 hf0),
        property :=
          (_ :
            IsBadSeq r s ↑(minBadSeqOfBadSeq r rk s 0 f0 hf0) ∧
              IsMinBadSeq r rk s 0 ↑(minBadSeqOfBadSeq r rk s 0 f0 hf0)) }
      (fun n fn =>
        { val := ↑(minBadSeqOfBadSeq r rk s (n + 1) ↑fn (_ : IsBadSeq r s ↑fn)),
          property :=
            (_ :
              IsBadSeq r s ↑(minBadSeqOfBadSeq r rk s (n + 1) ↑fn (_ : IsBadSeq r s ↑fn)) ∧
                IsMinBadSeq r rk s (n + 1) ↑(minBadSeqOfBadSeq r rk s (n + 1) ↑fn (_ : IsBadSeq r s ↑fn))) })
      t
h : ∀ (m n : ℕ), m ≤ n → ↑(fs m) m = ↑(fs n) m
⊢ ∃ f, IsBadSeq r s f ∧ ∀ (n : ℕ), IsMinBadSeq r rk s n f
[PROOFSTEP]
refine ⟨fun n => (fs n).1 n, ⟨fun n => (fs n).2.1.1 n, fun m n mn => ?_⟩, fun n g hg1 hg2 => ?_⟩
[GOAL]
case intro.refine_1
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r✝ r : α → α → Prop
rk : α → ℕ
s : Set α
f0 : ℕ → α
hf0 : IsBadSeq r s f0
fs : (n : ℕ) → { f // IsBadSeq r s f ∧ IsMinBadSeq r rk s n f } :=
  fun t =>
    Nat.rec
      { val := ↑(minBadSeqOfBadSeq r rk s 0 f0 hf0),
        property :=
          (_ :
            IsBadSeq r s ↑(minBadSeqOfBadSeq r rk s 0 f0 hf0) ∧
              IsMinBadSeq r rk s 0 ↑(minBadSeqOfBadSeq r rk s 0 f0 hf0)) }
      (fun n fn =>
        { val := ↑(minBadSeqOfBadSeq r rk s (n + 1) ↑fn (_ : IsBadSeq r s ↑fn)),
          property :=
            (_ :
              IsBadSeq r s ↑(minBadSeqOfBadSeq r rk s (n + 1) ↑fn (_ : IsBadSeq r s ↑fn)) ∧
                IsMinBadSeq r rk s (n + 1) ↑(minBadSeqOfBadSeq r rk s (n + 1) ↑fn (_ : IsBadSeq r s ↑fn))) })
      t
h : ∀ (m n : ℕ), m ≤ n → ↑(fs m) m = ↑(fs n) m
m n : ℕ
mn : m < n
⊢ ¬r ((fun n => ↑(fs n) n) m) ((fun n => ↑(fs n) n) n)
[PROOFSTEP]
dsimp
[GOAL]
case intro.refine_1
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r✝ r : α → α → Prop
rk : α → ℕ
s : Set α
f0 : ℕ → α
hf0 : IsBadSeq r s f0
fs : (n : ℕ) → { f // IsBadSeq r s f ∧ IsMinBadSeq r rk s n f } :=
  fun t =>
    Nat.rec
      { val := ↑(minBadSeqOfBadSeq r rk s 0 f0 hf0),
        property :=
          (_ :
            IsBadSeq r s ↑(minBadSeqOfBadSeq r rk s 0 f0 hf0) ∧
              IsMinBadSeq r rk s 0 ↑(minBadSeqOfBadSeq r rk s 0 f0 hf0)) }
      (fun n fn =>
        { val := ↑(minBadSeqOfBadSeq r rk s (n + 1) ↑fn (_ : IsBadSeq r s ↑fn)),
          property :=
            (_ :
              IsBadSeq r s ↑(minBadSeqOfBadSeq r rk s (n + 1) ↑fn (_ : IsBadSeq r s ↑fn)) ∧
                IsMinBadSeq r rk s (n + 1) ↑(minBadSeqOfBadSeq r rk s (n + 1) ↑fn (_ : IsBadSeq r s ↑fn))) })
      t
h : ∀ (m n : ℕ), m ≤ n → ↑(fs m) m = ↑(fs n) m
m n : ℕ
mn : m < n
⊢ ¬r
      (↑(Nat.rec
            { val := ↑(minBadSeqOfBadSeq r rk s 0 f0 hf0),
              property :=
                (_ :
                  IsBadSeq r s ↑(minBadSeqOfBadSeq r rk s 0 f0 hf0) ∧
                    IsMinBadSeq r rk s 0 ↑(minBadSeqOfBadSeq r rk s 0 f0 hf0)) }
            (fun n fn =>
              { val := ↑(minBadSeqOfBadSeq r rk s (n + 1) ↑fn (_ : IsBadSeq r s ↑fn)),
                property :=
                  (_ :
                    IsBadSeq r s ↑(minBadSeqOfBadSeq r rk s (n + 1) ↑fn (_ : IsBadSeq r s ↑fn)) ∧
                      IsMinBadSeq r rk s (n + 1) ↑(minBadSeqOfBadSeq r rk s (n + 1) ↑fn (_ : IsBadSeq r s ↑fn))) })
            m)
        m)
      (↑(Nat.rec
            { val := ↑(minBadSeqOfBadSeq r rk s 0 f0 hf0),
              property :=
                (_ :
                  IsBadSeq r s ↑(minBadSeqOfBadSeq r rk s 0 f0 hf0) ∧
                    IsMinBadSeq r rk s 0 ↑(minBadSeqOfBadSeq r rk s 0 f0 hf0)) }
            (fun n fn =>
              { val := ↑(minBadSeqOfBadSeq r rk s (n + 1) ↑fn (_ : IsBadSeq r s ↑fn)),
                property :=
                  (_ :
                    IsBadSeq r s ↑(minBadSeqOfBadSeq r rk s (n + 1) ↑fn (_ : IsBadSeq r s ↑fn)) ∧
                      IsMinBadSeq r rk s (n + 1) ↑(minBadSeqOfBadSeq r rk s (n + 1) ↑fn (_ : IsBadSeq r s ↑fn))) })
            n)
        n)
[PROOFSTEP]
rw [h m n mn.le]
[GOAL]
case intro.refine_1
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r✝ r : α → α → Prop
rk : α → ℕ
s : Set α
f0 : ℕ → α
hf0 : IsBadSeq r s f0
fs : (n : ℕ) → { f // IsBadSeq r s f ∧ IsMinBadSeq r rk s n f } :=
  fun t =>
    Nat.rec
      { val := ↑(minBadSeqOfBadSeq r rk s 0 f0 hf0),
        property :=
          (_ :
            IsBadSeq r s ↑(minBadSeqOfBadSeq r rk s 0 f0 hf0) ∧
              IsMinBadSeq r rk s 0 ↑(minBadSeqOfBadSeq r rk s 0 f0 hf0)) }
      (fun n fn =>
        { val := ↑(minBadSeqOfBadSeq r rk s (n + 1) ↑fn (_ : IsBadSeq r s ↑fn)),
          property :=
            (_ :
              IsBadSeq r s ↑(minBadSeqOfBadSeq r rk s (n + 1) ↑fn (_ : IsBadSeq r s ↑fn)) ∧
                IsMinBadSeq r rk s (n + 1) ↑(minBadSeqOfBadSeq r rk s (n + 1) ↑fn (_ : IsBadSeq r s ↑fn))) })
      t
h : ∀ (m n : ℕ), m ≤ n → ↑(fs m) m = ↑(fs n) m
m n : ℕ
mn : m < n
⊢ ¬r (↑(fs n) m)
      (↑(Nat.rec
            { val := ↑(minBadSeqOfBadSeq r rk s 0 f0 hf0),
              property :=
                (_ :
                  IsBadSeq r s ↑(minBadSeqOfBadSeq r rk s 0 f0 hf0) ∧
                    IsMinBadSeq r rk s 0 ↑(minBadSeqOfBadSeq r rk s 0 f0 hf0)) }
            (fun n fn =>
              { val := ↑(minBadSeqOfBadSeq r rk s (n + 1) ↑fn (_ : IsBadSeq r s ↑fn)),
                property :=
                  (_ :
                    IsBadSeq r s ↑(minBadSeqOfBadSeq r rk s (n + 1) ↑fn (_ : IsBadSeq r s ↑fn)) ∧
                      IsMinBadSeq r rk s (n + 1) ↑(minBadSeqOfBadSeq r rk s (n + 1) ↑fn (_ : IsBadSeq r s ↑fn))) })
            n)
        n)
[PROOFSTEP]
exact (fs n).2.1.2 m n mn
[GOAL]
case intro.refine_2
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r✝ r : α → α → Prop
rk : α → ℕ
s : Set α
f0 : ℕ → α
hf0 : IsBadSeq r s f0
fs : (n : ℕ) → { f // IsBadSeq r s f ∧ IsMinBadSeq r rk s n f } :=
  fun t =>
    Nat.rec
      { val := ↑(minBadSeqOfBadSeq r rk s 0 f0 hf0),
        property :=
          (_ :
            IsBadSeq r s ↑(minBadSeqOfBadSeq r rk s 0 f0 hf0) ∧
              IsMinBadSeq r rk s 0 ↑(minBadSeqOfBadSeq r rk s 0 f0 hf0)) }
      (fun n fn =>
        { val := ↑(minBadSeqOfBadSeq r rk s (n + 1) ↑fn (_ : IsBadSeq r s ↑fn)),
          property :=
            (_ :
              IsBadSeq r s ↑(minBadSeqOfBadSeq r rk s (n + 1) ↑fn (_ : IsBadSeq r s ↑fn)) ∧
                IsMinBadSeq r rk s (n + 1) ↑(minBadSeqOfBadSeq r rk s (n + 1) ↑fn (_ : IsBadSeq r s ↑fn))) })
      t
h : ∀ (m n : ℕ), m ≤ n → ↑(fs m) m = ↑(fs n) m
n : ℕ
g : ℕ → α
hg1 : ∀ (m : ℕ), m < n → (fun n => ↑(fs n) n) m = g m
hg2 : rk (g n) < rk ((fun n => ↑(fs n) n) n)
⊢ ¬IsBadSeq r s g
[PROOFSTEP]
refine (fs n).2.2 g (fun m mn => ?_) hg2
[GOAL]
case intro.refine_2
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r✝ r : α → α → Prop
rk : α → ℕ
s : Set α
f0 : ℕ → α
hf0 : IsBadSeq r s f0
fs : (n : ℕ) → { f // IsBadSeq r s f ∧ IsMinBadSeq r rk s n f } :=
  fun t =>
    Nat.rec
      { val := ↑(minBadSeqOfBadSeq r rk s 0 f0 hf0),
        property :=
          (_ :
            IsBadSeq r s ↑(minBadSeqOfBadSeq r rk s 0 f0 hf0) ∧
              IsMinBadSeq r rk s 0 ↑(minBadSeqOfBadSeq r rk s 0 f0 hf0)) }
      (fun n fn =>
        { val := ↑(minBadSeqOfBadSeq r rk s (n + 1) ↑fn (_ : IsBadSeq r s ↑fn)),
          property :=
            (_ :
              IsBadSeq r s ↑(minBadSeqOfBadSeq r rk s (n + 1) ↑fn (_ : IsBadSeq r s ↑fn)) ∧
                IsMinBadSeq r rk s (n + 1) ↑(minBadSeqOfBadSeq r rk s (n + 1) ↑fn (_ : IsBadSeq r s ↑fn))) })
      t
h : ∀ (m n : ℕ), m ≤ n → ↑(fs m) m = ↑(fs n) m
n : ℕ
g : ℕ → α
hg1 : ∀ (m : ℕ), m < n → (fun n => ↑(fs n) n) m = g m
hg2 : rk (g n) < rk ((fun n => ↑(fs n) n) n)
m : ℕ
mn : m < n
⊢ ↑(fs n) m = g m
[PROOFSTEP]
rw [← h m n mn.le, ← hg1 m mn]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r : α → α → Prop
rk : α → ℕ
s : Set α
⊢ PartiallyWellOrderedOn s r ↔ ¬∃ f, IsBadSeq r s f ∧ ∀ (n : ℕ), IsMinBadSeq r rk s n f
[PROOFSTEP]
rw [iff_forall_not_isBadSeq, ← not_exists, not_congr]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r : α → α → Prop
rk : α → ℕ
s : Set α
⊢ (∃ x, IsBadSeq r s x) ↔ ∃ f, IsBadSeq r s f ∧ ∀ (n : ℕ), IsMinBadSeq r rk s n f
[PROOFSTEP]
constructor
[GOAL]
case mp
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r : α → α → Prop
rk : α → ℕ
s : Set α
⊢ (∃ x, IsBadSeq r s x) → ∃ f, IsBadSeq r s f ∧ ∀ (n : ℕ), IsMinBadSeq r rk s n f
[PROOFSTEP]
apply exists_min_bad_of_exists_bad
[GOAL]
case mpr
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r : α → α → Prop
rk : α → ℕ
s : Set α
⊢ (∃ f, IsBadSeq r s f ∧ ∀ (n : ℕ), IsMinBadSeq r rk s n f) → ∃ x, IsBadSeq r s x
[PROOFSTEP]
rintro ⟨f, hf1, -⟩
[GOAL]
case mpr.intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r : α → α → Prop
rk : α → ℕ
s : Set α
f : ℕ → α
hf1 : IsBadSeq r s f
⊢ ∃ x, IsBadSeq r s x
[PROOFSTEP]
exact ⟨f, hf1⟩
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r✝ r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : PartiallyWellOrderedOn s r
⊢ PartiallyWellOrderedOn {l | ∀ (x : α), x ∈ l → x ∈ s} (List.SublistForall₂ r)
[PROOFSTEP]
rcases isEmpty_or_nonempty α
[GOAL]
case inl
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r✝ r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : PartiallyWellOrderedOn s r
h✝ : IsEmpty α
⊢ PartiallyWellOrderedOn {l | ∀ (x : α), x ∈ l → x ∈ s} (List.SublistForall₂ r)
[PROOFSTEP]
exact subsingleton_of_subsingleton.partiallyWellOrderedOn
[GOAL]
case inr
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r✝ r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : PartiallyWellOrderedOn s r
h✝ : Nonempty α
⊢ PartiallyWellOrderedOn {l | ∀ (x : α), x ∈ l → x ∈ s} (List.SublistForall₂ r)
[PROOFSTEP]
inhabit α
[GOAL]
case inr
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r✝ r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : PartiallyWellOrderedOn s r
h✝ : Nonempty α
inhabited_h : Inhabited α
⊢ PartiallyWellOrderedOn {l | ∀ (x : α), x ∈ l → x ∈ s} (List.SublistForall₂ r)
[PROOFSTEP]
rw [iff_not_exists_isMinBadSeq List.length]
[GOAL]
case inr
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r✝ r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : PartiallyWellOrderedOn s r
h✝ : Nonempty α
inhabited_h : Inhabited α
⊢ ¬∃ f,
      IsBadSeq (List.SublistForall₂ r) {l | ∀ (x : α), x ∈ l → x ∈ s} f ∧
        ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ (x : α), x ∈ l → x ∈ s} n f
[PROOFSTEP]
rintro ⟨f, hf1, hf2⟩
[GOAL]
case inr.intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r✝ r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : PartiallyWellOrderedOn s r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ (x : α), x ∈ l → x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ (x : α), x ∈ l → x ∈ s} n f
⊢ False
[PROOFSTEP]
have hnil : ∀ n, f n ≠ List.nil := fun n con => hf1.2 n n.succ n.lt_succ_self (con.symm ▸ List.SublistForall₂.nil)
[GOAL]
case inr.intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r✝ r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : PartiallyWellOrderedOn s r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ (x : α), x ∈ l → x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ (x : α), x ∈ l → x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
⊢ False
[PROOFSTEP]
have : ∀ n, (f n).headI ∈ s
[GOAL]
case this
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r✝ r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : PartiallyWellOrderedOn s r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ (x : α), x ∈ l → x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ (x : α), x ∈ l → x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
⊢ ∀ (n : ℕ), List.headI (f n) ∈ s
[PROOFSTEP]
exact fun n => hf1.1 n _ (List.head!_mem_self (hnil n))
[GOAL]
case inr.intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r✝ r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : PartiallyWellOrderedOn s r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ (x : α), x ∈ l → x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ (x : α), x ∈ l → x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
this : ∀ (n : ℕ), List.headI (f n) ∈ s
⊢ False
[PROOFSTEP]
obtain ⟨g, hg⟩ := h.exists_monotone_subseq (fun n => (f n).headI) this
[GOAL]
case inr.intro.intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r✝ r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : PartiallyWellOrderedOn s r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ (x : α), x ∈ l → x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ (x : α), x ∈ l → x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
this : ∀ (n : ℕ), List.headI (f n) ∈ s
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (List.headI (f (↑g m))) (List.headI (f (↑g n)))
⊢ False
[PROOFSTEP]
have hf' := hf2 (g 0) (fun n => if n < g 0 then f n else List.tail (f (g (n - g 0)))) (fun m hm => (if_pos hm).symm) ?_
[GOAL]
case inr.intro.intro.intro.refine_2
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r✝ r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : PartiallyWellOrderedOn s r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ (x : α), x ∈ l → x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ (x : α), x ∈ l → x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
this : ∀ (n : ℕ), List.headI (f n) ∈ s
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (List.headI (f (↑g m))) (List.headI (f (↑g n)))
hf' :
  ¬IsBadSeq (List.SublistForall₂ r) {l | ∀ (x : α), x ∈ l → x ∈ s} fun n =>
      if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0)))
⊢ False
case inr.intro.intro.intro.refine_1
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r✝ r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : PartiallyWellOrderedOn s r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ (x : α), x ∈ l → x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ (x : α), x ∈ l → x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
this : ∀ (n : ℕ), List.headI (f n) ∈ s
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (List.headI (f (↑g m))) (List.headI (f (↑g n)))
⊢ List.length ((fun n => if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0)))) (↑g 0)) < List.length (f (↑g 0))
[PROOFSTEP]
swap
[GOAL]
case inr.intro.intro.intro.refine_1
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r✝ r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : PartiallyWellOrderedOn s r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ (x : α), x ∈ l → x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ (x : α), x ∈ l → x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
this : ∀ (n : ℕ), List.headI (f n) ∈ s
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (List.headI (f (↑g m))) (List.headI (f (↑g n)))
⊢ List.length ((fun n => if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0)))) (↑g 0)) < List.length (f (↑g 0))
[PROOFSTEP]
simp only [if_neg (lt_irrefl (g 0)), tsub_self]
[GOAL]
case inr.intro.intro.intro.refine_1
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r✝ r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : PartiallyWellOrderedOn s r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ (x : α), x ∈ l → x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ (x : α), x ∈ l → x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
this : ∀ (n : ℕ), List.headI (f n) ∈ s
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (List.headI (f (↑g m))) (List.headI (f (↑g n)))
⊢ List.length (List.tail (f (↑g 0))) < List.length (f (↑g 0))
[PROOFSTEP]
rw [List.length_tail, ← Nat.pred_eq_sub_one]
[GOAL]
case inr.intro.intro.intro.refine_1
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r✝ r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : PartiallyWellOrderedOn s r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ (x : α), x ∈ l → x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ (x : α), x ∈ l → x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
this : ∀ (n : ℕ), List.headI (f n) ∈ s
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (List.headI (f (↑g m))) (List.headI (f (↑g n)))
⊢ Nat.pred (List.length (f (↑g 0))) < List.length (f (↑g 0))
[PROOFSTEP]
exact Nat.pred_lt fun con => hnil _ (List.length_eq_zero.1 con)
[GOAL]
case inr.intro.intro.intro.refine_2
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r✝ r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : PartiallyWellOrderedOn s r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ (x : α), x ∈ l → x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ (x : α), x ∈ l → x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
this : ∀ (n : ℕ), List.headI (f n) ∈ s
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (List.headI (f (↑g m))) (List.headI (f (↑g n)))
hf' :
  ¬IsBadSeq (List.SublistForall₂ r) {l | ∀ (x : α), x ∈ l → x ∈ s} fun n =>
      if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0)))
⊢ False
[PROOFSTEP]
rw [IsBadSeq] at hf' 
[GOAL]
case inr.intro.intro.intro.refine_2
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r✝ r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : PartiallyWellOrderedOn s r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ (x : α), x ∈ l → x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ (x : α), x ∈ l → x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
this : ∀ (n : ℕ), List.headI (f n) ∈ s
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (List.headI (f (↑g m))) (List.headI (f (↑g n)))
hf' :
  ¬((∀ (n : ℕ), (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0)))) ∈ {l | ∀ (x : α), x ∈ l → x ∈ s}) ∧
      ∀ (m n : ℕ),
        m < n →
          ¬List.SublistForall₂ r (if m < ↑g 0 then f m else List.tail (f (↑g (m - ↑g 0))))
              (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0)))))
⊢ False
[PROOFSTEP]
push_neg at hf' 
[GOAL]
case inr.intro.intro.intro.refine_2
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r✝ r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : PartiallyWellOrderedOn s r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ (x : α), x ∈ l → x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ (x : α), x ∈ l → x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
this : ∀ (n : ℕ), List.headI (f n) ∈ s
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (List.headI (f (↑g m))) (List.headI (f (↑g n)))
hf' :
  (∀ (n : ℕ), (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0)))) ∈ {l | ∀ (x : α), x ∈ l → x ∈ s}) →
    ∃ m n,
      m < n ∧
        List.SublistForall₂ r (if m < ↑g 0 then f m else List.tail (f (↑g (m - ↑g 0))))
          (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0))))
⊢ False
[PROOFSTEP]
obtain ⟨m, n, mn, hmn⟩ :=
  hf' <| fun n x hx => by
    split_ifs at hx  with hn
    exacts [hf1.1 _ _ hx, hf1.1 _ _ (List.tail_subset _ hx)]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r✝ r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : PartiallyWellOrderedOn s r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ (x : α), x ∈ l → x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ (x : α), x ∈ l → x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
this : ∀ (n : ℕ), List.headI (f n) ∈ s
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (List.headI (f (↑g m))) (List.headI (f (↑g n)))
hf' :
  (∀ (n : ℕ), (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0)))) ∈ {l | ∀ (x : α), x ∈ l → x ∈ s}) →
    ∃ m n,
      m < n ∧
        List.SublistForall₂ r (if m < ↑g 0 then f m else List.tail (f (↑g (m - ↑g 0))))
          (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0))))
n : ℕ
x : α
hx : x ∈ if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0)))
⊢ x ∈ s
[PROOFSTEP]
split_ifs at hx  with hn
[GOAL]
case pos
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r✝ r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : PartiallyWellOrderedOn s r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ (x : α), x ∈ l → x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ (x : α), x ∈ l → x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
this : ∀ (n : ℕ), List.headI (f n) ∈ s
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (List.headI (f (↑g m))) (List.headI (f (↑g n)))
hf' :
  (∀ (n : ℕ), (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0)))) ∈ {l | ∀ (x : α), x ∈ l → x ∈ s}) →
    ∃ m n,
      m < n ∧
        List.SublistForall₂ r (if m < ↑g 0 then f m else List.tail (f (↑g (m - ↑g 0))))
          (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0))))
n : ℕ
x : α
hn : n < ↑g 0
hx : x ∈ f n
⊢ x ∈ s
case neg
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r✝ r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : PartiallyWellOrderedOn s r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ (x : α), x ∈ l → x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ (x : α), x ∈ l → x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
this : ∀ (n : ℕ), List.headI (f n) ∈ s
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (List.headI (f (↑g m))) (List.headI (f (↑g n)))
hf' :
  (∀ (n : ℕ), (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0)))) ∈ {l | ∀ (x : α), x ∈ l → x ∈ s}) →
    ∃ m n,
      m < n ∧
        List.SublistForall₂ r (if m < ↑g 0 then f m else List.tail (f (↑g (m - ↑g 0))))
          (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0))))
n : ℕ
x : α
hn : ¬n < ↑g 0
hx : x ∈ List.tail (f (↑g (n - ↑g 0)))
⊢ x ∈ s
[PROOFSTEP]
exacts [hf1.1 _ _ hx, hf1.1 _ _ (List.tail_subset _ hx)]
[GOAL]
case inr.intro.intro.intro.refine_2.intro.intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r✝ r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : PartiallyWellOrderedOn s r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ (x : α), x ∈ l → x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ (x : α), x ∈ l → x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
this : ∀ (n : ℕ), List.headI (f n) ∈ s
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (List.headI (f (↑g m))) (List.headI (f (↑g n)))
hf' :
  (∀ (n : ℕ), (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0)))) ∈ {l | ∀ (x : α), x ∈ l → x ∈ s}) →
    ∃ m n,
      m < n ∧
        List.SublistForall₂ r (if m < ↑g 0 then f m else List.tail (f (↑g (m - ↑g 0))))
          (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0))))
m n : ℕ
mn : m < n
hmn :
  List.SublistForall₂ r (if m < ↑g 0 then f m else List.tail (f (↑g (m - ↑g 0))))
    (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0))))
⊢ False
[PROOFSTEP]
by_cases hn : n < g 0
[GOAL]
case pos
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r✝ r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : PartiallyWellOrderedOn s r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ (x : α), x ∈ l → x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ (x : α), x ∈ l → x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
this : ∀ (n : ℕ), List.headI (f n) ∈ s
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (List.headI (f (↑g m))) (List.headI (f (↑g n)))
hf' :
  (∀ (n : ℕ), (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0)))) ∈ {l | ∀ (x : α), x ∈ l → x ∈ s}) →
    ∃ m n,
      m < n ∧
        List.SublistForall₂ r (if m < ↑g 0 then f m else List.tail (f (↑g (m - ↑g 0))))
          (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0))))
m n : ℕ
mn : m < n
hmn :
  List.SublistForall₂ r (if m < ↑g 0 then f m else List.tail (f (↑g (m - ↑g 0))))
    (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0))))
hn : n < ↑g 0
⊢ False
[PROOFSTEP]
apply hf1.2 m n mn
[GOAL]
case pos
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r✝ r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : PartiallyWellOrderedOn s r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ (x : α), x ∈ l → x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ (x : α), x ∈ l → x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
this : ∀ (n : ℕ), List.headI (f n) ∈ s
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (List.headI (f (↑g m))) (List.headI (f (↑g n)))
hf' :
  (∀ (n : ℕ), (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0)))) ∈ {l | ∀ (x : α), x ∈ l → x ∈ s}) →
    ∃ m n,
      m < n ∧
        List.SublistForall₂ r (if m < ↑g 0 then f m else List.tail (f (↑g (m - ↑g 0))))
          (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0))))
m n : ℕ
mn : m < n
hmn :
  List.SublistForall₂ r (if m < ↑g 0 then f m else List.tail (f (↑g (m - ↑g 0))))
    (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0))))
hn : n < ↑g 0
⊢ List.SublistForall₂ r (f m) (f n)
[PROOFSTEP]
rwa [if_pos hn, if_pos (mn.trans hn)] at hmn 
[GOAL]
case neg
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r✝ r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : PartiallyWellOrderedOn s r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ (x : α), x ∈ l → x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ (x : α), x ∈ l → x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
this : ∀ (n : ℕ), List.headI (f n) ∈ s
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (List.headI (f (↑g m))) (List.headI (f (↑g n)))
hf' :
  (∀ (n : ℕ), (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0)))) ∈ {l | ∀ (x : α), x ∈ l → x ∈ s}) →
    ∃ m n,
      m < n ∧
        List.SublistForall₂ r (if m < ↑g 0 then f m else List.tail (f (↑g (m - ↑g 0))))
          (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0))))
m n : ℕ
mn : m < n
hmn :
  List.SublistForall₂ r (if m < ↑g 0 then f m else List.tail (f (↑g (m - ↑g 0))))
    (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0))))
hn : ¬n < ↑g 0
⊢ False
[PROOFSTEP]
obtain ⟨n', rfl⟩ := exists_add_of_le (not_lt.1 hn)
[GOAL]
case neg.intro
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r✝ r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : PartiallyWellOrderedOn s r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ (x : α), x ∈ l → x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ (x : α), x ∈ l → x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
this : ∀ (n : ℕ), List.headI (f n) ∈ s
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (List.headI (f (↑g m))) (List.headI (f (↑g n)))
hf' :
  (∀ (n : ℕ), (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0)))) ∈ {l | ∀ (x : α), x ∈ l → x ∈ s}) →
    ∃ m n,
      m < n ∧
        List.SublistForall₂ r (if m < ↑g 0 then f m else List.tail (f (↑g (m - ↑g 0))))
          (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0))))
m n' : ℕ
mn : m < ↑g 0 + n'
hmn :
  List.SublistForall₂ r (if m < ↑g 0 then f m else List.tail (f (↑g (m - ↑g 0))))
    (if ↑g 0 + n' < ↑g 0 then f (↑g 0 + n') else List.tail (f (↑g (↑g 0 + n' - ↑g 0))))
hn : ¬↑g 0 + n' < ↑g 0
⊢ False
[PROOFSTEP]
rw [if_neg hn, add_comm (g 0) n', add_tsub_cancel_right] at hmn 
[GOAL]
case neg.intro
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r✝ r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : PartiallyWellOrderedOn s r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ (x : α), x ∈ l → x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ (x : α), x ∈ l → x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
this : ∀ (n : ℕ), List.headI (f n) ∈ s
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (List.headI (f (↑g m))) (List.headI (f (↑g n)))
hf' :
  (∀ (n : ℕ), (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0)))) ∈ {l | ∀ (x : α), x ∈ l → x ∈ s}) →
    ∃ m n,
      m < n ∧
        List.SublistForall₂ r (if m < ↑g 0 then f m else List.tail (f (↑g (m - ↑g 0))))
          (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0))))
m n' : ℕ
mn : m < ↑g 0 + n'
hmn : List.SublistForall₂ r (if m < ↑g 0 then f m else List.tail (f (↑g (m - ↑g 0)))) (List.tail (f (↑g n')))
hn : ¬↑g 0 + n' < ↑g 0
⊢ False
[PROOFSTEP]
split_ifs at hmn  with hm
[GOAL]
case pos
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r✝ r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : PartiallyWellOrderedOn s r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ (x : α), x ∈ l → x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ (x : α), x ∈ l → x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
this : ∀ (n : ℕ), List.headI (f n) ∈ s
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (List.headI (f (↑g m))) (List.headI (f (↑g n)))
hf' :
  (∀ (n : ℕ), (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0)))) ∈ {l | ∀ (x : α), x ∈ l → x ∈ s}) →
    ∃ m n,
      m < n ∧
        List.SublistForall₂ r (if m < ↑g 0 then f m else List.tail (f (↑g (m - ↑g 0))))
          (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0))))
m n' : ℕ
mn : m < ↑g 0 + n'
hn : ¬↑g 0 + n' < ↑g 0
hm : m < ↑g 0
hmn : List.SublistForall₂ r (f m) (List.tail (f (↑g n')))
⊢ False
[PROOFSTEP]
apply hf1.2 m (g n') (lt_of_lt_of_le hm (g.monotone n'.zero_le))
[GOAL]
case pos
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r✝ r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : PartiallyWellOrderedOn s r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ (x : α), x ∈ l → x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ (x : α), x ∈ l → x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
this : ∀ (n : ℕ), List.headI (f n) ∈ s
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (List.headI (f (↑g m))) (List.headI (f (↑g n)))
hf' :
  (∀ (n : ℕ), (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0)))) ∈ {l | ∀ (x : α), x ∈ l → x ∈ s}) →
    ∃ m n,
      m < n ∧
        List.SublistForall₂ r (if m < ↑g 0 then f m else List.tail (f (↑g (m - ↑g 0))))
          (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0))))
m n' : ℕ
mn : m < ↑g 0 + n'
hn : ¬↑g 0 + n' < ↑g 0
hm : m < ↑g 0
hmn : List.SublistForall₂ r (f m) (List.tail (f (↑g n')))
⊢ List.SublistForall₂ r (f m) (f (↑g n'))
[PROOFSTEP]
exact _root_.trans hmn (List.tail_sublistForall₂_self _)
[GOAL]
case neg
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r✝ r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : PartiallyWellOrderedOn s r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ (x : α), x ∈ l → x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ (x : α), x ∈ l → x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
this : ∀ (n : ℕ), List.headI (f n) ∈ s
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (List.headI (f (↑g m))) (List.headI (f (↑g n)))
hf' :
  (∀ (n : ℕ), (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0)))) ∈ {l | ∀ (x : α), x ∈ l → x ∈ s}) →
    ∃ m n,
      m < n ∧
        List.SublistForall₂ r (if m < ↑g 0 then f m else List.tail (f (↑g (m - ↑g 0))))
          (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0))))
m n' : ℕ
mn : m < ↑g 0 + n'
hn : ¬↑g 0 + n' < ↑g 0
hm : ¬m < ↑g 0
hmn : List.SublistForall₂ r (List.tail (f (↑g (m - ↑g 0)))) (List.tail (f (↑g n')))
⊢ False
[PROOFSTEP]
rw [← tsub_lt_iff_left (le_of_not_lt hm)] at mn 
[GOAL]
case neg
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r✝ r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : PartiallyWellOrderedOn s r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ (x : α), x ∈ l → x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ (x : α), x ∈ l → x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
this : ∀ (n : ℕ), List.headI (f n) ∈ s
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (List.headI (f (↑g m))) (List.headI (f (↑g n)))
hf' :
  (∀ (n : ℕ), (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0)))) ∈ {l | ∀ (x : α), x ∈ l → x ∈ s}) →
    ∃ m n,
      m < n ∧
        List.SublistForall₂ r (if m < ↑g 0 then f m else List.tail (f (↑g (m - ↑g 0))))
          (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0))))
m n' : ℕ
mn : m - ↑g 0 < n'
hn : ¬↑g 0 + n' < ↑g 0
hm : ¬m < ↑g 0
hmn : List.SublistForall₂ r (List.tail (f (↑g (m - ↑g 0)))) (List.tail (f (↑g n')))
⊢ False
[PROOFSTEP]
apply hf1.2 _ _ (g.lt_iff_lt.2 mn)
[GOAL]
case neg
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r✝ r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : PartiallyWellOrderedOn s r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ (x : α), x ∈ l → x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ (x : α), x ∈ l → x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
this : ∀ (n : ℕ), List.headI (f n) ∈ s
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (List.headI (f (↑g m))) (List.headI (f (↑g n)))
hf' :
  (∀ (n : ℕ), (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0)))) ∈ {l | ∀ (x : α), x ∈ l → x ∈ s}) →
    ∃ m n,
      m < n ∧
        List.SublistForall₂ r (if m < ↑g 0 then f m else List.tail (f (↑g (m - ↑g 0))))
          (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0))))
m n' : ℕ
mn : m - ↑g 0 < n'
hn : ¬↑g 0 + n' < ↑g 0
hm : ¬m < ↑g 0
hmn : List.SublistForall₂ r (List.tail (f (↑g (m - ↑g 0)))) (List.tail (f (↑g n')))
⊢ List.SublistForall₂ r (f (↑g (m - ↑g 0))) (f (↑g n'))
[PROOFSTEP]
rw [← List.cons_head!_tail (hnil (g (m - g 0))), ← List.cons_head!_tail (hnil (g n'))]
[GOAL]
case neg
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r✝ r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : PartiallyWellOrderedOn s r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ (x : α), x ∈ l → x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ (x : α), x ∈ l → x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
this : ∀ (n : ℕ), List.headI (f n) ∈ s
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (List.headI (f (↑g m))) (List.headI (f (↑g n)))
hf' :
  (∀ (n : ℕ), (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0)))) ∈ {l | ∀ (x : α), x ∈ l → x ∈ s}) →
    ∃ m n,
      m < n ∧
        List.SublistForall₂ r (if m < ↑g 0 then f m else List.tail (f (↑g (m - ↑g 0))))
          (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0))))
m n' : ℕ
mn : m - ↑g 0 < n'
hn : ¬↑g 0 + n' < ↑g 0
hm : ¬m < ↑g 0
hmn : List.SublistForall₂ r (List.tail (f (↑g (m - ↑g 0)))) (List.tail (f (↑g n')))
⊢ List.SublistForall₂ r (List.head! (f (↑g (m - ↑g 0))) :: List.tail (f (↑g (m - ↑g 0))))
    (List.head! (f (↑g n')) :: List.tail (f (↑g n')))
[PROOFSTEP]
exact List.SublistForall₂.cons (hg _ _ (le_of_lt mn)) hmn
[GOAL]
ι : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
α : ι → Type u_6
inst✝² : (i : ι) → LinearOrder (α i)
inst✝¹ : ∀ (i : ι), IsWellOrder (α i) fun x x_1 => x < x_1
inst✝ : Finite ι
s : Set ((i : ι) → α i)
⊢ IsPwo s
[PROOFSTEP]
cases nonempty_fintype ι
[GOAL]
case intro
ι : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
α : ι → Type u_6
inst✝² : (i : ι) → LinearOrder (α i)
inst✝¹ : ∀ (i : ι), IsWellOrder (α i) fun x x_1 => x < x_1
inst✝ : Finite ι
s : Set ((i : ι) → α i)
val✝ : Fintype ι
⊢ IsPwo s
[PROOFSTEP]
suffices ∀ (s : Finset ι) (f : ℕ → ∀ s, α s), ∃ g : ℕ ↪o ℕ, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ x, x ∈ s → (f ∘ g) a x ≤ (f ∘ g) b x
  by
  refine isPwo_iff_exists_monotone_subseq.2 fun f _ => ?_
  simpa only [Finset.mem_univ, true_imp_iff] using this Finset.univ f
[GOAL]
ι : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
α : ι → Type u_6
inst✝² : (i : ι) → LinearOrder (α i)
inst✝¹ : ∀ (i : ι), IsWellOrder (α i) fun x x_1 => x < x_1
inst✝ : Finite ι
s : Set ((i : ι) → α i)
val✝ : Fintype ι
this :
  ∀ (s : Finset ι) (f : ℕ → (s : ι) → α s), ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ (x : ι), x ∈ s → (f ∘ ↑g) a x ≤ (f ∘ ↑g) b x
⊢ IsPwo s
[PROOFSTEP]
refine isPwo_iff_exists_monotone_subseq.2 fun f _ => ?_
[GOAL]
ι : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
α : ι → Type u_6
inst✝² : (i : ι) → LinearOrder (α i)
inst✝¹ : ∀ (i : ι), IsWellOrder (α i) fun x x_1 => x < x_1
inst✝ : Finite ι
s : Set ((i : ι) → α i)
val✝ : Fintype ι
this :
  ∀ (s : Finset ι) (f : ℕ → (s : ι) → α s), ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ (x : ι), x ∈ s → (f ∘ ↑g) a x ≤ (f ∘ ↑g) b x
f : ℕ → (i : ι) → α i
x✝ : ∀ (n : ℕ), f n ∈ s
⊢ ∃ g, Monotone (f ∘ ↑g)
[PROOFSTEP]
simpa only [Finset.mem_univ, true_imp_iff] using this Finset.univ f
[GOAL]
case intro
ι : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
α : ι → Type u_6
inst✝² : (i : ι) → LinearOrder (α i)
inst✝¹ : ∀ (i : ι), IsWellOrder (α i) fun x x_1 => x < x_1
inst✝ : Finite ι
s : Set ((i : ι) → α i)
val✝ : Fintype ι
⊢ ∀ (s : Finset ι) (f : ℕ → (s : ι) → α s), ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ (x : ι), x ∈ s → (f ∘ ↑g) a x ≤ (f ∘ ↑g) b x
[PROOFSTEP]
refine' Finset.cons_induction _ _
[GOAL]
case intro.refine'_1
ι : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
α : ι → Type u_6
inst✝² : (i : ι) → LinearOrder (α i)
inst✝¹ : ∀ (i : ι), IsWellOrder (α i) fun x x_1 => x < x_1
inst✝ : Finite ι
s : Set ((i : ι) → α i)
val✝ : Fintype ι
⊢ ∀ (f : ℕ → (s : ι) → α s), ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ (x : ι), x ∈ ∅ → (f ∘ ↑g) a x ≤ (f ∘ ↑g) b x
[PROOFSTEP]
intro f
[GOAL]
case intro.refine'_1
ι : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
α : ι → Type u_6
inst✝² : (i : ι) → LinearOrder (α i)
inst✝¹ : ∀ (i : ι), IsWellOrder (α i) fun x x_1 => x < x_1
inst✝ : Finite ι
s : Set ((i : ι) → α i)
val✝ : Fintype ι
f : ℕ → (s : ι) → α s
⊢ ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ (x : ι), x ∈ ∅ → (f ∘ ↑g) a x ≤ (f ∘ ↑g) b x
[PROOFSTEP]
exists RelEmbedding.refl (· ≤ ·)
[GOAL]
case intro.refine'_1
ι : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
α : ι → Type u_6
inst✝² : (i : ι) → LinearOrder (α i)
inst✝¹ : ∀ (i : ι), IsWellOrder (α i) fun x x_1 => x < x_1
inst✝ : Finite ι
s : Set ((i : ι) → α i)
val✝ : Fintype ι
f : ℕ → (s : ι) → α s
⊢ ∀ ⦃a b : ℕ⦄,
    a ≤ b →
      ∀ (x : ι),
        x ∈ ∅ →
          (f ∘ ↑(RelEmbedding.refl fun x x_1 => x ≤ x_1)) a x ≤ (f ∘ ↑(RelEmbedding.refl fun x x_1 => x ≤ x_1)) b x
[PROOFSTEP]
simp only [IsEmpty.forall_iff, imp_true_iff, forall_const, Finset.not_mem_empty]
[GOAL]
case intro.refine'_2
ι : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
α : ι → Type u_6
inst✝² : (i : ι) → LinearOrder (α i)
inst✝¹ : ∀ (i : ι), IsWellOrder (α i) fun x x_1 => x < x_1
inst✝ : Finite ι
s : Set ((i : ι) → α i)
val✝ : Fintype ι
⊢ ∀ ⦃a : ι⦄ {s : Finset ι} (h : ¬a ∈ s),
    (∀ (f : ℕ → (s : ι) → α s), ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ (x : ι), x ∈ s → (f ∘ ↑g) a x ≤ (f ∘ ↑g) b x) →
      ∀ (f : ℕ → (s : ι) → α s),
        ∃ g, ∀ ⦃a_2 b : ℕ⦄, a_2 ≤ b → ∀ (x : ι), x ∈ Finset.cons a s h → (f ∘ ↑g) a_2 x ≤ (f ∘ ↑g) b x
[PROOFSTEP]
intro x s hx ih f
[GOAL]
case intro.refine'_2
ι : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
α : ι → Type u_6
inst✝² : (i : ι) → LinearOrder (α i)
inst✝¹ : ∀ (i : ι), IsWellOrder (α i) fun x x_1 => x < x_1
inst✝ : Finite ι
s✝ : Set ((i : ι) → α i)
val✝ : Fintype ι
x : ι
s : Finset ι
hx : ¬x ∈ s
ih : ∀ (f : ℕ → (s : ι) → α s), ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ (x : ι), x ∈ s → (f ∘ ↑g) a x ≤ (f ∘ ↑g) b x
f : ℕ → (s : ι) → α s
⊢ ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ (x_1 : ι), x_1 ∈ Finset.cons x s hx → (f ∘ ↑g) a x_1 ≤ (f ∘ ↑g) b x_1
[PROOFSTEP]
obtain ⟨g, hg⟩ := (IsWellFounded.wf.isWf univ).isPwo.exists_monotone_subseq (fun n => f n x) mem_univ
[GOAL]
case intro.refine'_2.intro
ι : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
α : ι → Type u_6
inst✝² : (i : ι) → LinearOrder (α i)
inst✝¹ : ∀ (i : ι), IsWellOrder (α i) fun x x_1 => x < x_1
inst✝ : Finite ι
s✝ : Set ((i : ι) → α i)
val✝ : Fintype ι
x : ι
s : Finset ι
hx : ¬x ∈ s
ih : ∀ (f : ℕ → (s : ι) → α s), ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ (x : ι), x ∈ s → (f ∘ ↑g) a x ≤ (f ∘ ↑g) b x
f : ℕ → (s : ι) → α s
g : ℕ ↪o ℕ
hg : Monotone ((fun n => f n x) ∘ ↑g)
⊢ ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ (x_1 : ι), x_1 ∈ Finset.cons x s hx → (f ∘ ↑g) a x_1 ≤ (f ∘ ↑g) b x_1
[PROOFSTEP]
obtain ⟨g', hg'⟩ := ih (f ∘ g)
[GOAL]
case intro.refine'_2.intro.intro
ι : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
α : ι → Type u_6
inst✝² : (i : ι) → LinearOrder (α i)
inst✝¹ : ∀ (i : ι), IsWellOrder (α i) fun x x_1 => x < x_1
inst✝ : Finite ι
s✝ : Set ((i : ι) → α i)
val✝ : Fintype ι
x : ι
s : Finset ι
hx : ¬x ∈ s
ih : ∀ (f : ℕ → (s : ι) → α s), ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ (x : ι), x ∈ s → (f ∘ ↑g) a x ≤ (f ∘ ↑g) b x
f : ℕ → (s : ι) → α s
g : ℕ ↪o ℕ
hg : Monotone ((fun n => f n x) ∘ ↑g)
g' : ℕ ↪o ℕ
hg' : ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ (x : ι), x ∈ s → ((f ∘ ↑g) ∘ ↑g') a x ≤ ((f ∘ ↑g) ∘ ↑g') b x
⊢ ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ (x_1 : ι), x_1 ∈ Finset.cons x s hx → (f ∘ ↑g) a x_1 ≤ (f ∘ ↑g) b x_1
[PROOFSTEP]
refine' ⟨g'.trans g, fun a b hab => (Finset.forall_mem_cons _ _).2 _⟩
[GOAL]
case intro.refine'_2.intro.intro
ι : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
α : ι → Type u_6
inst✝² : (i : ι) → LinearOrder (α i)
inst✝¹ : ∀ (i : ι), IsWellOrder (α i) fun x x_1 => x < x_1
inst✝ : Finite ι
s✝ : Set ((i : ι) → α i)
val✝ : Fintype ι
x : ι
s : Finset ι
hx : ¬x ∈ s
ih : ∀ (f : ℕ → (s : ι) → α s), ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ (x : ι), x ∈ s → (f ∘ ↑g) a x ≤ (f ∘ ↑g) b x
f : ℕ → (s : ι) → α s
g : ℕ ↪o ℕ
hg : Monotone ((fun n => f n x) ∘ ↑g)
g' : ℕ ↪o ℕ
hg' : ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ (x : ι), x ∈ s → ((f ∘ ↑g) ∘ ↑g') a x ≤ ((f ∘ ↑g) ∘ ↑g') b x
a b : ℕ
hab : a ≤ b
⊢ (f ∘ ↑(RelEmbedding.trans g' g)) a x ≤ (f ∘ ↑(RelEmbedding.trans g' g)) b x ∧
    ∀ (x : ι), x ∈ s → (f ∘ ↑(RelEmbedding.trans g' g)) a x ≤ (f ∘ ↑(RelEmbedding.trans g' g)) b x
[PROOFSTEP]
exact ⟨hg (OrderHomClass.mono g' hab), hg' hab⟩
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
rα : α → α → Prop
rβ : β → β → Prop
f : γ → α
g : γ → β
s : Set γ
hα : WellFounded (rα on f)
hβ : ∀ (a : α), WellFoundedOn (f ⁻¹' {a}) (rβ on g)
⊢ WellFounded (Prod.Lex rα rβ on fun c => (f c, g c))
[PROOFSTEP]
refine' (PSigma.lex_wf (wellFoundedOn_range.2 hα) fun a => hβ a).onFun.mono fun c c' h => _
[GOAL]
case refine'_1
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
rα : α → α → Prop
rβ : β → β → Prop
f : γ → α
g : γ → β
s : Set γ
hα : WellFounded (rα on f)
hβ : ∀ (a : α), WellFoundedOn (f ⁻¹' {a}) (rβ on g)
⊢ γ → (a : ↑(range f)) ×' ↑(f ⁻¹' {↑a})
case refine'_2
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
rα : α → α → Prop
rβ : β → β → Prop
f : γ → α
g : γ → β
s : Set γ
hα : WellFounded (rα on f)
hβ : ∀ (a : α), WellFoundedOn (f ⁻¹' {a}) (rβ on g)
c c' : γ
h : (Prod.Lex rα rβ on fun c => (f c, g c)) c c'
⊢ ((PSigma.Lex (fun a b => rα ↑a ↑b) fun a a_1 b => (rβ on g) ↑a_1 ↑b) on ?refine'_1) c c'
[PROOFSTEP]
exact fun c => ⟨⟨_, c, rfl⟩, c, rfl⟩
[GOAL]
case refine'_2
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
rα : α → α → Prop
rβ : β → β → Prop
f : γ → α
g : γ → β
s : Set γ
hα : WellFounded (rα on f)
hβ : ∀ (a : α), WellFoundedOn (f ⁻¹' {a}) (rβ on g)
c c' : γ
h : (Prod.Lex rα rβ on fun c => (f c, g c)) c c'
⊢ ((PSigma.Lex (fun a b => rα ↑a ↑b) fun a a_1 b => (rβ on g) ↑a_1 ↑b) on fun c =>
      { fst := { val := f c, property := (_ : ∃ y, f y = f c) }, snd := { val := c, property := (_ : f c = f c) } })
    c c'
[PROOFSTEP]
obtain h' | h' := Prod.lex_iff.1 h
[GOAL]
case refine'_2.inl
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
rα : α → α → Prop
rβ : β → β → Prop
f : γ → α
g : γ → β
s : Set γ
hα : WellFounded (rα on f)
hβ : ∀ (a : α), WellFoundedOn (f ⁻¹' {a}) (rβ on g)
c c' : γ
h : (Prod.Lex rα rβ on fun c => (f c, g c)) c c'
h' : rα ((fun c => (f c, g c)) c).fst ((fun c => (f c, g c)) c').fst
⊢ ((PSigma.Lex (fun a b => rα ↑a ↑b) fun a a_1 b => (rβ on g) ↑a_1 ↑b) on fun c =>
      { fst := { val := f c, property := (_ : ∃ y, f y = f c) }, snd := { val := c, property := (_ : f c = f c) } })
    c c'
[PROOFSTEP]
exact PSigma.Lex.left _ _ h'
[GOAL]
case refine'_2.inr
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
rα : α → α → Prop
rβ : β → β → Prop
f : γ → α
g : γ → β
s : Set γ
hα : WellFounded (rα on f)
hβ : ∀ (a : α), WellFoundedOn (f ⁻¹' {a}) (rβ on g)
c c' : γ
h : (Prod.Lex rα rβ on fun c => (f c, g c)) c c'
h' :
  ((fun c => (f c, g c)) c).fst = ((fun c => (f c, g c)) c').fst ∧
    rβ ((fun c => (f c, g c)) c).snd ((fun c => (f c, g c)) c').snd
⊢ ((PSigma.Lex (fun a b => rα ↑a ↑b) fun a a_1 b => (rβ on g) ↑a_1 ↑b) on fun c =>
      { fst := { val := f c, property := (_ : ∃ y, f y = f c) }, snd := { val := c, property := (_ : f c = f c) } })
    c c'
[PROOFSTEP]
dsimp only [InvImage, (· on ·)] at h' ⊢
[GOAL]
case refine'_2.inr
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
rα : α → α → Prop
rβ : β → β → Prop
f : γ → α
g : γ → β
s : Set γ
hα : WellFounded (rα on f)
hβ : ∀ (a : α), WellFoundedOn (f ⁻¹' {a}) (rβ on g)
c c' : γ
h : (Prod.Lex rα rβ on fun c => (f c, g c)) c c'
h' : f c = f c' ∧ rβ (g c) (g c')
⊢ PSigma.Lex (fun a b => rα ↑a ↑b) (fun a a_1 b => rβ (g ↑a_1) (g ↑b))
    { fst := { val := f c, property := (_ : ∃ y, f y = f c) }, snd := { val := c, property := (_ : f c = f c) } }
    { fst := { val := f c', property := (_ : ∃ y, f y = f c') }, snd := { val := c', property := (_ : f c' = f c') } }
[PROOFSTEP]
convert PSigma.Lex.right (⟨_, c', rfl⟩ : range f) _ using 1
[GOAL]
case h.e'_5.h
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
rα : α → α → Prop
rβ : β → β → Prop
f : γ → α
g : γ → β
s : Set γ
hα : WellFounded (rα on f)
hβ : ∀ (a : α), WellFoundedOn (f ⁻¹' {a}) (rβ on g)
c c' : γ
h : (Prod.Lex rα rβ on fun c => (f c, g c)) c c'
h' : f c = f c' ∧ rβ (g c) (g c')
⊢ { fst := { val := f c, property := (_ : ∃ y, f y = f c) }, snd := { val := c, property := (_ : f c = f c) } } =
    { fst := { val := f c', property := (_ : ∃ y, f y = f c') }, snd := ?refine'_2.inr.convert_4 }
case refine'_2.inr.convert_4
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
rα : α → α → Prop
rβ : β → β → Prop
f : γ → α
g : γ → β
s : Set γ
hα : WellFounded (rα on f)
hβ : ∀ (a : α), WellFoundedOn (f ⁻¹' {a}) (rβ on g)
c c' : γ
h : (Prod.Lex rα rβ on fun c => (f c, g c)) c c'
h' : f c = f c' ∧ rβ (g c) (g c')
⊢ ↑(f ⁻¹' {↑{ val := f c', property := (_ : ∃ y, f y = f c') }})
case refine'_2.inr.convert_6
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
rα : α → α → Prop
rβ : β → β → Prop
f : γ → α
g : γ → β
s : Set γ
hα : WellFounded (rα on f)
hβ : ∀ (a : α), WellFoundedOn (f ⁻¹' {a}) (rβ on g)
c c' : γ
h : (Prod.Lex rα rβ on fun c => (f c, g c)) c c'
h' : f c = f c' ∧ rβ (g c) (g c')
⊢ rβ (g ↑?refine'_2.inr.convert_4) (g ↑{ val := c', property := (_ : f c' = f c') })
[PROOFSTEP]
swap
[GOAL]
case refine'_2.inr.convert_4
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
rα : α → α → Prop
rβ : β → β → Prop
f : γ → α
g : γ → β
s : Set γ
hα : WellFounded (rα on f)
hβ : ∀ (a : α), WellFoundedOn (f ⁻¹' {a}) (rβ on g)
c c' : γ
h : (Prod.Lex rα rβ on fun c => (f c, g c)) c c'
h' : f c = f c' ∧ rβ (g c) (g c')
⊢ ↑(f ⁻¹' {↑{ val := f c', property := (_ : ∃ y, f y = f c') }})
case h.e'_5.h
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
rα : α → α → Prop
rβ : β → β → Prop
f : γ → α
g : γ → β
s : Set γ
hα : WellFounded (rα on f)
hβ : ∀ (a : α), WellFoundedOn (f ⁻¹' {a}) (rβ on g)
c c' : γ
h : (Prod.Lex rα rβ on fun c => (f c, g c)) c c'
h' : f c = f c' ∧ rβ (g c) (g c')
⊢ { fst := { val := f c, property := (_ : ∃ y, f y = f c) }, snd := { val := c, property := (_ : f c = f c) } } =
    { fst := { val := f c', property := (_ : ∃ y, f y = f c') }, snd := ?refine'_2.inr.convert_4 }
case refine'_2.inr.convert_6
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
rα : α → α → Prop
rβ : β → β → Prop
f : γ → α
g : γ → β
s : Set γ
hα : WellFounded (rα on f)
hβ : ∀ (a : α), WellFoundedOn (f ⁻¹' {a}) (rβ on g)
c c' : γ
h : (Prod.Lex rα rβ on fun c => (f c, g c)) c c'
h' : f c = f c' ∧ rβ (g c) (g c')
⊢ rβ (g ↑?refine'_2.inr.convert_4) (g ↑{ val := c', property := (_ : f c' = f c') })
[PROOFSTEP]
exacts [⟨c, h'.1⟩, PSigma.subtype_ext (Subtype.ext h'.1) rfl, h'.2]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
rα : α → α → Prop
rβ : β → β → Prop
f : γ → α
g : γ → β
s : Set γ
hα : WellFoundedOn s (rα on f)
hβ : ∀ (a : α), WellFoundedOn (s ∩ f ⁻¹' {a}) (rβ on g)
⊢ WellFoundedOn s (Prod.Lex rα rβ on fun c => (f c, g c))
[PROOFSTEP]
refine' WellFounded.prod_lex_of_wellFoundedOn_fiber hα fun a ↦ (hβ a).onFun.mono (fun b c h ↦ _)
[GOAL]
case refine'_1
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
rα : α → α → Prop
rβ : β → β → Prop
f : γ → α
g : γ → β
s : Set γ
hα : WellFoundedOn s (rα on f)
hβ : ∀ (a : α), WellFoundedOn (s ∩ f ⁻¹' {a}) (rβ on g)
a : α
b c : ↑((fun a => f ↑a) ⁻¹' {a})
h : (rβ on fun a => g ↑a) ↑b ↑c
⊢ ((fun a_1 b => (rβ on g) ↑a_1 ↑b) on ?refine'_2 a) b c
case refine'_2
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
rα : α → α → Prop
rβ : β → β → Prop
f : γ → α
g : γ → β
s : Set γ
hα : WellFoundedOn s (rα on f)
hβ : ∀ (a : α), WellFoundedOn (s ∩ f ⁻¹' {a}) (rβ on g)
⊢ (a : α) → ↑((fun a => f ↑a) ⁻¹' {a}) → ↑(s ∩ f ⁻¹' {a})
[PROOFSTEP]
swap
[GOAL]
case refine'_2
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
rα : α → α → Prop
rβ : β → β → Prop
f : γ → α
g : γ → β
s : Set γ
hα : WellFoundedOn s (rα on f)
hβ : ∀ (a : α), WellFoundedOn (s ∩ f ⁻¹' {a}) (rβ on g)
⊢ (a : α) → ↑((fun a => f ↑a) ⁻¹' {a}) → ↑(s ∩ f ⁻¹' {a})
case refine'_1
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
rα : α → α → Prop
rβ : β → β → Prop
f : γ → α
g : γ → β
s : Set γ
hα : WellFoundedOn s (rα on f)
hβ : ∀ (a : α), WellFoundedOn (s ∩ f ⁻¹' {a}) (rβ on g)
a : α
b c : ↑((fun a => f ↑a) ⁻¹' {a})
h : (rβ on fun a => g ↑a) ↑b ↑c
⊢ ((fun a_1 b => (rβ on g) ↑a_1 ↑b) on ?refine'_2 a) b c
[PROOFSTEP]
exact fun _ x => ⟨x, x.1.2, x.2⟩
[GOAL]
case refine'_1
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
rα : α → α → Prop
rβ : β → β → Prop
f : γ → α
g : γ → β
s : Set γ
hα : WellFoundedOn s (rα on f)
hβ : ∀ (a : α), WellFoundedOn (s ∩ f ⁻¹' {a}) (rβ on g)
a : α
b c : ↑((fun a => f ↑a) ⁻¹' {a})
h : (rβ on fun a => g ↑a) ↑b ↑c
⊢ ((fun a_1 b => (rβ on g) ↑a_1 ↑b) on fun x => { val := ↑↑x, property := (_ : ↑↑x ∈ s ∧ ↑↑x ∈ f ⁻¹' {a}) }) b c
[PROOFSTEP]
assumption
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
rι : ι → ι → Prop
rπ : (i : ι) → π i → π i → Prop
f : γ → ι
g : (i : ι) → γ → π i
s : Set γ
hι : WellFounded (rι on f)
hπ : ∀ (i : ι), WellFoundedOn (f ⁻¹' {i}) (rπ i on g i)
⊢ WellFounded (Sigma.Lex rι rπ on fun c => { fst := f c, snd := g (f c) c })
[PROOFSTEP]
refine' (PSigma.lex_wf (wellFoundedOn_range.2 hι) fun a => hπ a).onFun.mono fun c c' h => _
[GOAL]
case refine'_1
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
rι : ι → ι → Prop
rπ : (i : ι) → π i → π i → Prop
f : γ → ι
g : (i : ι) → γ → π i
s : Set γ
hι : WellFounded (rι on f)
hπ : ∀ (i : ι), WellFoundedOn (f ⁻¹' {i}) (rπ i on g i)
⊢ γ → (a : ↑(range f)) ×' ↑(f ⁻¹' {↑a})
case refine'_2
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
rι : ι → ι → Prop
rπ : (i : ι) → π i → π i → Prop
f : γ → ι
g : (i : ι) → γ → π i
s : Set γ
hι : WellFounded (rι on f)
hπ : ∀ (i : ι), WellFoundedOn (f ⁻¹' {i}) (rπ i on g i)
c c' : γ
h : (Sigma.Lex rι rπ on fun c => { fst := f c, snd := g (f c) c }) c c'
⊢ ((PSigma.Lex (fun a b => rι ↑a ↑b) fun a a_1 b => (rπ ↑a on g ↑a) ↑a_1 ↑b) on ?refine'_1) c c'
[PROOFSTEP]
exact fun c => ⟨⟨_, c, rfl⟩, c, rfl⟩
[GOAL]
case refine'_2
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
rι : ι → ι → Prop
rπ : (i : ι) → π i → π i → Prop
f : γ → ι
g : (i : ι) → γ → π i
s : Set γ
hι : WellFounded (rι on f)
hπ : ∀ (i : ι), WellFoundedOn (f ⁻¹' {i}) (rπ i on g i)
c c' : γ
h : (Sigma.Lex rι rπ on fun c => { fst := f c, snd := g (f c) c }) c c'
⊢ ((PSigma.Lex (fun a b => rι ↑a ↑b) fun a a_1 b => (rπ ↑a on g ↑a) ↑a_1 ↑b) on fun c =>
      { fst := { val := f c, property := (_ : ∃ y, f y = f c) }, snd := { val := c, property := (_ : f c = f c) } })
    c c'
[PROOFSTEP]
obtain h' | ⟨h', h''⟩ := Sigma.lex_iff.1 h
[GOAL]
case refine'_2.inl
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
rι : ι → ι → Prop
rπ : (i : ι) → π i → π i → Prop
f : γ → ι
g : (i : ι) → γ → π i
s : Set γ
hι : WellFounded (rι on f)
hπ : ∀ (i : ι), WellFoundedOn (f ⁻¹' {i}) (rπ i on g i)
c c' : γ
h : (Sigma.Lex rι rπ on fun c => { fst := f c, snd := g (f c) c }) c c'
h' : rι ((fun c => { fst := f c, snd := g (f c) c }) c).fst ((fun c => { fst := f c, snd := g (f c) c }) c').fst
⊢ ((PSigma.Lex (fun a b => rι ↑a ↑b) fun a a_1 b => (rπ ↑a on g ↑a) ↑a_1 ↑b) on fun c =>
      { fst := { val := f c, property := (_ : ∃ y, f y = f c) }, snd := { val := c, property := (_ : f c = f c) } })
    c c'
[PROOFSTEP]
exact PSigma.Lex.left _ _ h'
[GOAL]
case refine'_2.inr.intro
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
rι : ι → ι → Prop
rπ : (i : ι) → π i → π i → Prop
f : γ → ι
g : (i : ι) → γ → π i
s : Set γ
hι : WellFounded (rι on f)
hπ : ∀ (i : ι), WellFoundedOn (f ⁻¹' {i}) (rπ i on g i)
c c' : γ
h : (Sigma.Lex rι rπ on fun c => { fst := f c, snd := g (f c) c }) c c'
h' : ((fun c => { fst := f c, snd := g (f c) c }) c).fst = ((fun c => { fst := f c, snd := g (f c) c }) c').fst
h'' :
  rπ ((fun c => { fst := f c, snd := g (f c) c }) c').fst (h' ▸ ((fun c => { fst := f c, snd := g (f c) c }) c).snd)
    ((fun c => { fst := f c, snd := g (f c) c }) c').snd
⊢ ((PSigma.Lex (fun a b => rι ↑a ↑b) fun a a_1 b => (rπ ↑a on g ↑a) ↑a_1 ↑b) on fun c =>
      { fst := { val := f c, property := (_ : ∃ y, f y = f c) }, snd := { val := c, property := (_ : f c = f c) } })
    c c'
[PROOFSTEP]
dsimp only [InvImage, (· on ·)] at h' ⊢
[GOAL]
case refine'_2.inr.intro
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
rι : ι → ι → Prop
rπ : (i : ι) → π i → π i → Prop
f : γ → ι
g : (i : ι) → γ → π i
s : Set γ
hι : WellFounded (rι on f)
hπ : ∀ (i : ι), WellFoundedOn (f ⁻¹' {i}) (rπ i on g i)
c c' : γ
h : (Sigma.Lex rι rπ on fun c => { fst := f c, snd := g (f c) c }) c c'
h' : f c = f c'
h'' :
  rπ ((fun c => { fst := f c, snd := g (f c) c }) c').fst (h' ▸ ((fun c => { fst := f c, snd := g (f c) c }) c).snd)
    ((fun c => { fst := f c, snd := g (f c) c }) c').snd
⊢ PSigma.Lex (fun a b => rι ↑a ↑b) (fun a a_1 b => rπ (↑a) (g ↑a ↑a_1) (g ↑a ↑b))
    { fst := { val := f c, property := (_ : ∃ y, f y = f c) }, snd := { val := c, property := (_ : f c = f c) } }
    { fst := { val := f c', property := (_ : ∃ y, f y = f c') }, snd := { val := c', property := (_ : f c' = f c') } }
[PROOFSTEP]
convert PSigma.Lex.right (⟨_, c', rfl⟩ : range f) _ using 1
[GOAL]
case h.e'_5.h
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
rι : ι → ι → Prop
rπ : (i : ι) → π i → π i → Prop
f : γ → ι
g : (i : ι) → γ → π i
s : Set γ
hι : WellFounded (rι on f)
hπ : ∀ (i : ι), WellFoundedOn (f ⁻¹' {i}) (rπ i on g i)
c c' : γ
h : (Sigma.Lex rι rπ on fun c => { fst := f c, snd := g (f c) c }) c c'
h' : f c = f c'
h'' :
  rπ ((fun c => { fst := f c, snd := g (f c) c }) c').fst (h' ▸ ((fun c => { fst := f c, snd := g (f c) c }) c).snd)
    ((fun c => { fst := f c, snd := g (f c) c }) c').snd
⊢ { fst := { val := f c, property := (_ : ∃ y, f y = f c) }, snd := { val := c, property := (_ : f c = f c) } } =
    { fst := { val := f c', property := (_ : ∃ y, f y = f c') }, snd := ?refine'_2.inr.intro.convert_4 }
case refine'_2.inr.intro.convert_4
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
rι : ι → ι → Prop
rπ : (i : ι) → π i → π i → Prop
f : γ → ι
g : (i : ι) → γ → π i
s : Set γ
hι : WellFounded (rι on f)
hπ : ∀ (i : ι), WellFoundedOn (f ⁻¹' {i}) (rπ i on g i)
c c' : γ
h : (Sigma.Lex rι rπ on fun c => { fst := f c, snd := g (f c) c }) c c'
h' : f c = f c'
h'' :
  rπ ((fun c => { fst := f c, snd := g (f c) c }) c').fst (h' ▸ ((fun c => { fst := f c, snd := g (f c) c }) c).snd)
    ((fun c => { fst := f c, snd := g (f c) c }) c').snd
⊢ ↑(f ⁻¹' {↑{ val := f c', property := (_ : ∃ y, f y = f c') }})
case refine'_2.inr.intro.convert_6
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
rι : ι → ι → Prop
rπ : (i : ι) → π i → π i → Prop
f : γ → ι
g : (i : ι) → γ → π i
s : Set γ
hι : WellFounded (rι on f)
hπ : ∀ (i : ι), WellFoundedOn (f ⁻¹' {i}) (rπ i on g i)
c c' : γ
h : (Sigma.Lex rι rπ on fun c => { fst := f c, snd := g (f c) c }) c c'
h' : f c = f c'
h'' :
  rπ ((fun c => { fst := f c, snd := g (f c) c }) c').fst (h' ▸ ((fun c => { fst := f c, snd := g (f c) c }) c).snd)
    ((fun c => { fst := f c, snd := g (f c) c }) c').snd
⊢ rπ (↑{ val := f c', property := (_ : ∃ y, f y = f c') })
    (g ↑{ val := f c', property := (_ : ∃ y, f y = f c') } ↑?refine'_2.inr.intro.convert_4)
    (g ↑{ val := f c', property := (_ : ∃ y, f y = f c') } ↑{ val := c', property := (_ : f c' = f c') })
[PROOFSTEP]
swap
[GOAL]
case refine'_2.inr.intro.convert_4
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
rι : ι → ι → Prop
rπ : (i : ι) → π i → π i → Prop
f : γ → ι
g : (i : ι) → γ → π i
s : Set γ
hι : WellFounded (rι on f)
hπ : ∀ (i : ι), WellFoundedOn (f ⁻¹' {i}) (rπ i on g i)
c c' : γ
h : (Sigma.Lex rι rπ on fun c => { fst := f c, snd := g (f c) c }) c c'
h' : f c = f c'
h'' :
  rπ ((fun c => { fst := f c, snd := g (f c) c }) c').fst (h' ▸ ((fun c => { fst := f c, snd := g (f c) c }) c).snd)
    ((fun c => { fst := f c, snd := g (f c) c }) c').snd
⊢ ↑(f ⁻¹' {↑{ val := f c', property := (_ : ∃ y, f y = f c') }})
[PROOFSTEP]
exact ⟨c, h'⟩
[GOAL]
case h.e'_5.h
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
rι : ι → ι → Prop
rπ : (i : ι) → π i → π i → Prop
f : γ → ι
g : (i : ι) → γ → π i
s : Set γ
hι : WellFounded (rι on f)
hπ : ∀ (i : ι), WellFoundedOn (f ⁻¹' {i}) (rπ i on g i)
c c' : γ
h : (Sigma.Lex rι rπ on fun c => { fst := f c, snd := g (f c) c }) c c'
h' : f c = f c'
h'' :
  rπ ((fun c => { fst := f c, snd := g (f c) c }) c').fst (h' ▸ ((fun c => { fst := f c, snd := g (f c) c }) c).snd)
    ((fun c => { fst := f c, snd := g (f c) c }) c').snd
⊢ { fst := { val := f c, property := (_ : ∃ y, f y = f c) }, snd := { val := c, property := (_ : f c = f c) } } =
    { fst := { val := f c', property := (_ : ∃ y, f y = f c') }, snd := { val := c, property := h' } }
[PROOFSTEP]
exact PSigma.subtype_ext (Subtype.ext h') rfl
[GOAL]
case refine'_2.inr.intro.convert_6
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
rι : ι → ι → Prop
rπ : (i : ι) → π i → π i → Prop
f : γ → ι
g : (i : ι) → γ → π i
s : Set γ
hι : WellFounded (rι on f)
hπ : ∀ (i : ι), WellFoundedOn (f ⁻¹' {i}) (rπ i on g i)
c c' : γ
h : (Sigma.Lex rι rπ on fun c => { fst := f c, snd := g (f c) c }) c c'
h' : f c = f c'
h'' :
  rπ ((fun c => { fst := f c, snd := g (f c) c }) c').fst (h' ▸ ((fun c => { fst := f c, snd := g (f c) c }) c).snd)
    ((fun c => { fst := f c, snd := g (f c) c }) c').snd
⊢ rπ (↑{ val := f c', property := (_ : ∃ y, f y = f c') })
    (g ↑{ val := f c', property := (_ : ∃ y, f y = f c') } ↑{ val := c, property := h' })
    (g ↑{ val := f c', property := (_ : ∃ y, f y = f c') } ↑{ val := c', property := (_ : f c' = f c') })
[PROOFSTEP]
dsimp only [Subtype.coe_mk] at *
[GOAL]
case refine'_2.inr.intro.convert_6
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
rι : ι → ι → Prop
rπ : (i : ι) → π i → π i → Prop
f : γ → ι
g : (i : ι) → γ → π i
s : Set γ
hι : WellFounded (rι on f)
hπ : ∀ (i : ι), WellFoundedOn (f ⁻¹' {i}) (rπ i on g i)
c c' : γ
h : (Sigma.Lex rι rπ on fun c => { fst := f c, snd := g (f c) c }) c c'
h' : f c = f c'
h'' : rπ (f c') (h' ▸ g (f c) c) (g (f c') c')
⊢ rπ (f c') (g (f c') c) (g (f c') c')
[PROOFSTEP]
revert h'
[GOAL]
case refine'_2.inr.intro.convert_6
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
rι : ι → ι → Prop
rπ : (i : ι) → π i → π i → Prop
f : γ → ι
g : (i : ι) → γ → π i
s : Set γ
hι : WellFounded (rι on f)
hπ : ∀ (i : ι), WellFoundedOn (f ⁻¹' {i}) (rπ i on g i)
c c' : γ
h : (Sigma.Lex rι rπ on fun c => { fst := f c, snd := g (f c) c }) c c'
⊢ ∀ (h' : f c = f c'), rπ (f c') (h' ▸ g (f c) c) (g (f c') c') → rπ (f c') (g (f c') c) (g (f c') c')
[PROOFSTEP]
generalize f c = d
[GOAL]
case refine'_2.inr.intro.convert_6
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
rι : ι → ι → Prop
rπ : (i : ι) → π i → π i → Prop
f : γ → ι
g : (i : ι) → γ → π i
s : Set γ
hι : WellFounded (rι on f)
hπ : ∀ (i : ι), WellFoundedOn (f ⁻¹' {i}) (rπ i on g i)
c c' : γ
h : (Sigma.Lex rι rπ on fun c => { fst := f c, snd := g (f c) c }) c c'
d : ι
⊢ ∀ (h' : d = f c'), rπ (f c') (h' ▸ g d c) (g (f c') c') → rπ (f c') (g (f c') c) (g (f c') c')
[PROOFSTEP]
rintro rfl h''
[GOAL]
case refine'_2.inr.intro.convert_6
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
rι : ι → ι → Prop
rπ : (i : ι) → π i → π i → Prop
f : γ → ι
g : (i : ι) → γ → π i
s : Set γ
hι : WellFounded (rι on f)
hπ : ∀ (i : ι), WellFoundedOn (f ⁻¹' {i}) (rπ i on g i)
c c' : γ
h : (Sigma.Lex rι rπ on fun c => { fst := f c, snd := g (f c) c }) c c'
h'' : rπ (f c') ((_ : f c' = f c') ▸ g (f c') c) (g (f c') c')
⊢ rπ (f c') (g (f c') c) (g (f c') c')
[PROOFSTEP]
exact h''
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
rι : ι → ι → Prop
rπ : (i : ι) → π i → π i → Prop
f : γ → ι
g : (i : ι) → γ → π i
s : Set γ
hι : WellFoundedOn s (rι on f)
hπ : ∀ (i : ι), WellFoundedOn (s ∩ f ⁻¹' {i}) (rπ i on g i)
⊢ WellFoundedOn s (Sigma.Lex rι rπ on fun c => { fst := f c, snd := g (f c) c })
[PROOFSTEP]
show WellFounded (Sigma.Lex rι rπ on fun c : s => ⟨f c, g (f c) c⟩)
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
rι : ι → ι → Prop
rπ : (i : ι) → π i → π i → Prop
f : γ → ι
g : (i : ι) → γ → π i
s : Set γ
hι : WellFoundedOn s (rι on f)
hπ : ∀ (i : ι), WellFoundedOn (s ∩ f ⁻¹' {i}) (rπ i on g i)
⊢ WellFounded (Sigma.Lex rι rπ on fun c => { fst := f ↑c, snd := g (f ↑c) ↑c })
[PROOFSTEP]
refine'
  @WellFounded.sigma_lex_of_wellFoundedOn_fiber _ s _ _ rπ (fun c => f c) (fun i c => g _ c) hι fun i =>
    (hπ i).onFun.mono (fun b c h => _)
[GOAL]
case refine'_1
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
rι : ι → ι → Prop
rπ : (i : ι) → π i → π i → Prop
f : γ → ι
g : (i : ι) → γ → π i
s : Set γ
hι : WellFoundedOn s (rι on f)
hπ : ∀ (i : ι), WellFoundedOn (s ∩ f ⁻¹' {i}) (rπ i on g i)
i : ι
b c : ↑((fun c => f ↑c) ⁻¹' {i})
h : (rπ i on (fun i c => g i ↑c) i) ↑b ↑c
⊢ ((fun a b => (rπ i on g i) ↑a ↑b) on ?refine'_2 i) b c
case refine'_2
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
rι : ι → ι → Prop
rπ : (i : ι) → π i → π i → Prop
f : γ → ι
g : (i : ι) → γ → π i
s : Set γ
hι : WellFoundedOn s (rι on f)
hπ : ∀ (i : ι), WellFoundedOn (s ∩ f ⁻¹' {i}) (rπ i on g i)
⊢ (i : ι) → ↑((fun c => f ↑c) ⁻¹' {i}) → ↑(s ∩ f ⁻¹' {i})
[PROOFSTEP]
swap
[GOAL]
case refine'_2
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
rι : ι → ι → Prop
rπ : (i : ι) → π i → π i → Prop
f : γ → ι
g : (i : ι) → γ → π i
s : Set γ
hι : WellFoundedOn s (rι on f)
hπ : ∀ (i : ι), WellFoundedOn (s ∩ f ⁻¹' {i}) (rπ i on g i)
⊢ (i : ι) → ↑((fun c => f ↑c) ⁻¹' {i}) → ↑(s ∩ f ⁻¹' {i})
case refine'_1
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
rι : ι → ι → Prop
rπ : (i : ι) → π i → π i → Prop
f : γ → ι
g : (i : ι) → γ → π i
s : Set γ
hι : WellFoundedOn s (rι on f)
hπ : ∀ (i : ι), WellFoundedOn (s ∩ f ⁻¹' {i}) (rπ i on g i)
i : ι
b c : ↑((fun c => f ↑c) ⁻¹' {i})
h : (rπ i on (fun i c => g i ↑c) i) ↑b ↑c
⊢ ((fun a b => (rπ i on g i) ↑a ↑b) on ?refine'_2 i) b c
[PROOFSTEP]
exact fun _ x => ⟨x, x.1.2, x.2⟩
[GOAL]
case refine'_1
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
rι : ι → ι → Prop
rπ : (i : ι) → π i → π i → Prop
f : γ → ι
g : (i : ι) → γ → π i
s : Set γ
hι : WellFoundedOn s (rι on f)
hπ : ∀ (i : ι), WellFoundedOn (s ∩ f ⁻¹' {i}) (rπ i on g i)
i : ι
b c : ↑((fun c => f ↑c) ⁻¹' {i})
h : (rπ i on (fun i c => g i ↑c) i) ↑b ↑c
⊢ ((fun a b => (rπ i on g i) ↑a ↑b) on fun x => { val := ↑↑x, property := (_ : ↑↑x ∈ s ∧ ↑↑x ∈ f ⁻¹' {i}) }) b c
[PROOFSTEP]
assumption
