[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
⊢ Monotone (↑toDual ∘ f ∘ ↑ofDual) ↔ Monotone f
[PROOFSTEP]
rw [monotone_toDual_comp_iff, antitone_comp_ofDual_iff]
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
⊢ Antitone (↑toDual ∘ f ∘ ↑ofDual) ↔ Antitone f
[PROOFSTEP]
rw [antitone_toDual_comp_iff, monotone_comp_ofDual_iff]
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
⊢ MonotoneOn (↑toDual ∘ f ∘ ↑ofDual) s ↔ MonotoneOn f s
[PROOFSTEP]
rw [monotoneOn_toDual_comp_iff, antitoneOn_comp_ofDual_iff]
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
⊢ AntitoneOn (↑toDual ∘ f ∘ ↑ofDual) s ↔ AntitoneOn f s
[PROOFSTEP]
rw [antitoneOn_toDual_comp_iff, monotoneOn_comp_ofDual_iff]
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
⊢ StrictMono (↑toDual ∘ f ∘ ↑ofDual) ↔ StrictMono f
[PROOFSTEP]
rw [strictMono_toDual_comp_iff, strictAnti_comp_ofDual_iff]
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
⊢ StrictAnti (↑toDual ∘ f ∘ ↑ofDual) ↔ StrictAnti f
[PROOFSTEP]
rw [strictAnti_toDual_comp_iff, strictMono_comp_ofDual_iff]
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
⊢ StrictMonoOn (↑toDual ∘ f ∘ ↑ofDual) s ↔ StrictMonoOn f s
[PROOFSTEP]
rw [strictMonoOn_toDual_comp_iff, strictAntiOn_comp_ofDual_iff]
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
⊢ StrictAntiOn (↑toDual ∘ f ∘ ↑ofDual) s ↔ StrictAntiOn f s
[PROOFSTEP]
rw [strictAntiOn_toDual_comp_iff, strictMonoOn_comp_ofDual_iff]
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝ : LinearOrder α
f : α → β
h : ∀ (x y : α), x < y → f x ≠ f y
⊢ Injective f
[PROOFSTEP]
intro x y hf
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝ : LinearOrder α
f : α → β
h : ∀ (x y : α), x < y → f x ≠ f y
x y : α
hf : f x = f y
⊢ x = y
[PROOFSTEP]
rcases lt_trichotomy x y with (hxy | rfl | hxy)
[GOAL]
case inl
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝ : LinearOrder α
f : α → β
h : ∀ (x y : α), x < y → f x ≠ f y
x y : α
hf : f x = f y
hxy : x < y
⊢ x = y
[PROOFSTEP]
exact absurd hf <| h _ _ hxy
[GOAL]
case inr.inl
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝ : LinearOrder α
f : α → β
h : ∀ (x y : α), x < y → f x ≠ f y
x : α
hf : f x = f x
⊢ x = x
[PROOFSTEP]
rfl
[GOAL]
case inr.inr
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝ : LinearOrder α
f : α → β
h : ∀ (x y : α), x < y → f x ≠ f y
x y : α
hf : f x = f y
hxy : y < x
⊢ x = y
[PROOFSTEP]
exact absurd hf.symm <| h _ _ hxy
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝² : Preorder α
inst✝¹ : Preorder β
f g : α → β
a : α
hf : StrictMono f
hg : StrictMono g
p : α → Prop
inst✝ : DecidablePred p
hp : ∀ ⦃x y : α⦄, x < y → p y → p x
hfg : ∀ ⦃x y : α⦄, p x → ¬p y → x < y → f x < g y
⊢ StrictMono fun x => if p x then f x else g x
[PROOFSTEP]
intro x y h
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝² : Preorder α
inst✝¹ : Preorder β
f g : α → β
a : α
hf : StrictMono f
hg : StrictMono g
p : α → Prop
inst✝ : DecidablePred p
hp : ∀ ⦃x y : α⦄, x < y → p y → p x
hfg : ∀ ⦃x y : α⦄, p x → ¬p y → x < y → f x < g y
x y : α
h : x < y
⊢ (fun x => if p x then f x else g x) x < (fun x => if p x then f x else g x) y
[PROOFSTEP]
by_cases hy : p y
[GOAL]
case pos
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝² : Preorder α
inst✝¹ : Preorder β
f g : α → β
a : α
hf : StrictMono f
hg : StrictMono g
p : α → Prop
inst✝ : DecidablePred p
hp : ∀ ⦃x y : α⦄, x < y → p y → p x
hfg : ∀ ⦃x y : α⦄, p x → ¬p y → x < y → f x < g y
x y : α
h : x < y
hy : p y
⊢ (fun x => if p x then f x else g x) x < (fun x => if p x then f x else g x) y
[PROOFSTEP]
have hx : p x := hp h hy
[GOAL]
case pos
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝² : Preorder α
inst✝¹ : Preorder β
f g : α → β
a : α
hf : StrictMono f
hg : StrictMono g
p : α → Prop
inst✝ : DecidablePred p
hp : ∀ ⦃x y : α⦄, x < y → p y → p x
hfg : ∀ ⦃x y : α⦄, p x → ¬p y → x < y → f x < g y
x y : α
h : x < y
hy : p y
hx : p x
⊢ (fun x => if p x then f x else g x) x < (fun x => if p x then f x else g x) y
[PROOFSTEP]
simpa [hx, hy] using hf h
[GOAL]
case neg
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝² : Preorder α
inst✝¹ : Preorder β
f g : α → β
a : α
hf : StrictMono f
hg : StrictMono g
p : α → Prop
inst✝ : DecidablePred p
hp : ∀ ⦃x y : α⦄, x < y → p y → p x
hfg : ∀ ⦃x y : α⦄, p x → ¬p y → x < y → f x < g y
x y : α
h : x < y
hy : ¬p y
⊢ (fun x => if p x then f x else g x) x < (fun x => if p x then f x else g x) y
[PROOFSTEP]
by_cases hx : p x
[GOAL]
case pos
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝² : Preorder α
inst✝¹ : Preorder β
f g : α → β
a : α
hf : StrictMono f
hg : StrictMono g
p : α → Prop
inst✝ : DecidablePred p
hp : ∀ ⦃x y : α⦄, x < y → p y → p x
hfg : ∀ ⦃x y : α⦄, p x → ¬p y → x < y → f x < g y
x y : α
h : x < y
hy : ¬p y
hx : p x
⊢ (fun x => if p x then f x else g x) x < (fun x => if p x then f x else g x) y
[PROOFSTEP]
simpa [hx, hy] using hfg hx hy h
[GOAL]
case neg
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝² : Preorder α
inst✝¹ : Preorder β
f g : α → β
a : α
hf : StrictMono f
hg : StrictMono g
p : α → Prop
inst✝ : DecidablePred p
hp : ∀ ⦃x y : α⦄, x < y → p y → p x
hfg : ∀ ⦃x y : α⦄, p x → ¬p y → x < y → f x < g y
x y : α
h : x < y
hy : ¬p y
hx : ¬p x
⊢ (fun x => if p x then f x else g x) x < (fun x => if p x then f x else g x) y
[PROOFSTEP]
simpa [hx, hy] using hg h
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
s : Set α
hf : StrictMonoOn f s
a b : α
ha : a ∈ s
hb : b ∈ s
⊢ a = b → f a = f b
[PROOFSTEP]
rintro rfl
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
s : Set α
hf : StrictMonoOn f s
a : α
ha hb : a ∈ s
⊢ f a = f a
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
s : Set α
hf : StrictMonoOn f s
a b : α
ha : a ∈ s
hb : b ∈ s
⊢ f a < f b ↔ a < b
[PROOFSTEP]
rw [lt_iff_le_not_le, lt_iff_le_not_le, hf.le_iff_le ha hb, hf.le_iff_le hb ha]
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y : α
⊢ ¬Monotone f ∧ ¬Antitone f ↔ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
[PROOFSTEP]
simp_rw [Monotone, Antitone, not_forall, not_le]
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y : α
⊢ ((∃ x x_1 h, f x_1 < f x) ∧ ∃ x x_1 h, f x < f x_1) ↔
    ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
[PROOFSTEP]
refine' Iff.symm ⟨_, _⟩
[GOAL]
case refine'_1
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y : α
⊢ (∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)) →
    (∃ x x_1 h, f x_1 < f x) ∧ ∃ x x_1 h, f x < f x_1
