ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>δ : Type u_7<VAR>m : α → β → γ<VAR>f : Filter α<VAR>g : Filter β<VAR>n : γ → δ<VAR>m' : α' → β' → δ<VAR>n₁ : α → α'<VAR>n₂ : β → β'<VAR>h_distrib : ∀ (a : α) (b : β), n (m a b) = m' (n₁ a) (n₂ b)<GOAL>Filter.map n (Filter.map₂ m f g) = Filter.map₂ m' (Filter.map n₁ f) (Filter.map n₂ g)
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>δ : Type u_7<VAR>m : α → β → γ<VAR>f : Filter α<VAR>g : Filter β<VAR>n : γ → δ<VAR>m' : α' → β → δ<VAR>n' : α → α'<VAR>h_distrib : ∀ (a : α) (b : β), n (m a b) = m' (n' a) b<GOAL>Filter.map n (Filter.map₂ m f g) = Filter.map₂ m' (Filter.map n' f) g
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>δ : Type u_7<VAR>m : α → β → γ<VAR>f : Filter α<VAR>g : Filter β<VAR>n : γ → δ<VAR>m' : α → β' → δ<VAR>n' : β → β'<VAR>h_distrib : ∀ (a : α) (b : β), n (m a b) = m' a (n' b)<GOAL>Filter.map n (Filter.map₂ m f g) = Filter.map₂ m' f (Filter.map n' g)
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>δ : Type u_7<VAR>f : Filter α<VAR>g : Filter β<VAR>m : α' → β → γ<VAR>n : α → α'<VAR>m' : α → β → δ<VAR>n' : δ → γ<VAR>h_left_comm : ∀ (a : α) (b : β), m (n a) b = n' (m' a b)<GOAL>Filter.map₂ m (Filter.map n f) g = Filter.map n' (Filter.map₂ m' f g)
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>δ : Type u_7<VAR>f : Filter α<VAR>g : Filter β<VAR>m : α → β' → γ<VAR>n : β → β'<VAR>m' : α → β → δ<VAR>n' : δ → γ<VAR>h_right_comm : ∀ (a : α) (b : β), m a (n b) = n' (m' a b)<GOAL>Filter.map₂ m f (Filter.map n g) = Filter.map n' (Filter.map₂ m' f g)
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>γ' : Type u_6<VAR>δ : Type u_7<VAR>ε : Type u_9<VAR>f : Filter α<VAR>g : Filter β<VAR>h : Filter γ<VAR>m : α → δ → ε<VAR>n : β → γ → δ<VAR>m₁ : α → β → β'<VAR>m₂ : α → γ → γ'<VAR>n' : β' → γ' → ε<VAR>h_distrib : ∀ (a : α) (b : β) (c : γ), m a (n b c) = n' (m₁ a b) (m₂ a c)<GOAL>Filter.map₂ m f (Filter.map₂ n g h) ≤ Filter.map₂ n' (Filter.map₂ m₁ f g) (Filter.map₂ m₂ f h)
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>δ : Type u_7<VAR>ε : Type u_9<VAR>f : Filter α<VAR>g : Filter β<VAR>h : Filter γ<VAR>m : δ → γ → ε<VAR>n : α → β → δ<VAR>m₁ : α → γ → α'<VAR>m₂ : β → γ → β'<VAR>n' : α' → β' → ε<VAR>h_distrib : ∀ (a : α) (b : β) (c : γ), m (n a b) c = n' (m₁ a c) (m₂ b c)<GOAL>Filter.map₂ m (Filter.map₂ n f g) h ≤ Filter.map₂ n' (Filter.map₂ m₁ f h) (Filter.map₂ m₂ g h)
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>δ : Type u_7<VAR>m : α → β → γ<VAR>f : Filter α<VAR>g : Filter β<VAR>n : γ → δ<VAR>m' : β' → α' → δ<VAR>n₁ : β → β'<VAR>n₂ : α → α'<VAR>h_antidistrib : ∀ (a : α) (b : β), n (m a b) = m' (n₁ b) (n₂ a)<GOAL>Filter.map n (Filter.map₂ m f g) = Filter.map₂ m' (Filter.map n₁ g) (Filter.map n₂ f)
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>δ : Type u_7<VAR>m : α → β → γ<VAR>f : Filter α<VAR>g : Filter β<VAR>n : γ → δ<VAR>m' : β' → α → δ<VAR>n' : β → β'<VAR>h_antidistrib : ∀ (a : α) (b : β), n (m a b) = m' (n' b) a<GOAL>Filter.map n (Filter.map₂ m f g) = Filter.map₂ m' (Filter.map n' g) f
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>δ : Type u_7<VAR>m : α → β → γ<VAR>f : Filter α<VAR>g : Filter β<VAR>n : γ → δ<VAR>m' : β → α' → δ<VAR>n' : α → α'<VAR>h_antidistrib : ∀ (a : α) (b : β), n (m a b) = m' b (n' a)<GOAL>Filter.map n (Filter.map₂ m f g) = Filter.map₂ m' g (Filter.map n' f)
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>δ : Type u_7<VAR>f : Filter α<VAR>g : Filter β<VAR>m : α' → β → γ<VAR>n : α → α'<VAR>m' : β → α → δ<VAR>n' : δ → γ<VAR>h_left_anticomm : ∀ (a : α) (b : β), m (n a) b = n' (m' b a)<GOAL>Filter.map₂ m (Filter.map n f) g = Filter.map n' (Filter.map₂ m' g f)
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>δ : Type u_7<VAR>f : Filter α<VAR>g : Filter β<VAR>m : α → β' → γ<VAR>n : β → β'<VAR>m' : β → α → δ<VAR>n' : δ → γ<VAR>h_right_anticomm : ∀ (a : α) (b : β), m a (n b) = n' (m' b a)<GOAL>Filter.map₂ m f (Filter.map n g) = Filter.map n' (Filter.map₂ m' g f)
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>f : α → β → β<VAR>a : α<VAR>h : ∀ (b : β), f a b = b<VAR>l : Filter β<GOAL>Filter.map₂ f (pure a) l = l
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>f : α → β → α<VAR>b : β<VAR>h : ∀ (a : α), f a b = a<VAR>l : Filter α<GOAL>Filter.map₂ f l (pure b) = l
<VAR>α : Type u_2<VAR>Preorder α<VAR>a b c : α<GOAL>b ≤ c → a ≤ b → a ≤ c
<VAR>α : Type u_2<VAR>Preorder α<VAR>a b c : α<GOAL>b < c → a < b → a < c
<VAR>α : Type u_2<VAR>Preorder α<VAR>a b c : α<GOAL>b ≤ c → a < b → a < c
<VAR>α : Type u_2<VAR>Preorder α<VAR>a b c : α<GOAL>b < c → a ≤ b → a < c
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>a b : α<GOAL>a ≤ b → b ≤ a → b = a
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>a b : α<GOAL>a ≤ b → b ≠ a → a < b
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>a b : α<GOAL>a ≠ b → a ≤ b → a < b
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>a b : α<GOAL>b ≠ a → a ≤ b → a < b
<VAR>α : Type u_2<VAR>Preorder α<VAR>x : α<GOAL>x < x ↔ False
<VAR>α : Type u_2<VAR>Preorder α<VAR>a b c : α<GOAL>b ≤ c → a = b → a ≤ c
<VAR>α : Type u_2<VAR>Preorder α<VAR>a b c : α<GOAL>b = c → a ≤ b → a ≤ c
<VAR>α : Type u_2<VAR>Preorder α<VAR>a b c : α<GOAL>b < c → a = b → a < c
<VAR>α : Type u_2<VAR>Preorder α<VAR>a b c : α<GOAL>b = c → a < b → a < c
<VAR>α : Type u_2<VAR>Preorder α<VAR>x y : α<VAR>h : x = y<GOAL>y ≤ x
<VAR>α : Type u_2<VAR>Preorder α<VAR>x y : α<VAR>h : x = y<GOAL>¬x < y
<VAR>α : Type u_2<VAR>Preorder α<VAR>x y : α<VAR>h : x = y<GOAL>¬y < x
<VAR>α : Type u_2<VAR>Preorder α<VAR>a b : α<VAR>Subsingleton α<GOAL>a ≤ b
<VAR>α : Type u_2<VAR>Preorder α<VAR>a b : α<VAR>Subsingleton α<GOAL>¬a < b
<VAR>α : Type u_2<VAR>LE α<VAR>x y : α<VAR>h : x ≤ y<GOAL>y ≥ x
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>a b : α<VAR>h : a ≤ b<GOAL>a < b ↔ a ≠ b
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>a b : α<VAR>h : a ≤ b<GOAL>a < b ↔ b ≠ a
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>a b : α<VAR>h : a ≤ b<GOAL>¬a < b ↔ a = b
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>a b : α<VAR>h : a ≤ b<GOAL>¬a < b ↔ b = a
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>a b : α<VAR>h : a ≤ b<GOAL>b ≤ a ↔ b = a
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>a b : α<VAR>h : a ≤ b<GOAL>b ≤ a ↔ a = b
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>a b : α<VAR>h : a ≤ b<VAR>c : α<GOAL>a < c ∨ c ≤ b
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>a b : α<VAR>h : a ≤ b<VAR>c : α<GOAL>a ≤ c ∨ c < b
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>a b : α<VAR>h : a ≤ b<VAR>c : α<GOAL>a ≤ c ∨ c ≤ b
<VAR>α : Type u_2<VAR>LT α<VAR>x y : α<VAR>h : x < y<GOAL>y > x
<VAR>α : Type u_2<VAR>Preorder α<VAR>x : α<GOAL>x < x → False
<VAR>α : Type u_2<VAR>Preorder α<VAR>x y : α<VAR>h : x < y<GOAL>y ≠ x
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>x y : α<VAR>h : x < y<VAR>z : α<GOAL>x < z ∨ z < y
<VAR>α : Type u_2<VAR>LE α<VAR>x y : α<VAR>h : x ≥ y<GOAL>y ≤ x
<VAR>α : Type u_2<VAR>LT α<VAR>x y : α<VAR>h : x > y<GOAL>y < x
<VAR>α : Type u_2<VAR>Preorder α<VAR>a b : α<VAR>h : a = b<GOAL>a ≥ b
<VAR>α : Type u_2<VAR>Preorder α<VAR>a b : α<VAR>h : a < b<GOAL>¬b ≤ a
<VAR>α : Type u_2<VAR>Preorder α<VAR>a b : α<VAR>h : a ≤ b<GOAL>¬b < a
<VAR>α : Type u_2<VAR>Preorder α<VAR>a b : α<VAR>h : ¬a ≤ b<GOAL>a ≠ b
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>DecidableRel fun x x_1 => x ≤ x_1<VAR>a b : α<GOAL>a ≤ b ↔ a = b ∨ a < b
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>a b : α<GOAL>a ≤ b ↔ a = b ∨ a < b
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>a b : α<GOAL>a < b ↔ a ≤ b ∧ a ≠ b
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>x y : α<GOAL>x ≤ y → y = x ↔ ¬x < y
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>DecidableRel fun x x_1 => x ≤ x_1<VAR>a b : α<GOAL>a = b ↔ a ≤ b ∧ ¬a < b
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>a b : α<GOAL>a = b ↔ a ≤ b ∧ ¬a < b
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>a b : α<VAR>h : a ≤ b<GOAL>a = b ∨ a < b
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>a b : α<VAR>h : a ≤ b<GOAL>b = a ∨ a < b
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>a b : α<VAR>h : a ≤ b<GOAL>a < b ∨ b = a
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>a b : α<VAR>hab : a ≤ b<VAR>hba : ¬a < b<GOAL>a = b
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>a b : α<VAR>hab : a ≤ b<VAR>hba : ¬a < b<GOAL>b = a
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>a b : α<VAR>h : a ≠ b<GOAL>a ≤ b ↔ a < b
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>a b : α<VAR>h : a ≠ b<GOAL>¬a ≤ b ∨ ¬b ≤ a
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>DecidableEq α<VAR>a b : α<GOAL>(a ≠ b ↔ a < b) ↔ a ≤ b
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>a b : α<GOAL>(a ≠ b ↔ a < b) ↔ a ≤ b
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>a b : α<GOAL>min a b = if b ≤ a then b else a
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>a b : α<GOAL>max a b = if b ≤ a then a else b
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>a b : α<VAR>h : ¬b ≤ a<GOAL>a < b
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>x y : α<GOAL>x < y ↔ ¬y ≤ x
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>x y : α<VAR>h : x ≠ y<GOAL>x < y ∨ y < x
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>x y : α<GOAL>x < y ∨ y < x ↔ x ≠ y
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>a b : α<GOAL>¬a < b ↔ a = b ∨ b < a
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>a b : α<GOAL>∃ c, a ≤ c ∧ b ≤ c
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>p q : α → Prop<GOAL>(∃ i, ∀ (j : α), j ≥ i → p j) → (∃ i, ∀ (j : α), j ≥ i → q j) → ∃ i, ∀ (j : α), j ≥ i → p j ∧ q j
<VAR>α : Type u_2<VAR>β : Type u_5<VAR>LinearOrder α<VAR>Preorder β<VAR>a b : α<VAR>c d : β<VAR>H : a ≤ b → c ≤ d<VAR>h : d < c<GOAL>b < a
<VAR>α : Type u_2<VAR>β : Type u_5<VAR>LinearOrder α<VAR>LinearOrder β<VAR>a b : α<VAR>c d : β<GOAL>a ≤ b → c ≤ d ↔ d < c → b < a
<VAR>α : Type u_2<VAR>β : Type u_5<VAR>Preorder α<VAR>Preorder β<VAR>a b : α<VAR>c d : β<VAR>H : a ≤ b ↔ c ≤ d<VAR>H' : b ≤ a ↔ d ≤ c<GOAL>b < a ↔ d < c
<VAR>α : Type u_2<VAR>β : Type u_5<VAR>LinearOrder α<VAR>LinearOrder β<VAR>a b : α<VAR>c d : β<VAR>H : a ≤ b ↔ c ≤ d<GOAL>b < a ↔ d < c
<VAR>α : Type u_2<VAR>β : Type u_5<VAR>LinearOrder α<VAR>LinearOrder β<VAR>a b : α<VAR>c d : β<GOAL>(a ≤ b ↔ c ≤ d) ↔ (b < a ↔ d < c)
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>a b : α<VAR>H : ∀ (c : α), c ≤ a ↔ c ≤ b<GOAL>a = b
<VAR>α : Type u_2<VAR>Preorder α<VAR>a b : α<VAR>H : ∀ (c : α), c ≤ a → c ≤ b<GOAL>a ≤ b
<VAR>α : Type u_2<VAR>Preorder α<VAR>a b : α<VAR>H : ∀ (c : α), a ≤ c → b ≤ c<GOAL>b ≤ a
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>a b : α<VAR>H : ∀ (c : α), c < a → c < b<GOAL>a ≤ b
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>a b : α<GOAL>(∀ ⦃c : α⦄, c < a → c < b) ↔ a ≤ b
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>a b : α<VAR>H : ∀ (c : α), a < c → b < c<GOAL>b ≤ a
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>a b : α<GOAL>(∀ ⦃c : α⦄, a < c → b < c) ↔ b ≤ a
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>a b : α<VAR>H : ∀ (c : α), a ≤ c ↔ b ≤ c<GOAL>a = b
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>a b : α<VAR>h : ∀ (c : α), c < a ↔ c < b<GOAL>a = b
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>a b : α<VAR>h : ∀ (c : α), a < c ↔ b < c<GOAL>a = b
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>PartialOrder β<VAR>r : α → α → Prop<VAR>IsSymm α r<VAR>f : α → β<VAR>h : ∀ (a b : α), r a b → f a ≤ f b<VAR>a b : α<GOAL>r a b → f a = f b
<VAR>α : Type u_2<VAR>a b c d : α<VAR>Preorder α<VAR>hca : c ≤ a<VAR>hbd : b ≤ d<GOAL>a ≤ b → c ≤ d
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>PartialOrder α<VAR>f : β → β → α<VAR>comm : ∀ (a b : β), f a b ≤ f b a<VAR>a b : β<GOAL>f a b = f b a
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>f : α → α → α<VAR>comm : Commutative f<VAR>assoc : ∀ (a b c : α), f (f a b) c ≤ f a (f b c)<GOAL>Associative f
<VAR>α : Type u_2<GOAL>Function.Injective (@Preorder.toLE α)
<VAR>α : Type u_2<GOAL>Function.Injective (@PartialOrder.toPreorder α)
<VAR>α : Type u_2<GOAL>Function.Injective (@LinearOrder.toPartialOrder α)
<VAR>α : Type u_2<VAR>A B : Preorder α<VAR>H : ∀ (x y : α), x ≤ y ↔ x ≤ y<GOAL>A = B
<VAR>α : Type u_2<VAR>A B : PartialOrder α<VAR>H : ∀ (x y : α), x ≤ y ↔ x ≤ y<GOAL>A = B
<VAR>α : Type u_2<VAR>A B : LinearOrder α<VAR>H : ∀ (x y : α), x ≤ y ↔ x ≤ y<GOAL>A = B
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>P : Sort u_5<VAR>x y : α<VAR>h : x < y<VAR>h₁ : x < y → P<VAR>h₂ : x = y → P<VAR>h₃ : y < x → P<GOAL>ltByCases x y h₁ h₂ h₃ = h₁ h
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>P : Sort u_5<VAR>x y : α<VAR>h : y < x<VAR>h₁ : x < y → P<VAR>h₂ : x = y → P<VAR>h₃ : y < x → P<GOAL>ltByCases x y h₁ h₂ h₃ = h₃ h
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>P : Sort u_5<VAR>x y : α<VAR>h : x = y<VAR>h₁ : x < y → P<VAR>h₂ : x = y → P<VAR>h₃ : y < x → P<GOAL>ltByCases x y h₁ h₂ h₃ = h₂ h
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>P : Sort u_5<VAR>x y : α<VAR>h : ¬x < y<VAR>h₁ : x < y → P<VAR>h₂ : x = y → P<VAR>h₃ : y < x → P<VAR>p : ¬y < x → x = y := ⋯<GOAL>ltByCases x y h₁ h₂ h₃ = if h' : y < x then h₃ h' else h₂ ⋯
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>P : Sort u_5<VAR>x y : α<VAR>h : ¬y < x<VAR>h₁ : x < y → P<VAR>h₂ : x = y → P<VAR>h₃ : y < x → P<VAR>p : ¬x < y → x = y := ⋯<GOAL>ltByCases x y h₁ h₂ h₃ = if h' : x < y then h₁ h' else h₂ ⋯
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>P : Sort u_5<VAR>x y : α<VAR>h : x ≠ y<VAR>h₁ : x < y → P<VAR>h₂ : x = y → P<VAR>h₃ : y < x → P<VAR>p : ¬x < y → y < x := ⋯<GOAL>ltByCases x y h₁ h₂ h₃ = if h' : x < y then h₁ h' else h₃ ⋯
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>P : Sort u_5<VAR>x y : α<VAR>h₁ : x < y → P<VAR>h₂ : x = y → P<VAR>h₃ : y < x → P<VAR>p : y = x → x = y := ⋯<GOAL>ltByCases x y h₁ h₂ h₃ = ltByCases y x h₃ (h₂ ∘ p) h₁
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>x y x' y' : α<VAR>ltc : x < y ↔ x' < y'<VAR>gtc : y < x ↔ y' < x'<GOAL>x = y ↔ x' = y'
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>P : Sort u_5<VAR>x y : α<VAR>h₁ : x < y → P<VAR>h₂ : x = y → P<VAR>h₃ : y < x → P<VAR>p : P<VAR>hlt : ∀ (h : x < y), h₁ h = p<VAR>heq : ∀ (h : x = y), h₂ h = p<VAR>hgt : ∀ (h : y < x), h₃ h = p<GOAL>ltByCases x y h₁ h₂ h₃ = p
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>P : Sort u_5<VAR>x y : α<VAR>h₁ : x < y → P<VAR>h₂ : x = y → P<VAR>h₃ : y < x → P<VAR>p : P<GOAL>ltByCases x y h₁ h₂ h₃ = p ↔ (∃ h, h₁ h = p) ∨ (∃ h, h₂ h = p) ∨ ∃ h, h₃ h = p
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>P : Sort u_5<VAR>x y x' y' : α<VAR>h₁ : x < y → P<VAR>h₂ : x = y → P<VAR>h₃ : y < x → P<VAR>h₁' : x' < y' → P<VAR>h₂' : x' = y' → P<VAR>h₃' : y' < x' → P<VAR>ltc : x < y ↔ x' < y'<VAR>gtc : y < x ↔ y' < x'<VAR>hh'₁ : ∀ (h : x' < y'), h₁ ⋯ = h₁' h<VAR>hh'₂ : ∀ (h : x' = y'), h₂ ⋯ = h₂' h<VAR>hh'₃ : ∀ (h : y' < x'), h₃ ⋯ = h₃' h<GOAL>ltByCases x y h₁ h₂ h₃ = ltByCases x' y' h₁' h₂' h₃'
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>P : Sort u_5<VAR>x y : α<VAR>p q r : P<VAR>h : x < y<GOAL>ltTrichotomy x y p q r = p
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>P : Sort u_5<VAR>x y : α<VAR>p q r : P<VAR>h : y < x<GOAL>ltTrichotomy x y p q r = r
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>P : Sort u_5<VAR>x y : α<VAR>p q r : P<VAR>h : x = y<GOAL>ltTrichotomy x y p q r = q
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>P : Sort u_5<VAR>x y : α<VAR>p q r : P<VAR>h : ¬x < y<GOAL>ltTrichotomy x y p q r = if y < x then r else q
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>P : Sort u_5<VAR>x y : α<VAR>p q r : P<VAR>h : ¬y < x<GOAL>ltTrichotomy x y p q r = if x < y then p else q
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>P : Sort u_5<VAR>x y : α<VAR>p q r : P<VAR>h : x ≠ y<GOAL>ltTrichotomy x y p q r = if x < y then p else r
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>P : Sort u_5<VAR>x y : α<VAR>p q r : P<GOAL>ltTrichotomy x y p q r = ltTrichotomy y x r q p
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>P : Sort u_5<VAR>x y : α<VAR>p : P<GOAL>ltTrichotomy x y p p p = p
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>P : Sort u_5<VAR>x y : α<VAR>p q r s : P<GOAL>ltTrichotomy x y p q r = s ↔ x < y ∧ p = s ∨ x = y ∧ q = s ∨ y < x ∧ r = s
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>P : Sort u_5<VAR>x y : α<VAR>p q r : P<VAR>x' y' : α<VAR>p' q' r' : P<VAR>ltc : x < y ↔ x' < y'<VAR>gtc : y < x ↔ y' < x'<VAR>hh'₁ : x' < y' → p = p'<VAR>hh'₂ : x' = y' → q = q'<VAR>hh'₃ : y' < x' → r = r'<GOAL>ltTrichotomy x y p q r = ltTrichotomy x' y' p' q' r'
<VAR>α : Type u_5<VAR>H : Preorder α<GOAL>OrderDual.instPreorder αᵒᵈ = H
<VAR>α : Type u_5<VAR>H : PartialOrder α<GOAL>OrderDual.instPartialOrder αᵒᵈ = H
<VAR>α : Type u_5<VAR>H : LinearOrder α<GOAL>OrderDual.instLinearOrder αᵒᵈ = H
<VAR>ι : Type u_1<VAR>π : ι → Type u_4<VAR>(i : ι) → HasCompl (π i)<VAR>x : (i : ι) → π i<GOAL>xᶜ = fun i => (x i)ᶜ
<VAR>ι : Type u_1<VAR>π : ι → Type u_4<VAR>(i : ι) → HasCompl (π i)<VAR>x : (i : ι) → π i<VAR>i : ι<GOAL>xᶜ i = (x i)ᶜ
<VAR>ι : Type u_1<VAR>π : ι → Type u_4<VAR>(i : ι) → LE (π i)<VAR>x y : (i : ι) → π i<GOAL>x ≤ y ↔ ∀ (i : ι), x i ≤ y i
<VAR>ι : Type u_1<VAR>π : ι → Type u_4<VAR>(i : ι) → Preorder (π i)<VAR>x y : (i : ι) → π i<GOAL>x < y ↔ x ≤ y ∧ ∃ i, x i < y i
<VAR>β : Type u_3<VAR>α₁ : Type u_5<VAR>α₂ : Type u_6<VAR>LE β<VAR>u₁ v₁ : α₁ → β<VAR>u₂ v₂ : α₂ → β<GOAL>Sum.elim u₁ u₂ ≤ Sum.elim v₁ v₂ ↔ u₁ ≤ v₁ ∧ u₂ ≤ v₂
<VAR>β : Type u_3<VAR>α₁ : Type u_5<VAR>α₂ : Type u_6<VAR>LE β<VAR>b : β<VAR>v₁ : α₁ → β<VAR>v₂ : α₂ → β<GOAL>Function.const (α₁ ⊕ α₂) b ≤ Sum.elim v₁ v₂ ↔ Function.const α₁ b ≤ v₁ ∧ Function.const α₂ b ≤ v₂
<VAR>β : Type u_3<VAR>α₁ : Type u_5<VAR>α₂ : Type u_6<VAR>LE β<VAR>b : β<VAR>u₁ : α₁ → β<VAR>u₂ : α₂ → β<GOAL>Sum.elim u₁ u₂ ≤ Function.const (α₁ ⊕ α₂) b ↔ u₁ ≤ Function.const α₁ b ∧ u₂ ≤ Function.const α₂ b
<VAR>ι : Type u_1<VAR>π : ι → Type u_4<VAR>(i : ι) → Preorder (π i)<VAR>a b : (i : ι) → π i<VAR>h : StrongLT a b<GOAL>a ≤ b
<VAR>ι : Type u_1<VAR>π : ι → Type u_4<VAR>(i : ι) → Preorder (π i)<VAR>a b : (i : ι) → π i<VAR>Nonempty ι<VAR>h : StrongLT a b<GOAL>a < b
<VAR>ι : Type u_1<VAR>π : ι → Type u_4<VAR>(i : ι) → Preorder (π i)<VAR>a b c : (i : ι) → π i<VAR>hab : StrongLT a b<VAR>hbc : b ≤ c<GOAL>StrongLT a c
<VAR>ι : Type u_1<VAR>π : ι → Type u_4<VAR>(i : ι) → Preorder (π i)<VAR>a b c : (i : ι) → π i<VAR>hab : a ≤ b<VAR>hbc : StrongLT b c<GOAL>StrongLT a c
<VAR>ι : Type u_1<VAR>π : ι → Type u_4<VAR>DecidableEq ι<VAR>(i : ι) → Preorder (π i)<VAR>x y : (i : ι) → π i<VAR>i : ι<VAR>a : π i<GOAL>x ≤ Function.update y i a ↔ x i ≤ a ∧ ∀ (j : ι), j ≠ i → x j ≤ y j
<VAR>ι : Type u_1<VAR>π : ι → Type u_4<VAR>DecidableEq ι<VAR>(i : ι) → Preorder (π i)<VAR>x y : (i : ι) → π i<VAR>i : ι<VAR>a : π i<GOAL>Function.update x i a ≤ y ↔ a ≤ y i ∧ ∀ (j : ι), j ≠ i → x j ≤ y j
<VAR>ι : Type u_1<VAR>π : ι → Type u_4<VAR>DecidableEq ι<VAR>(i : ι) → Preorder (π i)<VAR>x y : (i : ι) → π i<VAR>i : ι<VAR>a b : π i<GOAL>Function.update x i a ≤ Function.update y i b ↔ a ≤ b ∧ ∀ (j : ι), j ≠ i → x j ≤ y j
<VAR>ι : Type u_1<VAR>π : ι → Type u_4<VAR>DecidableEq ι<VAR>(i : ι) → Preorder (π i)<VAR>x : (i : ι) → π i<VAR>i : ι<VAR>a b : π i<GOAL>Function.update x i a ≤ Function.update x i b ↔ a ≤ b
<VAR>ι : Type u_1<VAR>π : ι → Type u_4<VAR>DecidableEq ι<VAR>(i : ι) → Preorder (π i)<VAR>x : (i : ι) → π i<VAR>i : ι<VAR>a b : π i<GOAL>Function.update x i a < Function.update x i b ↔ a < b
<VAR>ι : Type u_1<VAR>π : ι → Type u_4<VAR>DecidableEq ι<VAR>(i : ι) → Preorder (π i)<VAR>x : (i : ι) → π i<VAR>i : ι<VAR>a : π i<GOAL>x ≤ Function.update x i a ↔ x i ≤ a
<VAR>ι : Type u_1<VAR>π : ι → Type u_4<VAR>DecidableEq ι<VAR>(i : ι) → Preorder (π i)<VAR>x : (i : ι) → π i<VAR>i : ι<VAR>a : π i<GOAL>Function.update x i a ≤ x ↔ a ≤ x i
<VAR>ι : Type u_1<VAR>π : ι → Type u_4<VAR>DecidableEq ι<VAR>(i : ι) → Preorder (π i)<VAR>x : (i : ι) → π i<VAR>i : ι<VAR>a : π i<GOAL>x < Function.update x i a ↔ x i < a
<VAR>ι : Type u_1<VAR>π : ι → Type u_4<VAR>DecidableEq ι<VAR>(i : ι) → Preorder (π i)<VAR>x : (i : ι) → π i<VAR>i : ι<VAR>a : π i<GOAL>Function.update x i a < x ↔ a < x i
<VAR>ι : Type u_1<VAR>π : ι → Type u_4<VAR>(i : ι) → SDiff (π i)<VAR>x y : (i : ι) → π i<GOAL>x \ y = fun i => x i \ y i
<VAR>ι : Type u_1<VAR>π : ι → Type u_4<VAR>(i : ι) → SDiff (π i)<VAR>x y : (i : ι) → π i<VAR>i : ι<GOAL>(x \ y) i = x i \ y i
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Nonempty β<VAR>a b : α<GOAL>Function.const β a ≤ Function.const β b ↔ a ≤ b
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Nonempty β<VAR>a b : α<GOAL>Function.const β a < Function.const β b ↔ a < b
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>p : α → Prop<VAR>x y : α<VAR>hx : x ≤ y → p x<VAR>hy : y ≤ x → p y<GOAL>p (min x y)
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>p : α → Prop<VAR>x y : α<VAR>hx : y ≤ x → p x<VAR>hy : x ≤ y → p y<GOAL>p (max x y)
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>x y : α<VAR>p : α → Prop<VAR>hx : p x<VAR>hy : p y<GOAL>p (min x y)
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>x y : α<VAR>p : α → Prop<VAR>hx : p x<VAR>hy : p y<GOAL>p (max x y)
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>x y : α<GOAL>min x y = if x < y then x else y
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>x y : α<GOAL>max x y = if x < y then y else x
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>a b : α<VAR>LinearOrder β<VAR>DecidableEq α<VAR>f : α → β<VAR>inj : Function.Injective f<VAR>Decidable (a < b)<GOAL>compare (f a) (f b) = compareOfLessAndEq a b
<VAR>α : Type u_2<VAR>LE α<VAR>p : α → Prop<VAR>x y : α<VAR>hx : p x<VAR>hy : p y<GOAL>⟨x, hx⟩ ≤ ⟨y, hy⟩ ↔ x ≤ y
<VAR>α : Type u_2<VAR>LT α<VAR>p : α → Prop<VAR>x y : α<VAR>hx : p x<VAR>hy : p y<GOAL>⟨x, hx⟩ < ⟨y, hy⟩ ↔ x < y
<VAR>α : Type u_2<VAR>LE α<VAR>p : α → Prop<VAR>x y : Subtype p<GOAL>↑x ≤ ↑y ↔ x ≤ y
<VAR>α : Type u_2<VAR>LT α<VAR>p : α → Prop<VAR>x y : Subtype p<GOAL>↑x < ↑y ↔ x < y
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LE α<VAR>LE β<VAR>x y : α × β<GOAL>x ≤ y ↔ x.1 ≤ y.1 ∧ x.2 ≤ y.2
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LE α<VAR>LE β<VAR>x₁ x₂ : α<VAR>y₁ y₂ : β<GOAL>(x₁, y₁) ≤ (x₂, y₂) ↔ x₁ ≤ x₂ ∧ y₁ ≤ y₂
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LE α<VAR>LE β<VAR>x y : α × β<GOAL>x.swap ≤ y.swap ↔ x ≤ y
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>x y : α × β<GOAL>x.swap < y.swap ↔ x < y
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>a₁ a₂ : α<VAR>b : β<GOAL>(a₁, b) ≤ (a₂, b) ↔ a₁ ≤ a₂
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>a : α<VAR>b₁ b₂ : β<GOAL>(a, b₁) ≤ (a, b₂) ↔ b₁ ≤ b₂
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>a₁ a₂ : α<VAR>b : β<GOAL>(a₁, b) < (a₂, b) ↔ a₁ < a₂
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>a : α<VAR>b₁ b₂ : β<GOAL>(a, b₁) < (a, b₂) ↔ b₁ < b₂
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>x y : α × β<GOAL>x < y ↔ x.1 < y.1 ∧ x.2 ≤ y.2 ∨ x.1 ≤ y.1 ∧ x.2 < y.2
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>a₁ a₂ : α<VAR>b₁ b₂ : β<GOAL>(a₁, b₁) < (a₂, b₂) ↔ a₁ < a₂ ∧ b₁ ≤ b₂ ∨ a₁ ≤ a₂ ∧ b₁ < b₂
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>x y : α × β<VAR>h₁ : x.1 < y.1<VAR>h₂ : x.2 ≤ y.2<GOAL>x < y
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>x y : α × β<VAR>h₁ : x.1 ≤ y.1<VAR>h₂ : x.2 < y.2<GOAL>x < y
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>a₁ a₂ : α<VAR>b₁ b₂ : β<VAR>h₁ : a₁ < a₂<VAR>h₂ : b₁ ≤ b₂<GOAL>(a₁, b₁) < (a₂, b₂)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>a₁ a₂ : α<VAR>b₁ b₂ : β<VAR>h₁ : a₁ ≤ a₂<VAR>h₂ : b₁ < b₂<GOAL>(a₁, b₁) < (a₂, b₂)
<VAR>α : Type u_5<VAR>LT α<VAR>self : DenselyOrdered α<VAR>a₁ a₂ : α<GOAL>a₁ < a₂ → ∃ a, a₁ < a ∧ a < a₂
<VAR>α : Type u_2<VAR>LT α<VAR>DenselyOrdered α<VAR>a₁ a₂ : α<GOAL>a₁ < a₂ → ∃ a, a₁ < a ∧ a < a₂
<VAR>α : Type u_2<VAR>LT α<GOAL>DenselyOrdered αᵒᵈ ↔ DenselyOrdered α
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>DenselyOrdered α<VAR>a₁ a₂ : α<VAR>h : ∀ (a : α), a₂ < a → a₁ ≤ a<GOAL>a₁ ≤ a₂
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>DenselyOrdered α<VAR>a₁ a₂ : α<VAR>h₁ : a₂ ≤ a₁<VAR>h₂ : ∀ (a : α), a₂ < a → a₁ ≤ a<GOAL>a₁ = a₂
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>DenselyOrdered α<VAR>a₁ a₂ : α<VAR>h : ∀ (a₃ : α), a₃ < a₁ → a₃ ≤ a₂<GOAL>a₁ ≤ a₂
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>DenselyOrdered α<VAR>a₁ a₂ : α<VAR>h₁ : a₂ ≤ a₁<VAR>h₂ : ∀ (a₃ : α), a₃ < a₁ → a₃ ≤ a₂<GOAL>a₁ = a₂
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>a₁ a₂ : α<GOAL>(∃ a, a₁ < a ∧ a < a₂) ∨ (∀ (a : α), a₁ < a → a₂ ≤ a) ∧ ∀ (a : α), a < a₂ → a ≤ a₁
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>h : ∀ ⦃x y z : α⦄, x < y → y < z → False<VAR>x y z : α<GOAL>x = y ∨ y = z ∨ x = z
<VAR>a b : PUnit.{u_5 + 1}<GOAL>max a b = PUnit.unit
<VAR>a b : PUnit.{u_5 + 1}<GOAL>min a b = PUnit.unit
<VAR>a b : PUnit.{u_5 + 1}<GOAL>a ≤ b
<VAR>a b : PUnit.{u_5 + 1}<GOAL>¬a < b
<GOAL>(fun x x_1 => x ≤ x_1) = fun x x_1 => x → x_1