ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<GOAL>∀ {α : Type u_1} {α_1 : Type u_2} {f : α → Option α_1} {a : α} (l : List α), (f a).isNone = true → List.findSome? f (a :: l) = List.findSome? f l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>b : β<VAR>l : List α<VAR>f : α → Option β<VAR>w : List.findSome? f l = some b<GOAL>∃ a, a ∈ l ∧ f a = some b
<VAR>β : Type u_1<VAR>γ : Type u_2<GOAL>∀ {α : Type u_3} {p : γ → Option α} (f : β → γ) (l : List β), List.findSome? p (List.map f l) = List.findSome? (p ∘ f) l
<GOAL>∀ {α : Type u_1} {α_1 : Type u_2} {f : α → Option α_1} {n : Nat} {a : α}, List.findSome? f (List.replicate n a) = if n = 0 then none else f a
<VAR>n : Nat<GOAL>∀ {α : Type u_1} {α_1 : Type u_2} {f : α → Option α_1} {a : α}, 0 < n → List.findSome? f (List.replicate n a) = f a
<GOAL>∀ {α : Type u_1} {α_1 : Type u_2} {f : α → Option α_1} {n : Nat} {a : α}, (f a).isSome = true → List.findSome? f (List.replicate n a) = if n = 0 then none else f a
<GOAL>∀ {α : Type u_1} {α_1 : Type u_2} {f : α → Option α_1} {n : Nat} {a : α}, (f a).isNone = true → List.findSome? f (List.replicate n a) = none
<VAR>α : Type u_2<VAR>BEq α<VAR>LawfulBEq α<GOAL>∀ {β : Type u_1} {b : β} {es : List (α × β)} {k : α}, List.lookup k ((k, b) :: es) = some b
<VAR>α : Type u_2<VAR>BEq α<VAR>LawfulBEq α<VAR>n : Nat<VAR>a : α<GOAL>∀ {α_1 : Type u_1} {b : α_1} {k : α}, List.lookup k (List.replicate n (a, b)) = if n = 0 then none else if (k == a) = true then some b else none
<VAR>α : Type u_2<VAR>BEq α<VAR>LawfulBEq α<VAR>n : Nat<VAR>a : α<GOAL>∀ {α_1 : Type u_1} {b : α_1} {k : α}, 0 < n → List.lookup k (List.replicate n (a, b)) = if (k == a) = true then some b else none
<VAR>α : Type u_2<VAR>BEq α<VAR>LawfulBEq α<VAR>n : Nat<GOAL>∀ {α_1 : Type u_1} {b : α_1} {a : α}, List.lookup a (List.replicate n (a, b)) = if n = 0 then none else some b
<VAR>α : Type u_2<VAR>BEq α<VAR>LawfulBEq α<VAR>n : Nat<GOAL>∀ {α_1 : Type u_1} {b : α_1} {a : α}, 0 < n → List.lookup a (List.replicate n (a, b)) = some b
<VAR>α : Type u_2<VAR>BEq α<VAR>LawfulBEq α<VAR>a : α<VAR>n : Nat<GOAL>∀ {α_1 : Type u_1} {b : α_1} {k : α}, (!k == a) = true → List.lookup k (List.replicate n (a, b)) = none
<VAR>α : Type u_1<VAR>l : List α<VAR>p : α → Bool<GOAL>(!l.any p) = l.all fun a => !p a
<VAR>α : Type u_1<VAR>l : List α<VAR>p : α → Bool<GOAL>(!l.all p) = l.any fun a => !p a
<VAR>α : Type u_1<VAR>l : List α<VAR>p : α → Bool<VAR>q : Bool<GOAL>(q && l.any p) = l.any fun a => q && p a
<VAR>α : Type u_1<VAR>l : List α<VAR>p : α → Bool<VAR>q : Bool<GOAL>(l.any p && q) = l.any fun a => p a && q
<VAR>α : Type u_1<VAR>l : List α<VAR>p : α → Bool<VAR>q : Bool<GOAL>(q || l.all p) = l.all fun a => q || p a
<VAR>α : Type u_1<VAR>l : List α<VAR>p : α → Bool<VAR>q : Bool<GOAL>(l.all p || q) = l.all fun a => p a || q
<VAR>α : Type u_1<VAR>l : List α<VAR>p : α → Bool<GOAL>l.any p = !l.all fun x => !p x
<VAR>α : Type u_1<VAR>l : List α<VAR>p : α → Bool<GOAL>l.all p = !l.any fun x => !p x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>l : List α<VAR>p : β → Bool<GOAL>(List.map f l).any p = l.any (p ∘ f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>l : List α<VAR>p : β → Bool<GOAL>(List.map f l).all p = l.all (p ∘ f)
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>f : α → γ<VAR>g : β → δ<VAR>l₁ : List α<VAR>l₂ : List β<GOAL>(List.map f l₁).zip (List.map g l₂) = List.map (Prod.map f g) (l₁.zip l₂)
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>β : Type u_3<VAR>f : α → γ<VAR>l₁ : List α<VAR>l₂ : List β<GOAL>(List.map f l₁).zip l₂ = List.map (Prod.map f id) (l₁.zip l₂)
<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>α : Type u_3<VAR>f : β → γ<VAR>l₁ : List α<VAR>l₂ : List β<GOAL>l₁.zip (List.map f l₂) = List.map (Prod.map id f) (l₁.zip l₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l₁ r₁ : List α<VAR>l₂ r₂ : List β<VAR>_h : l₁.length = l₂.length<GOAL>(l₁ ++ r₁).zip (l₂ ++ r₂) = l₁.zip l₂ ++ r₁.zip r₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β<VAR>g : α → γ<VAR>l : List α<GOAL>(List.map f l).zip (List.map g l) = List.map (fun a => (f a, g a)) l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a : α<VAR>b : β<VAR>l₁ : List α<VAR>l₂ : List β<GOAL>(a, b) ∈ l₁.zip l₂ → a ∈ l₁ ∧ b ∈ l₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l₁ : List α<VAR>l₂ : List β<GOAL>l₁.length ≤ l₂.length → List.map Prod.fst (l₁.zip l₂) = l₁
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l₁ : List α<VAR>l₂ : List β<GOAL>l₂.length ≤ l₁.length → List.map Prod.snd (l₁.zip l₂) = l₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a : α<VAR>b : β<VAR>n : Nat<GOAL>(List.replicate n a).zip (List.replicate n b) = List.replicate n (a, b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>as : List α<VAR>bs : List β<VAR>f : α → β → γ<VAR>i : Nat<GOAL>(List.zipWith f as bs)[i]? = match as[i]?, bs[i]? with | some a, some b => some (f a b) | x, x_1 => none
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>as : List α<VAR>bs : List β<VAR>i : Nat<VAR>f : α → β → γ<GOAL>(List.zipWith f as bs).get? i = match as.get? i, bs.get? i with | some a, some b => some (f a b) | x, x_1 => none
<VAR>γ : Type u_1<VAR>δ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>μ : Type u_5<VAR>f : γ → δ → μ<VAR>g : α → γ<VAR>h : β → δ<VAR>l₁ : List α<VAR>l₂ : List β<GOAL>List.zipWith f (List.map g l₁) (List.map h l₂) = List.zipWith (fun a b => f (g a) (h b)) l₁ l₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>α' : Type u_3<VAR>γ : Type u_4<VAR>l₁ : List α<VAR>l₂ : List β<VAR>f : α → α'<VAR>g : α' → β → γ<GOAL>List.zipWith g (List.map f l₁) l₂ = List.zipWith (fun a b => g (f a) b) l₁ l₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>β' : Type u_3<VAR>γ : Type u_4<VAR>l₁ : List α<VAR>l₂ : List β<VAR>f : β → β'<VAR>g : α → β' → γ<GOAL>List.zipWith g l₁ (List.map f l₂) = List.zipWith (fun a b => g a (f b)) l₁ l₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>l₁ : List α<VAR>l₂ : List β<VAR>g : γ → δ → δ<VAR>f : α → β → γ<VAR>i : δ<GOAL>List.foldr g i (List.zipWith f l₁ l₂) = List.foldr (fun p r => g (f p.fst p.snd) r) i (l₁.zip l₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>l₁ : List α<VAR>l₂ : List β<VAR>g : δ → γ → δ<VAR>f : α → β → γ<VAR>i : δ<GOAL>List.foldl g i (List.zipWith f l₁ l₂) = List.foldl (fun r p => g r (f p.fst p.snd)) i (l₁.zip l₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β → γ<VAR>l : List α<VAR>l' : List β<GOAL>List.zipWith f l l' = [] ↔ l = [] ∨ l' = []
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>f : α → β<VAR>g : γ → δ → α<VAR>l : List γ<VAR>l' : List δ<GOAL>List.map f (List.zipWith g l l') = List.zipWith (fun x y => f (g x y)) l l'
<GOAL>∀ {α : Type u_1} {α_1 : Type u_2} {α_2 : Type u_3} {f : α → α_1 → α_2} {l : List α} {l' : List α_1} {n : Nat}, List.take n (List.zipWith f l l') = List.zipWith f (List.take n l) (List.take n l')
<GOAL>∀ {α : Type u_1} {α_1 : Type u_2} {α_2 : Type u_3} {f : α → α_1 → α_2} {l : List α} {l' : List α_1} {n : Nat}, List.drop n (List.zipWith f l l') = List.zipWith f (List.drop n l) (List.drop n l')
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β → γ<VAR>l la : List α<VAR>l' lb : List β<VAR>h : l.length = l'.length<GOAL>List.zipWith f (l ++ la) (l' ++ lb) = List.zipWith f l l' ++ List.zipWith f la lb
<VAR>α : Type u_1<VAR>β : Type u_2<GOAL>∀ {α_1 : Type u_3} {f : α → β → α_1} {a : α} {b : β} {n : Nat}, List.zipWith f (List.replicate n a) (List.replicate n b) = List.replicate n (f a b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>as : List α<VAR>bs : List β<VAR>f : Option α → Option β → γ<VAR>i : Nat<GOAL>(List.zipWithAll f as bs)[i]? = match as[i]?, bs[i]? with | none, none => none | a?, b? => some (f a? b?)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>as : List α<VAR>bs : List β<VAR>i : Nat<VAR>f : Option α → Option β → γ<GOAL>(List.zipWithAll f as bs).get? i = match as.get? i, bs.get? i with | none, none => none | a?, b? => some (f a? b?)
<VAR>γ : Type u_1<VAR>δ : Type u_2<VAR>α : Type u_1<VAR>β : Type u_2<VAR>μ : Type u_3<VAR>f : Option γ → Option δ → μ<VAR>g : α → γ<VAR>h : β → δ<VAR>l₁ : List α<VAR>l₂ : List β<GOAL>List.zipWithAll f (List.map g l₁) (List.map h l₂) = List.zipWithAll (fun a b => f (g <$> a) (h <$> b)) l₁ l₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>α' : Type u_1<VAR>γ : Type u_3<VAR>l₁ : List α<VAR>l₂ : List β<VAR>f : α → α'<VAR>g : Option α' → Option β → γ<GOAL>List.zipWithAll g (List.map f l₁) l₂ = List.zipWithAll (fun a b => g (f <$> a) b) l₁ l₂
<VAR>α : Type u_1<VAR>β β' : Type u_2<VAR>γ : Type u_3<VAR>l₁ : List α<VAR>l₂ : List β<VAR>f : β → β'<VAR>g : Option α → Option β' → γ<GOAL>List.zipWithAll g l₁ (List.map f l₂) = List.zipWithAll (fun a b => g a (f <$> b)) l₁ l₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>f : α → β<VAR>g : Option γ → Option δ → α<VAR>l : List γ<VAR>l' : List δ<GOAL>List.map f (List.zipWithAll g l l') = List.zipWithAll (fun x y => f (g x y)) l l'
<VAR>α : Type u_1<VAR>β : Type u_2<GOAL>∀ {α_1 : Type u_3} {f : Option α → Option β → α_1} {a : α} {b : β} {n : Nat}, List.zipWithAll f (List.replicate n a) (List.replicate n b) = List.replicate n (f (some a) (some b))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n : Nat<VAR>a : α<VAR>b : β<GOAL>(List.replicate n (a, b)).unzip = (List.replicate n a, List.replicate n b)
<VAR>α : Type u_1<VAR>n : Nat<VAR>l : List α<GOAL>(List.enumFrom n l).length = l.length
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>n : Nat<VAR>l : List α<GOAL>List.map (Prod.map id f) (List.enumFrom n l) = List.enumFrom n (List.map f l)
<GOAL>∀ {α : Type u_1} {l : List α}, l.enum.length = l.length
<GOAL>∀ {α : Type u_1} {a : α} {as : List α}, (a :: as).enum = (0, a) :: List.enumFrom 1 as
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>l : List α<GOAL>List.map (Prod.map id f) l.enum = (List.map f l).enum
<VAR>α : Type u_1<VAR>Min α<GOAL>[].minimum? = none
<VAR>α : Type u_1<VAR>x : α<VAR>Min α<VAR>xs : List α<GOAL>(x :: xs).minimum? = some (List.foldl min x xs)
<VAR>α : Type u_1<VAR>xs : List α<VAR>Min α<GOAL>xs.minimum? = none ↔ xs = []
<VAR>α : Type u_1<VAR>a : α<VAR>Min α<VAR>min_eq_or : ∀ (a b : α), min a b = a ∨ min a b = b<VAR>xs : List α<GOAL>xs.minimum? = some a → a ∈ xs
<VAR>α : Type u_1<VAR>a : α<VAR>Min α<VAR>LE α<VAR>le_min_iff : ∀ (a b c : α), a ≤ min b c ↔ a ≤ b ∧ a ≤ c<VAR>xs : List α<GOAL>xs.minimum? = some a → ∀ (x : α), x ≤ a ↔ ∀ (b : α), b ∈ xs → x ≤ b
<VAR>α : Type u_1<VAR>a : α<VAR>Min α<VAR>LE α<VAR>anti : Antisymm fun x x_1 => x ≤ x_1<VAR>le_refl : ∀ (a : α), a ≤ a<VAR>min_eq_or : ∀ (a b : α), min a b = a ∨ min a b = b<VAR>le_min_iff : ∀ (a b c : α), a ≤ min b c ↔ a ≤ b ∧ a ≤ c<VAR>xs : List α<GOAL>xs.minimum? = some a ↔ a ∈ xs ∧ ∀ (b : α), b ∈ xs → a ≤ b
<VAR>α : Type u_1<VAR>Min α<VAR>n : Nat<VAR>a : α<VAR>w : min a a = a<GOAL>(List.replicate n a).minimum? = if n = 0 then none else some a
<VAR>α : Type u_1<VAR>Min α<VAR>n : Nat<VAR>a : α<VAR>w : min a a = a<VAR>h : 0 < n<GOAL>(List.replicate n a).minimum? = some a
<VAR>α : Type u_1<VAR>Max α<GOAL>[].maximum? = none
<VAR>α : Type u_1<VAR>x : α<VAR>Max α<VAR>xs : List α<GOAL>(x :: xs).maximum? = some (List.foldl max x xs)
<VAR>α : Type u_1<VAR>xs : List α<VAR>Max α<GOAL>xs.maximum? = none ↔ xs = []
<VAR>α : Type u_1<VAR>a : α<VAR>Max α<VAR>min_eq_or : ∀ (a b : α), max a b = a ∨ max a b = b<VAR>xs : List α<GOAL>xs.maximum? = some a → a ∈ xs
<VAR>α : Type u_1<VAR>a : α<VAR>Max α<VAR>LE α<VAR>max_le_iff : ∀ (a b c : α), max b c ≤ a ↔ b ≤ a ∧ c ≤ a<VAR>xs : List α<GOAL>xs.maximum? = some a → ∀ (x : α), a ≤ x ↔ ∀ (b : α), b ∈ xs → b ≤ x
<VAR>α : Type u_1<VAR>a : α<VAR>Max α<VAR>LE α<VAR>anti : Antisymm fun x x_1 => x ≤ x_1<VAR>le_refl : ∀ (a : α), a ≤ a<VAR>max_eq_or : ∀ (a b : α), max a b = a ∨ max a b = b<VAR>max_le_iff : ∀ (a b c : α), max b c ≤ a ↔ b ≤ a ∧ c ≤ a<VAR>xs : List α<GOAL>xs.maximum? = some a ↔ a ∈ xs ∧ ∀ (b : α), b ∈ xs → b ≤ a
<VAR>α : Type u_1<VAR>Max α<VAR>n : Nat<VAR>a : α<VAR>w : max a a = a<GOAL>(List.replicate n a).maximum? = if n = 0 then none else some a
<VAR>α : Type u_1<VAR>Max α<VAR>n : Nat<VAR>a : α<VAR>w : max a a = a<VAR>h : 0 < n<GOAL>(List.replicate n a).maximum? = some a
<VAR>m : Type u_1 → Type u_2<VAR>α : Type u_3<VAR>β : Type u_1<VAR>Monad m<VAR>f : α → m β<GOAL>List.mapM' f [] = pure []
<VAR>m : Type u_1 → Type u_2<VAR>α : Type u_3<VAR>β : Type u_1<VAR>a : α<VAR>l : List α<VAR>Monad m<VAR>f : α → m β<GOAL>List.mapM' f (a :: l) = do let __do_lift ← f a let __do_lift_1 ← List.mapM' f l pure (__do_lift :: __do_lift_1)
<VAR>m : Type u_1 → Type u_2<VAR>α : Type u_3<VAR>β : Type u_1<VAR>Monad m<VAR>LawfulMonad m<VAR>f : α → m β<VAR>l : List α<GOAL>List.mapM' f l = List.mapM f l
<VAR>m : Type u_1 → Type u_2<VAR>α : Type u_3<VAR>β : Type u_1<VAR>Monad m<VAR>LawfulMonad m<VAR>f : α → m β<VAR>l : List α<VAR>acc : List β<GOAL>List.mapM.loop f l acc = do let __do_lift ← List.mapM' f l pure (acc.reverse ++ __do_lift)
<VAR>m : Type u_1 → Type u_2<VAR>α : Type u_3<VAR>β : Type u_1<VAR>Monad m<VAR>f : α → m β<GOAL>List.mapM f [] = pure []
<VAR>m : Type u_1 → Type u_2<VAR>α : Type u_3<VAR>β : Type u_1<VAR>a : α<VAR>l : List α<VAR>Monad m<VAR>LawfulMonad m<VAR>f : α → m β<GOAL>List.mapM f (a :: l) = do let __do_lift ← f a let __do_lift_1 ← List.mapM f l pure (__do_lift :: __do_lift_1)
<VAR>m : Type u_1 → Type u_2<VAR>α : Type u_3<VAR>β : Type u_1<VAR>Monad m<VAR>LawfulMonad m<VAR>f : α → m β<VAR>l₁ l₂ : List α<GOAL>List.mapM f (l₁ ++ l₂) = do let __do_lift ← List.mapM f l₁ let __do_lift_1 ← List.mapM f l₂ pure (__do_lift ++ __do_lift_1)
<VAR>m : Type u_1 → Type u_2<VAR>α : Type u_3<VAR>f : α → m PUnit<VAR>Monad m<GOAL>[].forM f = pure PUnit.unit
<VAR>m : Type u_1 → Type u_2<GOAL>∀ {α : Type u_3} {a : α} {as : List α} {f : α → m PUnit} [inst : Monad m], (a :: as).forM f = do f a as.forM f
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>H : ∀ {x : α}, p x<VAR>t : Batteries.RBNode α<GOAL>Batteries.RBNode.All p t
<VAR>α : Type u_1<VAR>p q : α → Prop<VAR>t : Batteries.RBNode α<GOAL>Batteries.RBNode.All (fun a => p a ∧ q a) t ↔ Batteries.RBNode.All p t ∧ Batteries.RBNode.All q t
<GOAL>∀ {α : Sort u_1} {cmp : α → α → Ordering} {x y : α}, Batteries.RBNode.cmpLT cmp x y → Batteries.RBNode.cmpLT (flip cmp) y x
<GOAL>∀ {α : Sort u_1} {cmp : α → α → Ordering} {x y z : α}, Batteries.RBNode.cmpLT cmp x y → Batteries.RBNode.cmpLT cmp y z → Batteries.RBNode.cmpLT cmp x z
<VAR>α : Type u_1<VAR>cmp : α → α → Ordering<VAR>x y : α<VAR>H : Batteries.RBNode.cmpLT cmp x y<VAR>t : Batteries.RBNode α<VAR>h : Batteries.RBNode.All (fun x => Batteries.RBNode.cmpLT cmp y x) t<GOAL>Batteries.RBNode.All (fun x_1 => Batteries.RBNode.cmpLT cmp x x_1) t
<VAR>α : Type u_1<VAR>cmp : α → α → Ordering<VAR>x y : α<VAR>H : Batteries.RBNode.cmpLT cmp x y<VAR>a : Batteries.RBNode α<VAR>h : Batteries.RBNode.All (fun x_1 => Batteries.RBNode.cmpLT cmp x_1 x) a<GOAL>Batteries.RBNode.All (fun x => Batteries.RBNode.cmpLT cmp x y) a
<GOAL>∀ {α : Sort u_1} {cmp : α → α → Ordering} {x y z : α}, Batteries.RBNode.cmpEq cmp x y → (Batteries.RBNode.cmpLT cmp x z ↔ Batteries.RBNode.cmpLT cmp y z)
<GOAL>∀ {α : Sort u_1} {cmp : α → α → Ordering} {y z x : α}, Batteries.RBNode.cmpEq cmp y z → (Batteries.RBNode.cmpLT cmp x y ↔ Batteries.RBNode.cmpLT cmp x z)
<VAR>α : Type u_1<VAR>t : Batteries.RBNode α<GOAL>t.reverse.reverse = t
<VAR>α : Type u_1<VAR>t t' : Batteries.RBNode α<GOAL>t.reverse = t' ↔ t = t'.reverse
<VAR>α : Type u_1<VAR>l : Batteries.RBNode α<VAR>v : α<VAR>r : Batteries.RBNode α<GOAL>(l.balance1 v r).reverse = r.reverse.balance2 v l.reverse
<VAR>α : Type u_1<VAR>l : Batteries.RBNode α<VAR>v : α<VAR>r : Batteries.RBNode α<GOAL>(l.balance2 v r).reverse = r.reverse.balance1 v l.reverse
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>t : Batteries.RBNode α<GOAL>Batteries.RBNode.All p t.reverse ↔ Batteries.RBNode.All p t
<VAR>α : Type u_1<VAR>cmp : α → α → Ordering<VAR>t : Batteries.RBNode α<GOAL>Batteries.RBNode.Ordered cmp t → Batteries.RBNode.Ordered (flip cmp) t.reverse
<VAR>α : Type u_1<VAR>c : Batteries.RBColor<VAR>n : Nat<VAR>t : Batteries.RBNode α<GOAL>t.Balanced c n → t.reverse.Balanced c n
<VAR>α : Type u_1<VAR>cmp : α → α → Ordering<VAR>l : Batteries.RBNode α<VAR>v : α<VAR>r : Batteries.RBNode α<VAR>lv : Batteries.RBNode.All (fun x => Batteries.RBNode.cmpLT cmp x v) l<VAR>vr : Batteries.RBNode.All (fun x => Batteries.RBNode.cmpLT cmp v x) r<VAR>hl : Batteries.RBNode.Ordered cmp l<VAR>hr : Batteries.RBNode.Ordered cmp r<GOAL>Batteries.RBNode.Ordered cmp (l.balance1 v r)
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>l : Batteries.RBNode α<VAR>v : α<VAR>r : Batteries.RBNode α<GOAL>Batteries.RBNode.All p (l.balance1 v r) ↔ p v ∧ Batteries.RBNode.All p l ∧ Batteries.RBNode.All p r
<VAR>α : Type u_1<VAR>cmp : α → α → Ordering<VAR>l : Batteries.RBNode α<VAR>v : α<VAR>r : Batteries.RBNode α<VAR>lv : Batteries.RBNode.All (fun x => Batteries.RBNode.cmpLT cmp x v) l<VAR>vr : Batteries.RBNode.All (fun x => Batteries.RBNode.cmpLT cmp v x) r<VAR>hl : Batteries.RBNode.Ordered cmp l<VAR>hr : Batteries.RBNode.Ordered cmp r<GOAL>Batteries.RBNode.Ordered cmp (l.balance2 v r)
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>l : Batteries.RBNode α<VAR>v : α<VAR>r : Batteries.RBNode α<GOAL>Batteries.RBNode.All p (l.balance2 v r) ↔ p v ∧ Batteries.RBNode.All p l ∧ Batteries.RBNode.All p r
<VAR>α : Type u_1<VAR>t : Batteries.RBNode α<GOAL>t.setBlack.reverse = t.reverse.setBlack
<VAR>α : Type u_1<VAR>cmp : α → α → Ordering<VAR>t : Batteries.RBNode α<GOAL>Batteries.RBNode.Ordered cmp t.setBlack ↔ Batteries.RBNode.Ordered cmp t
<GOAL>∀ {α : Type u_1} {t : Batteries.RBNode α} {c : Batteries.RBColor} {n : Nat}, t.Balanced c n → ∃ n', t.setBlack.Balanced Batteries.RBColor.black n'
<VAR>α : Type u_1<VAR>t : Batteries.RBNode α<GOAL>t.setBlack.setBlack = t.setBlack
<VAR>α : Type u_1<VAR>cmp : α → α → Ordering<VAR>x : α<VAR>inst : Batteries.OrientedCmp cmp<VAR>t : Batteries.RBNode α<GOAL>(Batteries.RBNode.ins cmp x t).reverse = Batteries.RBNode.ins (flip cmp) x t.reverse
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>cmp : α → α → Ordering<VAR>x : α<VAR>t : Batteries.RBNode α<VAR>h₁ : p x<VAR>h₂ : Batteries.RBNode.All p t<GOAL>Batteries.RBNode.All p (Batteries.RBNode.ins cmp x t)
<VAR>α : Type u_1<VAR>cmp : α → α → Ordering<VAR>x : α<VAR>t : Batteries.RBNode α<GOAL>Batteries.RBNode.Ordered cmp t → Batteries.RBNode.Ordered cmp (Batteries.RBNode.ins cmp x t)
<VAR>α : Type u_1<VAR>t : Batteries.RBNode α<GOAL>t.reverse.isRed = t.isRed
<VAR>α : Type u_1<VAR>cmp : α → α → Ordering<VAR>x : α<VAR>inst : Batteries.OrientedCmp cmp<VAR>t : Batteries.RBNode α<GOAL>(Batteries.RBNode.insert cmp t x).reverse = Batteries.RBNode.insert (flip cmp) t.reverse x
<VAR>α : Type u_1<VAR>cmp : α → α → Ordering<VAR>v : α<VAR>t : Batteries.RBNode α<GOAL>(Batteries.RBNode.insert cmp t v).setBlack = (Batteries.RBNode.ins cmp v t).setBlack
<GOAL>∀ {α : Type u_1} {cmp : α → α → Ordering} {t : Batteries.RBNode α} {v : α}, Batteries.RBNode.Ordered cmp t → Batteries.RBNode.Ordered cmp (Batteries.RBNode.insert cmp t v)
<VAR>p : Prop<GOAL>∀ {α : Type u_1} {t : Batteries.RBNode α} {n : Nat}, ¬p → Batteries.RBNode.RedRed p t n → ∃ c, t.Balanced c n
<VAR>p : Prop<GOAL>∀ {α : Type u_1} {a : Batteries.RBNode α} {x : α} {b : Batteries.RBNode α} {n : Nat}, Batteries.RBNode.RedRed p (Batteries.RBNode.node Batteries.RBColor.red a x b) n → ∃ c₁ c₂, a.Balanced c₁ n ∧ b.Balanced c₂ n
<VAR>p q : Prop<GOAL>∀ {α : Type u_1} {t : Batteries.RBNode α} {n : Nat}, (p → q) → Batteries.RBNode.RedRed p t n → Batteries.RBNode.RedRed q t n
<VAR>p : Prop<GOAL>∀ {α : Type u_1} {t : Batteries.RBNode α} {n : Nat}, Batteries.RBNode.RedRed p t n → Batteries.RBNode.RedRed p t.reverse n
<GOAL>∀ {α : Type u_1} {t : Batteries.RBNode α} {p : Prop} {n : Nat}, Batteries.RBNode.RedRed p t n → ∃ n', t.setBlack.Balanced Batteries.RBColor.black n'
<VAR>α : Type u_1<VAR>p : Prop<VAR>n : Nat<VAR>c : Batteries.RBColor<VAR>l : Batteries.RBNode α<VAR>v : α<VAR>r : Batteries.RBNode α<VAR>hl : Batteries.RBNode.RedRed p l n<VAR>hr : r.Balanced c n<GOAL>∃ c, (l.balance1 v r).Balanced c (n + 1)
<VAR>α : Type u_1<VAR>c : Batteries.RBColor<VAR>n : Nat<VAR>p : Prop<VAR>l : Batteries.RBNode α<VAR>v : α<VAR>r : Batteries.RBNode α<VAR>hl : l.Balanced c n<VAR>hr : Batteries.RBNode.RedRed p r n<GOAL>∃ c, (l.balance2 v r).Balanced c (n + 1)
<VAR>α : Type u_1<VAR>c : Batteries.RBColor<VAR>n : Nat<VAR>l : Batteries.RBNode α<VAR>v : α<VAR>r : Batteries.RBNode α<VAR>hl : l.Balanced c n<GOAL>l.balance1 v r = Batteries.RBNode.node Batteries.RBColor.black l v r
<VAR>α : Type u_1<VAR>c : Batteries.RBColor<VAR>n : Nat<VAR>l : Batteries.RBNode α<VAR>v : α<VAR>r : Batteries.RBNode α<VAR>hr : r.Balanced c n<GOAL>l.balance2 v r = Batteries.RBNode.node Batteries.RBColor.black l v r
<VAR>α : Type u_1<VAR>c : Batteries.RBColor<VAR>n : Nat<VAR>cmp : α → α → Ordering<VAR>v : α<VAR>t : Batteries.RBNode α<VAR>h : t.Balanced c n<GOAL>Batteries.RBNode.RedRed (t.isRed = Batteries.RBColor.red) (Batteries.RBNode.ins cmp v t) n
<VAR>α : Type u_1<VAR>c : Batteries.RBColor<VAR>n : Nat<VAR>cmp : α → α → Ordering<VAR>v : α<VAR>t : Batteries.RBNode α<VAR>h : t.Balanced c n<GOAL>∃ c' n', (Batteries.RBNode.insert cmp t v).Balanced c' n'
<VAR>α : Type u_1<VAR>t : Batteries.RBNode α<GOAL>t.setRed.reverse = t.reverse.setRed
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>t : Batteries.RBNode α<VAR>h : Batteries.RBNode.All p t<GOAL>Batteries.RBNode.All p t.setRed
<VAR>α : Type u_1<VAR>cmp : α → α → Ordering<VAR>t : Batteries.RBNode α<GOAL>Batteries.RBNode.Ordered cmp t.setRed ↔ Batteries.RBNode.Ordered cmp t
<VAR>α : Type u_1<VAR>l : Batteries.RBNode α<VAR>v : α<VAR>r : Batteries.RBNode α<GOAL>(l.balLeft v r).reverse = r.reverse.balRight v l.reverse
<VAR>α : Type u_1<VAR>l : Batteries.RBNode α<VAR>v : α<VAR>r : Batteries.RBNode α<GOAL>(l.balRight v r).reverse = r.reverse.balLeft v l.reverse
<GOAL>∀ {α : Type u_1} {p : α → Prop} {l : Batteries.RBNode α} {v : α} {r : Batteries.RBNode α}, Batteries.RBNode.All p l → p v → Batteries.RBNode.All p r → Batteries.RBNode.All p (l.balLeft v r)
<VAR>α : Type u_1<VAR>cmp : α → α → Ordering<VAR>l : Batteries.RBNode α<VAR>v : α<VAR>r : Batteries.RBNode α<VAR>lv : Batteries.RBNode.All (fun x => Batteries.RBNode.cmpLT cmp x v) l<VAR>vr : Batteries.RBNode.All (fun x => Batteries.RBNode.cmpLT cmp v x) r<VAR>hl : Batteries.RBNode.Ordered cmp l<VAR>hr : Batteries.RBNode.Ordered cmp r<GOAL>Batteries.RBNode.Ordered cmp (l.balLeft v r)
<GOAL>∀ {α : Type u_1} {l : Batteries.RBNode α} {v : α} {r : Batteries.RBNode α} {cr : Batteries.RBColor} {n : Nat}, Batteries.RBNode.RedRed True l n → r.Balanced cr (n + 1) → Batteries.RBNode.RedRed (cr = Batteries.RBColor.red) (l.balLeft v r) (n + 1)
<GOAL>∀ {α : Type u_1} {p : α → Prop} {l : Batteries.RBNode α} {v : α} {r : Batteries.RBNode α}, Batteries.RBNode.All p l → p v → Batteries.RBNode.All p r → Batteries.RBNode.All p (l.balRight v r)
<VAR>α : Type u_1<VAR>cmp : α → α → Ordering<VAR>l : Batteries.RBNode α<VAR>v : α<VAR>r : Batteries.RBNode α<VAR>lv : Batteries.RBNode.All (fun x => Batteries.RBNode.cmpLT cmp x v) l<VAR>vr : Batteries.RBNode.All (fun x => Batteries.RBNode.cmpLT cmp v x) r<VAR>hl : Batteries.RBNode.Ordered cmp l<VAR>hr : Batteries.RBNode.Ordered cmp r<GOAL>Batteries.RBNode.Ordered cmp (l.balRight v r)
<GOAL>∀ {α : Type u_1} {l : Batteries.RBNode α} {v : α} {r : Batteries.RBNode α} {cl : Batteries.RBColor} {n : Nat}, l.Balanced cl (n + 1) → Batteries.RBNode.RedRed True r n → Batteries.RBNode.RedRed (cl = Batteries.RBColor.red) (l.balRight v r) (n + 1)
<GOAL>∀ {α : Type u_1} {l r : Batteries.RBNode α} {p : α → Prop}, Batteries.RBNode.All p l → Batteries.RBNode.All p r → Batteries.RBNode.All p (l.append r)
<VAR>α : Type u_1<VAR>cmp : α → α → Ordering<VAR>l : Batteries.RBNode α<VAR>v : α<VAR>r : Batteries.RBNode α<VAR>lv : Batteries.RBNode.All (fun x => Batteries.RBNode.cmpLT cmp x v) l<VAR>vr : Batteries.RBNode.All (fun x => Batteries.RBNode.cmpLT cmp v x) r<VAR>hl : Batteries.RBNode.Ordered cmp l<VAR>hr : Batteries.RBNode.Ordered cmp r<GOAL>Batteries.RBNode.Ordered cmp (l.append r)
<VAR>α : Type u_1<VAR>c₁ : Batteries.RBColor<VAR>n : Nat<VAR>c₂ : Batteries.RBColor<VAR>l r : Batteries.RBNode α<VAR>hl : l.Balanced c₁ n<VAR>hr : r.Balanced c₂ n<GOAL>Batteries.RBNode.RedRed (c₁ = Batteries.RBColor.black → c₂ ≠ Batteries.RBColor.black) (l.append r) n
<VAR>c : Batteries.RBColor<GOAL>∀ {α : Type u_1} {t : Batteries.RBNode α} {n : Nat}, Batteries.RBNode.DelProp c t n → ∃ n', Batteries.RBNode.RedRed (c = Batteries.RBColor.black) t n'