case refine'_2
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y : α
⊢ ((∃ x x_1 h, f x_1 < f x) ∧ ∃ x x_1 h, f x < f x_1) →
    ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
[PROOFSTEP]
{ rintro ⟨a, b, c, hab, hbc, ⟨hfab, hfcb⟩ | ⟨hfba, hfbc⟩⟩
  exacts [⟨⟨_, _, hbc, hfcb⟩, _, _, hab, hfab⟩, ⟨⟨_, _, hab, hfba⟩, _, _, hbc, hfbc⟩]
}
[GOAL]
case refine'_1
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y : α
⊢ (∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)) →
    (∃ x x_1 h, f x_1 < f x) ∧ ∃ x x_1 h, f x < f x_1
[PROOFSTEP]
rintro ⟨a, b, c, hab, hbc, ⟨hfab, hfcb⟩ | ⟨hfba, hfbc⟩⟩
[GOAL]
case refine'_1.intro.intro.intro.intro.intro.inl.intro
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y a b c : α
hab : a ≤ b
hbc : b ≤ c
hfab : f a < f b
hfcb : f c < f b
⊢ (∃ x x_1 h, f x_1 < f x) ∧ ∃ x x_1 h, f x < f x_1
case refine'_1.intro.intro.intro.intro.intro.inr.intro
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y a b c : α
hab : a ≤ b
hbc : b ≤ c
hfba : f b < f a
hfbc : f b < f c
⊢ (∃ x x_1 h, f x_1 < f x) ∧ ∃ x x_1 h, f x < f x_1
[PROOFSTEP]
exacts [⟨⟨_, _, hbc, hfcb⟩, _, _, hab, hfab⟩, ⟨⟨_, _, hab, hfba⟩, _, _, hbc, hfbc⟩]
[GOAL]
case refine'_2
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y : α
⊢ ((∃ x x_1 h, f x_1 < f x) ∧ ∃ x x_1 h, f x < f x_1) →
    ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
