α✝ : Type ?u.114601
β✝ : Type ?u.114604
γ : Type ?u.114607
ι : Sort ?u.114610
π : α✝ → Type ?u.114615
fa : α✝ → α✝
fb : β✝ → β✝
f : α✝ → β✝
g : β✝ → γ
s✝ t✝ : Set α✝
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LinearOrder β
φ : β → α
ψ : α → β
t : Set β
s : Set α
hφ : MonotoneOn φ t
φψs : RightInvOn ψ φ s
ψts : MapsTo ψ s t
x : α
xs : x ∈ s
y : α
ys : y ∈ s
l : x ≤ y
⊢ ψ x ≤ ψ y
α✝ : Type ?u.114601
β✝ : Type ?u.114604
γ : Type ?u.114607
ι : Sort ?u.114610
π : α✝ → Type ?u.114615
fa : α✝ → α✝
fb : β✝ → β✝
f : α✝ → β✝
g : β✝ → γ
s✝ t✝ : Set α✝
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LinearOrder β
φ : β → α
ψ : α → β
t : Set β
s : Set α
hφ : MonotoneOn φ t
φψs : RightInvOn ψ φ s
ψts : MapsTo ψ s t
⊢ MonotoneOn ψ s
rintro x xs y ys l
case inl
α✝ : Type ?u.114601
β✝ : Type ?u.114604
γ : Type ?u.114607
ι : Sort ?u.114610
π : α✝ → Type ?u.114615
fa : α✝ → α✝
fb : β✝ → β✝
f : α✝ → β✝
g : β✝ → γ
s✝ t✝ : Set α✝
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LinearOrder β
φ : β → α
ψ : α → β
t : Set β
s : Set α
hφ : MonotoneOn φ t
φψs : RightInvOn ψ φ s
ψts : MapsTo ψ s t
x : α
xs : x ∈ s
y : α
ys : y ∈ s
l : x ≤ y
ψxy : ψ x ≤ ψ y
⊢ ψ x ≤ ψ y

