ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>Preorder α<VAR>Nonempty α<VAR>NoMinOrder α<VAR>NoMaxOrder α<GOAL>∃ f, StrictAnti f
<VAR>α : Type u<VAR>Preorder α<VAR>f : ℕ → α<VAR>hf : Monotone f<VAR>n : ℕ<VAR>x : α<VAR>h1 : f n < x<VAR>h2 : x < f (n + 1)<VAR>a : ℕ<GOAL>f a ≠ x
<VAR>α : Type u<VAR>Preorder α<VAR>f : ℕ → α<VAR>hf : Antitone f<VAR>n : ℕ<VAR>x : α<VAR>h1 : f (n + 1) < x<VAR>h2 : x < f n<VAR>a : ℕ<GOAL>f a ≠ x
<VAR>α : Type u<VAR>Preorder α<VAR>f : ℤ → α<VAR>hf : Monotone f<VAR>n : ℤ<VAR>x : α<VAR>h1 : f n < x<VAR>h2 : x < f (n + 1)<VAR>a : ℤ<GOAL>f a ≠ x
<VAR>α : Type u<VAR>Preorder α<VAR>f : ℤ → α<VAR>hf : Antitone f<VAR>n : ℤ<VAR>x : α<VAR>h1 : f (n + 1) < x<VAR>h2 : x < f n<VAR>a : ℤ<GOAL>f a ≠ x
<VAR>φ : ℕ → ℕ<VAR>h : StrictMono φ<VAR>n : ℕ<GOAL>n ≤ φ n
<VAR>α : Type u<VAR>Preorder α<VAR>t : Set α<GOAL>Monotone Subtype.val
<VAR>α : Type u<VAR>Preorder α<VAR>t : Set α<GOAL>StrictMono Subtype.val
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<GOAL>Monotone Prod.fst
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<GOAL>Monotone Prod.snd
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>Preorder δ<VAR>f : α → γ<VAR>g : β → δ<VAR>hf : Monotone f<VAR>hg : Monotone g<GOAL>Monotone (Prod.map f g)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>Preorder δ<VAR>f : α → γ<VAR>g : β → δ<VAR>hf : Antitone f<VAR>hg : Antitone g<GOAL>Antitone (Prod.map f g)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_2<VAR>PartialOrder α<VAR>PartialOrder β<VAR>Preorder γ<VAR>Preorder δ<VAR>f : α → γ<VAR>g : β → δ<VAR>hf : StrictMono f<VAR>hg : StrictMono g<GOAL>StrictMono (Prod.map f g)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_2<VAR>PartialOrder α<VAR>PartialOrder β<VAR>Preorder γ<VAR>Preorder δ<VAR>f : α → γ<VAR>g : β → δ<VAR>hf : StrictAnti f<VAR>hg : StrictAnti g<GOAL>StrictAnti (Prod.map f g)
<VAR>ι : Type u_1<VAR>π : ι → Type u_3<VAR>DecidableEq ι<VAR>(i : ι) → Preorder (π i)<VAR>f : (i : ι) → π i<VAR>i : ι<GOAL>Monotone (Function.update f i)
<VAR>ι : Type u_1<VAR>π : ι → Type u_3<VAR>DecidableEq ι<VAR>(i : ι) → Preorder (π i)<VAR>f : (i : ι) → π i<VAR>i : ι<GOAL>StrictMono (Function.update f i)
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<GOAL>Monotone (Function.const β)
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Nonempty β<GOAL>StrictMono (Function.const β)
<VAR>ι : Type u_4<VAR>α : Type u_5<VAR>β : ι → Type u_6<VAR>(i : ι) → Preorder (β i)<VAR>Preorder α<VAR>f : α → (i : ι) → β i<GOAL>Monotone f ↔ ∀ (i : ι), Monotone fun x => f x i
<VAR>ι : Type u_4<VAR>α : Type u_5<VAR>β : ι → Type u_6<VAR>(i : ι) → Preorder (β i)<VAR>Preorder α<VAR>f : α → (i : ι) → β i<GOAL>Antitone f ↔ ∀ (i : ι), Antitone fun x => f x i
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>IsRefl α r<VAR>a b : α<GOAL>a = b → r a b
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>IsSymm α r<VAR>a b : α<GOAL>r a b ↔ r b a
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>IsAntisymm α r<VAR>a b : α<GOAL>r a b → r b a → b = a
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>IsRefl α r<VAR>IsAntisymm α r<VAR>a b : α<GOAL>r a b ∧ r b a ↔ a = b
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>IsAntisymm α r<VAR>a b : α<GOAL>r a b → r b a → a = b
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>IsRefl α r<GOAL>IsRefl α (Function.swap r)
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>IsIrrefl α r<GOAL>IsIrrefl α (Function.swap r)
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>IsTrans α r<GOAL>IsTrans α (Function.swap r)
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>IsAntisymm α r<GOAL>IsAntisymm α (Function.swap r)
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>IsAsymm α r<GOAL>IsAsymm α (Function.swap r)
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>IsTotal α r<GOAL>IsTotal α (Function.swap r)
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>IsTrichotomous α r<GOAL>IsTrichotomous α (Function.swap r)
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>IsPreorder α r<GOAL>IsPreorder α (Function.swap r)
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>IsStrictOrder α r<GOAL>IsStrictOrder α (Function.swap r)
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>IsPartialOrder α r<GOAL>IsPartialOrder α (Function.swap r)
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>IsTotalPreorder α r<GOAL>IsTotalPreorder α (Function.swap r)
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>IsLinearOrder α r<GOAL>IsLinearOrder α (Function.swap r)
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>IsAsymm α r<GOAL>IsAntisymm α r
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>IsAsymm α r<GOAL>IsIrrefl α r
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>IsTotal α r<GOAL>IsTrichotomous α r
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>IsIrrefl α r<VAR>x y : α<GOAL>r x y → x ≠ y
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>IsIrrefl α r<VAR>x y : α<GOAL>r x y → y ≠ x
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>IsIrrefl α r<VAR>Subsingleton α<VAR>x y : α<GOAL>¬r x y
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>IsRefl α r<VAR>Subsingleton α<VAR>x y : α<GOAL>r x y
<VAR>α : Type u<VAR>a b : α<GOAL>EmptyRelation a b ↔ False
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>IsIrrefl α r<VAR>Subsingleton α<GOAL>r = EmptyRelation
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>IsTrans α r<VAR>IsTrichotomous α r<VAR>a b c : α<GOAL>¬r b a → r b c → r a c
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>IsTrans α r<VAR>IsTrichotomous α r<VAR>a b c : α<GOAL>r a b → ¬r c b → r a c
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>IsTrans α r<GOAL>Transitive r
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>IsTrichotomous α r<VAR>IsIrrefl α r<VAR>a b : α<VAR>H : ∀ (x : α), r x a ↔ r x b<GOAL>a = b
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>IsStrictTotalOrder α r<GOAL>IsStrictTotalOrder α (Function.swap r)
<VAR>α : Type u<VAR>lt : α → α → Prop<VAR>self : IsOrderConnected α lt<VAR>a b c : α<GOAL>lt a c → lt a b ∨ lt b c
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>IsOrderConnected α r<VAR>a b c : α<VAR>h₁ : ¬r a b<VAR>h₂ : ¬r b c<GOAL>¬r a c
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>IsAsymm α r<VAR>IsOrderConnected α r<GOAL>IsStrictWeakOrder α r
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>self : IsWellFounded α r<GOAL>WellFounded r
<VAR>α : Type u<VAR>r : α → α → Prop<GOAL>IsWellFounded α r ↔ WellFounded r
<VAR>α : Sort u_1<VAR>WellFoundedRelation α<VAR>a b : α<GOAL>WellFoundedRelation.rel a b → ¬WellFoundedRelation.rel b a
<VAR>α : Type u<VAR>β : Type v<VAR>ra : α → α → Prop<VAR>rb : β → β → Prop<VAR>ha : WellFounded ra<VAR>hb : WellFounded rb<GOAL>WellFounded (Prod.Lex ra rb)
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>IsWellFounded α r<VAR>C : α → Prop<VAR>a : α<GOAL>(∀ (x : α), (∀ (y : α), r y x → C y) → C x) → C a
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>IsWellFounded α r<VAR>a : α<GOAL>Acc r a
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>IsWellFounded α r<VAR>C : α → Sort u_1<VAR>F : (x : α) → ((y : α) → r y x → C y) → C x<VAR>x : α<GOAL>IsWellFounded.fix r F x = F x fun y x => IsWellFounded.fix r F y
<VAR>α : Sort u_1<VAR>r : α → α → Prop<VAR>h : WellFounded r<VAR>a b : α<GOAL>r a b → ¬r b a
<VAR>α : Type u<VAR>LT α<VAR>WellFoundedLT α<GOAL>WellFounded fun x x_1 => x < x_1
<VAR>α : Type u<VAR>LT α<VAR>WellFoundedGT α<GOAL>WellFounded fun x x_1 => x > x_1
<VAR>α : Type u_1<VAR>LT α<GOAL>WellFoundedGT αᵒᵈ ↔ WellFoundedLT α
<VAR>α : Type u_1<VAR>LT α<GOAL>WellFoundedLT αᵒᵈ ↔ WellFoundedGT α
<VAR>α : Type u<VAR>LT α<VAR>WellFoundedLT α<VAR>C : α → Prop<VAR>a : α<GOAL>(∀ (x : α), (∀ (y : α), y < x → C y) → C x) → C a
<VAR>α : Type u<VAR>LT α<VAR>WellFoundedLT α<VAR>a : α<GOAL>Acc (fun x x_1 => x < x_1) a
<VAR>α : Type u<VAR>LT α<VAR>WellFoundedLT α<VAR>C : α → Sort u_1<VAR>F : (x : α) → ((y : α) → y < x → C y) → C x<VAR>x : α<GOAL>WellFoundedLT.fix F x = F x fun y x => WellFoundedLT.fix F y
<VAR>α : Type u<VAR>LT α<VAR>WellFoundedGT α<VAR>C : α → Prop<VAR>a : α<GOAL>(∀ (x : α), (∀ (y : α), x < y → C y) → C x) → C a
<VAR>α : Type u<VAR>LT α<VAR>WellFoundedGT α<VAR>a : α<GOAL>Acc (fun x x_1 => x > x_1) a
<VAR>α : Type u<VAR>LT α<VAR>WellFoundedGT α<VAR>C : α → Sort u_1<VAR>F : (x : α) → ((y : α) → x < y → C y) → C x<VAR>x : α<GOAL>WellFoundedGT.fix F x = F x fun y x => WellFoundedGT.fix F y
<VAR>α : Type u<VAR>Subsingleton α<VAR>r : α → α → Prop<VAR>hr : IsIrrefl α r<GOAL>IsWellOrder α r
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>IsWellFounded α r<VAR>s : α → α → Prop<VAR>h : Subrelation s r<GOAL>IsWellFounded α s
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>s : Set α<GOAL>¬Set.Bounded r s ↔ Set.Unbounded r s
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>s : Set α<GOAL>¬Set.Unbounded r s ↔ Set.Bounded r s
<VAR>α : Type u<VAR>IsEmpty α<VAR>r : α → α → Prop<VAR>s : Set α<GOAL>Set.Unbounded r s
<VAR>α : Type u_1<VAR>r : semiOutParam (α → α → Prop)<VAR>s : α → α → Prop<VAR>self : IsNonstrictStrictOrder α r s<VAR>a b : α<GOAL>s a b ↔ r a b ∧ ¬r b a
<VAR>α : Type u<VAR>r s : α → α → Prop<VAR>IsNonstrictStrictOrder α r s<VAR>a b : α<GOAL>s a b ↔ r a b ∧ ¬r b a
<VAR>α : Type u<VAR>HasSubset α<VAR>a b c : α<VAR>hab : a = b<VAR>hbc : b ⊆ c<GOAL>a ⊆ c
<VAR>α : Type u<VAR>HasSubset α<VAR>a b c : α<VAR>hab : a ⊆ b<VAR>hbc : b = c<GOAL>a ⊆ c
<VAR>α : Type u<VAR>HasSubset α<VAR>IsRefl α fun x x_1 => x ⊆ x_1<VAR>a : α<GOAL>a ⊆ a
<VAR>α : Type u<VAR>HasSubset α<VAR>a : α<VAR>IsRefl α fun x x_1 => x ⊆ x_1<GOAL>a ⊆ a
<VAR>α : Type u<VAR>HasSubset α<VAR>a b : α<VAR>IsRefl α fun x x_1 => x ⊆ x_1<GOAL>a = b → a ⊆ b
<VAR>α : Type u<VAR>HasSubset α<VAR>a b : α<VAR>IsRefl α fun x x_1 => x ⊆ x_1<GOAL>a = b → b ⊆ a
<VAR>α : Type u<VAR>HasSubset α<VAR>a b : α<VAR>IsRefl α fun x x_1 => x ⊆ x_1<GOAL>¬a ⊆ b → a ≠ b
<VAR>α : Type u<VAR>HasSubset α<VAR>a b : α<VAR>IsRefl α fun x x_1 => x ⊆ x_1<GOAL>¬a ⊆ b → b ≠ a
<VAR>α : Type u<VAR>HasSubset α<VAR>IsTrans α fun x x_1 => x ⊆ x_1<VAR>a b c : α<GOAL>a ⊆ b → b ⊆ c → a ⊆ c
<VAR>α : Type u<VAR>HasSubset α<VAR>a b : α<VAR>IsAntisymm α fun x x_1 => x ⊆ x_1<GOAL>a ⊆ b → b ⊆ a → a = b
<VAR>α : Type u<VAR>HasSubset α<VAR>a b : α<VAR>IsAntisymm α fun x x_1 => x ⊆ x_1<GOAL>a ⊆ b → b ⊆ a → b = a
<VAR>α : Type u<VAR>HasSubset α<VAR>a b : α<VAR>IsRefl α fun x x_1 => x ⊆ x_1<VAR>IsAntisymm α fun x x_1 => x ⊆ x_1<GOAL>a = b ↔ a ⊆ b ∧ b ⊆ a
<VAR>α : Type u<VAR>HasSubset α<VAR>a b : α<VAR>IsRefl α fun x x_1 => x ⊆ x_1<VAR>IsAntisymm α fun x x_1 => x ⊆ x_1<GOAL>a = b ↔ b ⊆ a ∧ a ⊆ b
<VAR>α : Type u<VAR>HasSSubset α<VAR>a b c : α<VAR>hab : a = b<VAR>hbc : b ⊂ c<GOAL>a ⊂ c
<VAR>α : Type u<VAR>HasSSubset α<VAR>a b c : α<VAR>hab : a ⊂ b<VAR>hbc : b = c<GOAL>a ⊂ c
<VAR>α : Type u<VAR>HasSSubset α<VAR>IsIrrefl α fun x x_1 => x ⊂ x_1<VAR>a : α<GOAL>¬a ⊂ a
<VAR>α : Type u<VAR>HasSSubset α<VAR>IsIrrefl α fun x x_1 => x ⊂ x_1<VAR>a b : α<GOAL>a ⊂ b → a ≠ b
<VAR>α : Type u<VAR>HasSSubset α<VAR>IsIrrefl α fun x x_1 => x ⊂ x_1<VAR>a b : α<GOAL>a ⊂ b → b ≠ a
<VAR>α : Type u<VAR>HasSSubset α<VAR>IsTrans α fun x x_1 => x ⊂ x_1<VAR>a b c : α<GOAL>a ⊂ b → b ⊂ c → a ⊂ c
<VAR>α : Type u<VAR>HasSSubset α<VAR>IsAsymm α fun x x_1 => x ⊂ x_1<VAR>a b : α<GOAL>a ⊂ b → ¬b ⊂ a
<VAR>α : Type u<VAR>HasSubset α<VAR>HasSSubset α<VAR>IsNonstrictStrictOrder α (fun x x_1 => x ⊆ x_1) fun x x_1 => x ⊂ x_1<VAR>a b : α<GOAL>a ⊂ b ↔ a ⊆ b ∧ ¬b ⊆ a
<VAR>α : Type u<VAR>HasSubset α<VAR>HasSSubset α<VAR>IsNonstrictStrictOrder α (fun x x_1 => x ⊆ x_1) fun x x_1 => x ⊂ x_1<VAR>a b : α<VAR>h : a ⊂ b<GOAL>a ⊆ b
<VAR>α : Type u<VAR>HasSubset α<VAR>HasSSubset α<VAR>IsNonstrictStrictOrder α (fun x x_1 => x ⊆ x_1) fun x x_1 => x ⊂ x_1<VAR>a b : α<VAR>h : a ⊂ b<GOAL>¬b ⊆ a
<VAR>α : Type u<VAR>HasSubset α<VAR>HasSSubset α<VAR>IsNonstrictStrictOrder α (fun x x_1 => x ⊆ x_1) fun x x_1 => x ⊂ x_1<VAR>a b : α<VAR>h : a ⊆ b<GOAL>¬b ⊂ a
<VAR>α : Type u<VAR>HasSubset α<VAR>HasSSubset α<VAR>IsNonstrictStrictOrder α (fun x x_1 => x ⊆ x_1) fun x x_1 => x ⊂ x_1<VAR>a b : α<VAR>h₁ : a ⊆ b<VAR>h₂ : ¬b ⊆ a<GOAL>a ⊂ b
<VAR>α : Type u<VAR>HasSubset α<VAR>HasSSubset α<VAR>IsNonstrictStrictOrder α (fun x x_1 => x ⊆ x_1) fun x x_1 => x ⊂ x_1<VAR>a b c : α<VAR>IsTrans α fun x x_1 => x ⊆ x_1<VAR>h₁ : a ⊆ b<VAR>h₂ : b ⊂ c<GOAL>a ⊂ c
<VAR>α : Type u<VAR>HasSubset α<VAR>HasSSubset α<VAR>IsNonstrictStrictOrder α (fun x x_1 => x ⊆ x_1) fun x x_1 => x ⊂ x_1<VAR>a b c : α<VAR>IsTrans α fun x x_1 => x ⊆ x_1<VAR>h₁ : a ⊂ b<VAR>h₂ : b ⊆ c<GOAL>a ⊂ c
<VAR>α : Type u<VAR>HasSubset α<VAR>HasSSubset α<VAR>IsNonstrictStrictOrder α (fun x x_1 => x ⊆ x_1) fun x x_1 => x ⊂ x_1<VAR>a b : α<VAR>IsAntisymm α fun x x_1 => x ⊆ x_1<VAR>h₁ : a ⊆ b<VAR>h₂ : a ≠ b<GOAL>a ⊂ b
<VAR>α : Type u<VAR>HasSubset α<VAR>HasSSubset α<VAR>IsNonstrictStrictOrder α (fun x x_1 => x ⊆ x_1) fun x x_1 => x ⊂ x_1<VAR>a b : α<VAR>IsAntisymm α fun x x_1 => x ⊆ x_1<VAR>h₁ : a ≠ b<VAR>h₂ : a ⊆ b<GOAL>a ⊂ b
<VAR>α : Type u<VAR>HasSubset α<VAR>HasSSubset α<VAR>IsNonstrictStrictOrder α (fun x x_1 => x ⊆ x_1) fun x x_1 => x ⊂ x_1<VAR>a b : α<VAR>IsAntisymm α fun x x_1 => x ⊆ x_1<VAR>h : a ⊆ b<GOAL>a = b ∨ a ⊂ b
<VAR>α : Type u<VAR>HasSubset α<VAR>HasSSubset α<VAR>IsNonstrictStrictOrder α (fun x x_1 => x ⊆ x_1) fun x x_1 => x ⊂ x_1<VAR>a b : α<VAR>IsAntisymm α fun x x_1 => x ⊆ x_1<VAR>h : a ⊆ b<GOAL>a ⊂ b ∨ a = b
<VAR>α : Type u<VAR>HasSubset α<VAR>HasSSubset α<VAR>IsNonstrictStrictOrder α (fun x x_1 => x ⊆ x_1) fun x x_1 => x ⊂ x_1<VAR>a b : α<VAR>IsAntisymm α fun x x_1 => x ⊆ x_1<VAR>hab : a ⊆ b<VAR>hba : ¬a ⊂ b<GOAL>a = b
<VAR>α : Type u<VAR>HasSubset α<VAR>HasSSubset α<VAR>IsNonstrictStrictOrder α (fun x x_1 => x ⊆ x_1) fun x x_1 => x ⊂ x_1<VAR>a b : α<VAR>IsAntisymm α fun x x_1 => x ⊆ x_1<VAR>hab : a ⊆ b<VAR>hba : ¬a ⊂ b<GOAL>b = a
<VAR>α : Type u<VAR>HasSubset α<VAR>HasSSubset α<VAR>IsNonstrictStrictOrder α (fun x x_1 => x ⊆ x_1) fun x x_1 => x ⊂ x_1<VAR>a b : α<VAR>IsAntisymm α fun x x_1 => x ⊆ x_1<GOAL>a ⊂ b ↔ a ⊆ b ∧ a ≠ b
<VAR>α : Type u<VAR>HasSubset α<VAR>HasSSubset α<VAR>IsNonstrictStrictOrder α (fun x x_1 => x ⊆ x_1) fun x x_1 => x ⊂ x_1<VAR>a b : α<VAR>IsRefl α fun x x_1 => x ⊆ x_1<VAR>IsAntisymm α fun x x_1 => x ⊆ x_1<GOAL>a ⊆ b ↔ a ⊂ b ∨ a = b
<VAR>α : Type u<VAR>Preorder α<GOAL>Transitive LE.le
<VAR>α : Type u<VAR>Preorder α<GOAL>Transitive LT.lt
<VAR>α : Type u<VAR>Preorder α<GOAL>Transitive GE.ge
<VAR>α : Type u<VAR>Preorder α<GOAL>Transitive GT.gt
<VAR>α β : Sort u<VAR>h₁ h₂ : α = β<VAR>a : α<GOAL>cast h₁ a = cast h₂ a
<VAR>α : Sort u<VAR>φ : α → Sort v<VAR>a a' : α<VAR>p₁ : φ a<VAR>p₂ : φ a'<VAR>e : a = a'<VAR>h₂ : e ▸ p₁ = p₂<GOAL>HEq p₁ p₂
<VAR>α : Sort u<VAR>φ : α → Sort v<VAR>a a' : α<VAR>p₁ : φ a<VAR>p₂ : φ a'<VAR>e : a' = a<VAR>h₂ : p₁ = e ▸ p₂<GOAL>HEq p₁ p₂
<VAR>a : Prop<VAR>h : HEq a True<GOAL>a
<VAR>α β φ : Sort u<VAR>p₁ : β = φ<VAR>p₂ : α = β<VAR>a : α<GOAL>Eq.recOn p₁ (Eq.recOn p₂ a) = Eq.recOn ⋯ a
<VAR>P Q : Prop<VAR>p : P<VAR>q : Q<GOAL>HEq p q
<VAR>p : Prop<GOAL>p ∧ True ↔ p
<VAR>p : Prop<GOAL>True ∧ p ↔ p
<VAR>p : Prop<GOAL>p ∧ False ↔ False
<VAR>p : Prop<GOAL>False ∧ p ↔ False
<VAR>p : Prop<GOAL>True ∨ p ↔ True
<VAR>p : Prop<GOAL>p ∨ True ↔ True
<VAR>p : Prop<GOAL>False ∨ p ↔ p
<VAR>p : Prop<GOAL>p ∨ False ↔ p
<VAR>a b : Prop<GOAL>¬a → ¬b → ¬(a ∨ b)
<VAR>a : Prop<GOAL>(a ↔ True) ↔ a
<VAR>a : Prop<GOAL>(True ↔ a) ↔ a
<VAR>a : Prop<GOAL>(a ↔ False) ↔ ¬a
<VAR>a : Prop<GOAL>(False ↔ a) ↔ ¬a
<VAR>a : Prop<GOAL>(a ↔ a) ↔ True
<VAR>α : Sort u<VAR>p : α → Prop<VAR>w : α<VAR>h₁ : p w<VAR>h₂ : ∀ (y : α), p y → y = w<GOAL>∃! x, p x
<VAR>α : Sort u<VAR>p : α → Prop<VAR>b : Prop<VAR>h₂ : ∃! x, p x<VAR>h₁ : ∀ (x : α), p x → (∀ (y : α), p y → y = x) → b<GOAL>b
<VAR>α : Sort u<VAR>p : α → Prop<VAR>hex : ∃ x, p x<VAR>hunique : ∀ (y₁ y₂ : α), p y₁ → p y₂ → y₁ = y₂<GOAL>∃! x, p x
<VAR>α : Sort u<VAR>p : α → Prop<GOAL>(∃! x, p x) → ∃ x, p x
<VAR>α : Sort u<VAR>p : α → Prop<VAR>h : ∃! x, p x<VAR>y₁ y₂ : α<VAR>py₁ : p y₁<VAR>py₂ : p y₂<GOAL>y₁ = y₂
<VAR>α : Sort u<VAR>p q : α → Prop<VAR>h : ∀ (a : α), p a ↔ q a<GOAL>(∃! a, p a) ↔ ∃! a, q a
<VAR>α : Sort u<VAR>h : DecidableEq α<VAR>a : α<GOAL>h a a = isTrue ⋯
<VAR>α : Sort u<VAR>h : DecidableEq α<VAR>a b : α<VAR>n : a ≠ b<GOAL>h a b = isFalse n
<VAR>p : Prop<VAR>h : Decidable p<VAR>h₁ : p → Sort u<VAR>h₂ : ¬p → Sort u<VAR>h₃ : ∀ (h : p), Subsingleton (h₁ h)<VAR>h₄ : ∀ (h : ¬p), Subsingleton (h₂ h)<GOAL>Subsingleton (Decidable.recOn h h₂ h₁)
<VAR>c t e : Prop<VAR>Decidable c<VAR>h : if c then t else e<VAR>hc : c<GOAL>t
<VAR>c t e : Prop<VAR>Decidable c<VAR>h : if c then t else e<VAR>hnc : ¬c<GOAL>e
<VAR>α : Sort u<VAR>b c : Prop<VAR>dec_b : Decidable b<VAR>dec_c : Decidable c<VAR>x y u v : α<VAR>h_c : b ↔ c<VAR>h_t : c → x = u<VAR>h_e : ¬c → y = v<GOAL>(if b then x else y) = if c then u else v
<VAR>α : Sort u<VAR>b c : Prop<VAR>Decidable b<VAR>Decidable c<VAR>x y u v : α<VAR>h_c : b ↔ c<VAR>h_t : x = u<VAR>h_e : y = v<GOAL>(if b then x else y) = if c then u else v
<VAR>b c x y u v : Prop<VAR>dec_b : Decidable b<VAR>dec_c : Decidable c<VAR>h_c : b ↔ c<VAR>h_t : c → (x ↔ u)<VAR>h_e : ¬c → (y ↔ v)<GOAL>(if b then x else y) ↔ if c then u else v
<VAR>b c x y u v : Prop<VAR>Decidable b<VAR>Decidable c<VAR>h_c : b ↔ c<VAR>h_t : x ↔ u<VAR>h_e : y ↔ v<GOAL>(if b then x else y) ↔ if c then u else v
<VAR>b c x y u v : Prop<VAR>Decidable b<VAR>h_c : b ↔ c<VAR>h_t : c → (x ↔ u)<VAR>h_e : ¬c → (y ↔ v)<GOAL>(if b then x else y) ↔ if c then u else v
<VAR>b c x y u v : Prop<VAR>Decidable b<VAR>h_c : b ↔ c<VAR>h_t : x ↔ u<VAR>h_e : y ↔ v<GOAL>(if b then x else y) ↔ if c then u else v
<VAR>α : Sort u<VAR>b c : Prop<VAR>dec_b : Decidable b<VAR>dec_c : Decidable c<VAR>x : b → α<VAR>u : c → α<VAR>y : ¬b → α<VAR>v : ¬c → α<VAR>h_c : b ↔ c<VAR>h_t : ∀ (h : c), x ⋯ = u h<VAR>h_e : ∀ (h : ¬c), y ⋯ = v h<GOAL>dite b x y = dite c u v
<VAR>α : Sort u<VAR>b c : Prop<VAR>Decidable b<VAR>x : b → α<VAR>u : c → α<VAR>y : ¬b → α<VAR>v : ¬c → α<VAR>h_c : b ↔ c<VAR>h_t : ∀ (h : c), x ⋯ = u h<VAR>h_e : ∀ (h : ¬c), y ⋯ = v h<GOAL>dite b x y = dite c u v
<VAR>c : Prop<VAR>h₁ : Decidable c<GOAL>AsTrue c → c
<VAR>α : Sort u<VAR>β : Sort v<VAR>a₁ a₂ : α<VAR>b : α → β<VAR>h : a₁ = a₂<GOAL>(let x := a₁; b x) = let x := a₂; b x
<VAR>α : Sort v<VAR>β : α → Sort u<VAR>a₁ a₂ : α<VAR>b : (x : α) → β x<VAR>h : a₁ = a₂<GOAL>HEq (let x := a₁; b x) (let x := a₂; b x)
<VAR>α : Sort v<VAR>β : α → Sort u<VAR>a : α<VAR>b₁ b₂ : (x : α) → β x<VAR>h : ∀ (x : α), b₁ x = b₂ x<GOAL>(let x := a; b₁ x) = let x := a; b₂ x
<VAR>α : Sort v<VAR>β : Sort u<VAR>a₁ a₂ : α<VAR>b₁ b₂ : α → β<VAR>h₁ : a₁ = a₂<VAR>h₂ : ∀ (x : α), b₁ x = b₂ x<GOAL>(let x := a₁; b₁ x) = let x := a₂; b₂ x
<VAR>β : Sort v<VAR>r : β → β → Prop<VAR>h : Equivalence r<GOAL>Reflexive r
<VAR>β : Sort v<VAR>r : β → β → Prop<VAR>h : Equivalence r<GOAL>Symmetric r
<VAR>β : Sort v<VAR>r : β → β → Prop<VAR>h : Equivalence r<GOAL>Transitive r
<VAR>α : Sort u<VAR>β : Sort v<VAR>r : β → β → Prop<VAR>f : α → β<VAR>h : Transitive r<GOAL>Transitive (InvImage r f)
<VAR>α : Sort u<VAR>β : Sort v<VAR>r : β → β → Prop<VAR>f : α → β<VAR>h : Irreflexive r<GOAL>Irreflexive (InvImage r f)
<VAR>α : Type u<VAR>f : α → α → α<GOAL>Commutative f → Associative f → LeftCommutative f
<VAR>α : Type u<VAR>f : α → α → α<GOAL>Commutative f → Associative f → RightCommutative f
<VAR>α : Type u<VAR>a : α<GOAL>pure a = [a]
<VAR>α : Type u<VAR>Inhabited α<GOAL>[].headI = default
<VAR>α : Type u<VAR>Inhabited α<VAR>h : α<VAR>t : List α<GOAL>(h :: t).headI = h
<VAR>α : Type u<VAR>LT α<VAR>l₁ l₂ : List α<GOAL>(l₁ ≤ l₂) = ¬l₂ < l₁
<VAR>α : Sort u<VAR>β : Sort v<VAR>op : α → α → β<VAR>self : IsSymmOp α β op<VAR>a b : α<GOAL>op a b = op b a
<VAR>α : Sort u<VAR>op : α → α → α<VAR>self : IsLeftCancel α op<VAR>a b c : α<GOAL>op a b = op a c → b = c
<VAR>α : Sort u<VAR>op : α → α → α<VAR>self : IsRightCancel α op<VAR>a b c : α<GOAL>op a b = op c b → a = c
<VAR>α : Sort u<VAR>r : α → α → Prop<VAR>self : IsIrrefl α r<VAR>a : α<GOAL>¬r a a
<VAR>α : Sort u<VAR>r : α → α → Prop<VAR>self : IsRefl α r<VAR>a : α<GOAL>r a a
<VAR>α : Sort u<VAR>r : α → α → Prop<VAR>self : IsSymm α r<VAR>a b : α<GOAL>r a b → r b a
<VAR>α : Sort u<VAR>r : α → α → Prop<VAR>self : IsAsymm α r<VAR>a b : α<GOAL>r a b → ¬r b a
<VAR>α : Sort u<VAR>r : α → α → Prop<VAR>self : IsAntisymm α r<VAR>a b : α<GOAL>r a b → r b a → a = b
<VAR>α : Sort u<VAR>r : α → α → Prop<VAR>self : IsTrans α r<VAR>a b c : α<GOAL>r a b → r b c → r a c
<VAR>α : Sort u<VAR>r : α → α → Prop<VAR>self : IsTotal α r<VAR>a b : α<GOAL>r a b ∨ r b a
<VAR>α : Sort u<VAR>lt : α → α → Prop<VAR>self : IsIncompTrans α lt<VAR>a b c : α<GOAL>¬lt a b ∧ ¬lt b a → ¬lt b c ∧ ¬lt c b → ¬lt a c ∧ ¬lt c a
<VAR>α : Sort u<VAR>lt : α → α → Prop<VAR>self : IsTrichotomous α lt<VAR>a b : α<GOAL>lt a b ∨ a = b ∨ lt b a
<VAR>α : Sort u<VAR>r : α → α → Prop<VAR>IsIrrefl α r<VAR>a : α<GOAL>¬r a a
<VAR>α : Sort u<VAR>r : α → α → Prop<VAR>IsRefl α r<VAR>a : α<GOAL>r a a
<VAR>α : Sort u<VAR>r : α → α → Prop<VAR>IsTrans α r<VAR>a b c : α<GOAL>r a b → r b c → r a c
<VAR>α : Sort u<VAR>r : α → α → Prop<VAR>IsSymm α r<VAR>a b : α<GOAL>r a b → r b a
<VAR>α : Sort u<VAR>r : α → α → Prop<VAR>IsAntisymm α r<VAR>a b : α<GOAL>r a b → r b a → a = b
<VAR>α : Sort u<VAR>r : α → α → Prop<VAR>IsAsymm α r<VAR>a b : α<GOAL>r a b → ¬r b a
<VAR>α : Sort u<VAR>r : α → α → Prop<VAR>IsTrichotomous α r<VAR>a b : α<GOAL>r a b ∨ a = b ∨ r b a
<VAR>α : Sort u<VAR>r : α → α → Prop<VAR>IsIncompTrans α r<VAR>a b c : α<GOAL>¬r a b ∧ ¬r b a → ¬r b c ∧ ¬r c b → ¬r a c ∧ ¬r c a
<VAR>α : Sort u<VAR>r : α → α → Prop<VAR>IsTotal α r<VAR>a b : α<GOAL>r a b ∨ r b a
<VAR>α : Sort u<VAR>r : α → α → Prop<VAR>IsStrictWeakOrder α r<VAR>a : α<GOAL>StrictWeakOrder.Equiv a a
<VAR>α : Sort u<VAR>r : α → α → Prop<VAR>a b : α<GOAL>StrictWeakOrder.Equiv a b → StrictWeakOrder.Equiv b a
<VAR>α : Sort u<VAR>r : α → α → Prop<VAR>IsStrictWeakOrder α r<VAR>a b c : α<GOAL>StrictWeakOrder.Equiv a b → StrictWeakOrder.Equiv b c → StrictWeakOrder.Equiv a c
<VAR>α : Sort u<VAR>r : α → α → Prop<VAR>a b : α<GOAL>StrictWeakOrder.Equiv a b → ¬r a b
<VAR>α : Sort u<VAR>r : α → α → Prop<VAR>a b : α<GOAL>StrictWeakOrder.Equiv a b → ¬r b a
<VAR>α : Sort u<VAR>le lt : α → α → Prop<VAR>DecidableRel le<VAR>IsTotalPreorder α le<VAR>h : ∀ (a b : α), lt a b ↔ ¬le b a<GOAL>IsStrictWeakOrder α lt
<VAR>α : Sort u<VAR>lt : α → α → Prop<VAR>IsStrictWeakOrder α lt<VAR>DecidableRel lt<VAR>a b c : α<GOAL>lt a b → ¬lt b c ∧ ¬lt c b → lt a c
<VAR>α : Sort u<VAR>lt : α → α → Prop<VAR>IsStrictWeakOrder α lt<VAR>DecidableRel lt<VAR>a b c : α<GOAL>¬lt a b ∧ ¬lt b a → lt b c → lt a c
<VAR>α : Sort u<VAR>lt : α → α → Prop<VAR>IsTrichotomous α lt<VAR>a b : α<GOAL>¬lt a b ∧ ¬lt b a → a = b
<VAR>α : Sort u<VAR>lt : α → α → Prop<VAR>IsTrichotomous α lt<VAR>a b : α<GOAL>StrictWeakOrder.Equiv a b → a = b
<VAR>α : Sort u<VAR>lt : α → α → Prop<VAR>IsTrichotomous α lt<VAR>IsIrrefl α lt<VAR>a b : α<GOAL>¬lt a b ∧ ¬lt b a ↔ a = b
<VAR>α : Sort u<VAR>lt : α → α → Prop<VAR>IsTrichotomous α lt<VAR>IsIrrefl α lt<VAR>a b : α<GOAL>StrictWeakOrder.Equiv a b ↔ a = b
<VAR>α : Sort u<VAR>lt : α → α → Prop<VAR>IsStrictOrder α lt<VAR>a b : α<GOAL>lt a b → ¬lt b a
<VAR>ι : Type u_2<VAR>β : ι → Type u_3<VAR>Fintype ι<VAR>(i : ι) → DecidableEq (β i)<VAR>x : (i : ι) → β i<GOAL>hammingDist x x = 0
<VAR>ι : Type u_2<VAR>β : ι → Type u_3<VAR>Fintype ι<VAR>(i : ι) → DecidableEq (β i)<VAR>x y : (i : ι) → β i<GOAL>0 ≤ hammingDist x y
<VAR>ι : Type u_2<VAR>β : ι → Type u_3<VAR>Fintype ι<VAR>(i : ι) → DecidableEq (β i)<VAR>x y : (i : ι) → β i<GOAL>hammingDist x y = hammingDist y x
<VAR>ι : Type u_2<VAR>β : ι → Type u_3<VAR>Fintype ι<VAR>(i : ι) → DecidableEq (β i)<VAR>x y z : (i : ι) → β i<GOAL>hammingDist x z ≤ hammingDist x y + hammingDist y z
<VAR>ι : Type u_2<VAR>β : ι → Type u_3<VAR>Fintype ι<VAR>(i : ι) → DecidableEq (β i)<VAR>x y z : (i : ι) → β i<GOAL>hammingDist x y ≤ hammingDist z x + hammingDist z y
<VAR>ι : Type u_2<VAR>β : ι → Type u_3<VAR>Fintype ι<VAR>(i : ι) → DecidableEq (β i)<VAR>x y z : (i : ι) → β i<GOAL>hammingDist x y ≤ hammingDist x z + hammingDist y z
<VAR>ι : Type u_2<VAR>β : ι → Type u_3<VAR>Fintype ι<VAR>(i : ι) → DecidableEq (β i)<GOAL>Function.swap hammingDist = hammingDist
<VAR>ι : Type u_2<VAR>β : ι → Type u_3<VAR>Fintype ι<VAR>(i : ι) → DecidableEq (β i)<VAR>x y : (i : ι) → β i<GOAL>hammingDist x y = 0 → x = y
<VAR>ι : Type u_2<VAR>β : ι → Type u_3<VAR>Fintype ι<VAR>(i : ι) → DecidableEq (β i)<VAR>x y : (i : ι) → β i<GOAL>hammingDist x y = 0 ↔ x = y
<VAR>ι : Type u_2<VAR>β : ι → Type u_3<VAR>Fintype ι<VAR>(i : ι) → DecidableEq (β i)<VAR>x y : (i : ι) → β i<GOAL>0 = hammingDist x y ↔ x = y
<VAR>ι : Type u_2<VAR>β : ι → Type u_3<VAR>Fintype ι<VAR>(i : ι) → DecidableEq (β i)<VAR>x y : (i : ι) → β i<GOAL>hammingDist x y ≠ 0 ↔ x ≠ y