ι : Type ?u.81761
α : Type u_1
β : Type ?u.81767
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
ι : Type ?u.81761
α : Type u_1
β : Type ?u.81767
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
refine' ⟨fun h t ht hrt => hrt.finite_of_partiallyWellOrderedOn (h.mono ht), _⟩
ι : Type ?u.81761
α : Type u_1
β : Type ?u.81767
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)
ι : Type ?u.81761
α : Type u_1
β : Type ?u.81767
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
rintro hs f hf
ι : Type ?u.81761
α : Type u_1
β : Type ?u.81767
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
ι : Type ?u.81761
α : Type u_1
β : Type ?u.81767
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)
by_contra' H
case refine'_1
ι : Type ?u.81761
α : Type u_1
β : Type ?u.81767
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

case refine'_2
ι : Type ?u.81761
α : Type u_1
β : Type ?u.81767
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)
ι : Type ?u.81761
α : Type u_1
β : Type ?u.81767
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
refine' infinite_range_of_injective (fun m n hmn => _) (hs _ (range_subset_iff.2 hf) _)
case refine'_2.intro.refl.intro.refl
ι : Type ?u.81761
α : Type u_1
β : Type ?u.81767
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)
case refine'_2
ι : Type ?u.81761
α : Type u_1
β : Type ?u.81767
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)
rintro _ ⟨m, hm, rfl⟩ _ ⟨n, hn, rfl⟩ hmn
case refine'_2.intro.refl.intro.refl.inl
ι : Type ?u.81761
α : Type u_1
β : Type ?u.81767
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)

case refine'_2.intro.refl.intro.refl.inr
ι : Type ?u.81761
α : Type u_1
β : Type ?u.81767
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)
case refine'_2.intro.refl.intro.refl
ι : Type ?u.81761
α : Type u_1
β : Type ?u.81767
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)
obtain h | h := (ne_of_apply_ne _ hmn).lt_or_lt
case refine'_1.inl
ι : Type ?u.81761
α : Type u_1
β : Type ?u.81767
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

case refine'_1.inr.inl
ι : Type ?u.81761
α : Type u_1
β : Type ?u.81767
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

case refine'_1.inr.inr
ι : Type ?u.81761
α : Type u_1
β : Type ?u.81767
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
case refine'_1
ι : Type ?u.81761
α : Type u_1
β : Type ?u.81767
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
obtain h | h | h := lt_trichotomy m n
case refine'_1.inl
ι : Type ?u.81761
α : Type u_1
β : Type ?u.81767
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)
case refine'_1.inl
ι : Type ?u.81761
α : Type u_1
β : Type ?u.81767
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
refine' (H _ _ h _).elim
case refine'_1.inl
ι : Type ?u.81761
α : Type u_1
β : Type ?u.81767
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)
case refine'_1.inl
ι : Type ?u.81761
α : Type u_1
β : Type ?u.81767
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)
rw [hmn]
no goals
case refine'_1.inl
ι : Type ?u.81761
α : Type u_1
β : Type ?u.81767
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)
exact refl _
no goals
case refine'_1.inr.inl
ι : Type ?u.81761
α : Type u_1
β : Type ?u.81767
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
exact h
case refine'_1.inr.inr
ι : Type ?u.81761
α : Type u_1
β : Type ?u.81767
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)
case refine'_1.inr.inr
ι : Type ?u.81761
α : Type u_1
β : Type ?u.81767
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
refine' (H _ _ h _).elim
case refine'_1.inr.inr
ι : Type ?u.81761
α : Type u_1
β : Type ?u.81767
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)
case refine'_1.inr.inr
ι : Type ?u.81761
α : Type u_1
β : Type ?u.81767
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)
rw [hmn]
no goals
case refine'_1.inr.inr
ι : Type ?u.81761
α : Type u_1
β : Type ?u.81767
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)
exact refl _
no goals
case refine'_2.intro.refl.intro.refl.inl
ι : Type ?u.81761
α : Type u_1
β : Type ?u.81767
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)
exact H _ _ h
no goals
case refine'_2.intro.refl.intro.refl.inr
ι : Type ?u.81761
α : Type u_1
β : Type ?u.81767
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)
exact mt symm (H _ _ h)