[PROOFSTEP]
rintro ⟨⟨a, b, hab, hfba⟩, c, d, hcd, hfcd⟩
[GOAL]
case refine'_2.intro.intro.intro.intro.intro.intro.intro
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
[PROOFSTEP]
obtain hda | had := le_total d a
[GOAL]
case refine'_2.intro.intro.intro.intro.intro.intro.intro.inl
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
hda : d ≤ a
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
case refine'_2.intro.intro.intro.intro.intro.intro.intro.inr
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
had : a ≤ d
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
[PROOFSTEP]
{ obtain hfad | hfda := le_total (f a) (f d)
  {exact ⟨c, d, b, hcd, hda.trans hab, Or.inl ⟨hfcd, hfba.trans_le hfad⟩⟩
  }
  {exact ⟨c, a, b, hcd.trans hda, hab, Or.inl ⟨hfcd.trans_le hfda, hfba⟩⟩
  }
}
[GOAL]
case refine'_2.intro.intro.intro.intro.intro.intro.intro.inl
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
hda : d ≤ a
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
[PROOFSTEP]
obtain hfad | hfda := le_total (f a) (f d)
[GOAL]
case refine'_2.intro.intro.intro.intro.intro.intro.intro.inl.inl
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
hda : d ≤ a
hfad : f a ≤ f d
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
case refine'_2.intro.intro.intro.intro.intro.intro.intro.inl.inr
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
hda : d ≤ a
hfda : f d ≤ f a
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
[PROOFSTEP]
{exact ⟨c, d, b, hcd, hda.trans hab, Or.inl ⟨hfcd, hfba.trans_le hfad⟩⟩
}
[GOAL]
case refine'_2.intro.intro.intro.intro.intro.intro.intro.inl.inl
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
hda : d ≤ a
hfad : f a ≤ f d
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
[PROOFSTEP]
exact ⟨c, d, b, hcd, hda.trans hab, Or.inl ⟨hfcd, hfba.trans_le hfad⟩⟩
[GOAL]
case refine'_2.intro.intro.intro.intro.intro.intro.intro.inl.inr
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
hda : d ≤ a
hfda : f d ≤ f a
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
[PROOFSTEP]
{exact ⟨c, a, b, hcd.trans hda, hab, Or.inl ⟨hfcd.trans_le hfda, hfba⟩⟩
}
[GOAL]
case refine'_2.intro.intro.intro.intro.intro.intro.intro.inl.inr
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
hda : d ≤ a
hfda : f d ≤ f a
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
[PROOFSTEP]
exact ⟨c, a, b, hcd.trans hda, hab, Or.inl ⟨hfcd.trans_le hfda, hfba⟩⟩
[GOAL]
case refine'_2.intro.intro.intro.intro.intro.intro.intro.inr
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
had : a ≤ d
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
[PROOFSTEP]
obtain hac | hca := le_total a c
[GOAL]
case refine'_2.intro.intro.intro.intro.intro.intro.intro.inr.inl
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
had : a ≤ d
hac : a ≤ c
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
case refine'_2.intro.intro.intro.intro.intro.intro.intro.inr.inr
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
had : a ≤ d
hca : c ≤ a
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
[PROOFSTEP]
{ obtain hfdb | hfbd := le_or_lt (f d) (f b)
  {exact ⟨a, c, d, hac, hcd, Or.inr ⟨hfcd.trans $ hfdb.trans_lt hfba, hfcd⟩⟩
  }
  obtain hfca | hfac := lt_or_le (f c) (f a)
  {exact ⟨a, c, d, hac, hcd, Or.inr ⟨hfca, hfcd⟩⟩
  }
  obtain hbd | hdb := le_total b d
  {exact ⟨a, b, d, hab, hbd, Or.inr ⟨hfba, hfbd⟩⟩
  }
  {exact ⟨a, d, b, had, hdb, Or.inl ⟨hfac.trans_lt hfcd, hfbd⟩⟩
  }
}
[GOAL]
case refine'_2.intro.intro.intro.intro.intro.intro.intro.inr.inl
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
had : a ≤ d
hac : a ≤ c
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
[PROOFSTEP]
obtain hfdb | hfbd := le_or_lt (f d) (f b)
[GOAL]
case refine'_2.intro.intro.intro.intro.intro.intro.intro.inr.inl.inl
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
had : a ≤ d
hac : a ≤ c
hfdb : f d ≤ f b
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
case refine'_2.intro.intro.intro.intro.intro.intro.intro.inr.inl.inr
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
had : a ≤ d
hac : a ≤ c
hfbd : f b < f d
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
[PROOFSTEP]
{exact ⟨a, c, d, hac, hcd, Or.inr ⟨hfcd.trans $ hfdb.trans_lt hfba, hfcd⟩⟩
}
[GOAL]
case refine'_2.intro.intro.intro.intro.intro.intro.intro.inr.inl.inl
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
had : a ≤ d
hac : a ≤ c
hfdb : f d ≤ f b
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
[PROOFSTEP]
exact ⟨a, c, d, hac, hcd, Or.inr ⟨hfcd.trans $ hfdb.trans_lt hfba, hfcd⟩⟩
[GOAL]
case refine'_2.intro.intro.intro.intro.intro.intro.intro.inr.inl.inr
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
had : a ≤ d
hac : a ≤ c
hfbd : f b < f d
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
[PROOFSTEP]
obtain hfca | hfac := lt_or_le (f c) (f a)
[GOAL]
case refine'_2.intro.intro.intro.intro.intro.intro.intro.inr.inl.inr.inl
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
had : a ≤ d
hac : a ≤ c
hfbd : f b < f d
hfca : f c < f a
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
case refine'_2.intro.intro.intro.intro.intro.intro.intro.inr.inl.inr.inr
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
had : a ≤ d
hac : a ≤ c
hfbd : f b < f d
hfac : f a ≤ f c
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
[PROOFSTEP]
{exact ⟨a, c, d, hac, hcd, Or.inr ⟨hfca, hfcd⟩⟩
}
[GOAL]
case refine'_2.intro.intro.intro.intro.intro.intro.intro.inr.inl.inr.inl
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
had : a ≤ d
hac : a ≤ c
hfbd : f b < f d
hfca : f c < f a
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
[PROOFSTEP]
exact ⟨a, c, d, hac, hcd, Or.inr ⟨hfca, hfcd⟩⟩
[GOAL]
case refine'_2.intro.intro.intro.intro.intro.intro.intro.inr.inl.inr.inr
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
had : a ≤ d
hac : a ≤ c
hfbd : f b < f d
hfac : f a ≤ f c
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
[PROOFSTEP]
obtain hbd | hdb := le_total b d
[GOAL]
case refine'_2.intro.intro.intro.intro.intro.intro.intro.inr.inl.inr.inr.inl
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
had : a ≤ d
hac : a ≤ c
hfbd : f b < f d
hfac : f a ≤ f c
hbd : b ≤ d
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
case refine'_2.intro.intro.intro.intro.intro.intro.intro.inr.inl.inr.inr.inr
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
had : a ≤ d
hac : a ≤ c
hfbd : f b < f d
hfac : f a ≤ f c
hdb : d ≤ b
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
[PROOFSTEP]
{exact ⟨a, b, d, hab, hbd, Or.inr ⟨hfba, hfbd⟩⟩
}
[GOAL]
case refine'_2.intro.intro.intro.intro.intro.intro.intro.inr.inl.inr.inr.inl
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
had : a ≤ d
hac : a ≤ c
hfbd : f b < f d
hfac : f a ≤ f c
hbd : b ≤ d
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
[PROOFSTEP]
exact ⟨a, b, d, hab, hbd, Or.inr ⟨hfba, hfbd⟩⟩
[GOAL]
case refine'_2.intro.intro.intro.intro.intro.intro.intro.inr.inl.inr.inr.inr
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
had : a ≤ d
hac : a ≤ c
hfbd : f b < f d
hfac : f a ≤ f c
hdb : d ≤ b
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
[PROOFSTEP]
{exact ⟨a, d, b, had, hdb, Or.inl ⟨hfac.trans_lt hfcd, hfbd⟩⟩
}
[GOAL]
case refine'_2.intro.intro.intro.intro.intro.intro.intro.inr.inl.inr.inr.inr
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
had : a ≤ d
hac : a ≤ c
hfbd : f b < f d
hfac : f a ≤ f c
hdb : d ≤ b
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
[PROOFSTEP]
exact ⟨a, d, b, had, hdb, Or.inl ⟨hfac.trans_lt hfcd, hfbd⟩⟩
[GOAL]
case refine'_2.intro.intro.intro.intro.intro.intro.intro.inr.inr
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
had : a ≤ d
hca : c ≤ a
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
[PROOFSTEP]
{ obtain hfdb | hfbd := le_or_lt (f d) (f b)
  {exact ⟨c, a, b, hca, hab, Or.inl ⟨hfcd.trans $ hfdb.trans_lt hfba, hfba⟩⟩
  }
  obtain hfca | hfac := lt_or_le (f c) (f a)
  {exact ⟨c, a, b, hca, hab, Or.inl ⟨hfca, hfba⟩⟩
  }
  obtain hbd | hdb := le_total b d
  {exact ⟨a, b, d, hab, hbd, Or.inr ⟨hfba, hfbd⟩⟩
  }
  {exact ⟨a, d, b, had, hdb, Or.inl ⟨hfac.trans_lt hfcd, hfbd⟩⟩
  }
}
[GOAL]
case refine'_2.intro.intro.intro.intro.intro.intro.intro.inr.inr
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
had : a ≤ d
hca : c ≤ a
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
[PROOFSTEP]
obtain hfdb | hfbd := le_or_lt (f d) (f b)
[GOAL]
case refine'_2.intro.intro.intro.intro.intro.intro.intro.inr.inr.inl
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
had : a ≤ d
hca : c ≤ a
hfdb : f d ≤ f b
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
case refine'_2.intro.intro.intro.intro.intro.intro.intro.inr.inr.inr
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
had : a ≤ d
hca : c ≤ a
hfbd : f b < f d
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
[PROOFSTEP]
{exact ⟨c, a, b, hca, hab, Or.inl ⟨hfcd.trans $ hfdb.trans_lt hfba, hfba⟩⟩
}
[GOAL]
case refine'_2.intro.intro.intro.intro.intro.intro.intro.inr.inr.inl
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
had : a ≤ d
hca : c ≤ a
hfdb : f d ≤ f b
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
[PROOFSTEP]
exact ⟨c, a, b, hca, hab, Or.inl ⟨hfcd.trans $ hfdb.trans_lt hfba, hfba⟩⟩
[GOAL]
case refine'_2.intro.intro.intro.intro.intro.intro.intro.inr.inr.inr
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
had : a ≤ d
hca : c ≤ a
hfbd : f b < f d
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
[PROOFSTEP]
obtain hfca | hfac := lt_or_le (f c) (f a)
[GOAL]
case refine'_2.intro.intro.intro.intro.intro.intro.intro.inr.inr.inr.inl
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
had : a ≤ d
hca : c ≤ a
hfbd : f b < f d
hfca : f c < f a
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
case refine'_2.intro.intro.intro.intro.intro.intro.intro.inr.inr.inr.inr
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
had : a ≤ d
hca : c ≤ a
hfbd : f b < f d
hfac : f a ≤ f c
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
[PROOFSTEP]
{exact ⟨c, a, b, hca, hab, Or.inl ⟨hfca, hfba⟩⟩
}
[GOAL]
case refine'_2.intro.intro.intro.intro.intro.intro.intro.inr.inr.inr.inl
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
had : a ≤ d
hca : c ≤ a
hfbd : f b < f d
hfca : f c < f a
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
[PROOFSTEP]
exact ⟨c, a, b, hca, hab, Or.inl ⟨hfca, hfba⟩⟩
[GOAL]
case refine'_2.intro.intro.intro.intro.intro.intro.intro.inr.inr.inr.inr
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
had : a ≤ d
hca : c ≤ a
hfbd : f b < f d
hfac : f a ≤ f c
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
[PROOFSTEP]
obtain hbd | hdb := le_total b d
[GOAL]
case refine'_2.intro.intro.intro.intro.intro.intro.intro.inr.inr.inr.inr.inl
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
had : a ≤ d
hca : c ≤ a
hfbd : f b < f d
hfac : f a ≤ f c
hbd : b ≤ d
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
case refine'_2.intro.intro.intro.intro.intro.intro.intro.inr.inr.inr.inr.inr
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
had : a ≤ d
hca : c ≤ a
hfbd : f b < f d
hfac : f a ≤ f c
hdb : d ≤ b
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
[PROOFSTEP]
{exact ⟨a, b, d, hab, hbd, Or.inr ⟨hfba, hfbd⟩⟩
}
[GOAL]
case refine'_2.intro.intro.intro.intro.intro.intro.intro.inr.inr.inr.inr.inl
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
had : a ≤ d
hca : c ≤ a
hfbd : f b < f d
hfac : f a ≤ f c
hbd : b ≤ d
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
[PROOFSTEP]
exact ⟨a, b, d, hab, hbd, Or.inr ⟨hfba, hfbd⟩⟩
[GOAL]
case refine'_2.intro.intro.intro.intro.intro.intro.intro.inr.inr.inr.inr.inr
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
had : a ≤ d
hca : c ≤ a
hfbd : f b < f d
hfac : f a ≤ f c
hdb : d ≤ b
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
[PROOFSTEP]
{exact ⟨a, d, b, had, hdb, Or.inl ⟨hfac.trans_lt hfcd, hfbd⟩⟩
}
[GOAL]
case refine'_2.intro.intro.intro.intro.intro.intro.intro.inr.inr.inr.inr.inr
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
had : a ≤ d
hca : c ≤ a
hfbd : f b < f d
hfac : f a ≤ f c
hdb : d ≤ b
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
[PROOFSTEP]
exact ⟨a, d, b, had, hdb, Or.inl ⟨hfac.trans_lt hfcd, hfbd⟩⟩
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y : α
⊢ ¬Monotone f ∧ ¬Antitone f ↔ ∃ a b c, a < b ∧ b < c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
[PROOFSTEP]
simp_rw [not_monotone_not_antitone_iff_exists_le_le, ← and_assoc]
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y : α
⊢ (∃ a b c, (a ≤ b ∧ b ≤ c) ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)) ↔
    ∃ a b c, (a < b ∧ b < c) ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
