ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>DecidableEq ι<VAR>(i : ι) → PartialOrder (α i)<VAR>f : (i : ι) → α i<VAR>i : ι<VAR>b : α i<GOAL>Function.update f i '' Set.Ioo (f i) b = Set.Ioo f (Function.update f i b)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>DecidableEq ι<VAR>(i : ι) → PartialOrder (α i)<VAR>(i : ι) → One (α i)<VAR>i : ι<VAR>a b : α i<GOAL>Pi.mulSingle i '' Set.Icc a b = Set.Icc (Pi.mulSingle i a) (Pi.mulSingle i b)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>DecidableEq ι<VAR>(i : ι) → PartialOrder (α i)<VAR>(i : ι) → Zero (α i)<VAR>i : ι<VAR>a b : α i<GOAL>Pi.single i '' Set.Icc a b = Set.Icc (Pi.single i a) (Pi.single i b)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>DecidableEq ι<VAR>(i : ι) → PartialOrder (α i)<VAR>(i : ι) → Zero (α i)<VAR>i : ι<VAR>a b : α i<GOAL>Pi.single i '' Set.Ico a b = Set.Ico (Pi.single i a) (Pi.single i b)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>DecidableEq ι<VAR>(i : ι) → PartialOrder (α i)<VAR>(i : ι) → One (α i)<VAR>i : ι<VAR>a b : α i<GOAL>Pi.mulSingle i '' Set.Ico a b = Set.Ico (Pi.mulSingle i a) (Pi.mulSingle i b)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>DecidableEq ι<VAR>(i : ι) → PartialOrder (α i)<VAR>(i : ι) → One (α i)<VAR>i : ι<VAR>a b : α i<GOAL>Pi.mulSingle i '' Set.Ioc a b = Set.Ioc (Pi.mulSingle i a) (Pi.mulSingle i b)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>DecidableEq ι<VAR>(i : ι) → PartialOrder (α i)<VAR>(i : ι) → Zero (α i)<VAR>i : ι<VAR>a b : α i<GOAL>Pi.single i '' Set.Ioc a b = Set.Ioc (Pi.single i a) (Pi.single i b)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>DecidableEq ι<VAR>(i : ι) → PartialOrder (α i)<VAR>(i : ι) → Zero (α i)<VAR>i : ι<VAR>a b : α i<GOAL>Pi.single i '' Set.Ioo a b = Set.Ioo (Pi.single i a) (Pi.single i b)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>DecidableEq ι<VAR>(i : ι) → PartialOrder (α i)<VAR>(i : ι) → One (α i)<VAR>i : ι<VAR>a b : α i<GOAL>Pi.mulSingle i '' Set.Ioo a b = Set.Ioo (Pi.mulSingle i a) (Pi.mulSingle i b)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>DecidableEq ι<VAR>(i : ι) → PartialOrder (α i)<VAR>(i : ι) → One (α i)<VAR>i : ι<VAR>a : α i<GOAL>Pi.mulSingle i '' Set.Icc a 1 = Set.Icc (Pi.mulSingle i a) 1
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>DecidableEq ι<VAR>(i : ι) → PartialOrder (α i)<VAR>(i : ι) → Zero (α i)<VAR>i : ι<VAR>a : α i<GOAL>Pi.single i '' Set.Icc a 0 = Set.Icc (Pi.single i a) 0
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>DecidableEq ι<VAR>(i : ι) → PartialOrder (α i)<VAR>(i : ι) → One (α i)<VAR>i : ι<VAR>a : α i<GOAL>Pi.mulSingle i '' Set.Ico a 1 = Set.Ico (Pi.mulSingle i a) 1
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>DecidableEq ι<VAR>(i : ι) → PartialOrder (α i)<VAR>(i : ι) → Zero (α i)<VAR>i : ι<VAR>a : α i<GOAL>Pi.single i '' Set.Ico a 0 = Set.Ico (Pi.single i a) 0
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>DecidableEq ι<VAR>(i : ι) → PartialOrder (α i)<VAR>(i : ι) → Zero (α i)<VAR>i : ι<VAR>a : α i<GOAL>Pi.single i '' Set.Ioc a 0 = Set.Ioc (Pi.single i a) 0
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>DecidableEq ι<VAR>(i : ι) → PartialOrder (α i)<VAR>(i : ι) → One (α i)<VAR>i : ι<VAR>a : α i<GOAL>Pi.mulSingle i '' Set.Ioc a 1 = Set.Ioc (Pi.mulSingle i a) 1
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>DecidableEq ι<VAR>(i : ι) → PartialOrder (α i)<VAR>(i : ι) → One (α i)<VAR>i : ι<VAR>a : α i<GOAL>Pi.mulSingle i '' Set.Ioo a 1 = Set.Ioo (Pi.mulSingle i a) 1
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>DecidableEq ι<VAR>(i : ι) → PartialOrder (α i)<VAR>(i : ι) → Zero (α i)<VAR>i : ι<VAR>a : α i<GOAL>Pi.single i '' Set.Ioo a 0 = Set.Ioo (Pi.single i a) 0
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>DecidableEq ι<VAR>(i : ι) → PartialOrder (α i)<VAR>(i : ι) → One (α i)<VAR>i : ι<VAR>b : α i<GOAL>Pi.mulSingle i '' Set.Icc 1 b = Set.Icc 1 (Pi.mulSingle i b)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>DecidableEq ι<VAR>(i : ι) → PartialOrder (α i)<VAR>(i : ι) → Zero (α i)<VAR>i : ι<VAR>b : α i<GOAL>Pi.single i '' Set.Icc 0 b = Set.Icc 0 (Pi.single i b)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>DecidableEq ι<VAR>(i : ι) → PartialOrder (α i)<VAR>(i : ι) → One (α i)<VAR>i : ι<VAR>b : α i<GOAL>Pi.mulSingle i '' Set.Ico 1 b = Set.Ico 1 (Pi.mulSingle i b)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>DecidableEq ι<VAR>(i : ι) → PartialOrder (α i)<VAR>(i : ι) → Zero (α i)<VAR>i : ι<VAR>b : α i<GOAL>Pi.single i '' Set.Ico 0 b = Set.Ico 0 (Pi.single i b)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>DecidableEq ι<VAR>(i : ι) → PartialOrder (α i)<VAR>(i : ι) → One (α i)<VAR>i : ι<VAR>b : α i<GOAL>Pi.mulSingle i '' Set.Ioc 1 b = Set.Ioc 1 (Pi.mulSingle i b)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>DecidableEq ι<VAR>(i : ι) → PartialOrder (α i)<VAR>(i : ι) → Zero (α i)<VAR>i : ι<VAR>b : α i<GOAL>Pi.single i '' Set.Ioc 0 b = Set.Ioc 0 (Pi.single i b)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>DecidableEq ι<VAR>(i : ι) → PartialOrder (α i)<VAR>(i : ι) → One (α i)<VAR>i : ι<VAR>b : α i<GOAL>Pi.mulSingle i '' Set.Ioo 1 b = Set.Ioo 1 (Pi.mulSingle i b)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>DecidableEq ι<VAR>(i : ι) → PartialOrder (α i)<VAR>(i : ι) → Zero (α i)<VAR>i : ι<VAR>b : α i<GOAL>Pi.single i '' Set.Ioo 0 b = Set.Ioo 0 (Pi.single i b)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → Lattice (α i)<VAR>a b : (i : ι) → α i<GOAL>(Set.univ.pi fun i => Set.uIcc (a i) (b i)) = Set.uIcc a b
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → Lattice (α i)<VAR>DecidableEq ι<VAR>f : (i : ι) → α i<VAR>i : ι<VAR>a b : α i<GOAL>Function.update f i '' Set.uIcc a b = Set.uIcc (Function.update f i a) (Function.update f i b)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → Lattice (α i)<VAR>DecidableEq ι<VAR>f : (i : ι) → α i<VAR>i : ι<VAR>a : α i<GOAL>Function.update f i '' Set.uIcc a (f i) = Set.uIcc (Function.update f i a) f
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → Lattice (α i)<VAR>DecidableEq ι<VAR>f : (i : ι) → α i<VAR>i : ι<VAR>b : α i<GOAL>Function.update f i '' Set.uIcc (f i) b = Set.uIcc f (Function.update f i b)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → Lattice (α i)<VAR>DecidableEq ι<VAR>(i : ι) → Zero (α i)<VAR>i : ι<VAR>a b : α i<GOAL>Pi.single i '' Set.uIcc a b = Set.uIcc (Pi.single i a) (Pi.single i b)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → Lattice (α i)<VAR>DecidableEq ι<VAR>(i : ι) → One (α i)<VAR>i : ι<VAR>a b : α i<GOAL>Pi.mulSingle i '' Set.uIcc a b = Set.uIcc (Pi.mulSingle i a) (Pi.mulSingle i b)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → Lattice (α i)<VAR>DecidableEq ι<VAR>(i : ι) → One (α i)<VAR>i : ι<VAR>a : α i<GOAL>Pi.mulSingle i '' Set.uIcc a 1 = Set.uIcc (Pi.mulSingle i a) 1
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → Lattice (α i)<VAR>DecidableEq ι<VAR>(i : ι) → Zero (α i)<VAR>i : ι<VAR>a : α i<GOAL>Pi.single i '' Set.uIcc a 0 = Set.uIcc (Pi.single i a) 0
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → Lattice (α i)<VAR>DecidableEq ι<VAR>(i : ι) → One (α i)<VAR>i : ι<VAR>b : α i<GOAL>Pi.mulSingle i '' Set.uIcc 1 b = Set.uIcc 1 (Pi.mulSingle i b)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → Lattice (α i)<VAR>DecidableEq ι<VAR>(i : ι) → Zero (α i)<VAR>i : ι<VAR>b : α i<GOAL>Pi.single i '' Set.uIcc 0 b = Set.uIcc 0 (Pi.single i b)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>DecidableEq ι<VAR>(i : ι) → LinearOrder (α i)<VAR>x y : (i : ι) → α i<VAR>i₀ : ι<VAR>m : α i₀<VAR>hm : m ∈ Set.Icc (x i₀) (y i₀)<GOAL>((Set.univ.pi fun i => Set.Ioc (x i) (Function.update y i₀ m i)) ∪ Set.univ.pi fun i => Set.Ioc (Function.update x i₀ m i) (y i)) = Set.univ.pi fun i => Set.Ioc (x i) (y i)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>DecidableEq ι<VAR>(i : ι) → LinearOrder (α i)<VAR>x y x' y' : (i : ι) → α i<GOAL>(Set.Icc x y \ Set.univ.pi fun i => Set.Ioo (x' i) (y' i)) ⊆ (⋃ i, Set.Icc x (Function.update y i (x' i))) ∪ ⋃ i, Set.Icc (Function.update x i (y' i)) y
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>DecidableEq ι<VAR>(i : ι) → LinearOrder (α i)<VAR>x y z : (i : ι) → α i<GOAL>(Set.Icc x z \ Set.univ.pi fun i => Set.Ioc (y i) (z i)) ⊆ ⋃ i, Set.Icc x (Function.update z i (y i))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>Preorder α<VAR>Preorder β<VAR>a : α<VAR>h : MonotoneOn f (Set.Ici a)<GOAL>Set.MapsTo f (Set.Ici a) (Set.Ici (f a))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>Preorder α<VAR>Preorder β<VAR>b : α<VAR>h : MonotoneOn f (Set.Iic b)<GOAL>Set.MapsTo f (Set.Iic b) (Set.Iic (f b))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>Preorder α<VAR>Preorder β<VAR>a b : α<VAR>h : MonotoneOn f (Set.Icc a b)<GOAL>Set.MapsTo f (Set.Icc a b) (Set.Icc (f a) (f b))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>Preorder α<VAR>Preorder β<VAR>a : α<VAR>h : AntitoneOn f (Set.Ici a)<GOAL>Set.MapsTo f (Set.Ici a) (Set.Iic (f a))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>Preorder α<VAR>Preorder β<VAR>b : α<VAR>h : AntitoneOn f (Set.Iic b)<GOAL>Set.MapsTo f (Set.Iic b) (Set.Ici (f b))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>Preorder α<VAR>Preorder β<VAR>a b : α<VAR>h : AntitoneOn f (Set.Icc a b)<GOAL>Set.MapsTo f (Set.Icc a b) (Set.Icc (f b) (f a))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>Preorder α<VAR>Preorder β<VAR>a : α<VAR>h : StrictMonoOn f (Set.Ici a)<GOAL>Set.MapsTo f (Set.Ioi a) (Set.Ioi (f a))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>Preorder α<VAR>Preorder β<VAR>b : α<VAR>h : StrictMonoOn f (Set.Iic b)<GOAL>Set.MapsTo f (Set.Iio b) (Set.Iio (f b))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>Preorder α<VAR>Preorder β<VAR>a b : α<VAR>h : StrictMonoOn f (Set.Icc a b)<GOAL>Set.MapsTo f (Set.Ioo a b) (Set.Ioo (f a) (f b))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>Preorder α<VAR>Preorder β<VAR>a : α<VAR>h : StrictAntiOn f (Set.Ici a)<GOAL>Set.MapsTo f (Set.Ioi a) (Set.Iio (f a))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>Preorder α<VAR>Preorder β<VAR>b : α<VAR>h : StrictAntiOn f (Set.Iic b)<GOAL>Set.MapsTo f (Set.Iio b) (Set.Ioi (f b))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>Preorder α<VAR>Preorder β<VAR>a b : α<VAR>h : StrictAntiOn f (Set.Icc a b)<GOAL>Set.MapsTo f (Set.Ioo a b) (Set.Ioo (f b) (f a))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>Preorder α<VAR>Preorder β<VAR>a : α<VAR>h : Monotone f<GOAL>Set.MapsTo f (Set.Ici a) (Set.Ici (f a))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>Preorder α<VAR>Preorder β<VAR>b : α<VAR>h : Monotone f<GOAL>Set.MapsTo f (Set.Iic b) (Set.Iic (f b))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>Preorder α<VAR>Preorder β<VAR>a b : α<VAR>h : Monotone f<GOAL>Set.MapsTo f (Set.Icc a b) (Set.Icc (f a) (f b))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>Preorder α<VAR>Preorder β<VAR>a : α<VAR>h : Antitone f<GOAL>Set.MapsTo f (Set.Ici a) (Set.Iic (f a))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>Preorder α<VAR>Preorder β<VAR>b : α<VAR>h : Antitone f<GOAL>Set.MapsTo f (Set.Iic b) (Set.Ici (f b))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>Preorder α<VAR>Preorder β<VAR>a b : α<VAR>h : Antitone f<GOAL>Set.MapsTo f (Set.Icc a b) (Set.Icc (f b) (f a))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>Preorder α<VAR>Preorder β<VAR>a : α<VAR>h : StrictMono f<GOAL>Set.MapsTo f (Set.Ioi a) (Set.Ioi (f a))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>Preorder α<VAR>Preorder β<VAR>b : α<VAR>h : StrictMono f<GOAL>Set.MapsTo f (Set.Iio b) (Set.Iio (f b))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>Preorder α<VAR>Preorder β<VAR>a b : α<VAR>h : StrictMono f<GOAL>Set.MapsTo f (Set.Ioo a b) (Set.Ioo (f a) (f b))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>Preorder α<VAR>Preorder β<VAR>a : α<VAR>h : StrictAnti f<GOAL>Set.MapsTo f (Set.Ioi a) (Set.Iio (f a))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>Preorder α<VAR>Preorder β<VAR>b : α<VAR>h : StrictAnti f<GOAL>Set.MapsTo f (Set.Iio b) (Set.Ioi (f b))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>Preorder α<VAR>Preorder β<VAR>a b : α<VAR>h : StrictAnti f<GOAL>Set.MapsTo f (Set.Ioo a b) (Set.Ioo (f b) (f a))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>Preorder α<VAR>Preorder β<VAR>a : α<VAR>h : MonotoneOn f (Set.Ici a)<GOAL>f '' Set.Ici a ⊆ Set.Ici (f a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>Preorder α<VAR>Preorder β<VAR>b : α<VAR>h : MonotoneOn f (Set.Iic b)<GOAL>f '' Set.Iic b ⊆ Set.Iic (f b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>Preorder α<VAR>Preorder β<VAR>a b : α<VAR>h : MonotoneOn f (Set.Icc a b)<GOAL>f '' Set.Icc a b ⊆ Set.Icc (f a) (f b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>Preorder α<VAR>Preorder β<VAR>a : α<VAR>h : AntitoneOn f (Set.Ici a)<GOAL>f '' Set.Ici a ⊆ Set.Iic (f a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>Preorder α<VAR>Preorder β<VAR>b : α<VAR>h : AntitoneOn f (Set.Iic b)<GOAL>f '' Set.Iic b ⊆ Set.Ici (f b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>Preorder α<VAR>Preorder β<VAR>a b : α<VAR>h : AntitoneOn f (Set.Icc a b)<GOAL>f '' Set.Icc a b ⊆ Set.Icc (f b) (f a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>Preorder α<VAR>Preorder β<VAR>a : α<VAR>h : StrictMonoOn f (Set.Ici a)<GOAL>f '' Set.Ioi a ⊆ Set.Ioi (f a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>Preorder α<VAR>Preorder β<VAR>b : α<VAR>h : StrictMonoOn f (Set.Iic b)<GOAL>f '' Set.Iio b ⊆ Set.Iio (f b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>Preorder α<VAR>Preorder β<VAR>a b : α<VAR>h : StrictMonoOn f (Set.Icc a b)<GOAL>f '' Set.Ioo a b ⊆ Set.Ioo (f a) (f b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>Preorder α<VAR>Preorder β<VAR>a : α<VAR>h : StrictAntiOn f (Set.Ici a)<GOAL>f '' Set.Ioi a ⊆ Set.Iio (f a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>Preorder α<VAR>Preorder β<VAR>b : α<VAR>h : StrictAntiOn f (Set.Iic b)<GOAL>f '' Set.Iio b ⊆ Set.Ioi (f b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>Preorder α<VAR>Preorder β<VAR>a b : α<VAR>h : StrictAntiOn f (Set.Icc a b)<GOAL>f '' Set.Ioo a b ⊆ Set.Ioo (f b) (f a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>Preorder α<VAR>Preorder β<VAR>a : α<VAR>h : Monotone f<GOAL>f '' Set.Ici a ⊆ Set.Ici (f a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>Preorder α<VAR>Preorder β<VAR>b : α<VAR>h : Monotone f<GOAL>f '' Set.Iic b ⊆ Set.Iic (f b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>Preorder α<VAR>Preorder β<VAR>a b : α<VAR>h : Monotone f<GOAL>f '' Set.Icc a b ⊆ Set.Icc (f a) (f b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>Preorder α<VAR>Preorder β<VAR>a : α<VAR>h : Antitone f<GOAL>f '' Set.Ici a ⊆ Set.Iic (f a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>Preorder α<VAR>Preorder β<VAR>b : α<VAR>h : Antitone f<GOAL>f '' Set.Iic b ⊆ Set.Ici (f b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>Preorder α<VAR>Preorder β<VAR>a b : α<VAR>h : Antitone f<GOAL>f '' Set.Icc a b ⊆ Set.Icc (f b) (f a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>Preorder α<VAR>Preorder β<VAR>a : α<VAR>h : StrictMono f<GOAL>f '' Set.Ioi a ⊆ Set.Ioi (f a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>Preorder α<VAR>Preorder β<VAR>b : α<VAR>h : StrictMono f<GOAL>f '' Set.Iio b ⊆ Set.Iio (f b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>Preorder α<VAR>Preorder β<VAR>a b : α<VAR>h : StrictMono f<GOAL>f '' Set.Ioo a b ⊆ Set.Ioo (f a) (f b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>Preorder α<VAR>Preorder β<VAR>a : α<VAR>h : StrictAnti f<GOAL>f '' Set.Ioi a ⊆ Set.Iio (f a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>Preorder α<VAR>Preorder β<VAR>b : α<VAR>h : StrictAnti f<GOAL>f '' Set.Iio b ⊆ Set.Ioi (f b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>Preorder α<VAR>Preorder β<VAR>a b : α<VAR>h : StrictAnti f<GOAL>f '' Set.Ioo a b ⊆ Set.Ioo (f b) (f a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>PartialOrder α<VAR>Preorder β<VAR>a b : α<VAR>h : StrictMonoOn f (Set.Icc a b)<GOAL>Set.MapsTo f (Set.Ico a b) (Set.Ico (f a) (f b))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>PartialOrder α<VAR>Preorder β<VAR>a b : α<VAR>h : StrictMonoOn f (Set.Icc a b)<GOAL>Set.MapsTo f (Set.Ioc a b) (Set.Ioc (f a) (f b))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>PartialOrder α<VAR>Preorder β<VAR>a b : α<VAR>h : StrictAntiOn f (Set.Icc a b)<GOAL>Set.MapsTo f (Set.Ico a b) (Set.Ioc (f b) (f a))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>PartialOrder α<VAR>Preorder β<VAR>a b : α<VAR>h : StrictAntiOn f (Set.Icc a b)<GOAL>Set.MapsTo f (Set.Ioc a b) (Set.Ico (f b) (f a))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>PartialOrder α<VAR>Preorder β<VAR>a b : α<VAR>h : StrictMono f<GOAL>Set.MapsTo f (Set.Ico a b) (Set.Ico (f a) (f b))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>PartialOrder α<VAR>Preorder β<VAR>a b : α<VAR>h : StrictMono f<GOAL>Set.MapsTo f (Set.Ioc a b) (Set.Ioc (f a) (f b))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>PartialOrder α<VAR>Preorder β<VAR>a b : α<VAR>h : StrictAnti f<GOAL>Set.MapsTo f (Set.Ico a b) (Set.Ioc (f b) (f a))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>PartialOrder α<VAR>Preorder β<VAR>a b : α<VAR>h : StrictAnti f<GOAL>Set.MapsTo f (Set.Ioc a b) (Set.Ico (f b) (f a))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>PartialOrder α<VAR>Preorder β<VAR>a b : α<VAR>h : StrictMonoOn f (Set.Icc a b)<GOAL>f '' Set.Ico a b ⊆ Set.Ico (f a) (f b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>PartialOrder α<VAR>Preorder β<VAR>a b : α<VAR>h : StrictMonoOn f (Set.Icc a b)<GOAL>f '' Set.Ioc a b ⊆ Set.Ioc (f a) (f b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>PartialOrder α<VAR>Preorder β<VAR>a b : α<VAR>h : StrictAntiOn f (Set.Icc a b)<GOAL>f '' Set.Ico a b ⊆ Set.Ioc (f b) (f a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>PartialOrder α<VAR>Preorder β<VAR>a b : α<VAR>h : StrictAntiOn f (Set.Icc a b)<GOAL>f '' Set.Ioc a b ⊆ Set.Ico (f b) (f a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>PartialOrder α<VAR>Preorder β<VAR>a b : α<VAR>h : StrictMono f<GOAL>f '' Set.Ico a b ⊆ Set.Ico (f a) (f b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>PartialOrder α<VAR>Preorder β<VAR>a b : α<VAR>h : StrictMono f<GOAL>f '' Set.Ioc a b ⊆ Set.Ioc (f a) (f b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>PartialOrder α<VAR>Preorder β<VAR>a b : α<VAR>h : StrictAnti f<GOAL>f '' Set.Ico a b ⊆ Set.Ioc (f b) (f a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>PartialOrder α<VAR>Preorder β<VAR>a b : α<VAR>h : StrictAnti f<GOAL>f '' Set.Ioc a b ⊆ Set.Ico (f b) (f a)
<VAR>α : Type u_1<VAR>p q r : α → α → Prop<VAR>a b : α<VAR>c : { x // p a x ∧ q x b }<VAR>h : ∀ {x : α}, r (↑c) x → p a x<GOAL>Subtype.val '' {y | r ↑c ↑y} = {y | r (↑c) y ∧ q y b}
<VAR>α : Type u_1<VAR>p q r : α → α → Prop<VAR>a b : α<VAR>c : { x // p a x ∧ q x b }<VAR>h : ∀ {x : α}, r x ↑c → q x b<GOAL>Subtype.val '' {y | r ↑y ↑c} = {y | p a y ∧ r y ↑c}
<VAR>α : Type u_1<VAR>Preorder α<VAR>p : α → Prop<VAR>a : { x // p x }<GOAL>Subtype.val ⁻¹' Set.Ici ↑a = Set.Ici a
<VAR>α : Type u_1<VAR>Preorder α<VAR>p : α → Prop<VAR>a : { x // p x }<GOAL>Subtype.val ⁻¹' Set.Iic ↑a = Set.Iic a
<VAR>α : Type u_1<VAR>Preorder α<VAR>p : α → Prop<VAR>a : { x // p x }<GOAL>Subtype.val ⁻¹' Set.Ioi ↑a = Set.Ioi a
<VAR>α : Type u_1<VAR>Preorder α<VAR>p : α → Prop<VAR>a : { x // p x }<GOAL>Subtype.val ⁻¹' Set.Iio ↑a = Set.Iio a
<VAR>α : Type u_1<VAR>Preorder α<VAR>p : α → Prop<VAR>a b : { x // p x }<GOAL>Subtype.val ⁻¹' Set.Icc ↑a ↑b = Set.Icc a b
<VAR>α : Type u_1<VAR>Preorder α<VAR>p : α → Prop<VAR>a b : { x // p x }<GOAL>Subtype.val ⁻¹' Set.Ico ↑a ↑b = Set.Ico a b
<VAR>α : Type u_1<VAR>Preorder α<VAR>p : α → Prop<VAR>a b : { x // p x }<GOAL>Subtype.val ⁻¹' Set.Ioc ↑a ↑b = Set.Ioc a b
<VAR>α : Type u_1<VAR>Preorder α<VAR>p : α → Prop<VAR>a b : { x // p x }<GOAL>Subtype.val ⁻¹' Set.Ioo ↑a ↑b = Set.Ioo a b
<VAR>α : Type u_1<VAR>Preorder α<VAR>p : α → Prop<VAR>a b : { x // p x }<GOAL>Subtype.val '' Set.Icc a b ⊆ Set.Icc ↑a ↑b
<VAR>α : Type u_1<VAR>Preorder α<VAR>p : α → Prop<VAR>a b : { x // p x }<GOAL>Subtype.val '' Set.Ico a b ⊆ Set.Ico ↑a ↑b
<VAR>α : Type u_1<VAR>Preorder α<VAR>p : α → Prop<VAR>a b : { x // p x }<GOAL>Subtype.val '' Set.Ioc a b ⊆ Set.Ioc ↑a ↑b
<VAR>α : Type u_1<VAR>Preorder α<VAR>p : α → Prop<VAR>a b : { x // p x }<GOAL>Subtype.val '' Set.Ioo a b ⊆ Set.Ioo ↑a ↑b
<VAR>α : Type u_1<VAR>Preorder α<VAR>p : α → Prop<VAR>a : { x // p x }<GOAL>Subtype.val '' Set.Iic a ⊆ Set.Iic ↑a
<VAR>α : Type u_1<VAR>Preorder α<VAR>p : α → Prop<VAR>a : { x // p x }<GOAL>Subtype.val '' Set.Iio a ⊆ Set.Iio ↑a
<VAR>α : Type u_1<VAR>Preorder α<VAR>p : α → Prop<VAR>a : { x // p x }<GOAL>Subtype.val '' Set.Ici a ⊆ Set.Ici ↑a
<VAR>α : Type u_1<VAR>Preorder α<VAR>p : α → Prop<VAR>a : { x // p x }<GOAL>Subtype.val '' Set.Ioi a ⊆ Set.Ioi ↑a
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<VAR>b : ↑(Set.Ici a)<GOAL>Subtype.val '' Set.Iic b = Set.Icc a ↑b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<VAR>b : ↑(Set.Ici a)<GOAL>Subtype.val '' Set.Iio b = Set.Ico a ↑b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<VAR>b : ↑(Set.Ici a)<GOAL>Subtype.val '' Set.Ici b = Set.Ici ↑b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<VAR>b : ↑(Set.Ici a)<GOAL>Subtype.val '' Set.Ioi b = Set.Ioi ↑b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<VAR>b : ↑(Set.Iic a)<GOAL>Subtype.val '' Set.Ici b = Set.Icc (↑b) a
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<VAR>b : ↑(Set.Iic a)<GOAL>Subtype.val '' Set.Ioi b = Set.Ioc (↑b) a
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<VAR>b : ↑(Set.Iic a)<GOAL>Subtype.val '' Set.Iic b = Set.Iic ↑b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<VAR>b : ↑(Set.Iic a)<GOAL>Subtype.val '' Set.Iio b = Set.Iio ↑b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<VAR>b : ↑(Set.Ioi a)<GOAL>Subtype.val '' Set.Ici b = Set.Ici ↑b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<VAR>b : ↑(Set.Ioi a)<GOAL>Subtype.val '' Set.Iic b = Set.Ioc a ↑b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<VAR>b : ↑(Set.Ioi a)<GOAL>Subtype.val '' Set.Ioi b = Set.Ioi ↑b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<VAR>b : ↑(Set.Ioi a)<GOAL>Subtype.val '' Set.Iio b = Set.Ioo a ↑b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<VAR>b : ↑(Set.Iio a)<GOAL>Subtype.val '' Set.Ici b = Set.Ico (↑b) a
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<VAR>b : ↑(Set.Iio a)<GOAL>Subtype.val '' Set.Iic b = Set.Iic ↑b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<VAR>b : ↑(Set.Iio a)<GOAL>Subtype.val '' Set.Ioi b = Set.Ioo (↑b) a
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<VAR>b : ↑(Set.Iio a)<GOAL>Subtype.val '' Set.Iio b = Set.Iio ↑b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<VAR>c : ↑(Set.Icc a b)<GOAL>Subtype.val '' Set.Ici c = Set.Icc (↑c) b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<VAR>c : ↑(Set.Icc a b)<GOAL>Subtype.val '' Set.Iic c = Set.Icc a ↑c
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<VAR>c : ↑(Set.Icc a b)<GOAL>Subtype.val '' Set.Ioi c = Set.Ioc (↑c) b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<VAR>c : ↑(Set.Icc a b)<GOAL>Subtype.val '' Set.Iio c = Set.Ico a ↑c
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<VAR>c : ↑(Set.Ico a b)<GOAL>Subtype.val '' Set.Ici c = Set.Ico (↑c) b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<VAR>c : ↑(Set.Ico a b)<GOAL>Subtype.val '' Set.Iic c = Set.Icc a ↑c
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<VAR>c : ↑(Set.Ico a b)<GOAL>Subtype.val '' Set.Ioi c = Set.Ioo (↑c) b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<VAR>c : ↑(Set.Ico a b)<GOAL>Subtype.val '' Set.Iio c = Set.Ico a ↑c
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<VAR>c : ↑(Set.Ioc a b)<GOAL>Subtype.val '' Set.Ici c = Set.Icc (↑c) b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<VAR>c : ↑(Set.Ioc a b)<GOAL>Subtype.val '' Set.Iic c = Set.Ioc a ↑c
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<VAR>c : ↑(Set.Ioc a b)<GOAL>Subtype.val '' Set.Ioi c = Set.Ioc (↑c) b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<VAR>c : ↑(Set.Ioc a b)<GOAL>Subtype.val '' Set.Iio c = Set.Ioo a ↑c
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<VAR>c : ↑(Set.Ioo a b)<GOAL>Subtype.val '' Set.Ici c = Set.Ico (↑c) b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<VAR>c : ↑(Set.Ioo a b)<GOAL>Subtype.val '' Set.Iic c = Set.Ioc a ↑c
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<VAR>c : ↑(Set.Ioo a b)<GOAL>Subtype.val '' Set.Ioi c = Set.Ioo (↑c) b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<VAR>c : ↑(Set.Ioo a b)<GOAL>Subtype.val '' Set.Iio c = Set.Ioo a ↑c
<VAR>α : Type u_1<VAR>Preorder α<VAR>b : α<GOAL>DirectedOn (fun x x_1 => x ≤ x_1) (Set.Iic b)