ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β → γ<VAR>BEq α<VAR>Hashable α<VAR>m : Batteries.HashMap.Imp α β<VAR>H : m.WF<GOAL>(Batteries.HashMap.Imp.mapVal f m).WF
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β → Option γ<VAR>BEq α<VAR>Hashable α<VAR>m : Batteries.HashMap.Imp α β<VAR>H : m.WF<GOAL>(Batteries.HashMap.Imp.filterMap f m).WF
<VAR>i : Nat<VAR>r : Std.Range<VAR>h : i ∈ r<GOAL>i < r.stop
<VAR>i : Nat<VAR>r : Std.Range<VAR>h : i ∈ r<GOAL>r.start ≤ i
<VAR>i n : Nat<VAR>r : Std.Range<VAR>h₁ : i ∈ r<VAR>h₂ : r.stop = n<GOAL>i < n
<VAR>α β : Sort u_1<VAR>h : α = β<GOAL>h.mp = cast h
<VAR>α β : Sort u_1<VAR>h : α = β<GOAL>h.mpr = cast ⋯
<VAR>α β γ : Sort u_1<VAR>ha : α = β<VAR>hb : β = γ<VAR>a : α<GOAL>cast hb (cast ha a) = cast ⋯ a
<VAR>p q : Prop<VAR>hp : p<VAR>hq : q<GOAL>HEq hp hq
<VAR>a : Prop<GOAL>¬¬(a ∨ ¬a)
<VAR>a : Prop<GOAL>a ∧ a ↔ a
<VAR>a : Prop<GOAL>a ∧ ¬a ↔ False
<VAR>a : Prop<GOAL>¬a ∧ a ↔ False
<VAR>a c b d : Prop<VAR>f : a → c<VAR>g : b → d<VAR>h : a ∧ b<GOAL>c ∧ d
<VAR>a b c : Prop<VAR>h : a → b<GOAL>a ∧ c → b ∧ c
<VAR>a b c : Prop<VAR>h : a → b<GOAL>c ∧ a → c ∧ b
<VAR>a c b d : Prop<VAR>h₁ : a ↔ c<VAR>h₂ : b ↔ d<GOAL>a ∧ b ↔ c ∧ d
<VAR>a b c : Prop<VAR>h : a ↔ b<GOAL>a ∧ c ↔ b ∧ c
<VAR>b c a : Prop<VAR>h : b ↔ c<GOAL>a ∧ b ↔ a ∧ c
<VAR>a : Prop<VAR>b : Prop<GOAL>¬a → ¬(a ∧ b)
<VAR>a : Prop<VAR>b : Prop<GOAL>¬b → ¬(a ∧ b)
<VAR>a b c : Prop<VAR>h : a → b = c<GOAL>(a ∧ b) = (a ∧ c)
<VAR>c a b : Prop<VAR>h : c → a = b<GOAL>(a ∧ c) = (b ∧ c)
<VAR>a b c : Prop<GOAL>a ∧ b ∧ c ↔ b ∧ a ∧ c
<VAR>a b c : Prop<GOAL>(a ∧ b) ∧ c ↔ (a ∧ c) ∧ b
<VAR>a b c : Prop<GOAL>a ∧ b ∧ c ↔ b ∧ c ∧ a
<VAR>a b c d : Prop<GOAL>(a ∧ b) ∧ c ∧ d ↔ (a ∧ c) ∧ b ∧ d
<VAR>a b c : Prop<GOAL>a ∧ b ∧ c ↔ (a ∧ b) ∧ a ∧ c
<VAR>a b c : Prop<GOAL>(a ∧ b) ∧ c ↔ (a ∧ c) ∧ b ∧ c
<VAR>b a : Prop<VAR>hb : b<GOAL>a ∧ b ↔ a
<VAR>a b : Prop<VAR>ha : a<GOAL>a ∧ b ↔ b
<VAR>a : Prop<GOAL>a ∨ a ↔ a
<VAR>a b : Prop<VAR>ha : ¬a<VAR>hb : ¬b<GOAL>¬(a ∨ b)
<VAR>a c b d : Prop<VAR>h₁ : a ↔ c<VAR>h₂ : b ↔ d<GOAL>a ∨ b ↔ c ∨ d
<VAR>a b c : Prop<VAR>h : a ↔ b<GOAL>a ∨ c ↔ b ∨ c
<VAR>b c a : Prop<VAR>h : b ↔ c<GOAL>a ∨ b ↔ a ∨ c
<VAR>a b c : Prop<GOAL>a ∨ b ∨ c ↔ b ∨ a ∨ c
<VAR>a b c : Prop<GOAL>(a ∨ b) ∨ c ↔ (a ∨ c) ∨ b
<VAR>a b c d : Prop<GOAL>(a ∨ b) ∨ c ∨ d ↔ (a ∨ c) ∨ b ∨ d
<VAR>a b c : Prop<GOAL>a ∨ b ∨ c ↔ (a ∨ b) ∨ a ∨ c
<VAR>a b c : Prop<GOAL>(a ∨ b) ∨ c ↔ (a ∨ c) ∨ b ∨ c
<VAR>a b c : Prop<GOAL>a ∨ b ∨ c ↔ b ∨ c ∨ a
<VAR>b a : Prop<VAR>hb : ¬b<GOAL>a ∨ b ↔ a
<VAR>a b : Prop<VAR>ha : ¬a<GOAL>a ∨ b ↔ b
<VAR>a b : Prop<GOAL>a ∧ ¬b → ¬(a → b)
<VAR>b c : Prop<VAR>α : Sort u_1<GOAL>α → b ∧ c ↔ (α → b) ∧ (α → c)
<VAR>a b : Prop<GOAL>¬(a ∧ b) ↔ b → ¬a
<VAR>a b c : Prop<GOAL>a ∧ (b ∨ c) ↔ a ∧ b ∨ a ∧ c
<VAR>a b c : Prop<GOAL>(a ∨ b) ∧ c ↔ a ∧ c ∨ b ∧ c
<VAR>a b c : Prop<GOAL>a ∨ b ∧ c ↔ (a ∨ b) ∧ (a ∨ c)
<VAR>a b c : Prop<GOAL>a ∧ b ∨ c ↔ (a ∨ c) ∧ (b ∨ c)
<VAR>a b c : Prop<GOAL>a ∨ b → c ↔ (a → c) ∧ (b → c)
<VAR>p q : Prop<GOAL>¬(p ∨ q) ↔ ¬p ∧ ¬q
<VAR>a b : Prop<VAR>h : ¬a ∨ ¬b<GOAL>¬(a ∧ b)
<VAR>p q : Prop<VAR>h : Decidable p<GOAL>(if p then False else q) ↔ ¬p ∧ q
<VAR>p q : Prop<VAR>h : Decidable p<GOAL>(if p then q else False) ↔ p ∧ q
<VAR>p q : Prop<VAR>h : Decidable p<GOAL>(if p then True else q) ↔ ¬p → q
<VAR>p q : Prop<VAR>h : Decidable p<GOAL>(if p then q else True) ↔ p → q
<VAR>p : Prop<VAR>α : Sort u_1<VAR>hn : Decidable ¬p<VAR>h : Decidable p<VAR>x : ¬p → α<VAR>y : ¬¬p → α<GOAL>dite (¬p) x y = dite p (fun h => y ⋯) x
<VAR>α : Sort u_1<VAR>p : Prop<VAR>Decidable p<VAR>x y : α<GOAL>(if ¬p then x else y) = if p then y else x
<VAR>p q : Prop<VAR>h : Decidable p<GOAL>(if p then p else q) = (¬p → q)
<VAR>p q : Prop<VAR>h : Decidable p<GOAL>(if p then q else p) = (p ∧ q)
<VAR>α : Sort u_1<VAR>p q : α → Prop<VAR>h : ∀ (a : α), p a → q a<GOAL>(∀ (a : α), p a) → ∀ (a : α), q a
<VAR>α : Sort u_1<VAR>p : α → Prop<VAR>q : (∃ x, p x) → Prop<GOAL>(∀ (h : ∃ x, p x), q h) ↔ ∀ (x : α) (h : p x), q ⋯
<VAR>α : Sort u_1<VAR>p q : α → Prop<VAR>h : ∀ (a : α), p a → q a<GOAL>(∃ a, p a) → ∃ a, q a
<VAR>α : Sort u_2<VAR>p : α → Prop<VAR>β : Sort u_1<VAR>q : β → Prop<VAR>f : α → β<VAR>hpq : ∀ (a : α), p a → q (f a)<GOAL>(∃ a, p a) → ∃ b, q b
<VAR>α : Sort u_1<VAR>p : α → Prop<VAR>b : Prop<GOAL>(∃ x, p x) → b ↔ ∀ (x : α), p x → b
<VAR>b : Prop<VAR>α : Sort u_1<VAR>i : Nonempty α<GOAL>(∃ x, b) ↔ b
<VAR>α : Sort u_1<VAR>p q : α → Prop<VAR>h : ∀ (a : α), p a ↔ q a<GOAL>(∀ (a : α), p a) ↔ ∀ (a : α), q a
<VAR>α : Sort u_1<VAR>p q : α → Prop<VAR>h : ∀ (a : α), p a ↔ q a<GOAL>(∃ a, p a) ↔ ∃ a, q a
<VAR>α : Sort u_1<VAR>β : α → Sort u_2<VAR>p q : (a : α) → β a → Prop<VAR>h : ∀ (a : α) (b : β a), p a b ↔ q a b<GOAL>(∀ (a : α) (b : β a), p a b) ↔ ∀ (a : α) (b : β a), q a b
<VAR>α : Sort u_1<VAR>β : α → Sort u_2<VAR>p q : (a : α) → β a → Prop<VAR>h : ∀ (a : α) (b : β a), p a b ↔ q a b<GOAL>(∃ a b, p a b) ↔ ∃ a b, q a b
<VAR>α : Sort u_1<VAR>β : α → Sort u_2<VAR>γ : (a : α) → β a → Sort u_3<VAR>p q : (a : α) → (b : β a) → γ a b → Prop<VAR>h : ∀ (a : α) (b : β a) (c : γ a b), p a b c ↔ q a b c<GOAL>(∀ (a : α) (b : β a) (c : γ a b), p a b c) ↔ ∀ (a : α) (b : β a) (c : γ a b), q a b c
<VAR>α : Sort u_1<VAR>β : α → Sort u_2<VAR>γ : (a : α) → β a → Sort u_3<VAR>p q : (a : α) → (b : β a) → γ a b → Prop<VAR>h : ∀ (a : α) (b : β a) (c : γ a b), p a b c ↔ q a b c<GOAL>(∃ a b c, p a b c) ↔ ∃ a b c, q a b c
<VAR>α : Sort u_1<VAR>β : α → Sort u_2<VAR>γ : (a : α) → β a → Sort u_3<VAR>δ : (a : α) → (b : β a) → γ a b → Sort u_4<VAR>p q : (a : α) → (b : β a) → (c : γ a b) → δ a b c → Prop<VAR>h : ∀ (a : α) (b : β a) (c : γ a b) (d : δ a b c), p a b c d ↔ q a b c d<GOAL>(∀ (a : α) (b : β a) (c : γ a b) (d : δ a b c), p a b c d) ↔ ∀ (a : α) (b : β a) (c : γ a b) (d : δ a b c), q a b c d
<VAR>α : Sort u_1<VAR>β : α → Sort u_2<VAR>γ : (a : α) → β a → Sort u_3<VAR>δ : (a : α) → (b : β a) → γ a b → Sort u_4<VAR>p q : (a : α) → (b : β a) → (c : γ a b) → δ a b c → Prop<VAR>h : ∀ (a : α) (b : β a) (c : γ a b) (d : δ a b c), p a b c d ↔ q a b c d<GOAL>(∃ a b c d, p a b c d) ↔ ∃ a b c d, q a b c d
<VAR>α : Sort u_1<VAR>β : α → Sort u_2<VAR>γ : (a : α) → β a → Sort u_3<VAR>δ : (a : α) → (b : β a) → γ a b → Sort u_4<VAR>ε : (a : α) → (b : β a) → (c : γ a b) → δ a b c → Sort u_5<VAR>p q : (a : α) → (b : β a) → (c : γ a b) → (d : δ a b c) → ε a b c d → Prop<VAR>h : ∀ (a : α) (b : β a) (c : γ a b) (d : δ a b c) (e : ε a b c d), p a b c d e ↔ q a b c d e<GOAL>(∀ (a : α) (b : β a) (c : γ a b) (d : δ a b c) (e : ε a b c d), p a b c d e) ↔ ∀ (a : α) (b : β a) (c : γ a b) (d : δ a b c) (e : ε a b c d), q a b c d e
<VAR>α : Sort u_1<VAR>β : α → Sort u_2<VAR>γ : (a : α) → β a → Sort u_3<VAR>δ : (a : α) → (b : β a) → γ a b → Sort u_4<VAR>ε : (a : α) → (b : β a) → (c : γ a b) → δ a b c → Sort u_5<VAR>p q : (a : α) → (b : β a) → (c : γ a b) → (d : δ a b c) → ε a b c d → Prop<VAR>h : ∀ (a : α) (b : β a) (c : γ a b) (d : δ a b c) (e : ε a b c d), p a b c d e ↔ q a b c d e<GOAL>(∃ a b c d e, p a b c d e) ↔ ∃ a b c d e, q a b c d e
<VAR>α : Sort u_1<VAR>p : α → Prop<GOAL>(¬∃ x, p x) ↔ ∀ (x : α), ¬p x
<VAR>α : Sort u_1<VAR>p q : α → Prop<GOAL>(∀ (x : α), p x ∧ q x) ↔ (∀ (x : α), p x) ∧ ∀ (x : α), q x
<VAR>α : Sort u_1<VAR>p q : α → Prop<GOAL>(∃ x, p x ∨ q x) ↔ (∃ x, p x) ∨ ∃ x, q x
<VAR>α : Sort u_1<GOAL>¬∃ _a, False
<VAR>b : Prop<VAR>α : Sort u_1<VAR>i : Nonempty α<GOAL>α → b ↔ b
<VAR>α : Sort u_1<VAR>p : α → Prop<GOAL>(∃ x, p x) → Nonempty α
<VAR>α : Sort u_1<VAR>p : α → Prop<GOAL>(∃ x, ¬p x) → ¬∀ (x : α), p x
<VAR>α : Sort u_1<VAR>p : α → Prop<VAR>a' : α<GOAL>(∀ (a : α), a = a' → p a) ↔ p a'
<VAR>α : Sort u_1<VAR>p : α → Prop<VAR>a' : α<GOAL>(∀ (a : α), a' = a → p a) ↔ p a'
<GOAL>∀ {α : Sort u_1} {a' : α}, ∃ a, a = a'
<GOAL>∀ {α : Sort u_1} {a' : α}, ∃ a, a' = a
<VAR>α : Sort u_1<VAR>p : α → Prop<VAR>a' : α<GOAL>(∃ a, a = a' ∧ p a) ↔ p a'
<VAR>α : Sort u_1<VAR>p : α → Prop<VAR>a' : α<GOAL>(∃ a, p a ∧ a = a') ↔ p a'
<VAR>α : Sort u_1<VAR>p : α → Prop<VAR>b : Prop<GOAL>(∃ x, b ∧ p x) ↔ b ∧ ∃ x, p x
<VAR>α : Sort u_1<VAR>p : α → Prop<VAR>b : Prop<GOAL>(∃ x, p x ∧ b) ↔ (∃ x, p x) ∧ b
<VAR>α : Sort u_1<VAR>p : α → Prop<VAR>a' : α<GOAL>(∃ a, a' = a ∧ p a) ↔ p a'
<VAR>α : Sort u_1<VAR>p q : α → Prop<VAR>a' : α<GOAL>(∀ (a : α), a = a' ∨ q a → p a) ↔ p a' ∧ ∀ (a : α), q a → p a
<VAR>α : Sort u_1<VAR>p q : α → Prop<VAR>a' : α<GOAL>(∃ a, (a = a' ∨ q a) ∧ p a) ↔ p a' ∨ ∃ a, q a ∧ p a
<VAR>α : Sort u_1<VAR>p q : α → Prop<VAR>a' : α<GOAL>(∃ a, p a ∧ q a ∧ a = a') ↔ p a' ∧ q a'
<VAR>α : Sort u_1<VAR>p q : α → Prop<VAR>a' : α<GOAL>(∃ a, p a ∧ q a ∧ a' = a) ↔ p a' ∧ q a'
<VAR>b a : Prop<GOAL>(∃ _h, b) ↔ a ∧ b
<VAR>α : Sort u_2<VAR>β : Sort u_1<VAR>f : α → β<VAR>a' : α<GOAL>∃ a, f a = f a'
<VAR>p : Prop<VAR>q : p → Prop<VAR>h : p<GOAL>(∀ (h' : p), q h') ↔ q h
<VAR>α : Sort u_2<VAR>β : Sort u_1<VAR>p : α → β → Prop<GOAL>(∀ (a : α) (b : β), p a b) ↔ ∀ (b : β) (a : α), p a b
<VAR>α : Sort u_2<VAR>β : Sort u_1<VAR>p : α → β → Prop<GOAL>(∃ a b, p a b) ↔ ∃ b a, p a b
<VAR>α : Sort u_2<VAR>β : Sort u_1<VAR>f : α → β<VAR>p : β → Prop<GOAL>(∀ (b : β) (a : α), f a = b → p b) ↔ ∀ (a : α), p (f a)
<VAR>α : Sort u_2<VAR>β : Sort u_1<VAR>f : α → β<VAR>p : β → Prop<GOAL>(∀ (b : β) (a : α), b = f a → p b) ↔ ∀ (a : α), p (f a)
<VAR>α : Sort u_2<VAR>β : Sort u_1<VAR>f : α → β<VAR>p : α → Prop<VAR>q : β → Prop<GOAL>(∀ (b : β) (a : α), p a → f a = b → q b) ↔ ∀ (a : α), p a → q (f a)
<VAR>p : Prop<VAR>q : p → Prop<VAR>hn : ¬p<GOAL>(∀ (h' : p), q h') ↔ True
<VAR>p : Prop<VAR>Decidable p<GOAL>¬¬p ↔ p
<VAR>p : Prop<VAR>h : Decidable p<GOAL>¬p ∨ p
<VAR>p : Prop<VAR>Decidable p<GOAL>(¬p → False) → p
<VAR>p : Prop<VAR>Decidable p<GOAL>decide p = true ↔ p
<VAR>p : Prop<GOAL>∀ {x : Decidable p}, decide p = false ↔ ¬p
<VAR>p q : Prop<GOAL>∀ {x : Decidable p} {x_1 : Decidable q}, decide p = decide q ↔ (p ↔ q)
<VAR>a b : Prop<VAR>Decidable a<VAR>h : ¬(a → b)<GOAL>a
<VAR>a b : Prop<VAR>Decidable a<VAR>h : ¬a → b<VAR>hb : ¬b<GOAL>a
<VAR>a b : Prop<VAR>Decidable a<VAR>Decidable b<GOAL>¬a → b ↔ ¬b → a
<VAR>a : Prop<VAR>Decidable a<GOAL>¬a → a ↔ a
<VAR>a b : Prop<VAR>Decidable a<GOAL>a ∨ b ↔ ¬a → b
<VAR>b a : Prop<VAR>Decidable b<GOAL>a ∨ b ↔ ¬b → a
<VAR>a b : Prop<VAR>Decidable a<GOAL>¬a → ¬b ↔ b → a
<VAR>a b : Prop<VAR>Decidable a<VAR>h : a → b<GOAL>¬a ∨ b
<VAR>a b : Prop<VAR>Decidable a<GOAL>a → b ↔ ¬a ∨ b
<VAR>b a : Prop<VAR>Decidable b<GOAL>b → a ↔ a ∨ ¬b
<VAR>a b c : Prop<VAR>h : Decidable a<GOAL>a → b ∨ c ↔ (a → b) ∨ (a → c)
<VAR>b : Prop<VAR>a : Sort u_1<VAR>c : Prop<VAR>Decidable b<GOAL>a → b ∨ c ↔ (a → b) ∨ (a → c)
<VAR>a b : Prop<VAR>Decidable a<GOAL>¬(a → b) ↔ a ∧ ¬b
<VAR>a b : Prop<VAR>Decidable a<GOAL>((a → b) → a) → a
<VAR>a : Prop<VAR>H : ∀ (b : Prop), (a → b) → a<GOAL>a
<VAR>a b : Prop<VAR>Decidable a<VAR>Decidable b<GOAL>(¬a ↔ ¬b) ↔ (a ↔ b)
<VAR>a b : Prop<VAR>Decidable a<VAR>Decidable b<GOAL>(¬a ↔ b) ↔ (¬b ↔ a)
<VAR>b a : Prop<VAR>Decidable b<GOAL>¬(a ↔ b) ↔ (¬a ↔ b)
<VAR>a b : Prop<VAR>Decidable a<VAR>Decidable b<GOAL>(a ↔ ¬b) ↔ (b ↔ ¬a)
<VAR>a b : Prop<VAR>Decidable b<GOAL>(a ↔ b) ↔ a ∧ b ∨ ¬a ∧ ¬b
<VAR>a b : Prop<VAR>Decidable a<VAR>Decidable b<GOAL>(a ↔ b) ↔ (¬a ∨ b) ∧ (a ∨ ¬b)
<VAR>b a : Prop<VAR>Decidable b<GOAL>¬(a ∧ ¬b) ↔ a → b
<VAR>a b : Prop<VAR>Decidable a<GOAL>¬(a ∧ b) ↔ ¬a ∨ ¬b
<VAR>b a : Prop<VAR>Decidable b<GOAL>¬(a ∧ b) ↔ ¬a ∨ ¬b
<VAR>a b : Prop<VAR>Decidable a<VAR>Decidable b<GOAL>a ∨ b ↔ ¬(¬a ∧ ¬b)
<VAR>a b : Prop<VAR>Decidable a<VAR>Decidable b<GOAL>a ∧ b ↔ ¬(¬a ∨ ¬b)
<VAR>a b : Prop<VAR>Decidable a<GOAL>(a → b ↔ b) ↔ a ∨ b
<VAR>a b : Prop<VAR>Decidable a<GOAL>(b ↔ a → b) ↔ a ∨ b
<VAR>a b c : Prop<VAR>Decidable a<GOAL>a ∧ b ∨ (a → c) ↔ a → b ∨ c
<VAR>c a b : Prop<VAR>Decidable c<VAR>h : ¬c → (a ↔ b)<GOAL>a ∨ c ↔ b ∨ c
<VAR>a b c : Prop<VAR>Decidable a<VAR>h : ¬a → (b ↔ c)<GOAL>a ∨ b ↔ a ∨ c
<VAR>α : Sort u_1<VAR>p : α → Prop<VAR>Decidable (∃ x, ¬p x)<VAR>(x : α) → Decidable (p x)<GOAL>(¬∀ (x : α), p x) ↔ ∃ x, ¬p x
<VAR>α : Sort u_1<VAR>p : α → Prop<VAR>Decidable (∃ x, p x)<GOAL>(¬∀ (x : α), ¬p x) ↔ ∃ x, p x
<VAR>α : Sort u_1<VAR>p : α → Prop<VAR>(x : α) → Decidable (p x)<GOAL>(¬∃ x, ¬p x) ↔ ∀ (x : α), p x
<VAR>u v : Prop<VAR>duv : Decidable (u → v)<VAR>du : Decidable u<VAR>dv : u → Decidable v<GOAL>decide (u → v) = if h : u then decide v else true
<VAR>u : Prop<VAR>du : Decidable u<VAR>p q : Prop<VAR>dpq : Decidable (if u then p else q)<VAR>dp : Decidable p<VAR>dq : Decidable q<GOAL>decide (if u then p else q) = if u then decide p else decide q
<VAR>p : Prop<VAR>h : Decidable p<VAR>b : Bool<GOAL>(if p then decide p else b) = (decide p || b)
<VAR>p : Prop<VAR>h : Decidable p<VAR>b : Bool<GOAL>(if p then b else decide p) = (decide p && b)
<VAR>α : Sort u_1<VAR>a : α<GOAL>Eq (id a) a
<VAR>α : Sort u<VAR>motive : α → Prop<VAR>a b : α<VAR>h₁ : Eq a b<VAR>h₂ : motive a<GOAL>motive b
<VAR>α : Sort u<VAR>a b : α<VAR>h : Eq a b<GOAL>Eq b a
<VAR>α : Sort u<VAR>a b c : α<VAR>h₁ : Eq a b<VAR>h₂ : Eq b c<GOAL>Eq a c
<VAR>α : Sort u<VAR>β : Sort v<VAR>a₁ a₂ : α<VAR>f : α → β<VAR>h : Eq a₁ a₂<GOAL>Eq (f a₁) (f a₂)
<VAR>α : Sort u<VAR>β : Sort v<VAR>f₁ f₂ : α → β<VAR>a₁ a₂ : α<VAR>h₁ : Eq f₁ f₂<VAR>h₂ : Eq a₁ a₂<GOAL>Eq (f₁ a₁) (f₂ a₂)
<VAR>α : Sort u<VAR>β : α → Sort v<VAR>f g : (x : α) → β x<VAR>h : Eq f g<VAR>a : α<GOAL>Eq (f a) (g a)
<VAR>α : Sort u<VAR>a a' : α<VAR>h : HEq a a'<GOAL>Eq a a'
<VAR>a b : Prop<VAR>self : And a b<GOAL>b
<VAR>a b : Prop<VAR>self : And a b<GOAL>a
<VAR>a : Prop<VAR>b : Prop<VAR>h : a<GOAL>Or a b
<VAR>b : Prop<VAR>a : Prop<VAR>h : b<GOAL>Or a b
<VAR>a b c : Prop<VAR>h : Or a b<VAR>left : a → c<VAR>right : b → c<GOAL>c
<VAR>a b : Prop<VAR>h : Or a b<VAR>na : Not a<GOAL>b
<VAR>a b : Prop<VAR>h : Or a b<VAR>nb : Not b<GOAL>a
<VAR>a b : Prop<VAR>h : Or (Not a) b<VAR>ha : a<GOAL>b
<VAR>a b : Prop<VAR>h : Or a (Not b)<VAR>nb : b<GOAL>a
<VAR>α : Sort u<VAR>p : α → Prop<VAR>self : Subtype p<GOAL>p self.val
<VAR>b : Bool<GOAL>Not (Eq b true) → Eq b false
<VAR>b : Bool<GOAL>Not (Eq b false) → Eq b true
<VAR>b : Bool<GOAL>Eq b true → Not (Eq b false)
<VAR>b : Bool<GOAL>Eq b false → Not (Eq b true)
<VAR>α : Sort u<VAR>p : Prop<VAR>h₁ : Nonempty α<VAR>h₂ : α → p<GOAL>p
<VAR>α : Sort u<VAR>b : PLift α<GOAL>Eq { down := b.down } b
<VAR>α : Sort u<VAR>a : α<GOAL>Eq { down := a }.down a
<VAR>α : Type u<VAR>b : ULift α<GOAL>Eq { down := b.down } b
<VAR>α : Type u<VAR>a : α<GOAL>Eq { down := a }.down a
<VAR>p : Prop<VAR>inst : Decidable p<GOAL>p → Eq (decide p) true
<VAR>p : Prop<VAR>Decidable p<GOAL>Not p → Eq (decide p) false
<VAR>p : Prop<VAR>inst : Decidable p<GOAL>Eq (decide p) true → p
<VAR>p : Prop<VAR>inst : Decidable p<GOAL>Eq (decide p) false → Not p
<VAR>α : Sort u_1<VAR>inst : DecidableEq α<VAR>a : α<GOAL>Eq (decide (Eq a a)) true
<VAR>n m : Nat<GOAL>Eq (n.beq m) true → Eq n m
<VAR>n m : Nat<GOAL>Eq (n.beq m) false → Not (Eq n m)
<VAR>n : Nat<GOAL>LE.le n.succ 0 → False
<VAR>n : Nat<GOAL>Not (LT.lt n 0)
<VAR>n m : Nat<GOAL>LE.le n m → LE.le n.succ m.succ
<VAR>n : Nat<GOAL>LT.lt 0 n.succ
<VAR>n m : Nat<VAR>h : LE.le n m<GOAL>LE.le n m.succ
<VAR>n m k : Nat<GOAL>LE.le n m → LE.le m k → LE.le n k
<VAR>n m k : Nat<VAR>h₁ : LT.lt n m<GOAL>LT.lt m k → LT.lt n k
<VAR>n : Nat<GOAL>LE.le n n.succ
<VAR>n m : Nat<GOAL>LE.le n m → LE.le n.pred m.pred
<VAR>n m : Nat<GOAL>LE.le n.succ m.succ → LE.le n m
<VAR>m n : Nat<GOAL>LT.lt m n.succ → LE.le m n
<VAR>n m : Nat<GOAL>LE.le n m → Or (Eq n m) (LT.lt n m)
<VAR>n m : Nat<GOAL>Or (LT.lt n m) (GE.ge n m)
<VAR>n : Nat<GOAL>Not (LE.le n.succ n)
<VAR>n : Nat<GOAL>Not (LT.lt n n)
<VAR>n m k : Nat<VAR>h₁ : LE.le n m<VAR>h₂ : LT.lt m k<GOAL>LT.lt n k
<VAR>n m : Nat<VAR>h₁ : LE.le n m<VAR>h₂ : LE.le m n<GOAL>Eq n m
<VAR>n m : Nat<VAR>h₁ : LE.le n m<VAR>h₂ : Not (Eq n m)<GOAL>LT.lt n m
<VAR>n m : Nat<VAR>h : Eq (n.ble m) true<GOAL>LE.le n m
<VAR>n : Nat<GOAL>Eq (n.ble n) true
<VAR>n m : Nat<GOAL>Eq (n.ble m) true → Eq (n.ble m.succ) true
<VAR>n m : Nat<VAR>h : LE.le n m<GOAL>Eq (n.ble m) true
<VAR>n m : Nat<VAR>h : Not (Eq (n.ble m) true)<GOAL>Not (LE.le n m)
<GOAL>Or (Eq System.Platform.numBits 32) (Eq System.Platform.numBits 64)
<GOAL>Or (Eq USize.size 4294967296) (Eq USize.size 18446744073709551616)
<VAR>n : Nat<VAR>h : n.isValidChar<GOAL>LT.lt n UInt32.size
<VAR>c d : Char<GOAL>Eq c.val d.val → Eq c d
<VAR>c d : Char<GOAL>Eq c d → Eq c.val d.val
<VAR>c d : Char<VAR>h : Not (Eq c.val d.val)<GOAL>Not (Eq c d)
<VAR>c d : Char<VAR>h : Not (Eq c d)<GOAL>Not (Eq c.val d.val)
<GOAL>@Batteries.BinomialHeap.Imp.HeapNode.rankTR = @Batteries.BinomialHeap.Imp.HeapNode.rank
<VAR>α : Type u_1<VAR>s : Batteries.BinomialHeap.Imp.HeapNode α<VAR>n : Nat<GOAL>Batteries.BinomialHeap.Imp.HeapNode.rankTR.go s n = s.rank + n
<VAR>α : Type u_1<VAR>le : α → α → Bool<VAR>s₁ s₂ : Batteries.BinomialHeap.Imp.Heap α<GOAL>(Batteries.BinomialHeap.Imp.Heap.merge le s₁ s₂).realSize = s₁.realSize + s₂.realSize
<VAR>α : Type u_1<VAR>k : Batteries.BinomialHeap.Imp.Heap α → Batteries.BinomialHeap.Imp.Heap α<VAR>n : Nat<VAR>le : α → α → Bool<VAR>res : Batteries.BinomialHeap.Imp.FindMin α<VAR>s : Batteries.BinomialHeap.Imp.Heap α<VAR>m : Nat<VAR>hk : ∀ (s : Batteries.BinomialHeap.Imp.Heap α), (k s).realSize = m + s.realSize<VAR>eq : n = m + s.realSize<VAR>hres : Batteries.BinomialHeap.Imp.FindMin.HasSize res n<GOAL>Batteries.BinomialHeap.Imp.FindMin.HasSize (Batteries.BinomialHeap.Imp.Heap.findMin le k s res) n
<VAR>α : Type u_1<VAR>n : Nat<VAR>res : Batteries.BinomialHeap.Imp.Heap α<VAR>s : Batteries.BinomialHeap.Imp.HeapNode α<GOAL>(Batteries.BinomialHeap.Imp.HeapNode.toHeap.go s n res).realSize = s.realSize + res.realSize
<VAR>α : Type u_1<VAR>s : Batteries.BinomialHeap.Imp.HeapNode α<GOAL>s.toHeap.realSize = s.realSize
<VAR>α : Type u_1<VAR>le : α → α → Bool<VAR>a : α<VAR>s' s : Batteries.BinomialHeap.Imp.Heap α<VAR>eq : Batteries.BinomialHeap.Imp.Heap.deleteMin le s = some (a, s')<GOAL>s.realSize = s'.realSize + 1
<VAR>α : Type u_1<VAR>le : α → α → Bool<VAR>s' s : Batteries.BinomialHeap.Imp.Heap α<GOAL>Batteries.BinomialHeap.Imp.Heap.tail? le s = some s' → s.realSize = s'.realSize + 1
<VAR>α : Type u_1<VAR>le : α → α → Bool<VAR>s : Batteries.BinomialHeap.Imp.Heap α<GOAL>(Batteries.BinomialHeap.Imp.Heap.tail le s).realSize = s.realSize - 1
<GOAL>∀ {α : Type u_1} {le : α → α → Bool} {n : Nat}, Batteries.BinomialHeap.Imp.Heap.WF le n Batteries.BinomialHeap.Imp.Heap.nil
<GOAL>∀ {α : Type u_1} {a : α} {le : α → α → Bool}, Batteries.BinomialHeap.Imp.Heap.WF le 0 (Batteries.BinomialHeap.Imp.Heap.singleton a)
<GOAL>∀ {α : Type u_1} {le : α → α → Bool} {n' : Nat} {s : Batteries.BinomialHeap.Imp.Heap α} {n : Nat}, s.rankGT n → Batteries.BinomialHeap.Imp.Heap.WF le n' s → Batteries.BinomialHeap.Imp.Heap.WF le (n + 1) s
<VAR>n n' : Nat<GOAL>∀ {α : Type u_1} {le : α → α → Bool} {s : Batteries.BinomialHeap.Imp.Heap α}, n ≤ n' → Batteries.BinomialHeap.Imp.Heap.WF le n' s → Batteries.BinomialHeap.Imp.Heap.WF le n s
<GOAL>∀ {α : Type u_1} {s : Batteries.BinomialHeap.Imp.Heap α} {n n' : Nat}, s.rankGT n → n' ≤ n → s.rankGT n'
<GOAL>∀ {α : Type u_1} {lt : α → α → Bool} {n : Nat} {s : Batteries.BinomialHeap.Imp.Heap α}, Batteries.BinomialHeap.Imp.Heap.WF lt (n + 1) s → s.rankGT n
<GOAL>∀ {α : Type u_1} {le : α → α → Bool} {s₁ s₂ : Batteries.BinomialHeap.Imp.Heap α} {n : Nat}, Batteries.BinomialHeap.Imp.Heap.WF le n s₁ → Batteries.BinomialHeap.Imp.Heap.WF le n s₂ → Batteries.BinomialHeap.Imp.Heap.WF le n (Batteries.BinomialHeap.Imp.Heap.merge le s₁ s₂) ∧ ((s₁.rankGT n ↔ s₂.rankGT n) → (Batteries.BinomialHeap.Imp.Heap.merge le s₁ s₂).rankGT n)
<GOAL>∀ {α : Type u_1} {le : α → α → Bool} {s₁ s₂ : Batteries.BinomialHeap.Imp.Heap α} {n : Nat}, Batteries.BinomialHeap.Imp.Heap.WF le n s₁ → Batteries.BinomialHeap.Imp.Heap.WF le n s₂ → Batteries.BinomialHeap.Imp.Heap.WF le n (Batteries.BinomialHeap.Imp.Heap.merge le s₁ s₂)
<VAR>α : Type u_1<VAR>le : α → α → Bool<VAR>a : α<VAR>n : Nat<VAR>s : Batteries.BinomialHeap.Imp.HeapNode α<GOAL>Batteries.BinomialHeap.Imp.HeapNode.WF le a s n → s.rank = n
<VAR>α : Type u_1<VAR>le : α → α → Bool<VAR>a : α<VAR>n : Nat<VAR>s : Batteries.BinomialHeap.Imp.HeapNode α<VAR>h : Batteries.BinomialHeap.Imp.HeapNode.WF le a s n<GOAL>Batteries.BinomialHeap.Imp.Heap.WF le 0 s.toHeap
<VAR>α : Type u_1<VAR>le : α → α → Bool<VAR>a : α<VAR>res : Batteries.BinomialHeap.Imp.Heap α<VAR>n : Nat<VAR>s : Batteries.BinomialHeap.Imp.HeapNode α<GOAL>Batteries.BinomialHeap.Imp.HeapNode.WF le a s n → Batteries.BinomialHeap.Imp.Heap.WF le s.rank res → Batteries.BinomialHeap.Imp.Heap.WF le 0 (Batteries.BinomialHeap.Imp.HeapNode.toHeap.go s s.rank res)
<VAR>α : Type u_1<VAR>le : α → α → Bool<VAR>res : Batteries.BinomialHeap.Imp.FindMin α<VAR>self : Batteries.BinomialHeap.Imp.FindMin.WF le res<GOAL>Batteries.BinomialHeap.Imp.Heap.WF le (self.rank + 1) res.next
<VAR>α : Type u_1<VAR>le : α → α → Bool<VAR>res : Batteries.BinomialHeap.Imp.FindMin α<VAR>self : Batteries.BinomialHeap.Imp.FindMin.WF le res<GOAL>Batteries.BinomialHeap.Imp.HeapNode.WF le res.val res.node self.rank
<VAR>α : Type u_1<VAR>le : α → α → Bool<VAR>res : Batteries.BinomialHeap.Imp.FindMin α<VAR>self : Batteries.BinomialHeap.Imp.FindMin.WF le res<VAR>s : Batteries.BinomialHeap.Imp.Heap α<GOAL>Batteries.BinomialHeap.Imp.Heap.WF le self.rank s → Batteries.BinomialHeap.Imp.Heap.WF le 0 (res.before s)
<VAR>α : Type u_1<VAR>le : α → α → Bool<VAR>n : Nat<VAR>a : α<VAR>s' s : Batteries.BinomialHeap.Imp.Heap α<VAR>h : Batteries.BinomialHeap.Imp.Heap.WF le n s<VAR>eq : Batteries.BinomialHeap.Imp.Heap.deleteMin le s = some (a, s')<GOAL>Batteries.BinomialHeap.Imp.Heap.WF le 0 s'
<VAR>α : Type u_1<VAR>s : Batteries.BinomialHeap.Imp.Heap α<VAR>le : α → α → Bool<VAR>n : Nat<VAR>tl : Batteries.BinomialHeap.Imp.Heap α<VAR>hwf : Batteries.BinomialHeap.Imp.Heap.WF le n s<GOAL>Batteries.BinomialHeap.Imp.Heap.tail? le s = some tl → Batteries.BinomialHeap.Imp.Heap.WF le 0 tl
<VAR>α : Type u_1<VAR>s : Batteries.BinomialHeap.Imp.Heap α<VAR>le : α → α → Bool<VAR>n : Nat<VAR>hwf : Batteries.BinomialHeap.Imp.Heap.WF le n s<GOAL>Batteries.BinomialHeap.Imp.Heap.WF le 0 (Batteries.BinomialHeap.Imp.Heap.tail le s)
<VAR>n : Nat<GOAL>Int.ofNat n = ↑n
<VAR>n : Int<VAR>s : Nat<GOAL>n >>> s = n.shiftRight s
<VAR>n s : Nat<GOAL>↑n >>> s = ↑(n >>> s)
<VAR>m n : Nat<GOAL>Int.negSucc m >>> n = Int.negSucc (m >>> n)
<VAR>i : Int<VAR>m n : Nat<GOAL>i >>> (m + n) = i >>> m >>> n
<VAR>m : Int<VAR>n : Nat<GOAL>m >>> n = m / ↑(2 ^ n)
<VAR>m n : Nat<GOAL>↑(m / n) = ↑m / ↑n
<VAR>m n : Nat<GOAL>↑(m / n) = (↑m).div ↑n
<VAR>m n : Nat<GOAL>↑(m / n) = (↑m).fdiv ↑n
<VAR>b : Int<VAR>e : Nat<GOAL>b ^ (e + 1) = b ^ e * b
<VAR>b : Int<VAR>e : Nat<GOAL>b ^ (e + 1) = b * b ^ e
<VAR>n m : Nat<VAR>h : n ≤ m<VAR>i : Nat<GOAL>n ^ i ≤ m ^ i
<VAR>n : Nat<VAR>hx : n > 0<VAR>i j : Nat<GOAL>i ≤ j → n ^ i ≤ n ^ j
<VAR>n : Nat<VAR>m : Nat<VAR>h : 0 < n<GOAL>0 < n ^ m
<VAR>b n : Nat<GOAL>↑(b ^ n) = ↑b ^ n
<VAR>a b : Int<GOAL>↑(a.gcd b) ∣ a
<VAR>a b : Int<GOAL>↑(a.gcd b) ∣ b
<VAR>a : Int<GOAL>Int.gcd 1 a = 1
<VAR>a : Int<GOAL>a.gcd 1 = 1
<VAR>a b : Int<GOAL>(-a).gcd b = a.gcd b
<VAR>a b : Int<GOAL>a.gcd (-b) = a.gcd b
<VAR>m n : Int<VAR>hm : m ≠ 0<VAR>hn : n ≠ 0<GOAL>m.lcm n ≠ 0
<VAR>a b : Int<GOAL>a ∣ ↑(a.lcm b)
<VAR>a b : Int<GOAL>b ∣ ↑(a.lcm b)
<VAR>a : Int<GOAL>a.lcm a = a.natAbs
<VAR>s₁ s₂ s₃ : String<GOAL>s₁ < s₂ → s₂ < s₃ → s₁ < s₃
<VAR>s₁ s₂ : String<VAR>h₁ : ¬s₁ < s₂<VAR>h₂ : ¬s₂ < s₁<GOAL>s₁ = s₂
<VAR>s : List Char<GOAL>{ data := s }.length = s.length
<VAR>i : Nat<VAR>c : Char<GOAL>0 < i + c.utf8Size
<VAR>i n : Nat<VAR>c : Char<GOAL>i ≠ n + c.utf8Size + i
<VAR>i n : Nat<VAR>c : Char<GOAL>i ≠ i + (n + c.utf8Size)
<VAR>cs : List Char<GOAL>{ data := cs }.utf8ByteSize = String.utf8Len cs
<VAR>c : Char<VAR>cs : List Char<GOAL>String.utf8Len (c :: cs) = String.utf8Len cs + c.utf8Size
<VAR>cs₁ cs₂ : List Char<GOAL>String.utf8Len (cs₁ ++ cs₂) = String.utf8Len cs₁ + String.utf8Len cs₂
<VAR>cs₁ cs₂ : List Char<GOAL>String.utf8Len (cs₁.reverseAux cs₂) = String.utf8Len cs₁ + String.utf8Len cs₂
<VAR>cs : List Char<GOAL>String.utf8Len cs.reverse = String.utf8Len cs
<VAR>l : List Char<GOAL>String.utf8Len l = 0 ↔ l = []
<VAR>cs₁ cs₂ : List Char<GOAL>cs₁.Sublist cs₂ → String.utf8Len cs₁ ≤ String.utf8Len cs₂
<VAR>cs₁ cs₂ : List Char<VAR>h : cs₁ <:+: cs₂<GOAL>String.utf8Len cs₁ ≤ String.utf8Len cs₂
<VAR>cs₁ cs₂ : List Char<VAR>h : cs₁ <:+ cs₂<GOAL>String.utf8Len cs₁ ≤ String.utf8Len cs₂
<VAR>cs₁ cs₂ : List Char<VAR>h : cs₁ <+: cs₂<GOAL>String.utf8Len cs₁ ≤ String.utf8Len cs₂
<VAR>cs : List Char<GOAL>{ data := cs }.endPos = { byteIdx := String.utf8Len cs }
<VAR>p : String.Pos<VAR>c : Char<GOAL>p < p + c