case inr
α✝ : Type ?u.114601
β✝ : Type ?u.114604
γ : Type ?u.114607
ι : Sort ?u.114610
π : α✝ → Type ?u.114615
fa : α✝ → α✝
fb : β✝ → β✝
f : α✝ → β✝
g : β✝ → γ
s✝ t✝ : Set α✝
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LinearOrder β
φ : β → α
ψ : α → β
t : Set β
s : Set α
hφ : MonotoneOn φ t
φψs : RightInvOn ψ φ s
ψts : MapsTo ψ s t
x : α
xs : x ∈ s
y : α
ys : y ∈ s
l : x ≤ y
ψyx : ψ y ≤ ψ x
⊢ ψ x ≤ ψ y
α✝ : Type ?u.114601
β✝ : Type ?u.114604
γ : Type ?u.114607
ι : Sort ?u.114610
π : α✝ → Type ?u.114615
fa : α✝ → α✝
fb : β✝ → β✝
f : α✝ → β✝
g : β✝ → γ
s✝ t✝ : Set α✝
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LinearOrder β
φ : β → α
ψ : α → β
t : Set β
s : Set α
hφ : MonotoneOn φ t
φψs : RightInvOn ψ φ s
ψts : MapsTo ψ s t
x : α
xs : x ∈ s
y : α
ys : y ∈ s
l : x ≤ y
⊢ ψ x ≤ ψ y
rcases le_total (ψ x) (ψ y) with (ψxy|ψyx)
no goals
case inl
α✝ : Type ?u.114601
β✝ : Type ?u.114604
γ : Type ?u.114607
ι : Sort ?u.114610
π : α✝ → Type ?u.114615
fa : α✝ → α✝
fb : β✝ → β✝
f : α✝ → β✝
g : β✝ → γ
s✝ t✝ : Set α✝
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LinearOrder β
φ : β → α
ψ : α → β
t : Set β
s : Set α
hφ : MonotoneOn φ t
φψs : RightInvOn ψ φ s
ψts : MapsTo ψ s t
x : α
xs : x ∈ s
y : α
ys : y ∈ s
l : x ≤ y
ψxy : ψ x ≤ ψ y
⊢ ψ x ≤ ψ y
exact ψxy
case inr
α✝ : Type ?u.114601
β✝ : Type ?u.114604
γ : Type ?u.114607
ι : Sort ?u.114610
π : α✝ → Type ?u.114615
fa : α✝ → α✝
fb : β✝ → β✝
f : α✝ → β✝
g : β✝ → γ
s✝ t✝ : Set α✝
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LinearOrder β
φ : β → α
ψ : α → β
t : Set β
s : Set α
hφ : MonotoneOn φ t
φψs : RightInvOn ψ φ s
ψts : MapsTo ψ s t
x : α
xs : x ∈ s
y : α
ys : y ∈ s
l : x ≤ y
ψyx : ψ y ≤ ψ x
this : φ (ψ y) ≤ φ (ψ x)
⊢ ψ x ≤ ψ y
case inr
α✝ : Type ?u.114601
β✝ : Type ?u.114604
γ : Type ?u.114607
ι : Sort ?u.114610
π : α✝ → Type ?u.114615
fa : α✝ → α✝
fb : β✝ → β✝
f : α✝ → β✝
g : β✝ → γ
s✝ t✝ : Set α✝
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LinearOrder β
φ : β → α
ψ : α → β
t : Set β
s : Set α
hφ : MonotoneOn φ t
φψs : RightInvOn ψ φ s
ψts : MapsTo ψ s t
x : α
xs : x ∈ s
y : α
ys : y ∈ s
l : x ≤ y
ψyx : ψ y ≤ ψ x
⊢ ψ x ≤ ψ y
have := hφ (ψts ys) (ψts xs) ψyx
case inr
α✝ : Type ?u.114601
β✝ : Type ?u.114604
γ : Type ?u.114607
ι : Sort ?u.114610
π : α✝ → Type ?u.114615
fa : α✝ → α✝
fb : β✝ → β✝
f : α✝ → β✝
g : β✝ → γ
s✝ t✝ : Set α✝
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LinearOrder β
φ : β → α
ψ : α → β
t : Set β
s : Set α
hφ : MonotoneOn φ t
φψs : RightInvOn ψ φ s
ψts : MapsTo ψ s t
x : α
xs : x ∈ s
y : α
ys : y ∈ s
l : x ≤ y
ψyx : ψ y ≤ ψ x
this : y ≤ x
⊢ ψ x ≤ ψ y
case inr
α✝ : Type ?u.114601
β✝ : Type ?u.114604
γ : Type ?u.114607
ι : Sort ?u.114610
π : α✝ → Type ?u.114615
fa : α✝ → α✝
fb : β✝ → β✝
f : α✝ → β✝
g : β✝ → γ
s✝ t✝ : Set α✝
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LinearOrder β
φ : β → α
ψ : α → β
t : Set β
s : Set α
hφ : MonotoneOn φ t
φψs : RightInvOn ψ φ s
ψts : MapsTo ψ s t
x : α
xs : x ∈ s
y : α
ys : y ∈ s
l : x ≤ y
ψyx : ψ y ≤ ψ x
this : φ (ψ y) ≤ φ (ψ x)
⊢ ψ x ≤ ψ y
rw [φψs.eq ys, φψs.eq xs] at this
case inr.refl
α✝ : Type ?u.114601
β✝ : Type ?u.114604
γ : Type ?u.114607
ι : Sort ?u.114610
π : α✝ → Type ?u.114615
fa : α✝ → α✝
fb : β✝ → β✝
f : α✝ → β✝
g : β✝ → γ
s✝ t✝ : Set α✝
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LinearOrder β
φ : β → α
ψ : α → β
t : Set β
s : Set α
hφ : MonotoneOn φ t
φψs : RightInvOn ψ φ s
ψts : MapsTo ψ s t
x : α
xs : x ∈ s
y : α
ys : x ∈ s
l : x ≤ x
ψyx : ψ x ≤ ψ x
this : x ≤ x
⊢ ψ x ≤ ψ x
case inr
α✝ : Type ?u.114601
β✝ : Type ?u.114604
γ : Type ?u.114607
ι : Sort ?u.114610
π : α✝ → Type ?u.114615
fa : α✝ → α✝
fb : β✝ → β✝
f : α✝ → β✝
g : β✝ → γ
s✝ t✝ : Set α✝
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LinearOrder β
φ : β → α
ψ : α → β
t : Set β
s : Set α
hφ : MonotoneOn φ t
φψs : RightInvOn ψ φ s
ψts : MapsTo ψ s t
x : α
xs : x ∈ s
y : α
ys : y ∈ s
l : x ≤ y
ψyx : ψ y ≤ ψ x
this : y ≤ x
⊢ ψ x ≤ ψ y
induction le_antisymm l this
no goals
case inr.refl
α✝ : Type ?u.114601
β✝ : Type ?u.114604
γ : Type ?u.114607
ι : Sort ?u.114610
π : α✝ → Type ?u.114615
fa : α✝ → α✝
fb : β✝ → β✝
f : α✝ → β✝
g : β✝ → γ
s✝ t✝ : Set α✝
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LinearOrder β
φ : β → α
ψ : α → β
t : Set β
s : Set α
hφ : MonotoneOn φ t
φψs : RightInvOn ψ φ s
ψts : MapsTo ψ s t
x : α
xs : x ∈ s
y : α
ys : x ∈ s
l : x ≤ x
ψyx : ψ x ≤ ψ x
this : x ≤ x
⊢ ψ x ≤ ψ x
exact le_refl _