ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → Part β<GOAL>Part.none.bind f = Part.none
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a : α<VAR>f : α → Part β<GOAL>(Part.some a).bind f = f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>o : Part α<VAR>a : α<VAR>h : a ∈ o<VAR>f : α → Part β<GOAL>o.bind f = f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>x : Part α<GOAL>x.bind (Part.some ∘ f) = Part.map f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → Part β<VAR>o : Part α<VAR>Decidable o.Dom<VAR>(a : α) → Decidable (f a).Dom<VAR>Decidable (o.bind f).Dom<GOAL>(o.bind f).toOption = o.toOption.elim none fun a => (f a).toOption
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_4<VAR>f : Part α<VAR>g : α → Part β<VAR>k : β → Part γ<GOAL>(f.bind g).bind k = f.bind fun x => (g x).bind k
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_4<VAR>f : α → β<VAR>x : Part α<VAR>g : β → Part γ<GOAL>(Part.map f x).bind g = x.bind fun y => g (f y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_4<VAR>f : α → Part β<VAR>x : Part α<VAR>g : β → γ<GOAL>Part.map g (x.bind f) = x.bind fun y => Part.map g (f y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>g : β → γ<VAR>f : α → β<VAR>o : Part α<GOAL>Part.map g (Part.map f o) = Part.map (g ∘ f) o
<VAR>α : Type u_1<VAR>f : α → α<VAR>H : ∀ (x : α), f x = x<VAR>o : Part α<GOAL>Part.map f o = o
<VAR>α : Type u_1<VAR>x : Part α<GOAL>x.bind Part.some = x
<VAR>α : Type u_1<VAR>a : α<GOAL>pure a = Part.some a
<VAR>α β : Type u_4<VAR>f : α → β<VAR>o : Part α<GOAL>f <$> o = Part.map f o
<VAR>α β : Type u_4<VAR>f : Part α<VAR>g : α → Part β<GOAL>f >>= g = f.bind g
<VAR>β α : Type u_2<VAR>x : Part α<VAR>f : α → Part β<VAR>y : Part β<GOAL>x >>= f ≤ y ↔ ∀ a ∈ x, f a ≤ y
<VAR>α : Type u_1<VAR>p : Prop<VAR>o : Part α<VAR>h : p → o.Dom<VAR>a : α<GOAL>a ∈ Part.restrict p o h ↔ p ∧ a ∈ o
<VAR>α : Type u_1<VAR>p : Prop<VAR>f : p → Part α<VAR>h : p<GOAL>(f h).Dom → (Part.assert p f).Dom
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : Part α<VAR>g : α → Part β<VAR>h : f.Dom<GOAL>(g (f.get h)).Dom → (f.bind g).Dom
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : Part α<VAR>g : α → Part β<GOAL>(f.bind g).Dom ↔ ∃ (h : f.Dom), (g (f.get h)).Dom
<VAR>α : Type u_1<VAR>Mul α<VAR>a b : Part α<GOAL>a * b = do let y ← a Part.map (fun x => y * x) b
<VAR>α : Type u_1<VAR>One α<GOAL>1 = Part.some 1
<VAR>α : Type u_1<VAR>Inv α<VAR>a : Part α<GOAL>a⁻¹ = Part.map (fun x => x⁻¹) a
<VAR>α : Type u_1<VAR>Div α<VAR>a b : Part α<GOAL>a / b = do let y ← a Part.map (fun x => y / x) b
<VAR>α : Type u_1<VAR>Mod α<VAR>a b : Part α<GOAL>a % b = do let y ← a Part.map (fun x => y % x) b
<VAR>α : Type u_1<VAR>Append α<VAR>a b : Part α<GOAL>a ++ b = do let y ← a Part.map (fun x => y ++ x) b
<VAR>α : Type u_1<VAR>Inter α<VAR>a b : Part α<GOAL>a ∩ b = do let y ← a Part.map (fun x => y ∩ x) b
<VAR>α : Type u_1<VAR>Union α<VAR>a b : Part α<GOAL>a ∪ b = do let y ← a Part.map (fun x => y ∪ x) b
<VAR>α : Type u_1<VAR>SDiff α<VAR>a b : Part α<GOAL>a \ b = do let y ← a Part.map (fun x => y \ x) b
<VAR>α : Type u_1<VAR>One α<GOAL>1 ∈ 1
<VAR>α : Type u_1<VAR>Zero α<GOAL>0 ∈ 0
<VAR>α : Type u_1<VAR>Add α<VAR>a b : Part α<VAR>ma mb : α<VAR>ha : ma ∈ a<VAR>hb : mb ∈ b<GOAL>ma + mb ∈ a + b
<VAR>α : Type u_1<VAR>Mul α<VAR>a b : Part α<VAR>ma mb : α<VAR>ha : ma ∈ a<VAR>hb : mb ∈ b<GOAL>ma * mb ∈ a * b
<VAR>α : Type u_1<VAR>Add α<VAR>a b : Part α<VAR>hab : (a + b).Dom<GOAL>a.Dom
<VAR>α : Type u_1<VAR>Mul α<VAR>a b : Part α<VAR>hab : (a * b).Dom<GOAL>a.Dom
<VAR>α : Type u_1<VAR>Mul α<VAR>a b : Part α<VAR>hab : (a * b).Dom<GOAL>b.Dom
<VAR>α : Type u_1<VAR>Add α<VAR>a b : Part α<VAR>hab : (a + b).Dom<GOAL>b.Dom
<VAR>α : Type u_1<VAR>Add α<VAR>a b : Part α<VAR>hab : (a + b).Dom<GOAL>(a + b).get hab = a.get ⋯ + b.get ⋯
<VAR>α : Type u_1<VAR>Mul α<VAR>a b : Part α<VAR>hab : (a * b).Dom<GOAL>(a * b).get hab = a.get ⋯ * b.get ⋯
<VAR>α : Type u_1<VAR>Add α<VAR>a b : α<GOAL>Part.some a + Part.some b = Part.some (a + b)
<VAR>α : Type u_1<VAR>Mul α<VAR>a b : α<GOAL>Part.some a * Part.some b = Part.some (a * b)
<VAR>α : Type u_1<VAR>Neg α<VAR>a : Part α<VAR>ma : α<VAR>ha : ma ∈ a<GOAL>-ma ∈ -a
<VAR>α : Type u_1<VAR>Inv α<VAR>a : Part α<VAR>ma : α<VAR>ha : ma ∈ a<GOAL>ma⁻¹ ∈ a⁻¹
<VAR>α : Type u_1<VAR>Neg α<VAR>a : α<GOAL>-Part.some a = Part.some (-a)
<VAR>α : Type u_1<VAR>Inv α<VAR>a : α<GOAL>(Part.some a)⁻¹ = Part.some a⁻¹
<VAR>α : Type u_1<VAR>Div α<VAR>a b : Part α<VAR>ma mb : α<VAR>ha : ma ∈ a<VAR>hb : mb ∈ b<GOAL>ma / mb ∈ a / b
<VAR>α : Type u_1<VAR>Sub α<VAR>a b : Part α<VAR>ma mb : α<VAR>ha : ma ∈ a<VAR>hb : mb ∈ b<GOAL>ma - mb ∈ a - b
<VAR>α : Type u_1<VAR>Sub α<VAR>a b : Part α<VAR>hab : (a - b).Dom<GOAL>a.Dom
<VAR>α : Type u_1<VAR>Div α<VAR>a b : Part α<VAR>hab : (a / b).Dom<GOAL>a.Dom
<VAR>α : Type u_1<VAR>Div α<VAR>a b : Part α<VAR>hab : (a / b).Dom<GOAL>b.Dom
<VAR>α : Type u_1<VAR>Sub α<VAR>a b : Part α<VAR>hab : (a - b).Dom<GOAL>b.Dom
<VAR>α : Type u_1<VAR>Div α<VAR>a b : Part α<VAR>hab : (a / b).Dom<GOAL>(a / b).get hab = a.get ⋯ / b.get ⋯
<VAR>α : Type u_1<VAR>Sub α<VAR>a b : Part α<VAR>hab : (a - b).Dom<GOAL>(a - b).get hab = a.get ⋯ - b.get ⋯
<VAR>α : Type u_1<VAR>Sub α<VAR>a b : α<GOAL>Part.some a - Part.some b = Part.some (a - b)
<VAR>α : Type u_1<VAR>Div α<VAR>a b : α<GOAL>Part.some a / Part.some b = Part.some (a / b)
<VAR>α : Type u_1<VAR>Mod α<VAR>a b : Part α<VAR>ma mb : α<VAR>ha : ma ∈ a<VAR>hb : mb ∈ b<GOAL>ma % mb ∈ a % b
<VAR>α : Type u_1<VAR>Mod α<VAR>a b : Part α<VAR>hab : (a % b).Dom<GOAL>a.Dom
<VAR>α : Type u_1<VAR>Mod α<VAR>a b : Part α<VAR>hab : (a % b).Dom<GOAL>b.Dom
<VAR>α : Type u_1<VAR>Mod α<VAR>a b : Part α<VAR>hab : (a % b).Dom<GOAL>(a % b).get hab = a.get ⋯ % b.get ⋯
<VAR>α : Type u_1<VAR>Mod α<VAR>a b : α<GOAL>Part.some a % Part.some b = Part.some (a % b)
<VAR>α : Type u_1<VAR>Append α<VAR>a b : Part α<VAR>ma mb : α<VAR>ha : ma ∈ a<VAR>hb : mb ∈ b<GOAL>ma ++ mb ∈ a ++ b
<VAR>α : Type u_1<VAR>Append α<VAR>a b : Part α<VAR>hab : (a ++ b).Dom<GOAL>a.Dom
<VAR>α : Type u_1<VAR>Append α<VAR>a b : Part α<VAR>hab : (a ++ b).Dom<GOAL>b.Dom
<VAR>α : Type u_1<VAR>Append α<VAR>a b : Part α<VAR>hab : (a ++ b).Dom<GOAL>(a ++ b).get hab = a.get ⋯ ++ b.get ⋯
<VAR>α : Type u_1<VAR>Append α<VAR>a b : α<GOAL>Part.some a ++ Part.some b = Part.some (a ++ b)
<VAR>α : Type u_1<VAR>Inter α<VAR>a b : Part α<VAR>ma mb : α<VAR>ha : ma ∈ a<VAR>hb : mb ∈ b<GOAL>ma ∩ mb ∈ a ∩ b
<VAR>α : Type u_1<VAR>Inter α<VAR>a b : Part α<VAR>hab : (a ∩ b).Dom<GOAL>a.Dom
<VAR>α : Type u_1<VAR>Inter α<VAR>a b : Part α<VAR>hab : (a ∩ b).Dom<GOAL>b.Dom
<VAR>α : Type u_1<VAR>Inter α<VAR>a b : Part α<VAR>hab : (a ∩ b).Dom<GOAL>(a ∩ b).get hab = a.get ⋯ ∩ b.get ⋯
<VAR>α : Type u_1<VAR>Inter α<VAR>a b : α<GOAL>Part.some a ∩ Part.some b = Part.some (a ∩ b)
<VAR>α : Type u_1<VAR>Union α<VAR>a b : Part α<VAR>ma mb : α<VAR>ha : ma ∈ a<VAR>hb : mb ∈ b<GOAL>ma ∪ mb ∈ a ∪ b
<VAR>α : Type u_1<VAR>Union α<VAR>a b : Part α<VAR>hab : (a ∪ b).Dom<GOAL>a.Dom
<VAR>α : Type u_1<VAR>Union α<VAR>a b : Part α<VAR>hab : (a ∪ b).Dom<GOAL>b.Dom
<VAR>α : Type u_1<VAR>Union α<VAR>a b : Part α<VAR>hab : (a ∪ b).Dom<GOAL>(a ∪ b).get hab = a.get ⋯ ∪ b.get ⋯
<VAR>α : Type u_1<VAR>Union α<VAR>a b : α<GOAL>Part.some a ∪ Part.some b = Part.some (a ∪ b)
<VAR>α : Type u_1<VAR>SDiff α<VAR>a b : Part α<VAR>ma mb : α<VAR>ha : ma ∈ a<VAR>hb : mb ∈ b<GOAL>ma \ mb ∈ a \ b
<VAR>α : Type u_1<VAR>SDiff α<VAR>a b : Part α<VAR>hab : (a \ b).Dom<GOAL>a.Dom
<VAR>α : Type u_1<VAR>SDiff α<VAR>a b : Part α<VAR>hab : (a \ b).Dom<GOAL>b.Dom
<VAR>α : Type u_1<VAR>SDiff α<VAR>a b : Part α<VAR>hab : (a \ b).Dom<GOAL>(a \ b).get hab = a.get ⋯ \ b.get ⋯
<VAR>α : Type u_1<VAR>SDiff α<VAR>a b : α<GOAL>Part.some a \ Part.some b = Part.some (a \ b)
<VAR>α : Type u<VAR>β : Type v<VAR>self : α ≃. β<VAR>a : α<VAR>b : β<GOAL>a ∈ self.invFun b ↔ b ∈ self.toFun a
<VAR>α : Type u<VAR>β : Type v<VAR>f₁ : α → Option β<VAR>f₂ : β → Option α<VAR>h : ∀ (a : α) (b : β), a ∈ f₂ b ↔ b ∈ f₁ a<GOAL>⇑{ toFun := f₁, invFun := f₂, inv := h } = f₁
<VAR>α : Type u<VAR>β : Type v<VAR>f₁ : α → Option β<VAR>f₂ : β → Option α<VAR>h : ∀ (a : α) (b : β), a ∈ f₂ b ↔ b ∈ f₁ a<VAR>x : α<GOAL>{ toFun := f₁, invFun := f₂, inv := h } x = f₁ x
<VAR>α : Type u<VAR>β : Type v<VAR>f g : α ≃. β<VAR>h : ∀ (x : α), f x = g x<GOAL>f = g
<VAR>α : Type u<VAR>β : Type v<VAR>f g : α ≃. β<GOAL>f = g ↔ ∀ (x : α), f x = g x
<VAR>α : Type u<VAR>β : Type v<VAR>f : α ≃. β<VAR>a : α<VAR>b : β<GOAL>a ∈ f.symm b ↔ b ∈ f a
<VAR>α : Type u<VAR>β : Type v<VAR>f : α ≃. β<VAR>a : α<VAR>b : β<GOAL>f.symm b = some a ↔ f a = some b
<VAR>α : Type u<VAR>a : α<GOAL>(PEquiv.refl α) a = some a
<VAR>α : Type u<GOAL>(PEquiv.refl α).symm = PEquiv.refl α
<VAR>α : Type u<VAR>β : Type v<VAR>f : α ≃. β<GOAL>f.symm.symm = f
<VAR>α : Type u<VAR>β : Type v<GOAL>Function.Bijective PEquiv.symm
<VAR>α : Type u<VAR>β : Type v<GOAL>Function.Injective PEquiv.symm
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type x<VAR>f : α ≃. β<VAR>g : β ≃. γ<VAR>h : γ ≃. δ<GOAL>(f.trans g).trans h = f.trans (g.trans h)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : α ≃. β<VAR>g : β ≃. γ<VAR>a : α<VAR>c : γ<GOAL>c ∈ (f.trans g) a ↔ ∃ b ∈ f a, c ∈ g b
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : α ≃. β<VAR>g : β ≃. γ<VAR>a : α<VAR>c : γ<GOAL>(f.trans g) a = some c ↔ ∃ b, f a = some b ∧ g b = some c
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : α ≃. β<VAR>g : β ≃. γ<VAR>a : α<GOAL>(f.trans g) a = none ↔ ∀ (b : β) (c : γ), b ∉ f a ∨ c ∉ g b
<VAR>α : Type u<VAR>β : Type v<VAR>f : α ≃. β<GOAL>(PEquiv.refl α).trans f = f
<VAR>α : Type u<VAR>β : Type v<VAR>f : α ≃. β<GOAL>f.trans (PEquiv.refl β) = f
<VAR>α : Type u<VAR>β : Type v<VAR>f : α ≃. β<VAR>a₁ a₂ : α<VAR>b : β<VAR>h₁ : b ∈ f a₁<VAR>h₂ : b ∈ f a₂<GOAL>a₁ = a₂
<VAR>α : Type u<VAR>β : Type v<VAR>f : α ≃. β<VAR>a₂ : α<VAR>h : ∀ (a₁ : α), a₁ ≠ a₂ → (f a₁).isSome = true<GOAL>Function.Injective ⇑f
<VAR>α : Type u<VAR>β : Type v<VAR>f : α ≃. β<VAR>h : ∀ (a : α), (f a).isSome = true<GOAL>Function.Injective ⇑f
<VAR>α : Type u<VAR>s : Set α<VAR>DecidablePred fun x => x ∈ s<VAR>a : α<GOAL>a ∈ (PEquiv.ofSet s) a ↔ a ∈ s
<VAR>α : Type u<VAR>s : Set α<VAR>DecidablePred fun x => x ∈ s<VAR>a b : α<GOAL>a ∈ (PEquiv.ofSet s) b ↔ a = b ∧ a ∈ s
<VAR>α : Type u<VAR>s : Set α<GOAL>∀ {x : DecidablePred fun x => x ∈ s} {a b : α}, (PEquiv.ofSet s) b = some a ↔ a = b ∧ a ∈ s
<VAR>α : Type u<VAR>s : Set α<GOAL>∀ {x : DecidablePred fun x => x ∈ s} {a : α}, (PEquiv.ofSet s) a = some a ↔ a ∈ s
<VAR>α : Type u<VAR>s : Set α<VAR>DecidablePred fun x => x ∈ s<GOAL>(PEquiv.ofSet s).symm = PEquiv.ofSet s
<VAR>α : Type u<GOAL>PEquiv.ofSet Set.univ = PEquiv.refl α
<VAR>α : Type u<VAR>s : Set α<VAR>DecidablePred fun x => x ∈ s<GOAL>PEquiv.ofSet s = PEquiv.refl α ↔ s = Set.univ
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : α ≃. β<VAR>g : β ≃. γ<GOAL>(f.trans g).symm = g.symm.trans f.symm
<VAR>α : Type u<VAR>β : Type v<VAR>f : α ≃. β<GOAL>f.trans f.symm = PEquiv.ofSet {a | (f a).isSome = true}
<VAR>α : Type u<VAR>β : Type v<VAR>f : α ≃. β<GOAL>f.symm.trans f = PEquiv.ofSet {b | (f.symm b).isSome = true}
<VAR>α : Type u<VAR>β : Type v<VAR>f : α ≃. β<GOAL>f.trans f.symm = PEquiv.refl α ↔ ∀ (a : α), (f a).isSome = true
<VAR>α : Type u<VAR>β : Type v<VAR>a : α<GOAL>⊥ a = none
<VAR>α : Type u<VAR>β : Type v<GOAL>⊥.symm = ⊥
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : α ≃. β<GOAL>f.trans ⊥ = ⊥
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : β ≃. γ<GOAL>⊥.trans f = ⊥
<VAR>α : Type u<VAR>β : Type v<VAR>f : α ≃. β<VAR>a : α<VAR>h : (f a).isSome = true<GOAL>(f.symm ((f a).get h)).isSome = true
<VAR>α : Type u<VAR>β : Type v<VAR>DecidableEq α<VAR>DecidableEq β<VAR>a : α<VAR>b : β<GOAL>b ∈ (PEquiv.single a b) a
<VAR>α : Type u<VAR>β : Type v<VAR>DecidableEq α<VAR>DecidableEq β<VAR>a₁ a₂ : α<VAR>b₁ b₂ : β<GOAL>b₁ ∈ (PEquiv.single a₂ b₂) a₁ ↔ a₁ = a₂ ∧ b₁ = b₂
<VAR>α : Type u<VAR>β : Type v<VAR>DecidableEq α<VAR>DecidableEq β<VAR>a : α<VAR>b : β<GOAL>(PEquiv.single a b).symm = PEquiv.single b a
<VAR>α : Type u<VAR>β : Type v<VAR>DecidableEq α<VAR>DecidableEq β<VAR>a : α<VAR>b : β<GOAL>(PEquiv.single a b) a = some b
<VAR>α : Type u<VAR>β : Type v<VAR>DecidableEq α<VAR>DecidableEq β<VAR>a₁ a₂ : α<VAR>h : a₁ ≠ a₂<VAR>b : β<GOAL>(PEquiv.single a₁ b) a₂ = none
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>DecidableEq α<VAR>DecidableEq β<VAR>DecidableEq γ<VAR>a : α<VAR>b : β<VAR>c : γ<VAR>f : β ≃. γ<VAR>h : c ∈ f b<GOAL>(PEquiv.single a b).trans f = PEquiv.single a c
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>DecidableEq α<VAR>DecidableEq β<VAR>DecidableEq γ<VAR>a : α<VAR>b : β<VAR>c : γ<VAR>f : α ≃. β<VAR>h : b ∈ f a<GOAL>f.trans (PEquiv.single b c) = PEquiv.single a c
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>DecidableEq α<VAR>DecidableEq β<VAR>DecidableEq γ<VAR>a : α<VAR>b : β<VAR>c : γ<GOAL>(PEquiv.single a b).trans (PEquiv.single b c) = PEquiv.single a c
<VAR>α : Type u<VAR>DecidableEq α<VAR>Subsingleton α<VAR>a b : α<GOAL>PEquiv.single a b = PEquiv.refl α
<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type x<VAR>DecidableEq β<VAR>DecidableEq γ<VAR>b : β<VAR>c : γ<VAR>f : δ ≃. β<VAR>h : f.symm b = none<GOAL>f.trans (PEquiv.single b c) = ⊥
<VAR>α : Type u<VAR>β : Type v<VAR>δ : Type x<VAR>DecidableEq α<VAR>DecidableEq β<VAR>a : α<VAR>b : β<VAR>f : β ≃. δ<VAR>h : f b = none<GOAL>(PEquiv.single a b).trans f = ⊥
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>DecidableEq α<VAR>DecidableEq β<VAR>DecidableEq γ<VAR>b₁ b₂ : β<VAR>h : b₁ ≠ b₂<VAR>a : α<VAR>c : γ<GOAL>(PEquiv.single a b₁).trans (PEquiv.single b₂ c) = ⊥
<VAR>α : Type u<VAR>β : Type v<VAR>f g : α ≃. β<GOAL>f ≤ g ↔ ∀ (a : α), ∀ b ∈ f a, b ∈ g a
<VAR>α : Type u_1<GOAL>(Equiv.refl α).toPEquiv = PEquiv.refl α
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α ≃ β<VAR>g : β ≃ γ<GOAL>(f.trans g).toPEquiv = f.toPEquiv.trans g.toPEquiv
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α ≃ β<GOAL>f.symm.toPEquiv = f.toPEquiv.symm
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α ≃ β<VAR>x : α<GOAL>f.toPEquiv x = some (f x)
<VAR>α : Type u_2<VAR>Monoid α<VAR>n : ℕ<VAR>a : α<VAR>s : Fin n → Set α<GOAL>a ∈ (List.ofFn s).prod ↔ ∃ f, (List.ofFn fun i => ↑(f i)).prod = a
<VAR>α : Type u_2<VAR>AddMonoid α<VAR>n : ℕ<VAR>a : α<VAR>s : Fin n → Set α<GOAL>a ∈ (List.ofFn s).sum ↔ ∃ f, (List.ofFn fun i => ↑(f i)).sum = a
<VAR>α : Type u_2<VAR>Monoid α<VAR>l : List (Set α)<VAR>a : α<GOAL>a ∈ l.prod ↔ ∃ l', (List.map (fun x => ↑x.snd) l').prod = a ∧ List.map Sigma.fst l' = l
<VAR>α : Type u_2<VAR>AddMonoid α<VAR>l : List (Set α)<VAR>a : α<GOAL>a ∈ l.sum ↔ ∃ l', (List.map (fun x => ↑x.snd) l').sum = a ∧ List.map Sigma.fst l' = l
<VAR>α : Type u_2<VAR>Monoid α<VAR>s : Set α<VAR>a : α<VAR>n : ℕ<GOAL>a ∈ s ^ n ↔ ∃ f, (List.ofFn fun i => ↑(f i)).prod = a
<VAR>α : Type u_2<VAR>AddMonoid α<VAR>s : Set α<VAR>a : α<VAR>n : ℕ<GOAL>a ∈ n • s ↔ ∃ f, (List.ofFn fun i => ↑(f i)).sum = a
<VAR>α : Type u<VAR>β : α → Type v<GOAL>[].keys = []
<VAR>α : Type u<VAR>β : α → Type v<VAR>s : Sigma β<VAR>l : List (Sigma β)<GOAL>(s :: l).keys = s.fst :: l.keys
<VAR>α : Type u<VAR>β : α → Type v<VAR>s : Sigma β<VAR>l : List (Sigma β)<GOAL>s ∈ l → s.fst ∈ l.keys
<VAR>α : Type u<VAR>β : α → Type v<VAR>a : α<VAR>l : List (Sigma β)<VAR>h : a ∈ l.keys<GOAL>∃ b, ⟨a, b⟩ ∈ l
<VAR>α : Type u<VAR>β : α → Type v<VAR>a : α<VAR>l : List (Sigma β)<GOAL>a ∈ l.keys ↔ ∃ b, ⟨a, b⟩ ∈ l
<VAR>α : Type u<VAR>β : α → Type v<VAR>a : α<VAR>l : List (Sigma β)<GOAL>a ∉ l.keys ↔ ∀ (b : β a), ⟨a, b⟩ ∉ l
<VAR>α : Type u<VAR>β : α → Type v<VAR>a : α<VAR>l : List (Sigma β)<GOAL>a ∉ l.keys ↔ ∀ s ∈ l, a ≠ s.fst
<VAR>α : Type u<VAR>β : α → Type v<VAR>l : List (Sigma β)<GOAL>l.NodupKeys ↔ List.Pairwise (fun s s' => s.fst ≠ s'.fst) l
<VAR>α : Type u<VAR>β : α → Type v<VAR>l : List (Sigma β)<VAR>h : l.NodupKeys<GOAL>List.Pairwise (fun s s' => s.fst ≠ s'.fst) l
<VAR>α : Type u<VAR>β : α → Type v<GOAL>[].NodupKeys
<VAR>α : Type u<VAR>β : α → Type v<VAR>s : Sigma β<VAR>l : List (Sigma β)<GOAL>(s :: l).NodupKeys ↔ s.fst ∉ l.keys ∧ l.NodupKeys
<VAR>α : Type u<VAR>β : α → Type v<VAR>s : Sigma β<VAR>l : List (Sigma β)<VAR>h : (s :: l).NodupKeys<GOAL>s.fst ∉ l.keys
<VAR>α : Type u<VAR>β : α → Type v<VAR>s : Sigma β<VAR>l : List (Sigma β)<VAR>h : (s :: l).NodupKeys<GOAL>l.NodupKeys
<VAR>α : Type u<VAR>β : α → Type v<VAR>l : List (Sigma β)<VAR>nd : l.NodupKeys<VAR>s s' : Sigma β<VAR>h : s ∈ l<VAR>h' : s' ∈ l<GOAL>s.fst = s'.fst → s = s'
<VAR>α : Type u<VAR>β : α → Type v<VAR>a : α<VAR>b b' : β a<VAR>l : List (Sigma β)<VAR>nd : l.NodupKeys<VAR>h : ⟨a, b⟩ ∈ l<VAR>h' : ⟨a, b'⟩ ∈ l<GOAL>b = b'
<VAR>α : Type u<VAR>β : α → Type v<VAR>s : Sigma β<GOAL>[s].NodupKeys
<VAR>α : Type u<VAR>β : α → Type v<VAR>l₁ l₂ : List (Sigma β)<VAR>h : l₁.Sublist l₂<GOAL>l₂.NodupKeys → l₁.NodupKeys
<VAR>α : Type u<VAR>β : α → Type v<VAR>l : List (Sigma β)<GOAL>l.NodupKeys → l.Nodup
<VAR>α : Type u<VAR>β : α → Type v<VAR>l₁ l₂ : List (Sigma β)<VAR>h : l₁.Perm l₂<GOAL>l₁.NodupKeys ↔ l₂.NodupKeys
<VAR>α : Type u<VAR>β : α → Type v<VAR>L : List (List (Sigma β))<GOAL>L.join.NodupKeys ↔ (∀ l ∈ L, l.NodupKeys) ∧ List.Pairwise List.Disjoint (List.map List.keys L)
<VAR>α : Type u<VAR>l : List α<GOAL>(List.map Prod.fst l.enum).Nodup
<VAR>α : Type u<VAR>β : α → Type v<VAR>l₀ l₁ : List (Sigma β)<VAR>nd₀ : l₀.Nodup<VAR>nd₁ : l₁.Nodup<VAR>h : ∀ (x : Sigma β), x ∈ l₀ ↔ x ∈ l₁<GOAL>l₀.Perm l₁
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<GOAL>List.dlookup a [] = none
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>l : List (Sigma β)<VAR>a : α<VAR>b : β a<GOAL>List.dlookup a (⟨a, b⟩ :: l) = some b
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>l : List (Sigma β)<VAR>a : α<VAR>s : Sigma β<GOAL>a ≠ s.fst → List.dlookup a (s :: l) = List.dlookup a l
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>l : List (Sigma β)<GOAL>(List.dlookup a l).isSome = true ↔ a ∈ l.keys
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>l : List (Sigma β)<GOAL>List.dlookup a l = none ↔ a ∉ l.keys
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>b : β a<VAR>l : List (Sigma β)<GOAL>b ∈ List.dlookup a l → ⟨a, b⟩ ∈ l
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>b : β a<VAR>l : List (Sigma β)<VAR>nd : l.NodupKeys<VAR>h : ⟨a, b⟩ ∈ l<GOAL>b ∈ List.dlookup a l
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>l : List (Sigma β)<GOAL>Option.map (Sigma.mk a) (List.dlookup a l) = List.find? (fun s => decide (a = s.fst)) l
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>b : β a<VAR>l : List (Sigma β)<VAR>nd : l.NodupKeys<GOAL>b ∈ List.dlookup a l ↔ ⟨a, b⟩ ∈ l
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>l₁ l₂ : List (Sigma β)<VAR>nd₁ : l₁.NodupKeys<VAR>nd₂ : l₂.NodupKeys<VAR>p : l₁.Perm l₂<GOAL>List.dlookup a l₁ = List.dlookup a l₂
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>l₀ l₁ : List (Sigma β)<VAR>nd₀ : l₀.NodupKeys<VAR>nd₁ : l₁.NodupKeys<VAR>h : ∀ (x : α) (y : β x), y ∈ List.dlookup x l₀ ↔ y ∈ List.dlookup x l₁<GOAL>l₀.Perm l₁
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<GOAL>List.lookupAll a [] = []
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>l : List (Sigma β)<VAR>a : α<VAR>b : β a<GOAL>List.lookupAll a (⟨a, b⟩ :: l) = b :: List.lookupAll a l
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>l : List (Sigma β)<VAR>a : α<VAR>s : Sigma β<GOAL>a ≠ s.fst → List.lookupAll a (s :: l) = List.lookupAll a l
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>l : List (Sigma β)<GOAL>List.lookupAll a l = [] ↔ ∀ (b : β a), ⟨a, b⟩ ∉ l
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>l : List (Sigma β)<GOAL>(List.lookupAll a l).head? = List.dlookup a l
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>b : β a<VAR>l : List (Sigma β)<GOAL>b ∈ List.lookupAll a l ↔ ⟨a, b⟩ ∈ l
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>l : List (Sigma β)<GOAL>(List.map (Sigma.mk a) (List.lookupAll a l)).Sublist l
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>l : List (Sigma β)<VAR>h : l.NodupKeys<GOAL>(List.lookupAll a l).length ≤ 1
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>l : List (Sigma β)<VAR>h : l.NodupKeys<GOAL>List.lookupAll a l = (List.dlookup a l).toList
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>l : List (Sigma β)<VAR>h : l.NodupKeys<GOAL>(List.lookupAll a l).Nodup
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>l₁ l₂ : List (Sigma β)<VAR>nd₁ : l₁.NodupKeys<VAR>nd₂ : l₂.NodupKeys<VAR>p : l₁.Perm l₂<GOAL>List.lookupAll a l₁ = List.lookupAll a l₂
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>b : β a<VAR>l : List (Sigma β)<VAR>H : ∀ (b : β a), ⟨a, b⟩ ∉ l<GOAL>List.kreplace a b l = l
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>b : β a<VAR>l : List (Sigma β)<VAR>nd : l.NodupKeys<VAR>h : ⟨a, b⟩ ∈ l<GOAL>List.kreplace a b l = l
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>b : β a<VAR>l : List (Sigma β)<GOAL>(List.kreplace a b l).keys = l.keys
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>b : β a<VAR>l : List (Sigma β)<GOAL>(List.kreplace a b l).NodupKeys ↔ l.NodupKeys
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>b : β a<VAR>l₁ l₂ : List (Sigma β)<VAR>nd : l₁.NodupKeys<GOAL>l₁.Perm l₂ → (List.kreplace a b l₁).Perm (List.kreplace a b l₂)
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<GOAL>List.kerase a [] = []
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>s : Sigma β<VAR>l : List (Sigma β)<VAR>h : a = s.fst<GOAL>List.kerase a (s :: l) = l
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>s : Sigma β<VAR>l : List (Sigma β)<VAR>h : a ≠ s.fst<GOAL>List.kerase a (s :: l) = s :: List.kerase a l
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>l : List (Sigma β)<VAR>h : a ∉ l.keys<GOAL>List.kerase a l = l
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>l : List (Sigma β)<GOAL>(List.kerase a l).Sublist l
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>l : List (Sigma β)<GOAL>(List.kerase a l).keys ⊆ l.keys
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a₁ a₂ : α<VAR>l : List (Sigma β)<GOAL>a₁ ∈ (List.kerase a₂ l).keys → a₁ ∈ l.keys
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>l : List (Sigma β)<VAR>h : a ∈ l.keys<GOAL>∃ b l₁ l₂, a ∉ l₁.keys ∧ l = l₁ ++ ⟨a, b⟩ :: l₂ ∧ List.kerase a l = l₁ ++ l₂
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a₁ a₂ : α<VAR>l : List (Sigma β)<VAR>h : a₁ ≠ a₂<GOAL>a₁ ∈ (List.kerase a₂ l).keys ↔ a₁ ∈ l.keys
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>l : List (Sigma β)<GOAL>(List.kerase a l).keys = l.keys.erase a
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a a' : α<VAR>l : List (Sigma β)<GOAL>List.kerase a (List.kerase a' l) = List.kerase a' (List.kerase a l)
<VAR>α : Type u<VAR>β : α → Type v<VAR>l : List (Sigma β)<VAR>DecidableEq α<VAR>a : α<GOAL>l.NodupKeys → (List.kerase a l).NodupKeys
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>l₁ l₂ : List (Sigma β)<VAR>nd : l₁.NodupKeys<GOAL>l₁.Perm l₂ → (List.kerase a l₁).Perm (List.kerase a l₂)
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>l : List (Sigma β)<VAR>nd : l.NodupKeys<GOAL>a ∉ (List.kerase a l).keys
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>l : List (Sigma β)<VAR>nd : l.NodupKeys<GOAL>List.dlookup a (List.kerase a l) = none
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a a' : α<VAR>l : List (Sigma β)<VAR>h : a ≠ a'<GOAL>List.dlookup a (List.kerase a' l) = List.dlookup a l
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>l₁ l₂ : List (Sigma β)<GOAL>a ∈ l₁.keys → List.kerase a (l₁ ++ l₂) = List.kerase a l₁ ++ l₂
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>l₁ l₂ : List (Sigma β)<GOAL>a ∉ l₁.keys → List.kerase a (l₁ ++ l₂) = l₁ ++ List.kerase a l₂
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a₁ a₂ : α<VAR>l : List (Sigma β)<GOAL>List.kerase a₂ (List.kerase a₁ l) = List.kerase a₁ (List.kerase a₂ l)
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>SizeOf (Sigma β)<VAR>x : α<VAR>xs : List (Sigma β)<GOAL>sizeOf (List.kerase x xs) ≤ sizeOf xs