[PROOFSTEP]
refine' exists₃_congr (fun a b c ↦ and_congr_left $ fun h ↦ (Ne.le_iff_lt _).and $ Ne.le_iff_lt _)
[GOAL]
case refine'_1
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y a b c : α
h : f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c
⊢ a ≠ b
[PROOFSTEP]
rintro rfl
[GOAL]
case refine'_1
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y a c : α
h : f a < f a ∧ f c < f a ∨ f a < f a ∧ f a < f c
⊢ False
[PROOFSTEP]
simp at h 
[GOAL]
case refine'_2
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y a b c : α
h : f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c
⊢ b ≠ c
[PROOFSTEP]
rintro rfl
[GOAL]
case refine'_2
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
x y a b : α
h : f a < f b ∧ f b < f b ∨ f b < f a ∧ f b < f b
⊢ False
[PROOFSTEP]
simp at h 
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r✝ : α → α → Prop
inst✝¹ : Preorder α
r : β → β → Prop
inst✝ : IsTrans β r
f : ℕ → β
a : ℕ
h : ∀ (n : ℕ), a ≤ n → r (f n) (f (n + 1))
b c : ℕ
hab : a ≤ b
hbc : b < c
⊢ r (f b) (f c)
[PROOFSTEP]
induction' hbc with k b_lt_k r_b_k
[GOAL]
case refl
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r✝ : α → α → Prop
inst✝¹ : Preorder α
r : β → β → Prop
inst✝ : IsTrans β r
f : ℕ → β
a : ℕ
h : ∀ (n : ℕ), a ≤ n → r (f n) (f (n + 1))
b c : ℕ
hab : a ≤ b
⊢ r (f b) (f (succ b))
case step
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r✝ : α → α → Prop
inst✝¹ : Preorder α
r : β → β → Prop
inst✝ : IsTrans β r
f : ℕ → β
a : ℕ
h : ∀ (n : ℕ), a ≤ n → r (f n) (f (n + 1))
b c : ℕ
hab : a ≤ b
k : ℕ
b_lt_k : Nat.le (succ b) k
r_b_k : r (f b) (f k)
⊢ r (f b) (f (succ k))
[PROOFSTEP]
exacts [h _ hab, _root_.trans r_b_k (h _ (hab.trans_lt b_lt_k).le)]
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
a : α
⊢ ∃ f, StrictMono f ∧ f 0 = a
[PROOFSTEP]
choose g hg using fun x : α ↦ exists_gt x
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
a : α
g : α → α
hg : ∀ (x : α), x < g x
⊢ ∃ f, StrictMono f ∧ f 0 = a
[PROOFSTEP]
exact ⟨fun n ↦ Nat.recOn n a fun _ ↦ g, strictMono_nat_of_lt_succ fun n ↦ hg _, rfl⟩
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r✝ : α → α → Prop
inst✝¹ : Preorder α
r : β → β → Prop
inst✝ : IsTrans β r
f : ℤ → β
h : ∀ (n : ℤ), r (f n) (f (n + 1))
a b : ℤ
hab : a < b
⊢ r (f a) (f b)
[PROOFSTEP]
rcases lt.dest hab with ⟨n, rfl⟩
[GOAL]
case intro
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r✝ : α → α → Prop
inst✝¹ : Preorder α
r : β → β → Prop
inst✝ : IsTrans β r
f : ℤ → β
h : ∀ (n : ℤ), r (f n) (f (n + 1))
a : ℤ
n : ℕ
hab : a < a + ↑(Nat.succ n)
⊢ r (f a) (f (a + ↑(Nat.succ n)))
[PROOFSTEP]
clear hab
[GOAL]
case intro
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r✝ : α → α → Prop
inst✝¹ : Preorder α
r : β → β → Prop
inst✝ : IsTrans β r
f : ℤ → β
h : ∀ (n : ℤ), r (f n) (f (n + 1))
a : ℤ
n : ℕ
⊢ r (f a) (f (a + ↑(Nat.succ n)))
[PROOFSTEP]
induction' n with n ihn
[GOAL]
case intro.zero
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r✝ : α → α → Prop
inst✝¹ : Preorder α
r : β → β → Prop
inst✝ : IsTrans β r
f : ℤ → β
h : ∀ (n : ℤ), r (f n) (f (n + 1))
a : ℤ
⊢ r (f a) (f (a + ↑(Nat.succ Nat.zero)))
[PROOFSTEP]
rw [Int.ofNat_one]
[GOAL]
case intro.zero
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r✝ : α → α → Prop
inst✝¹ : Preorder α
r : β → β → Prop
inst✝ : IsTrans β r
f : ℤ → β
h : ∀ (n : ℤ), r (f n) (f (n + 1))
a : ℤ
⊢ r (f a) (f (a + 1))
[PROOFSTEP]
apply h
[GOAL]
case intro.succ
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r✝ : α → α → Prop
inst✝¹ : Preorder α
r : β → β → Prop
inst✝ : IsTrans β r
f : ℤ → β
h : ∀ (n : ℤ), r (f n) (f (n + 1))
a : ℤ
n : ℕ
ihn : r (f a) (f (a + ↑(Nat.succ n)))
⊢ r (f a) (f (a + ↑(Nat.succ (Nat.succ n))))
[PROOFSTEP]
rw [Int.ofNat_succ, ← Int.add_assoc]
[GOAL]
case intro.succ
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r✝ : α → α → Prop
inst✝¹ : Preorder α
r : β → β → Prop
inst✝ : IsTrans β r
f : ℤ → β
h : ∀ (n : ℤ), r (f n) (f (n + 1))
a : ℤ
n : ℕ
ihn : r (f a) (f (a + ↑(Nat.succ n)))
⊢ r (f a) (f (a + ↑(n + 1) + 1))
[PROOFSTEP]
exact _root_.trans ihn (h _)
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝⁴ inst✝³ : Preorder α
inst✝² : Nonempty α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
⊢ ∃ f, StrictMono f
[PROOFSTEP]
inhabit α
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝⁴ inst✝³ : Preorder α
inst✝² : Nonempty α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
inhabited_h : Inhabited α
⊢ ∃ f, StrictMono f
[PROOFSTEP]
rcases Nat.exists_strictMono' (default : α) with ⟨f, hf, hf₀⟩
[GOAL]
case intro.intro
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝⁴ inst✝³ : Preorder α
inst✝² : Nonempty α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
inhabited_h : Inhabited α
f : ℕ → α
hf : StrictMono f
hf₀ : f 0 = default
⊢ ∃ f, StrictMono f
[PROOFSTEP]
rcases Nat.exists_strictAnti' (default : α) with ⟨g, hg, hg₀⟩
[GOAL]
case intro.intro.intro.intro
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝⁴ inst✝³ : Preorder α
inst✝² : Nonempty α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
inhabited_h : Inhabited α
f : ℕ → α
hf : StrictMono f
hf₀ : f 0 = default
g : ℕ → α
hg : StrictAnti g
hg₀ : g 0 = default
⊢ ∃ f, StrictMono f
[PROOFSTEP]
refine' ⟨fun n ↦ Int.casesOn n f fun n ↦ g (n + 1), strictMono_int_of_lt_succ _⟩
[GOAL]
case intro.intro.intro.intro
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝⁴ inst✝³ : Preorder α
inst✝² : Nonempty α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
inhabited_h : Inhabited α
f : ℕ → α
hf : StrictMono f
hf₀ : f 0 = default
g : ℕ → α
hg : StrictAnti g
hg₀ : g 0 = default
⊢ ∀ (n : ℤ), (Int.casesOn n f fun n => g (n + 1)) < Int.casesOn (n + 1) f fun n => g (n + 1)
[PROOFSTEP]
rintro (n | _ | n)
[GOAL]
case intro.intro.intro.intro.ofNat
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝⁴ inst✝³ : Preorder α
inst✝² : Nonempty α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
inhabited_h : Inhabited α
f : ℕ → α
hf : StrictMono f
hf₀ : f 0 = default
g : ℕ → α
hg : StrictAnti g
hg₀ : g 0 = default
n : ℕ
⊢ (Int.casesOn (ofNat n) f fun n => g (n + 1)) < Int.casesOn (ofNat n + 1) f fun n => g (n + 1)
[PROOFSTEP]
exact hf n.lt_succ_self
[GOAL]
case intro.intro.intro.intro.negSucc.zero
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝⁴ inst✝³ : Preorder α
inst✝² : Nonempty α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
inhabited_h : Inhabited α
f : ℕ → α
hf : StrictMono f
hf₀ : f 0 = default
g : ℕ → α
hg : StrictAnti g
hg₀ : g 0 = default
⊢ (Int.casesOn -[Nat.zero+1] f fun n => g (n + 1)) < Int.casesOn (-[Nat.zero+1] + 1) f fun n => g (n + 1)
[PROOFSTEP]
show g 1 < f 0
[GOAL]
case intro.intro.intro.intro.negSucc.zero
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝⁴ inst✝³ : Preorder α
inst✝² : Nonempty α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
inhabited_h : Inhabited α
f : ℕ → α
hf : StrictMono f
hf₀ : f 0 = default
g : ℕ → α
hg : StrictAnti g
hg₀ : g 0 = default
⊢ g 1 < f 0
[PROOFSTEP]
rw [hf₀, ← hg₀]
[GOAL]
case intro.intro.intro.intro.negSucc.zero
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝⁴ inst✝³ : Preorder α
inst✝² : Nonempty α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
inhabited_h : Inhabited α
f : ℕ → α
hf : StrictMono f
hf₀ : f 0 = default
g : ℕ → α
hg : StrictAnti g
hg₀ : g 0 = default
⊢ g 1 < g 0
[PROOFSTEP]
exact hg Nat.zero_lt_one
[GOAL]
case intro.intro.intro.intro.negSucc.succ
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝⁴ inst✝³ : Preorder α
inst✝² : Nonempty α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
inhabited_h : Inhabited α
f : ℕ → α
hf : StrictMono f
hf₀ : f 0 = default
g : ℕ → α
hg : StrictAnti g
hg₀ : g 0 = default
n : ℕ
⊢ (Int.casesOn -[Nat.succ n+1] f fun n => g (n + 1)) < Int.casesOn (-[Nat.succ n+1] + 1) f fun n => g (n + 1)
[PROOFSTEP]
exact hg (Nat.lt_succ_self _)
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝ : Preorder α
f : ℕ → α
hf : Monotone f
n : ℕ
x : α
h1 : f n < x
h2 : x < f (n + 1)
a : ℕ
⊢ f a ≠ x
[PROOFSTEP]
rintro rfl
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝ : Preorder α
f : ℕ → α
hf : Monotone f
n a : ℕ
h1 : f n < f a
h2 : f a < f (n + 1)
⊢ False
[PROOFSTEP]
exact (hf.reflect_lt h1).not_le (Nat.le_of_lt_succ <| hf.reflect_lt h2)
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝ : Preorder α
f : ℕ → α
hf : Antitone f
n : ℕ
x : α
h1 : f (n + 1) < x
h2 : x < f n
a : ℕ
⊢ f a ≠ x
[PROOFSTEP]
rintro rfl
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝ : Preorder α
f : ℕ → α
hf : Antitone f
n a : ℕ
h1 : f (n + 1) < f a
h2 : f a < f n
⊢ False
[PROOFSTEP]
exact (hf.reflect_lt h2).not_le (Nat.le_of_lt_succ <| hf.reflect_lt h1)
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝ : Preorder α
f : ℤ → α
hf : Monotone f
n : ℤ
x : α
h1 : f n < x
h2 : x < f (n + 1)
a : ℤ
⊢ f a ≠ x
[PROOFSTEP]
rintro rfl
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝ : Preorder α
f : ℤ → α
hf : Monotone f
n a : ℤ
h1 : f n < f a
h2 : f a < f (n + 1)
⊢ False
[PROOFSTEP]
exact (hf.reflect_lt h1).not_le (Int.le_of_lt_add_one <| hf.reflect_lt h2)
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝ : Preorder α
f : ℤ → α
hf : Antitone f
n : ℤ
x : α
h1 : f (n + 1) < x
h2 : x < f n
a : ℤ
⊢ f a ≠ x
[PROOFSTEP]
rintro rfl
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝ : Preorder α
f : ℤ → α
hf : Antitone f
n a : ℤ
h1 : f (n + 1) < f a
h2 : f a < f n
⊢ False
[PROOFSTEP]
exact (hf.reflect_lt h2).not_le (Int.le_of_lt_add_one <| hf.reflect_lt h1)
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : Preorder γ
inst✝ : Preorder δ
f : α → γ
g : β → δ
hf : StrictMono f
hg : StrictMono g
a b : α × β
⊢ a < b → Prod.map f g a < Prod.map f g b
[PROOFSTEP]
simp only [Prod.lt_iff]
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : Preorder γ
inst✝ : Preorder δ
f : α → γ
g : β → δ
hf : StrictMono f
hg : StrictMono g
a b : α × β
⊢ a.fst < b.fst ∧ a.snd ≤ b.snd ∨ a.fst ≤ b.fst ∧ a.snd < b.snd →
    (Prod.map f g a).fst < (Prod.map f g b).fst ∧ (Prod.map f g a).snd ≤ (Prod.map f g b).snd ∨
      (Prod.map f g a).fst ≤ (Prod.map f g b).fst ∧ (Prod.map f g a).snd < (Prod.map f g b).snd
[PROOFSTEP]
exact Or.imp (And.imp hf.imp hg.monotone.imp) (And.imp hf.monotone.imp hg.imp)
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : Preorder γ
inst✝ : Preorder δ
f : α → γ
g : β → δ
hf : StrictAnti f
hg : StrictAnti g
a b : α × β
⊢ a < b → Prod.map f g b < Prod.map f g a
[PROOFSTEP]
simp only [Prod.lt_iff]
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type u_2
π : ι → Type u_3
r : α → α → Prop
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : Preorder γ
inst✝ : Preorder δ
f : α → γ
g : β → δ
hf : StrictAnti f
hg : StrictAnti g
a b : α × β
⊢ a.fst < b.fst ∧ a.snd ≤ b.snd ∨ a.fst ≤ b.fst ∧ a.snd < b.snd →
    (Prod.map f g b).fst < (Prod.map f g a).fst ∧ (Prod.map f g b).snd ≤ (Prod.map f g a).snd ∨
      (Prod.map f g b).fst ≤ (Prod.map f g a).fst ∧ (Prod.map f g b).snd < (Prod.map f g a).snd
[PROOFSTEP]
exact Or.imp (And.imp hf.imp hg.antitone.imp) (And.imp hf.antitone.imp hg.imp)
