ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>f : α → β → γ<VAR>s : Set α<VAR>t : Set β<VAR>h₀ : ∀ (b : β), Antitone (Function.swap f b)<VAR>h₁ : ∀ (a : α), Monotone (f a)<GOAL>BddBelow s → BddAbove t → BddAbove (Set.image2 f s t)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>f : α → β → γ<VAR>s : Set α<VAR>t : Set β<VAR>h₀ : ∀ (b : β), Antitone (Function.swap f b)<VAR>h₁ : ∀ (a : α), Monotone (f a)<GOAL>BddAbove s → BddBelow t → BddBelow (Set.image2 f s t)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>f : α → β → γ<VAR>s : Set α<VAR>t : Set β<VAR>a : α<VAR>b : β<VAR>h₀ : ∀ (b : β), Antitone (Function.swap f b)<VAR>h₁ : ∀ (a : α), Monotone (f a)<VAR>ha : IsLeast s a<VAR>hb : IsGreatest t b<GOAL>IsGreatest (Set.image2 f s t) (f a b)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>f : α → β → γ<VAR>s : Set α<VAR>t : Set β<VAR>a : α<VAR>b : β<VAR>h₀ : ∀ (b : β), Antitone (Function.swap f b)<VAR>h₁ : ∀ (a : α), Monotone (f a)<VAR>ha : IsGreatest s a<VAR>hb : IsLeast t b<GOAL>IsLeast (Set.image2 f s t) (f a b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>s : Set (α × β)<GOAL>BddAbove s ↔ BddAbove (Prod.fst '' s) ∧ BddAbove (Prod.snd '' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>s : Set (α × β)<GOAL>BddBelow s ↔ BddBelow (Prod.fst '' s) ∧ BddBelow (Prod.snd '' s)
<VAR>ι : Sort x<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>F : ι → α × β<GOAL>BddAbove (Set.range F) ↔ BddAbove (Set.range (Prod.fst ∘ F)) ∧ BddAbove (Set.range (Prod.snd ∘ F))
<VAR>ι : Sort x<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>F : ι → α × β<GOAL>BddBelow (Set.range F) ↔ BddBelow (Set.range (Prod.fst ∘ F)) ∧ BddBelow (Set.range (Prod.snd ∘ F))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>s : Set (α × β)<VAR>p : α × β<GOAL>IsLUB s p ↔ IsLUB (Prod.fst '' s) p.1 ∧ IsLUB (Prod.snd '' s) p.2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>s : Set (α × β)<VAR>p : α × β<GOAL>IsGLB s p ↔ IsGLB (Prod.fst '' s) p.1 ∧ IsGLB (Prod.snd '' s) p.2
<VAR>α : Type u<VAR>π : α → Type u_1<VAR>(a : α) → Preorder (π a)<VAR>s : Set ((a : α) → π a)<GOAL>BddAbove s ↔ ∀ (a : α), BddAbove (Function.eval a '' s)
<VAR>α : Type u<VAR>π : α → Type u_1<VAR>(a : α) → Preorder (π a)<VAR>s : Set ((a : α) → π a)<GOAL>BddBelow s ↔ ∀ (a : α), BddBelow (Function.eval a '' s)
<VAR>α : Type u<VAR>ι : Sort x<VAR>π : α → Type u_1<VAR>(a : α) → Preorder (π a)<VAR>F : ι → (a : α) → π a<GOAL>BddAbove (Set.range F) ↔ ∀ (a : α), BddAbove (Set.range fun i => F i a)
<VAR>α : Type u<VAR>ι : Sort x<VAR>π : α → Type u_1<VAR>(a : α) → Preorder (π a)<VAR>F : ι → (a : α) → π a<GOAL>BddBelow (Set.range F) ↔ ∀ (a : α), BddBelow (Set.range fun i => F i a)
<VAR>α : Type u<VAR>π : α → Type u_1<VAR>(a : α) → Preorder (π a)<VAR>s : Set ((a : α) → π a)<VAR>f : (a : α) → π a<GOAL>IsLUB s f ↔ ∀ (a : α), IsLUB (Function.eval a '' s) (f a)
<VAR>α : Type u<VAR>π : α → Type u_1<VAR>(a : α) → Preorder (π a)<VAR>s : Set ((a : α) → π a)<VAR>f : (a : α) → π a<GOAL>IsGLB s f ↔ ∀ (a : α), IsGLB (Function.eval a '' s) (f a)
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>hf : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y<VAR>s : Set α<VAR>x : α<VAR>hx : IsGLB (f '' s) (f x)<GOAL>IsGLB s x
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>hf : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y<VAR>s : Set α<VAR>x : α<VAR>hx : IsLUB (f '' s) (f x)<GOAL>IsLUB s x
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder β<VAR>f : α → β<VAR>g : α → β<VAR>h : ∀ (a : α), f a ≤ g a<VAR>hbdd : BddAbove (Set.range g)<GOAL>BddAbove (Set.range f)
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder β<VAR>f : α → β<VAR>g : α → β<VAR>h : ∀ (a : α), f a ≤ g a<VAR>hbdd : BddBelow (Set.range f)<GOAL>BddBelow (Set.range g)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>Preorder β<VAR>Preorder γ<VAR>f : α → β<VAR>g : β → γ<VAR>hf : BddAbove (Set.range f)<VAR>hg : Monotone g<GOAL>BddAbove (Set.range fun x => g (f x))
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>Preorder β<VAR>Preorder γ<VAR>f : α → β<VAR>g : β → γ<VAR>hf : BddBelow (Set.range f)<VAR>hg : Monotone g<GOAL>BddBelow (Set.range fun x => g (f x))
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>h : ScottContinuous f<GOAL>Monotone f
<VAR>α : Type u_1<VAR>Preorder α<GOAL>Antitone Set.Ici
<VAR>α : Type u_1<VAR>Preorder α<GOAL>Monotone Set.Iic
<VAR>α : Type u_1<VAR>Preorder α<GOAL>Antitone Set.Ioi
<VAR>α : Type u_1<VAR>Preorder α<GOAL>Monotone Set.Iio
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>hf : Monotone f<GOAL>Antitone fun x => Set.Ici (f x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>s : Set α<VAR>hf : MonotoneOn f s<GOAL>AntitoneOn (fun x => Set.Ici (f x)) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>hf : Antitone f<GOAL>Monotone fun x => Set.Ici (f x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>s : Set α<VAR>hf : AntitoneOn f s<GOAL>MonotoneOn (fun x => Set.Ici (f x)) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>hf : Monotone f<GOAL>Monotone fun x => Set.Iic (f x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>s : Set α<VAR>hf : MonotoneOn f s<GOAL>MonotoneOn (fun x => Set.Iic (f x)) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>hf : Antitone f<GOAL>Antitone fun x => Set.Iic (f x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>s : Set α<VAR>hf : AntitoneOn f s<GOAL>AntitoneOn (fun x => Set.Iic (f x)) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>hf : Monotone f<GOAL>Antitone fun x => Set.Ioi (f x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>s : Set α<VAR>hf : MonotoneOn f s<GOAL>AntitoneOn (fun x => Set.Ioi (f x)) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>hf : Antitone f<GOAL>Monotone fun x => Set.Ioi (f x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>s : Set α<VAR>hf : AntitoneOn f s<GOAL>MonotoneOn (fun x => Set.Ioi (f x)) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>hf : Monotone f<GOAL>Monotone fun x => Set.Iio (f x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>s : Set α<VAR>hf : MonotoneOn f s<GOAL>MonotoneOn (fun x => Set.Iio (f x)) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>hf : Antitone f<GOAL>Antitone fun x => Set.Iio (f x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>s : Set α<VAR>hf : AntitoneOn f s<GOAL>AntitoneOn (fun x => Set.Iio (f x)) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>f g : α → β<VAR>hf : Monotone f<VAR>hg : Antitone g<GOAL>Antitone fun x => Set.Icc (f x) (g x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>f g : α → β<VAR>s : Set α<VAR>hf : MonotoneOn f s<VAR>hg : AntitoneOn g s<GOAL>AntitoneOn (fun x => Set.Icc (f x) (g x)) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>f g : α → β<VAR>hf : Antitone f<VAR>hg : Monotone g<GOAL>Monotone fun x => Set.Icc (f x) (g x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>f g : α → β<VAR>s : Set α<VAR>hf : AntitoneOn f s<VAR>hg : MonotoneOn g s<GOAL>MonotoneOn (fun x => Set.Icc (f x) (g x)) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>f g : α → β<VAR>hf : Monotone f<VAR>hg : Antitone g<GOAL>Antitone fun x => Set.Ico (f x) (g x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>f g : α → β<VAR>s : Set α<VAR>hf : MonotoneOn f s<VAR>hg : AntitoneOn g s<GOAL>AntitoneOn (fun x => Set.Ico (f x) (g x)) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>f g : α → β<VAR>hf : Antitone f<VAR>hg : Monotone g<GOAL>Monotone fun x => Set.Ico (f x) (g x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>f g : α → β<VAR>s : Set α<VAR>hf : AntitoneOn f s<VAR>hg : MonotoneOn g s<GOAL>MonotoneOn (fun x => Set.Ico (f x) (g x)) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>f g : α → β<VAR>hf : Monotone f<VAR>hg : Antitone g<GOAL>Antitone fun x => Set.Ioc (f x) (g x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>f g : α → β<VAR>s : Set α<VAR>hf : MonotoneOn f s<VAR>hg : AntitoneOn g s<GOAL>AntitoneOn (fun x => Set.Ioc (f x) (g x)) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>f g : α → β<VAR>hf : Antitone f<VAR>hg : Monotone g<GOAL>Monotone fun x => Set.Ioc (f x) (g x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>f g : α → β<VAR>s : Set α<VAR>hf : AntitoneOn f s<VAR>hg : MonotoneOn g s<GOAL>MonotoneOn (fun x => Set.Ioc (f x) (g x)) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>f g : α → β<VAR>hf : Monotone f<VAR>hg : Antitone g<GOAL>Antitone fun x => Set.Ioo (f x) (g x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>f g : α → β<VAR>s : Set α<VAR>hf : MonotoneOn f s<VAR>hg : AntitoneOn g s<GOAL>AntitoneOn (fun x => Set.Ioo (f x) (g x)) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>f g : α → β<VAR>hf : Antitone f<VAR>hg : Monotone g<GOAL>Monotone fun x => Set.Ioo (f x) (g x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>f g : α → β<VAR>s : Set α<VAR>hf : AntitoneOn f s<VAR>hg : MonotoneOn g s<GOAL>MonotoneOn (fun x => Set.Ioo (f x) (g x)) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>SemilatticeSup α<VAR>LinearOrder β<VAR>f g : α → β<VAR>a b : β<VAR>hf : Antitone f<VAR>hg : Monotone g<VAR>ha : IsGLB (Set.range f) a<VAR>hb : IsLUB (Set.range g) b<GOAL>⋃ x, Set.Ioo (f x) (g x) = Set.Ioo a b
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>SuccOrder α<VAR>IsSuccArchimedean α<VAR>OrderBot α<VAR>n : α<VAR>φ : α → α<VAR>hφ : StrictMonoOn φ (Set.Iic n)<VAR>m : α<GOAL>m ≤ n → m ≤ φ m
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>PredOrder α<VAR>IsPredArchimedean α<VAR>OrderTop α<VAR>n : α<VAR>φ : α → α<VAR>hφ : StrictMonoOn φ (Set.Ici n)<VAR>m : α<GOAL>n ≤ m → φ m ≤ m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PartialOrder α<VAR>Preorder β<VAR>ψ : α → β<VAR>SuccOrder α<VAR>IsSuccArchimedean α<VAR>n : α<VAR>hψ : ∀ m < n, ψ m < ψ (Order.succ m)<GOAL>StrictMonoOn ψ (Set.Iic n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PartialOrder α<VAR>Preorder β<VAR>ψ : α → β<VAR>SuccOrder α<VAR>IsSuccArchimedean α<VAR>n : α<VAR>hψ : ∀ m < n, ψ (Order.succ m) < ψ m<GOAL>StrictAntiOn ψ (Set.Iic n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PartialOrder α<VAR>Preorder β<VAR>ψ : α → β<VAR>PredOrder α<VAR>IsPredArchimedean α<VAR>n : α<VAR>hψ : ∀ (m : α), n < m → ψ (Order.pred m) < ψ m<GOAL>StrictMonoOn ψ (Set.Ici n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PartialOrder α<VAR>Preorder β<VAR>ψ : α → β<VAR>PredOrder α<VAR>IsPredArchimedean α<VAR>n : α<VAR>hψ : ∀ (m : α), n < m → ψ m < ψ (Order.pred m)<GOAL>StrictAntiOn ψ (Set.Ici n)
<VAR>X : Type u<VAR>Lattice X<VAR>self : JordanHolderLattice X<VAR>x y : X<GOAL>JordanHolderLattice.IsMaximal x (x ⊔ y) → JordanHolderLattice.IsMaximal y (x ⊔ y) → JordanHolderLattice.IsMaximal (x ⊓ y) x
<VAR>X : Type u<VAR>Lattice X<VAR>self : JordanHolderLattice X<VAR>x y z : X<GOAL>JordanHolderLattice.IsMaximal x z → JordanHolderLattice.IsMaximal y z → x ≠ y → x ⊔ y = z
<VAR>X : Type u<VAR>Lattice X<VAR>self : JordanHolderLattice X<VAR>x y : X<GOAL>JordanHolderLattice.IsMaximal x (x ⊔ y) → JordanHolderLattice.Iso (x, x ⊔ y) (x ⊓ y, y)
<VAR>X : Type u<VAR>Lattice X<VAR>self : JordanHolderLattice X<VAR>x y : X<GOAL>JordanHolderLattice.IsMaximal x y → x < y
<VAR>X : Type u<VAR>Lattice X<VAR>self : JordanHolderLattice X<VAR>x y : X × X<GOAL>JordanHolderLattice.Iso x y → JordanHolderLattice.Iso y x
<VAR>X : Type u<VAR>Lattice X<VAR>self : JordanHolderLattice X<VAR>x y z : X × X<GOAL>JordanHolderLattice.Iso x y → JordanHolderLattice.Iso y z → JordanHolderLattice.Iso x z
<VAR>X : Type u<VAR>Lattice X<VAR>JordanHolderLattice X<VAR>x y : X<VAR>hxz : JordanHolderLattice.IsMaximal x (x ⊔ y)<VAR>hyz : JordanHolderLattice.IsMaximal y (x ⊔ y)<GOAL>JordanHolderLattice.IsMaximal (x ⊓ y) y
<VAR>X : Type u<VAR>Lattice X<VAR>JordanHolderLattice X<VAR>x b : X<VAR>a y : X<VAR>ha : x ⊓ y = a<VAR>hxy : x ≠ y<VAR>hxb : JordanHolderLattice.IsMaximal x b<VAR>hyb : JordanHolderLattice.IsMaximal y b<GOAL>JordanHolderLattice.IsMaximal a y
<VAR>X : Type u<VAR>Lattice X<VAR>JordanHolderLattice X<VAR>x y a b : X<VAR>hm : JordanHolderLattice.IsMaximal x a<VAR>ha : x ⊔ y = a<VAR>hb : x ⊓ y = b<GOAL>JordanHolderLattice.Iso (x, a) (b, y)
<VAR>X : Type u<VAR>Lattice X<VAR>JordanHolderLattice X<VAR>x y : X<VAR>h : JordanHolderLattice.IsMaximal x y<GOAL>JordanHolderLattice.Iso (x, y) (x, y)
<VAR>X : Type u<VAR>Lattice X<VAR>JordanHolderLattice X<VAR>s : CompositionSeries X<VAR>i : Fin s.length<GOAL>s.toFun i.castSucc < s.toFun i.succ
<VAR>X : Type u<VAR>Lattice X<VAR>JordanHolderLattice X<VAR>s : CompositionSeries X<GOAL>StrictMono s.toFun
<VAR>X : Type u<VAR>Lattice X<VAR>JordanHolderLattice X<VAR>s : CompositionSeries X<GOAL>Function.Injective s.toFun
<VAR>X : Type u<VAR>Lattice X<VAR>JordanHolderLattice X<VAR>s : CompositionSeries X<VAR>i j : Fin s.length.succ<GOAL>s.toFun i = s.toFun j ↔ i = j
<VAR>X : Type u<VAR>Lattice X<VAR>JordanHolderLattice X<VAR>s : CompositionSeries X<VAR>x y : X<VAR>hx : x ∈ s<VAR>hy : y ∈ s<GOAL>x ≤ y ∨ y ≤ x
<VAR>X : Type u<VAR>Lattice X<VAR>JordanHolderLattice X<VAR>s : CompositionSeries X<GOAL>List.Sorted (fun x x_1 => x < x_1) (RelSeries.toList s)
<VAR>X : Type u<VAR>Lattice X<VAR>JordanHolderLattice X<VAR>s : CompositionSeries X<GOAL>(RelSeries.toList s).Nodup
<VAR>X : Type u<VAR>Lattice X<VAR>JordanHolderLattice X<VAR>s₁ s₂ : CompositionSeries X<VAR>h : ∀ (x : X), x ∈ s₁ ↔ x ∈ s₂<GOAL>s₁ = s₂
<VAR>X : Type u<VAR>Lattice X<VAR>JordanHolderLattice X<VAR>s : CompositionSeries X<VAR>i : Fin (s.length + 1)<GOAL>s.toFun i ≤ RelSeries.last s
<VAR>X : Type u<VAR>Lattice X<VAR>JordanHolderLattice X<VAR>s : CompositionSeries X<VAR>x : X<VAR>hx : x ∈ s<GOAL>x ≤ RelSeries.last s
<VAR>X : Type u<VAR>Lattice X<VAR>JordanHolderLattice X<VAR>s : CompositionSeries X<VAR>i : Fin (s.length + 1)<GOAL>RelSeries.head s ≤ s.toFun i
<VAR>X : Type u<VAR>Lattice X<VAR>JordanHolderLattice X<VAR>s : CompositionSeries X<VAR>x : X<VAR>hx : x ∈ s<GOAL>RelSeries.head s ≤ x
<VAR>X : Type u<VAR>Lattice X<VAR>JordanHolderLattice X<VAR>s : CompositionSeries X<GOAL>(RelSeries.eraseLast s).last ≤ RelSeries.last s
<VAR>X : Type u<VAR>Lattice X<VAR>JordanHolderLattice X<VAR>s : CompositionSeries X<VAR>x : X<VAR>hx : x ≠ RelSeries.last s<VAR>hxs : x ∈ s<GOAL>x ∈ RelSeries.eraseLast s
<VAR>X : Type u<VAR>Lattice X<VAR>JordanHolderLattice X<VAR>s : CompositionSeries X<VAR>x : X<VAR>h : 0 < s.length<GOAL>x ∈ RelSeries.eraseLast s ↔ x ≠ RelSeries.last s ∧ x ∈ s
<VAR>X : Type u<VAR>Lattice X<VAR>JordanHolderLattice X<VAR>s : CompositionSeries X<VAR>x : X<VAR>h : 0 < s.length<VAR>hx : x ∈ RelSeries.eraseLast s<GOAL>x < RelSeries.last s
<VAR>X : Type u<VAR>Lattice X<VAR>JordanHolderLattice X<VAR>s : CompositionSeries X<VAR>h : 0 < s.length<GOAL>JordanHolderLattice.IsMaximal (RelSeries.eraseLast s).last (RelSeries.last s)
<VAR>X : Type u<VAR>Lattice X<VAR>JordanHolderLattice X<VAR>s : CompositionSeries X<VAR>h : 0 < s.length<GOAL>s = (RelSeries.eraseLast s).snoc (RelSeries.last s) ⋯
<VAR>X : Type u<VAR>Lattice X<VAR>JordanHolderLattice X<VAR>s : CompositionSeries X<VAR>h : JordanHolderLattice.IsMaximal (RelSeries.eraseLast s).last (RelSeries.last s)<GOAL>(RelSeries.eraseLast s).snoc (RelSeries.last s) h = s
<VAR>X : Type u<VAR>Lattice X<VAR>JordanHolderLattice X<VAR>s : CompositionSeries X<GOAL>s.Equivalent s
<VAR>X : Type u<VAR>Lattice X<VAR>JordanHolderLattice X<VAR>s₁ s₂ : CompositionSeries X<VAR>h : s₁.Equivalent s₂<GOAL>s₂.Equivalent s₁
<VAR>X : Type u<VAR>Lattice X<VAR>JordanHolderLattice X<VAR>s₁ s₂ s₃ : CompositionSeries X<VAR>h₁ : s₁.Equivalent s₂<VAR>h₂ : s₂.Equivalent s₃<GOAL>s₁.Equivalent s₃
<VAR>X : Type u<VAR>Lattice X<VAR>JordanHolderLattice X<VAR>s₁ s₂ t₁ t₂ : CompositionSeries X<VAR>hs : RelSeries.last s₁ = RelSeries.head s₂<VAR>ht : RelSeries.last t₁ = RelSeries.head t₂<VAR>h₁ : s₁.Equivalent t₁<VAR>h₂ : s₂.Equivalent t₂<GOAL>CompositionSeries.Equivalent (RelSeries.smash s₁ s₂ hs) (RelSeries.smash t₁ t₂ ht)
<VAR>X : Type u<VAR>Lattice X<VAR>JordanHolderLattice X<VAR>s₁ s₂ : CompositionSeries X<VAR>x₁ x₂ : X<VAR>hsat₁ : JordanHolderLattice.IsMaximal (RelSeries.last s₁) x₁<VAR>hsat₂ : JordanHolderLattice.IsMaximal (RelSeries.last s₂) x₂<VAR>hequiv : s₁.Equivalent s₂<VAR>hlast : JordanHolderLattice.Iso (RelSeries.last s₁, x₁) (RelSeries.last s₂, x₂)<GOAL>CompositionSeries.Equivalent (RelSeries.snoc s₁ x₁ hsat₁) (RelSeries.snoc s₂ x₂ hsat₂)
<VAR>X : Type u<VAR>Lattice X<VAR>JordanHolderLattice X<VAR>s₁ s₂ : CompositionSeries X<VAR>h : s₁.Equivalent s₂<GOAL>s₁.length = s₂.length
<VAR>X : Type u<VAR>Lattice X<VAR>JordanHolderLattice X<VAR>s : CompositionSeries X<VAR>x₁ x₂ y₁ y₂ : X<VAR>hsat₁ : JordanHolderLattice.IsMaximal (RelSeries.last s) x₁<VAR>hsat₂ : JordanHolderLattice.IsMaximal (RelSeries.last s) x₂<VAR>hsaty₁ : JordanHolderLattice.IsMaximal (RelSeries.snoc s x₁ hsat₁).last y₁<VAR>hsaty₂ : JordanHolderLattice.IsMaximal (RelSeries.snoc s x₂ hsat₂).last y₂<VAR>hr₁ : JordanHolderLattice.Iso (RelSeries.last s, x₁) (x₂, y₂)<VAR>hr₂ : JordanHolderLattice.Iso (x₁, y₁) (RelSeries.last s, x₂)<GOAL>CompositionSeries.Equivalent ((RelSeries.snoc s x₁ hsat₁).snoc y₁ hsaty₁) ((RelSeries.snoc s x₂ hsat₂).snoc y₂ hsaty₂)
<VAR>X : Type u<VAR>Lattice X<VAR>JordanHolderLattice X<VAR>s₁ s₂ : CompositionSeries X<VAR>hb : RelSeries.head s₁ = RelSeries.head s₂<VAR>ht : RelSeries.last s₁ = RelSeries.last s₂<VAR>hs₁ : s₁.length = 0<GOAL>s₂.length = 0
<VAR>X : Type u<VAR>Lattice X<VAR>JordanHolderLattice X<VAR>s₁ s₂ : CompositionSeries X<VAR>hb : RelSeries.head s₁ = RelSeries.head s₂<VAR>ht : RelSeries.last s₁ = RelSeries.last s₂<GOAL>0 < s₁.length → 0 < s₂.length
<VAR>X : Type u<VAR>Lattice X<VAR>JordanHolderLattice X<VAR>s₁ s₂ : CompositionSeries X<VAR>hb : RelSeries.head s₁ = RelSeries.head s₂<VAR>ht : RelSeries.last s₁ = RelSeries.last s₂<VAR>hs₁0 : s₁.length = 0<GOAL>s₁ = s₂
<VAR>X : Type u<VAR>Lattice X<VAR>JordanHolderLattice X<VAR>s : CompositionSeries X<VAR>x : X<VAR>hm : JordanHolderLattice.IsMaximal x (RelSeries.last s)<VAR>hb : RelSeries.head s ≤ x<GOAL>∃ t, RelSeries.head t = RelSeries.head s ∧ t.length + 1 = s.length ∧ ∃ (htx : RelSeries.last t = x), s.Equivalent (RelSeries.snoc t (RelSeries.last s) ⋯)
<VAR>X : Type u<VAR>Lattice X<VAR>JordanHolderLattice X<VAR>s₁ s₂ : CompositionSeries X<VAR>hb : RelSeries.head s₁ = RelSeries.head s₂<VAR>ht : RelSeries.last s₁ = RelSeries.last s₂<GOAL>s₁.Equivalent s₂
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → Preorder (α i)<VAR>x : (i : ι) → α i<GOAL>(Set.univ.pi fun i => Set.Ici (x i)) = Set.Ici x
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → Preorder (α i)<VAR>x : (i : ι) → α i<GOAL>(Set.univ.pi fun i => Set.Iic (x i)) = Set.Iic x
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → Preorder (α i)<VAR>x y : (i : ι) → α i<GOAL>(Set.univ.pi fun i => Set.Icc (x i) (y i)) = Set.Icc x y
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → Preorder (α i)<VAR>s : Set ι<VAR>(j : ι) → Decidable (j ∈ s)<VAR>f₁ f₂ g₁ g₂ : (i : ι) → α i<VAR>h₁ : ∀ i ∈ s, f₁ i ∈ Set.Icc (g₁ i) (g₂ i)<VAR>h₂ : ∀ i ∉ s, f₂ i ∈ Set.Icc (g₁ i) (g₂ i)<GOAL>s.piecewise f₁ f₂ ∈ Set.Icc g₁ g₂
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → Preorder (α i)<VAR>s : Set ι<VAR>(j : ι) → Decidable (j ∈ s)<VAR>f₁ f₂ g₁ g₂ : (i : ι) → α i<VAR>h₁ : f₁ ∈ Set.Icc g₁ g₂<VAR>h₂ : f₂ ∈ Set.Icc g₁ g₂<GOAL>s.piecewise f₁ f₂ ∈ Set.Icc g₁ g₂
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → Preorder (α i)<VAR>x : (i : ι) → α i<VAR>Nonempty ι<GOAL>(Set.univ.pi fun i => Set.Ioi (x i)) ⊆ Set.Ioi x
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → Preorder (α i)<VAR>x : (i : ι) → α i<VAR>Nonempty ι<GOAL>(Set.univ.pi fun i => Set.Iio (x i)) ⊆ Set.Iio x
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → Preorder (α i)<VAR>x y : (i : ι) → α i<VAR>Nonempty ι<GOAL>(Set.univ.pi fun i => Set.Ioo (x i) (y i)) ⊆ Set.Ioo x y
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → Preorder (α i)<VAR>x y : (i : ι) → α i<VAR>Nonempty ι<GOAL>(Set.univ.pi fun i => Set.Ioc (x i) (y i)) ⊆ Set.Ioc x y
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → Preorder (α i)<VAR>x y : (i : ι) → α i<VAR>Nonempty ι<GOAL>(Set.univ.pi fun i => Set.Ico (x i) (y i)) ⊆ Set.Ico x y
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → Preorder (α i)<VAR>DecidableEq ι<VAR>x y : (i : ι) → α i<VAR>i₀ : ι<VAR>m : α i₀<VAR>hm : x i₀ ≤ m<GOAL>(Set.univ.pi fun i => Set.Ioc (Function.update x i₀ m i) (y i)) = {z | m < z i₀} ∩ Set.univ.pi fun i => Set.Ioc (x i) (y i)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → Preorder (α i)<VAR>DecidableEq ι<VAR>x y : (i : ι) → α i<VAR>i₀ : ι<VAR>m : α i₀<VAR>hm : m ≤ y i₀<GOAL>(Set.univ.pi fun i => Set.Ioc (x i) (Function.update y i₀ m i)) = {z | z i₀ ≤ m} ∩ Set.univ.pi fun i => Set.Ioc (x i) (y i)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → Preorder (α i)<VAR>DecidableEq ι<VAR>x y : (i : ι) → α i<VAR>i₀ : ι<VAR>m : α i₀<GOAL>Disjoint (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))
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>DecidableEq ι<VAR>(i : ι) → PartialOrder (α i)<VAR>f : (i : ι) → α i<VAR>i : ι<VAR>a b : α i<GOAL>Function.update f i '' Set.Icc a b = Set.Icc (Function.update f i a) (Function.update f i b)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>DecidableEq ι<VAR>(i : ι) → PartialOrder (α i)<VAR>f : (i : ι) → α i<VAR>i : ι<VAR>a b : α i<GOAL>Function.update f i '' Set.Ico a b = Set.Ico (Function.update f i a) (Function.update f i b)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>DecidableEq ι<VAR>(i : ι) → PartialOrder (α i)<VAR>f : (i : ι) → α i<VAR>i : ι<VAR>a b : α i<GOAL>Function.update f i '' Set.Ioc a b = Set.Ioc (Function.update f i a) (Function.update f i b)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>DecidableEq ι<VAR>(i : ι) → PartialOrder (α i)<VAR>f : (i : ι) → α i<VAR>i : ι<VAR>a b : α i<GOAL>Function.update f i '' Set.Ioo a b = Set.Ioo (Function.update f i a) (Function.update f i b)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>DecidableEq ι<VAR>(i : ι) → PartialOrder (α i)<VAR>f : (i : ι) → α i<VAR>i : ι<VAR>a : α i<GOAL>Function.update f i '' Set.Icc a (f i) = Set.Icc (Function.update f i a) f
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>DecidableEq ι<VAR>(i : ι) → PartialOrder (α i)<VAR>f : (i : ι) → α i<VAR>i : ι<VAR>a : α i<GOAL>Function.update f i '' Set.Ico a (f i) = Set.Ico (Function.update f i a) f
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>DecidableEq ι<VAR>(i : ι) → PartialOrder (α i)<VAR>f : (i : ι) → α i<VAR>i : ι<VAR>a : α i<GOAL>Function.update f i '' Set.Ioc a (f i) = Set.Ioc (Function.update f i a) f
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>DecidableEq ι<VAR>(i : ι) → PartialOrder (α i)<VAR>f : (i : ι) → α i<VAR>i : ι<VAR>a : α i<GOAL>Function.update f i '' Set.Ioo a (f i) = Set.Ioo (Function.update f i a) f
<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.Icc (f i) b = Set.Icc f (Function.update f i b)
<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.Ico (f i) b = Set.Ico f (Function.update f i b)
<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.Ioc (f i) b = Set.Ioc f (Function.update f i b)