ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>p : Prop<VAR>Decidable p<GOAL>p ∨ ¬p
<VAR>p : Prop<VAR>dec : Decidable p<VAR>h : ¬p → False<GOAL>p
<VAR>p : Prop<VAR>Decidable p<GOAL>¬¬p → p
<VAR>p q : Prop<VAR>d₁ : Decidable p<VAR>d₂ : Decidable q<GOAL>¬(p ∧ q) ↔ ¬p ∨ ¬q
<VAR>c : Prop<VAR>h : Decidable c<VAR>hc : c<VAR>α : Sort u<VAR>t e : α<GOAL>ite c t e = t
<VAR>c : Prop<VAR>h : Decidable c<VAR>hnc : ¬c<VAR>α : Sort u<VAR>t e : α<GOAL>ite c t e = e
<VAR>c : Prop<VAR>h : Decidable c<VAR>hc : c<VAR>α : Sort u<VAR>t : c → α<VAR>e : ¬c → α<GOAL>dite c t e = t hc
<VAR>c : Prop<VAR>h : Decidable c<VAR>hnc : ¬c<VAR>α : Sort u<VAR>t : c → α<VAR>e : ¬c → α<GOAL>dite c t e = e hnc
<VAR>c : Prop<VAR>h : Decidable c<VAR>α : Sort u<VAR>t e : α<GOAL>(if x : c then t else e) = ite c t e
<VAR>α : Sort u<VAR>p : α → Prop<GOAL>(Exists fun x => p x) → Nonempty α
<VAR>α : Sort u<VAR>self : Subsingleton α<VAR>a b : α<GOAL>a = b
<VAR>α : Sort u<VAR>h : Subsingleton α<VAR>a b : α<GOAL>a = b
<VAR>α β : Sort u<VAR>h₁ : Subsingleton α<VAR>h₂ : α = β<VAR>a : α<VAR>b : β<GOAL>HEq a b
<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.casesOn h h₂ h₁)
<VAR>α : Sort u<VAR>r : α → α → Prop<VAR>self : Equivalence r<VAR>x y z : α<GOAL>r x y → r y z → r x z
<VAR>α : Sort u<VAR>r : α → α → Prop<VAR>self : Equivalence r<VAR>x : α<GOAL>r x x
<VAR>α : Sort u<VAR>r : α → α → Prop<VAR>self : Equivalence r<VAR>x y : α<GOAL>r x y → r y x
<VAR>α : Type u<VAR>p : α → Prop<GOAL>(Subtype fun x => p x) → Exists fun x => p x
<VAR>α : Type u<VAR>p : α → Prop<VAR>a1 a2 : Subtype fun x => p x<GOAL>a1.val = a2.val → a1 = a2
<VAR>α : Type u<VAR>p : α → Prop<VAR>a : Subtype fun x => p x<VAR>h : p a.val<GOAL>⟨a.val, h⟩ = a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LT α<VAR>LT β<VAR>s t : α × β<GOAL>s.lexLt t = (s.fst < t.fst ∨ s.fst = t.fst ∧ s.snd < t.snd)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>p : α × β<GOAL>{ fst := p.fst, snd := p.snd } = p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>f : α → β<VAR>g : γ → δ<VAR>x : α<VAR>y : γ<GOAL>Prod.map f g { fst := x, snd := y } = { fst := f x, snd := g y }
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>f : α → β<VAR>g : γ → δ<VAR>x : α × γ<GOAL>(Prod.map f g x).fst = f x.fst
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>f : α → β<VAR>g : γ → δ<VAR>x : α × γ<GOAL>(Prod.map f g x).snd = g x.snd
<VAR>α : Sort u<VAR>β : α → Sort v<VAR>a₁ a₂ : α<VAR>b₁ : β a₁<VAR>b₂ : β a₂<VAR>h₁ : a₁ = a₂<VAR>h₂ : Eq.ndrec b₁ h₁ = b₂<GOAL>⟨a₁, b₁⟩ = ⟨a₂, b₂⟩
<VAR>α : Sort u<VAR>self : Setoid α<GOAL>Equivalence Setoid.r
<VAR>α : Sort u<VAR>Setoid α<VAR>a : α<GOAL>a ≈ a
<VAR>α : Sort u<VAR>Setoid α<VAR>a b : α<VAR>hab : a ≈ b<GOAL>b ≈ a
<VAR>α : Sort u<VAR>Setoid α<VAR>a b c : α<VAR>hab : a ≈ b<VAR>hbc : b ≈ c<GOAL>a ≈ c
<VAR>a b : Prop<VAR>h₁ : a → b<VAR>h₂ : b → a<GOAL>a = b
<VAR>m n : Nat<GOAL>m.succ = n.succ → m = n
<VAR>u v : Nat<GOAL>(u.succ = v.succ) = (u = v)
<VAR>α : Type u_1<VAR>BEq α<VAR>LawfulBEq α<VAR>a b : α<GOAL>(a == b) = true ↔ a = b
<VAR>a b : Prop<VAR>p : Prop → Prop<VAR>h₁ : a ↔ b<VAR>h₂ : p a<GOAL>p b
<VAR>a : Prop<VAR>h : a → False<GOAL>¬a
<VAR>a b : Prop<VAR>H2 : ¬b<VAR>H1 : a → b<GOAL>¬a
<VAR>a b : Prop<VAR>h : a ↔ b<GOAL>¬a ↔ ¬b
<VAR>a : Prop<GOAL>¬¬¬a ↔ ¬a
<VAR>a b : Prop<VAR>ha : a<VAR>hb : b<GOAL>a ↔ b
<VAR>a b : Prop<VAR>ha : ¬a<VAR>hb : ¬b<GOAL>a ↔ b
<VAR>a b : Prop<VAR>ha : a<GOAL>(a ↔ b) ↔ b
<VAR>a b : Prop<VAR>ha : a<GOAL>(b ↔ a) ↔ b
<VAR>a b : Prop<VAR>ha : ¬a<GOAL>(a ↔ b) ↔ ¬b
<VAR>a b : Prop<VAR>ha : ¬a<GOAL>(b ↔ a) ↔ ¬b
<VAR>a : Prop<VAR>h : a ↔ True<GOAL>a
<VAR>a : Prop<VAR>h : a<GOAL>a ↔ True
<VAR>p : Prop<GOAL>(p ↔ False) → ¬p
<VAR>a : Prop<VAR>h : ¬a<GOAL>a ↔ False
<VAR>a : Prop<VAR>h : a<GOAL>¬a ↔ False
<VAR>a b : Prop<GOAL>a = b → (a ↔ b)
<VAR>a b : Prop<GOAL>¬(a ↔ b) → a ≠ b
<VAR>a b : Prop<GOAL>(a ↔ b) ↔ a = b
<VAR>a b : Prop<GOAL>a = b ↔ (a ↔ b)
<VAR>α : Sort u_1<VAR>a : α<GOAL>a = a ↔ True
<VAR>α : Sort u_1<VAR>a : α<GOAL>a ≠ a ↔ False
<VAR>a b : Prop<GOAL>(a ↔ b) ↔ (b → a) ∧ (a → b)
<VAR>a : Prop<GOAL>¬(a ↔ ¬a)
<VAR>α : Sort u_1<VAR>a : α<GOAL>HEq a a ↔ True
<VAR>a b : Prop<GOAL>¬(a → b) → ¬¬a
<VAR>b a : Prop<GOAL>¬(a → b) → ¬b
<VAR>a : Prop<GOAL>a → ¬a ↔ ¬a
<VAR>α β : Prop<VAR>h : α<GOAL>β → α
<VAR>a b c d : Prop<VAR>h₀ : c → a<VAR>h₁ : b → d<GOAL>(a → b) → c → d
<VAR>b a : Prop<VAR>ha : a<GOAL>a → b ↔ b
<VAR>a : Prop<GOAL>a → False ↔ ¬a
<VAR>a b c : Prop<GOAL>a → b → c ↔ b → a → c
<VAR>a b : Prop<GOAL>a → ¬b ↔ b → ¬a
<VAR>a b c : Prop<VAR>h : a ↔ b<GOAL>a → c ↔ b → c
<VAR>a b c : Prop<VAR>h : a → (b ↔ c)<GOAL>a → b ↔ a → c
<VAR>a b c d : Prop<VAR>h₁ : a ↔ c<VAR>h₂ : c → (b ↔ d)<GOAL>a → b ↔ c → d
<VAR>a b c d : Prop<VAR>h₁ : a ↔ c<VAR>h₂ : b ↔ d<GOAL>a → b ↔ c → d
<VAR>a b : Prop<VAR>hb : ¬b<GOAL>a → b ↔ ¬a
<VAR>α : Sort u<VAR>r : α → α → Prop<VAR>β : Sort v<VAR>f : α → β<VAR>c : ∀ (a b : α), r a b → f a = f b<VAR>a : α<GOAL>Quot.lift f c (Quot.mk r a) = f a
<VAR>α : Sort u<VAR>r : α → α → Prop<VAR>motive : Quot r → Prop<VAR>p : ∀ (a : α), motive (Quot.mk r a)<VAR>a : α<GOAL>⋯ = ⋯
<VAR>α : Sort u<VAR>r : α → α → Prop<VAR>motive : Quot r → Prop<VAR>q : Quot r<VAR>h : ∀ (a : α), motive (Quot.mk r a)<GOAL>motive q
<VAR>α : Sort u<VAR>r : α → α → Prop<VAR>q : Quot r<GOAL>Exists fun a => Quot.mk r a = q
<VAR>α : Sort u<VAR>r : α → α → Prop<VAR>motive : Quot r → Sort v<VAR>f : (a : α) → motive (Quot.mk r a)<VAR>h : ∀ (a b : α) (p : r a b), Eq.ndrec (f a) ⋯ = f b<VAR>a b : α<GOAL>r a b → Quot.indep f a = Quot.indep f b
<VAR>α : Sort u<VAR>r : α → α → Prop<VAR>motive : Quot r → Sort v<VAR>f : (a : α) → motive (Quot.mk r a)<VAR>h : ∀ (a b : α) (p : r a b), Eq.ndrec (f a) ⋯ = f b<VAR>q : Quot r<GOAL>(Quot.lift (Quot.indep f) ⋯ q).fst = q
<VAR>α : Sort u<VAR>s : Setoid α<VAR>a b : α<GOAL>a ≈ b → Quotient.mk s a = Quotient.mk s b
<VAR>α : Sort u<VAR>s : Setoid α<VAR>motive : Quotient s → Prop<GOAL>(∀ (a : α), motive (Quotient.mk s a)) → ∀ (q : Quotient s), motive q
<VAR>α : Sort u<VAR>s : Setoid α<VAR>motive : Quotient s → Prop<VAR>q : Quotient s<VAR>h : ∀ (a : α), motive (Quotient.mk s a)<GOAL>motive q
<VAR>α : Sort u<VAR>s : Setoid α<VAR>q : Quotient s<GOAL>Exists fun a => Quotient.mk s a = q
<VAR>α : Sort uA<VAR>β : Sort uB<VAR>s₁ : Setoid α<VAR>s₂ : Setoid β<VAR>motive : Quotient s₁ → Quotient s₂ → Prop<VAR>h : ∀ (a : α) (b : β), motive (Quotient.mk s₁ a) (Quotient.mk s₂ b)<VAR>q₁ : Quotient s₁<VAR>q₂ : Quotient s₂<GOAL>motive q₁ q₂
<VAR>α : Sort uA<VAR>β : Sort uB<VAR>s₁ : Setoid α<VAR>s₂ : Setoid β<VAR>motive : Quotient s₁ → Quotient s₂ → Prop<VAR>q₁ : Quotient s₁<VAR>q₂ : Quotient s₂<VAR>h : ∀ (a : α) (b : β), motive (Quotient.mk s₁ a) (Quotient.mk s₂ b)<GOAL>motive q₁ q₂
<VAR>α : Sort uA<VAR>β : Sort uB<VAR>φ : Sort uC<VAR>s₁ : Setoid α<VAR>s₂ : Setoid β<VAR>s₃ : Setoid φ<VAR>motive : Quotient s₁ → Quotient s₂ → Quotient s₃ → Prop<VAR>q₁ : Quotient s₁<VAR>q₂ : Quotient s₂<VAR>q₃ : Quotient s₃<VAR>h : ∀ (a : α) (b : β) (c : φ), motive (Quotient.mk s₁ a) (Quotient.mk s₂ b) (Quotient.mk s₃ c)<GOAL>motive q₁ q₂ q₃
<VAR>α : Sort u<VAR>s : Setoid α<VAR>q : Quotient s<GOAL>Quotient.rel q q
<VAR>α : Sort u<VAR>s : Setoid α<VAR>q₁ q₂ : Quotient s<GOAL>q₁ = q₂ → Quotient.rel q₁ q₂
<VAR>α : Sort u<VAR>s : Setoid α<VAR>a b : α<GOAL>Quotient.mk s a = Quotient.mk s b → a ≈ b
<VAR>α : Sort u<VAR>β : α → Sort v<VAR>f g : (x : α) → β x<VAR>h : ∀ (x : α), f x = g x<GOAL>f = g
<VAR>α : Type u<VAR>motive : Squash α → Prop<VAR>h : ∀ (a : α), motive (Squash.mk a)<VAR>q : Squash α<GOAL>motive q
<VAR>α : Sort u<VAR>r : α → α → Prop<VAR>self : Antisymm r<VAR>a b : α<GOAL>r a b → r b a → a = b
<VAR>α : Type u<VAR>LE α<VAR>x y : α<GOAL>x ≥ y ↔ y ≤ x
<VAR>α : Type u<VAR>LT α<VAR>x y : α<GOAL>x > y ↔ y < x
<VAR>α : Type u<VAR>a b c : α<VAR>LE α<VAR>h₁ : a = b<VAR>h₂ : b ≤ c<GOAL>a ≤ c
<VAR>α : Type u<VAR>a b c : α<VAR>LE α<VAR>h₁ : a ≤ b<VAR>h₂ : b = c<GOAL>a ≤ c
<VAR>α : Type u<VAR>a b c : α<VAR>LT α<VAR>h₁ : a = b<VAR>h₂ : b < c<GOAL>a < c
<VAR>α : Type u<VAR>a b c : α<VAR>LT α<VAR>h₁ : a < b<VAR>h₂ : b = c<GOAL>a < c
<VAR>α : Sort u<VAR>op : α → α → α<VAR>self : Std.Associative op<VAR>a b c : α<GOAL>op (op a b) c = op a (op b c)
<VAR>α : Sort u<VAR>op : α → α → α<VAR>self : Std.Commutative op<VAR>a b : α<GOAL>op a b = op b a
<VAR>α : Sort u<VAR>op : α → α → α<VAR>self : Std.IdempotentOp op<VAR>x : α<GOAL>op x x = x
<VAR>α : Sort u<VAR>β : Sort u_1<VAR>op : α → β → β<VAR>o : outParam α<VAR>self : Std.LawfulLeftIdentity op o<VAR>a : β<GOAL>op o a = a
<VAR>α : Sort u<VAR>β : Sort u_1<VAR>op : α → β → α<VAR>o : outParam β<VAR>self : Std.LawfulRightIdentity op o<VAR>a : α<GOAL>op a o = a
<VAR>p q : Prop<GOAL>(p ↔ q) = (p = q)
<VAR>p : Prop<GOAL>(p = False) = ¬p
<VAR>p q : Prop<GOAL>(¬p = q) = (p = ¬q)
<VAR>p q : Prop<GOAL>(p → q) = (¬p ∨ q)
<VAR>p q : Prop<GOAL>(¬(p ∧ q)) = (¬p ∨ ¬q)
<VAR>p : Prop<GOAL>∀ {x : Decidable p} (q r : Prop), (¬if p then q else r) = if p then ¬q else ¬r
<VAR>α : Sort u_1<VAR>p : α → Prop<GOAL>(¬∀ (x : α), p x) = ∃ x, ¬p x
<VAR>α : Sort u_1<VAR>p : α → Prop<GOAL>(¬∃ x, p x) = ∀ (x : α), ¬p x
<VAR>α : Type u_1<VAR>c : Bool<VAR>a b : α<GOAL>(bif c then a else b) = if c = true then a else b
<VAR>a b : Nat<GOAL>(a < b) = (a + 1 ≤ b)
<VAR>a b : Int<GOAL>(a < b) = (a + 1 ≤ b)
<VAR>α : Type u_1<VAR>Inhabited α<GOAL>outOfBounds = default
<VAR>cont : Type u<VAR>idx : Type v<VAR>elem : outParam (Type w)<VAR>dom : outParam (cont → idx → Prop)<VAR>ge : GetElem? cont idx elem dom<VAR>self : LawfulGetElem cont idx elem dom<VAR>Inhabited elem<VAR>c : cont<VAR>i : idx<GOAL>getElem! c i = match getElem? c i with | some e => e | none => default
<VAR>cont : Type u<VAR>idx : Type v<VAR>elem : outParam (Type w)<VAR>dom : outParam (cont → idx → Prop)<VAR>ge : GetElem? cont idx elem dom<VAR>self : LawfulGetElem cont idx elem dom<VAR>c : cont<VAR>i : idx<VAR>Decidable (dom c i)<GOAL>getElem? c i = if h : dom c i then some (getElem c i h) else none
<VAR>cont : Type u_1<VAR>idx : Type u_2<VAR>elem : Type u_3<VAR>dom : cont → idx → Prop<VAR>GetElem? cont idx elem dom<VAR>LawfulGetElem cont idx elem dom<VAR>c : cont<VAR>i : idx<VAR>h : dom c i<VAR>Decidable (dom c i)<GOAL>getElem? c i = some (getElem c i h)
<VAR>cont : Type u_1<VAR>idx : Type u_2<VAR>elem : Type u_3<VAR>dom : cont → idx → Prop<VAR>GetElem? cont idx elem dom<VAR>LawfulGetElem cont idx elem dom<VAR>c : cont<VAR>i : idx<VAR>h : ¬dom c i<VAR>Decidable (dom c i)<GOAL>getElem? c i = none
<VAR>cont : Type u_1<VAR>idx : Type u_2<VAR>elem : Type u_3<VAR>dom : cont → idx → Prop<VAR>GetElem? cont idx elem dom<VAR>LawfulGetElem cont idx elem dom<VAR>Inhabited elem<VAR>c : cont<VAR>i : idx<VAR>h : dom c i<VAR>Decidable (dom c i)<GOAL>getElem! c i = getElem c i h
<VAR>cont : Type u_1<VAR>idx : Type u_2<VAR>elem : Type u_3<VAR>dom : cont → idx → Prop<VAR>GetElem? cont idx elem dom<VAR>LawfulGetElem cont idx elem dom<VAR>Inhabited elem<VAR>c : cont<VAR>i : idx<VAR>h : ¬dom c i<VAR>Decidable (dom c i)<GOAL>getElem! c i = default
<VAR>Cont : Type u_1<VAR>Elem : Type u_2<VAR>Dom : Cont → Nat → Prop<VAR>n : Nat<VAR>GetElem? Cont Nat Elem Dom<VAR>a : Cont<VAR>i : Fin n<VAR>h : Dom a ↑i<GOAL>getElem a i h = getElem a (↑i) h
<VAR>Cont : Type u_1<VAR>Elem : Type u_2<VAR>Dom : Cont → Nat → Prop<VAR>n : Nat<VAR>h : GetElem? Cont Nat Elem Dom<VAR>a : Cont<VAR>i : Fin n<VAR>Decidable (Dom a ↑i)<GOAL>getElem? a i = getElem? a ↑i
<VAR>Cont : Type u_1<VAR>Elem : Type u_2<VAR>Dom : Cont → Nat → Prop<VAR>n : Nat<VAR>GetElem? Cont Nat Elem Dom<VAR>a : Cont<VAR>i : Fin n<VAR>Decidable (Dom a ↑i)<VAR>Inhabited Elem<GOAL>getElem! a i = getElem! a ↑i
<VAR>α : Type u_1<VAR>a : α<VAR>as : List α<VAR>h : 0 < (a :: as).length<GOAL>getElem (a :: as) 0 h = a
<VAR>α : Type u_1<VAR>a : α<VAR>as : List α<VAR>i : Nat<VAR>h : i + 1 < (a :: as).length<GOAL>getElem (a :: as) (i + 1) h = getElem as i ⋯
<VAR>α : Type u_1<VAR>as : List α<VAR>i : Nat<VAR>h : i < as.length<GOAL>getElem as i h :: List.drop (i + 1) as = List.drop i as
<VAR>t : Int<VAR>c : Lean.Omega.Constraint<VAR>v : Int<GOAL>c.sat v = true → (c.translate t).sat (v + t) = true
<VAR>c : Lean.Omega.Constraint<VAR>v : Int<GOAL>c.sat v = true → c.neg.sat (-v) = true
<VAR>t : Int<GOAL>Lean.Omega.Constraint.trivial.sat t = true
<VAR>r t : Int<GOAL>(Lean.Omega.Constraint.exact r).sat t = decide (r = t)
<VAR>c : Lean.Omega.Constraint<VAR>h : c.isImpossible = true<VAR>t : Int<GOAL>¬c.sat t = true
<VAR>t : Int<VAR>c : Lean.Omega.Constraint<VAR>k : Int<VAR>w : c.sat t = true<GOAL>(Lean.Omega.Constraint.scale k c).sat (k * t) = true
<VAR>c₁ c₂ : Lean.Omega.Constraint<VAR>x₁ x₂ : Int<VAR>w₁ : c₁.sat x₁ = true<VAR>w₂ : c₂.sat x₂ = true<GOAL>(c₁.add c₂).sat (x₁ + x₂) = true
<VAR>c₁ c₂ : Lean.Omega.Constraint<VAR>x₁ x₂ : Int<VAR>a : Int<VAR>w₁ : c₁.sat x₁ = true<VAR>b : Int<VAR>w₂ : c₂.sat x₂ = true<GOAL>(Lean.Omega.Constraint.combo a c₁ b c₂).sat (a * x₁ + b * x₂) = true
<VAR>c c' : Lean.Omega.Constraint<VAR>t : Int<GOAL>((c.combine c').sat t = true) = (c.sat t = true ∧ c'.sat t = true)
<VAR>c : Lean.Omega.Constraint<VAR>t : Int<VAR>k : Nat<VAR>n : k ≠ 0<VAR>h : ↑k ∣ t<VAR>w : c.sat t = true<GOAL>(c.div k).sat (t / ↑k) = true
<VAR>s t : Lean.Omega.Constraint<VAR>x y : Lean.Omega.Coeffs<VAR>ws : s.sat' x y = true<VAR>wt : t.sat' x y = true<GOAL>(s.combine t).sat' x y = true
<VAR>c : Lean.Omega.Constraint<VAR>x y : Lean.Omega.Coeffs<VAR>h : x.gcd ≠ 0<VAR>w : c.sat (x.dot y) = true<GOAL>(c.div x.gcd).sat' (x.sdiv ↑x.gcd) y = true
<VAR>c : Lean.Omega.Constraint<VAR>h : c.isImpossible = true<VAR>x y : Lean.Omega.Coeffs<GOAL>¬c.sat' x y = true
<VAR>c : Int<VAR>x y : Lean.Omega.Coeffs<VAR>w : c + x.dot y ≥ 0<GOAL>{ lowerBound := some (-c), upperBound := none }.sat' x y = true
<VAR>c : Int<VAR>x y : Lean.Omega.Coeffs<VAR>w : c + x.dot y = 0<GOAL>{ lowerBound := some (-c), upperBound := some (-c) }.sat' x y = true
<VAR>s : Lean.Omega.Constraint<VAR>x : Lean.Omega.Coeffs<VAR>s' : Lean.Omega.Constraint<VAR>x' : Lean.Omega.Coeffs<VAR>w : Lean.Omega.normalize? (s, x) = some (s', x')<GOAL>Lean.Omega.normalizeConstraint s x = s' ∧ Lean.Omega.normalizeCoeffs s x = x'
<VAR>s : Lean.Omega.Constraint<VAR>x v : Lean.Omega.Coeffs<VAR>w : s.sat' x v = true<GOAL>(Lean.Omega.normalizeConstraint s x).sat' (Lean.Omega.normalizeCoeffs s x) v = true
<VAR>s : Lean.Omega.Constraint<VAR>x : Lean.Omega.Coeffs<VAR>s' : Lean.Omega.Constraint<VAR>x' : Lean.Omega.Coeffs<VAR>w : Lean.Omega.positivize? (s, x) = some (s', x')<GOAL>Lean.Omega.positivizeConstraint s x = s' ∧ Lean.Omega.positivizeCoeffs s x = x'
<VAR>s : Lean.Omega.Constraint<VAR>x v : Lean.Omega.Coeffs<VAR>w : s.sat' x v = true<GOAL>(Lean.Omega.positivizeConstraint s x).sat' (Lean.Omega.positivizeCoeffs s x) v = true
<VAR>s : Lean.Omega.Constraint<VAR>x v : Lean.Omega.Coeffs<VAR>w : s.sat' x v = true<GOAL>(Lean.Omega.tidyConstraint s x).sat' (Lean.Omega.tidyCoeffs s x) v = true
<VAR>s t : Lean.Omega.Constraint<VAR>a : Int<VAR>x : Lean.Omega.Coeffs<VAR>b : Int<VAR>y v : Lean.Omega.Coeffs<VAR>wx : s.sat' x v = true<VAR>wy : t.sat' y v = true<GOAL>(Lean.Omega.Constraint.combo a s b t).sat' (Lean.Omega.Coeffs.combo a x b y) v = true
<VAR>m : Nat<VAR>r : Int<VAR>i : Nat<VAR>x v : Lean.Omega.Coeffs<VAR>h : x.length ≤ i<VAR>p : v.get i = Lean.Omega.bmod_div_term m x v<VAR>w : (Lean.Omega.Constraint.exact r).sat' x v = true<GOAL>(Lean.Omega.Constraint.exact (r.bmod m)).sat' (Lean.Omega.bmod_coeffs m i x) v = true
<VAR>n : Nat<VAR>a : Fin n<GOAL>sizeOf a = ↑a + 1
<VAR>a : UInt8<GOAL>sizeOf a = a.toNat + 2
<VAR>a : UInt16<GOAL>sizeOf a = a.toNat + 2
<VAR>a : UInt32<GOAL>sizeOf a = a.toNat + 2
<VAR>a : UInt64<GOAL>sizeOf a = a.toNat + 2
<VAR>a : USize<GOAL>sizeOf a = a.toNat + 2
<VAR>a : Char<GOAL>sizeOf a = a.toNat + 3
<VAR>α : Sort u_1<VAR>p : α → Prop<VAR>s : Subtype p<GOAL>sizeOf s = sizeOf s.val + 1
<VAR>α : Sort u_1<GOAL>∀ {x : Decidable True} (t e : α), (if True then t else e) = t
<VAR>α : Sort u_1<GOAL>∀ {x : Decidable False} (t e : α), (if False then t else e) = e
<VAR>c : Prop<VAR>Decidable c<VAR>α : Sort u_1<VAR>t : α<GOAL>(if c then t else t) = t
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>f : α → β<VAR>P : Prop<VAR>Decidable P<VAR>x : P → α<VAR>y : ¬P → α<GOAL>f (dite P x y) = if h : P then f (x h) else f (y h)
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>f : α → β<VAR>P : Prop<VAR>Decidable P<VAR>x y : α<GOAL>f (if P then x else y) = if P then f x else f y
<VAR>α : Sort u_1<VAR>a : α<VAR>P : Prop<VAR>Decidable P<VAR>B : ¬P → α<GOAL>dite P (fun x => a) B = a ↔ ∀ (h : ¬P), B h = a
<VAR>α : Sort u_1<VAR>b : α<VAR>P : Prop<VAR>Decidable P<VAR>A : P → α<GOAL>(dite P A fun x => b) = b ↔ ∀ (h : P), A h = b
<GOAL>∀ {α : Sort u_1} {a b : α} {P : Prop} [inst : Decidable P], (if P then a else b) = a ↔ ¬P → b = a
<GOAL>∀ {α : Sort u_1} {a b : α} {P : Prop} [inst : Decidable P], (if P then a else b) = b ↔ P → a = b
<VAR>P : Prop<GOAL>∀ {α : Sort u_1} {a b : α} [inst : Decidable P], (if x : P then a else b) = if P then a else b
<VAR>P : Prop<GOAL>∀ {α : Type u_1} {x : α} [inst : Decidable P], (if P then some x else none) = none ↔ ¬P
<VAR>P : Prop<GOAL>∀ {α : Type u_1} {x y : α} [inst : Decidable P], (if P then some x else none) = some y ↔ P ∧ x = y
<VAR>P : Prop<VAR>α : Type u_1<VAR>Decidable P<VAR>x : P → α<GOAL>(if h : P then some (x h) else none) = none ↔ ¬P
<VAR>P : Prop<VAR>α : Type u_1<VAR>Decidable P<VAR>x : P → α<VAR>y : α<GOAL>(if h : P then some (x h) else none) = some y ↔ ∃ h, x h = y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>b₁ b₂ : Batteries.HashMap.Imp.Buckets α β<GOAL>b₁.val.data = b₂.val.data → b₁ = b₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>self : Batteries.HashMap.Imp.Buckets α β<VAR>i : USize<VAR>d : Batteries.AssocList α β<VAR>h : i.toNat < self.val.size<GOAL>(self.update i d h).val.data = self.val.data.set i.toNat d
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>self : Batteries.HashMap.Imp.Buckets α β<VAR>i : USize<VAR>d : Batteries.AssocList α β<VAR>h : i.toNat < self.val.size<GOAL>∃ l₁ l₂, self.val.data = l₁ ++ self.val[i] :: l₂ ∧ l₁.length = i.toNat ∧ (self.update i d h).val.data = l₁ ++ d :: l₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>self : Batteries.HashMap.Imp.Buckets α β<VAR>i : USize<VAR>d d' : Batteries.AssocList α β<VAR>h : i.toNat < self.val.size<VAR>h' : i.toNat < (self.update i d h).val.size<GOAL>(self.update i d h).update i d' h' = self.update i d' h
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>data : Batteries.HashMap.Imp.Buckets α β<GOAL>data.size = Nat.sum (List.map (fun x => x.toList.length) data.val.data)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n : Nat<VAR>h : 0 < n<GOAL>(Batteries.HashMap.Imp.Buckets.mk n h).size = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n : Nat<VAR>BEq α<VAR>Hashable α<VAR>h : 0 < n<GOAL>(Batteries.HashMap.Imp.Buckets.mk n h).WF
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>BEq α<VAR>Hashable α<VAR>buckets : Batteries.HashMap.Imp.Buckets α β<VAR>i : USize<VAR>d : Batteries.AssocList α β<VAR>h : i.toNat < buckets.val.size<VAR>H : buckets.WF<VAR>h₁ : ∀ [inst : PartialEquivBEq α] [inst : Batteries.HashMap.LawfulHashable α], List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) buckets.val[i].toList → List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) d.toList<VAR>h₂ : Batteries.AssocList.All (fun k x => ((hash k).toUSize % buckets.val.size).toNat = i.toNat) buckets.val[i] → Batteries.AssocList.All (fun k x => ((hash k).toUSize % buckets.val.size).toNat = i.toNat) d<GOAL>(buckets.update i d h).WF
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Hashable α<VAR>data : Batteries.HashMap.Imp.Buckets α β<VAR>a : α<VAR>b : β<GOAL>(Batteries.HashMap.Imp.reinsertAux data a b).size = data.size.succ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>BEq α<VAR>Hashable α<VAR>data : Batteries.HashMap.Imp.Buckets α β<VAR>a : α<VAR>b : β<VAR>H : data.WF<VAR>h₁ : ∀ [inst : PartialEquivBEq α] [inst : Batteries.HashMap.LawfulHashable α], Batteries.AssocList.All (fun x x_1 => ¬(a == x) = true) data.val[(Batteries.HashMap.Imp.mkIdx ⋯ (hash a).toUSize).val]<GOAL>(Batteries.HashMap.Imp.reinsertAux data a b).WF
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>sz : Nat<VAR>Hashable α<VAR>buckets : Batteries.HashMap.Imp.Buckets α β<GOAL>(Batteries.HashMap.Imp.expand sz buckets).buckets.size = buckets.size
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Hashable α<VAR>i : Nat<VAR>source : Array (Batteries.AssocList α β)<VAR>target : Batteries.HashMap.Imp.Buckets α β<VAR>hs : ∀ (j : Nat), j < i → source.data[j]?.getD Batteries.AssocList.nil = Batteries.AssocList.nil<GOAL>(Batteries.HashMap.Imp.expand.go i source target).size = Nat.sum (List.map (fun x => x.toList.length) source.data) + target.size
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>BEq α<VAR>Hashable α<VAR>rank : α → Nat<VAR>l : List (α × β)<VAR>i : Nat<VAR>hl₁ : ∀ [inst : PartialEquivBEq α] [inst : Batteries.HashMap.LawfulHashable α], List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) l<VAR>hl₂ : ∀ (x : α × β), x ∈ l → rank x.fst = i<VAR>target : Batteries.HashMap.Imp.Buckets α β<VAR>ht₁ : target.WF<VAR>ht₂ : ∀ (bucket : Batteries.AssocList α β), bucket ∈ target.val.data → Batteries.AssocList.All (fun k x => rank k ≤ i ∧ ∀ [inst : PartialEquivBEq α] [inst : Batteries.HashMap.LawfulHashable α] (x : α × β), x ∈ l → ¬(x.fst == k) = true) bucket<GOAL>(List.foldl (fun d x => Batteries.HashMap.Imp.reinsertAux d x.fst x.snd) target l).WF ∧ ∀ (bucket : Batteries.AssocList α β), bucket ∈ (List.foldl (fun d x => Batteries.HashMap.Imp.reinsertAux d x.fst x.snd) target l).val.data → Batteries.AssocList.All (fun k x => rank k ≤ i) bucket
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>BEq α<VAR>Hashable α<VAR>i : Nat<VAR>source : Array (Batteries.AssocList α β)<VAR>hs₁ : ∀ [inst : Batteries.HashMap.LawfulHashable α] [inst : PartialEquivBEq α] (bucket : Batteries.AssocList α β), bucket ∈ source.data → List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) bucket.toList<VAR>hs₂ : ∀ (j : Nat) (h : j < source.size), Batteries.AssocList.All (fun k x => ((hash k).toUSize % source.size).toNat = j) source[j]<VAR>target : Batteries.HashMap.Imp.Buckets α β<VAR>ht : target.WF ∧ ∀ (bucket : Batteries.AssocList α β), bucket ∈ target.val.data → Batteries.AssocList.All (fun k x => ((hash k).toUSize % source.size).toNat < i) bucket<GOAL>(Batteries.HashMap.Imp.expand.go i source target).WF
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>sz : Nat<VAR>BEq α<VAR>Hashable α<VAR>buckets : Batteries.HashMap.Imp.Buckets α β<VAR>H : buckets.WF<GOAL>(Batteries.HashMap.Imp.expand sz buckets).buckets.WF
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>BEq α<VAR>Hashable α<VAR>m : Batteries.HashMap.Imp α β<VAR>k : α<VAR>v : β<VAR>h : m.size = m.buckets.size<GOAL>(m.insert k v).size = (m.insert k v).buckets.size
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>k : α<VAR>l : List (α × β)<VAR>x : α × β<VAR>p : α × β → Bool<VAR>f : α × β → β<GOAL>x ∈ List.replaceF (fun a => bif p a then some (k, f a) else none) l → x.fst = k ∨ x ∈ l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>k : α<VAR>BEq α<VAR>PartialEquivBEq α<VAR>l : List (α × β)<VAR>f : α × β → β<VAR>H : List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) l<GOAL>List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) (List.replaceF (fun a => bif a.fst == k then some (k, f a) else none) l)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>BEq α<VAR>Hashable α<VAR>m : Batteries.HashMap.Imp α β<VAR>k : α<VAR>v : β<VAR>h : m.buckets.WF<GOAL>(m.insert k v).buckets.WF
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>BEq α<VAR>Hashable α<VAR>m : Batteries.HashMap.Imp α β<VAR>k : α<VAR>h : m.size = m.buckets.size<GOAL>(m.erase k).size = (m.erase k).buckets.size
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>BEq α<VAR>Hashable α<VAR>m : Batteries.HashMap.Imp α β<VAR>k : α<VAR>h : m.buckets.WF<GOAL>(m.erase k).buckets.WF
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β → β<VAR>BEq α<VAR>Hashable α<VAR>m : Batteries.HashMap.Imp α β<VAR>k : α<VAR>h : m.size = m.buckets.size<GOAL>(m.modify k f).size = (m.modify k f).buckets.size
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β → β<VAR>BEq α<VAR>Hashable α<VAR>m : Batteries.HashMap.Imp α β<VAR>k : α<VAR>h : m.buckets.WF<GOAL>(m.modify k f).buckets.WF
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>BEq α<VAR>Hashable α<VAR>m : Batteries.HashMap.Imp α β<VAR>h : m.WF<GOAL>m.size = m.buckets.size ∧ m.buckets.WF
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>BEq α<VAR>Hashable α<VAR>m : Batteries.HashMap.Imp α β<GOAL>m.WF ↔ m.size = m.buckets.size ∧ m.buckets.WF