ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>a b c : α<GOAL>(fun x => a - x) '' [[b, c]] = [[a - b, a - c]]
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>a b c : α<GOAL>(fun x => x - a) '' [[b, c]] = [[b - a, c - a]]
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>a b : α<GOAL>Neg.neg '' [[a, b]] = [[-a, -b]]
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>a b c d : α<VAR>h : [[c, d]] ⊆ [[a, b]]<GOAL>|d - c| ≤ |b - a|
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>a b c : α<VAR>h : c ∈ [[a, b]]<GOAL>|c - a| ≤ |b - a|
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>a b c : α<VAR>h : c ∈ [[a, b]]<GOAL>|b - c| ≤ |b - a|
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>a : α<VAR>c : α<VAR>h : 0 < c<GOAL>(fun x => x * c) ⁻¹' Set.Iio a = Set.Iio (a / c)
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>a : α<VAR>c : α<VAR>h : 0 < c<GOAL>(fun x => x * c) ⁻¹' Set.Ioi a = Set.Ioi (a / c)
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>a : α<VAR>c : α<VAR>h : 0 < c<GOAL>(fun x => x * c) ⁻¹' Set.Iic a = Set.Iic (a / c)
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>a : α<VAR>c : α<VAR>h : 0 < c<GOAL>(fun x => x * c) ⁻¹' Set.Ici a = Set.Ici (a / c)
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>a b : α<VAR>c : α<VAR>h : 0 < c<GOAL>(fun x => x * c) ⁻¹' Set.Ioo a b = Set.Ioo (a / c) (b / c)
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>a b : α<VAR>c : α<VAR>h : 0 < c<GOAL>(fun x => x * c) ⁻¹' Set.Ioc a b = Set.Ioc (a / c) (b / c)
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>a b : α<VAR>c : α<VAR>h : 0 < c<GOAL>(fun x => x * c) ⁻¹' Set.Ico a b = Set.Ico (a / c) (b / c)
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>a b : α<VAR>c : α<VAR>h : 0 < c<GOAL>(fun x => x * c) ⁻¹' Set.Icc a b = Set.Icc (a / c) (b / c)
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>a : α<VAR>c : α<VAR>h : c < 0<GOAL>(fun x => x * c) ⁻¹' Set.Iio a = Set.Ioi (a / c)
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>a : α<VAR>c : α<VAR>h : c < 0<GOAL>(fun x => x * c) ⁻¹' Set.Ioi a = Set.Iio (a / c)
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>a : α<VAR>c : α<VAR>h : c < 0<GOAL>(fun x => x * c) ⁻¹' Set.Iic a = Set.Ici (a / c)
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>a : α<VAR>c : α<VAR>h : c < 0<GOAL>(fun x => x * c) ⁻¹' Set.Ici a = Set.Iic (a / c)
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>a b : α<VAR>c : α<VAR>h : c < 0<GOAL>(fun x => x * c) ⁻¹' Set.Ioo a b = Set.Ioo (b / c) (a / c)
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>a b : α<VAR>c : α<VAR>h : c < 0<GOAL>(fun x => x * c) ⁻¹' Set.Ioc a b = Set.Ico (b / c) (a / c)
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>a b : α<VAR>c : α<VAR>h : c < 0<GOAL>(fun x => x * c) ⁻¹' Set.Ico a b = Set.Ioc (b / c) (a / c)
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>a b : α<VAR>c : α<VAR>h : c < 0<GOAL>(fun x => x * c) ⁻¹' Set.Icc a b = Set.Icc (b / c) (a / c)
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>a : α<VAR>c : α<VAR>h : 0 < c<GOAL>(fun x => c * x) ⁻¹' Set.Iio a = Set.Iio (a / c)
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>a : α<VAR>c : α<VAR>h : 0 < c<GOAL>(fun x => c * x) ⁻¹' Set.Ioi a = Set.Ioi (a / c)
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>a : α<VAR>c : α<VAR>h : 0 < c<GOAL>(fun x => c * x) ⁻¹' Set.Iic a = Set.Iic (a / c)
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>a : α<VAR>c : α<VAR>h : 0 < c<GOAL>(fun x => c * x) ⁻¹' Set.Ici a = Set.Ici (a / c)
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>a b : α<VAR>c : α<VAR>h : 0 < c<GOAL>(fun x => c * x) ⁻¹' Set.Ioo a b = Set.Ioo (a / c) (b / c)
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>a b : α<VAR>c : α<VAR>h : 0 < c<GOAL>(fun x => c * x) ⁻¹' Set.Ioc a b = Set.Ioc (a / c) (b / c)
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>a b : α<VAR>c : α<VAR>h : 0 < c<GOAL>(fun x => c * x) ⁻¹' Set.Ico a b = Set.Ico (a / c) (b / c)
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>a b : α<VAR>c : α<VAR>h : 0 < c<GOAL>(fun x => c * x) ⁻¹' Set.Icc a b = Set.Icc (a / c) (b / c)
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>a : α<VAR>c : α<VAR>h : c < 0<GOAL>(fun x => c * x) ⁻¹' Set.Iio a = Set.Ioi (a / c)
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>a : α<VAR>c : α<VAR>h : c < 0<GOAL>(fun x => c * x) ⁻¹' Set.Ioi a = Set.Iio (a / c)
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>a : α<VAR>c : α<VAR>h : c < 0<GOAL>(fun x => c * x) ⁻¹' Set.Iic a = Set.Ici (a / c)
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>a : α<VAR>c : α<VAR>h : c < 0<GOAL>(fun x => c * x) ⁻¹' Set.Ici a = Set.Iic (a / c)
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>a b : α<VAR>c : α<VAR>h : c < 0<GOAL>(fun x => c * x) ⁻¹' Set.Ioo a b = Set.Ioo (b / c) (a / c)
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>a b : α<VAR>c : α<VAR>h : c < 0<GOAL>(fun x => c * x) ⁻¹' Set.Ioc a b = Set.Ico (b / c) (a / c)
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>a b : α<VAR>c : α<VAR>h : c < 0<GOAL>(fun x => c * x) ⁻¹' Set.Ico a b = Set.Ioc (b / c) (a / c)
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>a b : α<VAR>c : α<VAR>h : c < 0<GOAL>(fun x => c * x) ⁻¹' Set.Icc a b = Set.Icc (b / c) (a / c)
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>a : α<VAR>ha : a ≠ 0<VAR>b c : α<GOAL>(fun x => x * a) ⁻¹' [[b, c]] = [[b / a, c / a]]
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>a : α<VAR>ha : a ≠ 0<VAR>b c : α<GOAL>(fun x => a * x) ⁻¹' [[b, c]] = [[b / a, c / a]]
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>a : α<VAR>ha : a ≠ 0<VAR>b c : α<GOAL>(fun x => x / a) ⁻¹' [[b, c]] = [[b * a, c * a]]
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>a b c : α<GOAL>(fun x => x * a) '' [[b, c]] = [[b * a, c * a]]
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>a b c : α<GOAL>(fun x => a * x) '' [[b, c]] = [[a * b, a * c]]
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>a b c : α<GOAL>(fun x => x / a) '' [[b, c]] = [[b / a, c / a]]
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>a b : α<VAR>c : α<VAR>h : 0 < c<GOAL>(fun x => x * c) '' Set.Icc a b = Set.Icc (a * c) (b * c)
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>a b c : α<VAR>hab : a ≤ b<VAR>hc : 0 ≤ c<GOAL>(fun x => x * c) '' Set.Icc a b = Set.Icc (a * c) (b * c)
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>a : α<VAR>h : 0 < a<VAR>b c : α<GOAL>(fun x => a * x) '' Set.Icc b c = Set.Icc (a * b) (a * c)
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>a b c : α<VAR>ha : 0 ≤ a<VAR>hbc : b ≤ c<GOAL>(fun x => a * x) '' Set.Icc b c = Set.Icc (a * b) (a * c)
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>a b : α<VAR>c : α<VAR>h : 0 < c<GOAL>(fun x => x * c) '' Set.Ioo a b = Set.Ioo (a * c) (b * c)
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>a : α<VAR>h : 0 < a<VAR>b c : α<GOAL>(fun x => a * x) '' Set.Ioo b c = Set.Ioo (a * b) (a * c)
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>a : α<VAR>ha : 0 < a<GOAL>(Set.Ioo 0 a)⁻¹ = Set.Ioi a⁻¹
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>a : α<VAR>ha : 0 < a<GOAL>(Set.Ioi a)⁻¹ = Set.Ioo 0 a⁻¹
<VAR>k : Type u_2<VAR>LinearOrderedField k<VAR>x : k<VAR>hx : 0 < x<GOAL>(fun y => x * y) '' Set.Ioi 0 = Set.Ioi 0
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>a : α<VAR>h : 0 < a<VAR>b c d : α<GOAL>(fun x => a * x + b) '' Set.Icc c d = Set.Icc (a * c + b) (a * d + b)
<VAR>α : Type u_1<VAR>SemilatticeSup α<VAR>OrderBot α<VAR>l : List α<GOAL>(↑l).sup = List.foldr (fun x x_1 => x ⊔ x_1) ⊥ l
<VAR>α : Type u_1<VAR>SemilatticeSup α<VAR>OrderBot α<GOAL>Multiset.sup 0 = ⊥
<VAR>α : Type u_1<VAR>SemilatticeSup α<VAR>OrderBot α<VAR>a : α<VAR>s : Multiset α<GOAL>(a ::ₘ s).sup = a ⊔ s.sup
<VAR>α : Type u_1<VAR>SemilatticeSup α<VAR>OrderBot α<VAR>a : α<GOAL>{a}.sup = a
<VAR>α : Type u_1<VAR>SemilatticeSup α<VAR>OrderBot α<VAR>s₁ s₂ : Multiset α<GOAL>(s₁ + s₂).sup = s₁.sup ⊔ s₂.sup
<VAR>α : Type u_1<VAR>SemilatticeSup α<VAR>OrderBot α<VAR>s : Multiset α<VAR>a : α<GOAL>s.sup ≤ a ↔ ∀ b ∈ s, b ≤ a
<VAR>α : Type u_1<VAR>SemilatticeSup α<VAR>OrderBot α<VAR>s : Multiset α<VAR>a : α<VAR>h : a ∈ s<GOAL>a ≤ s.sup
<VAR>α : Type u_1<VAR>SemilatticeSup α<VAR>OrderBot α<VAR>s₁ s₂ : Multiset α<VAR>h : s₁ ⊆ s₂<GOAL>s₁.sup ≤ s₂.sup
<VAR>α : Type u_1<VAR>SemilatticeSup α<VAR>OrderBot α<VAR>DecidableEq α<VAR>s : Multiset α<GOAL>s.dedup.sup = s.sup
<VAR>α : Type u_1<VAR>SemilatticeSup α<VAR>OrderBot α<VAR>DecidableEq α<VAR>s₁ s₂ : Multiset α<GOAL>(s₁.ndunion s₂).sup = s₁.sup ⊔ s₂.sup
<VAR>α : Type u_1<VAR>SemilatticeSup α<VAR>OrderBot α<VAR>DecidableEq α<VAR>s₁ s₂ : Multiset α<GOAL>(s₁ ∪ s₂).sup = s₁.sup ⊔ s₂.sup
<VAR>α : Type u_1<VAR>SemilatticeSup α<VAR>OrderBot α<VAR>DecidableEq α<VAR>a : α<VAR>s : Multiset α<GOAL>(Multiset.ndinsert a s).sup = a ⊔ s.sup
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>m : Multiset (Multiset α)<GOAL>m.sup.Nodup ↔ ∀ a ∈ m, a.Nodup
<VAR>α : Type u_1<VAR>SemilatticeInf α<VAR>OrderTop α<VAR>l : List α<GOAL>(↑l).inf = List.foldr (fun x x_1 => x ⊓ x_1) ⊤ l
<VAR>α : Type u_1<VAR>SemilatticeInf α<VAR>OrderTop α<GOAL>Multiset.inf 0 = ⊤
<VAR>α : Type u_1<VAR>SemilatticeInf α<VAR>OrderTop α<VAR>a : α<VAR>s : Multiset α<GOAL>(a ::ₘ s).inf = a ⊓ s.inf
<VAR>α : Type u_1<VAR>SemilatticeInf α<VAR>OrderTop α<VAR>a : α<GOAL>{a}.inf = a
<VAR>α : Type u_1<VAR>SemilatticeInf α<VAR>OrderTop α<VAR>s₁ s₂ : Multiset α<GOAL>(s₁ + s₂).inf = s₁.inf ⊓ s₂.inf
<VAR>α : Type u_1<VAR>SemilatticeInf α<VAR>OrderTop α<VAR>s : Multiset α<VAR>a : α<GOAL>a ≤ s.inf ↔ ∀ b ∈ s, a ≤ b
<VAR>α : Type u_1<VAR>SemilatticeInf α<VAR>OrderTop α<VAR>s : Multiset α<VAR>a : α<VAR>h : a ∈ s<GOAL>s.inf ≤ a
<VAR>α : Type u_1<VAR>SemilatticeInf α<VAR>OrderTop α<VAR>s₁ s₂ : Multiset α<VAR>h : s₁ ⊆ s₂<GOAL>s₂.inf ≤ s₁.inf
<VAR>α : Type u_1<VAR>SemilatticeInf α<VAR>OrderTop α<VAR>DecidableEq α<VAR>s : Multiset α<GOAL>s.dedup.inf = s.inf
<VAR>α : Type u_1<VAR>SemilatticeInf α<VAR>OrderTop α<VAR>DecidableEq α<VAR>s₁ s₂ : Multiset α<GOAL>(s₁.ndunion s₂).inf = s₁.inf ⊓ s₂.inf
<VAR>α : Type u_1<VAR>SemilatticeInf α<VAR>OrderTop α<VAR>DecidableEq α<VAR>s₁ s₂ : Multiset α<GOAL>(s₁ ∪ s₂).inf = s₁.inf ⊓ s₂.inf
<VAR>α : Type u_1<VAR>SemilatticeInf α<VAR>OrderTop α<VAR>DecidableEq α<VAR>a : α<VAR>s : Multiset α<GOAL>(Multiset.ndinsert a s).inf = a ⊓ s.inf
<VAR>α : Type u_3<VAR>n : ℕ<VAR>β : Type u_2<VAR>σ₁ : Type<VAR>γ : Type u_1<VAR>σ₂ : Type<VAR>xs : Mathlib.Vector α n<VAR>f₁ : β → σ₁ → σ₁ × γ<VAR>f₂ : α → σ₂ → σ₂ × β<VAR>s₂ : σ₂<VAR>s₁ : σ₁<GOAL>Mathlib.Vector.mapAccumr f₁ (Mathlib.Vector.mapAccumr f₂ xs s₂).2 s₁ = let m := Mathlib.Vector.mapAccumr (fun x s => let r₂ := f₂ x s.2; let r₁ := f₁ r₂.2 s.1; ((r₁.1, r₂.1), r₁.2)) xs (s₁, s₂); (m.1.1, m.2)
<VAR>α : Type u_3<VAR>n : ℕ<VAR>β : Type u_2<VAR>σ₁ : Type<VAR>γ : Type u_1<VAR>xs : Mathlib.Vector α n<VAR>f₁ : β → σ₁ → σ₁ × γ<VAR>s : σ₁<VAR>f₂ : α → β<GOAL>Mathlib.Vector.mapAccumr f₁ (Mathlib.Vector.map f₂ xs) s = Mathlib.Vector.mapAccumr (fun x s => f₁ (f₂ x) s) xs s
<VAR>α : Type u_3<VAR>n : ℕ<VAR>β : Type u_2<VAR>γ : Type u_1<VAR>σ₂ : Type<VAR>xs : Mathlib.Vector α n<VAR>f₂ : α → σ₂ → σ₂ × β<VAR>s : σ₂<VAR>f₁ : β → γ<GOAL>Mathlib.Vector.map f₁ (Mathlib.Vector.mapAccumr f₂ xs s).2 = (Mathlib.Vector.mapAccumr (fun x s => let r := f₂ x s; (r.1, f₁ r.2)) xs s).2
<VAR>α : Type u_3<VAR>n : ℕ<VAR>β : Type u_2<VAR>γ : Type u_1<VAR>xs : Mathlib.Vector α n<VAR>f₁ : β → γ<VAR>f₂ : α → β<GOAL>Mathlib.Vector.map f₁ (Mathlib.Vector.map f₂ xs) = Mathlib.Vector.map (fun x => f₁ (f₂ x)) xs
<VAR>α : Type<VAR>n : ℕ<VAR>β : Type<VAR>xs : Mathlib.Vector α n<VAR>ys : Mathlib.Vector β n<VAR>γ σ₁ ζ σ₂ : Type<VAR>s₂ : σ₂<VAR>s₁ : σ₁<VAR>f₁ : γ → β → σ₁ → σ₁ × ζ<VAR>f₂ : α → σ₂ → σ₂ × γ<GOAL>Mathlib.Vector.mapAccumr₂ f₁ (Mathlib.Vector.mapAccumr f₂ xs s₂).2 ys s₁ = let m := Mathlib.Vector.mapAccumr₂ (fun x y s => let r₂ := f₂ x s.2; let r₁ := f₁ r₂.2 y s.1; ((r₁.1, r₂.1), r₁.2)) xs ys (s₁, s₂); (m.1.1, m.2)
<VAR>α : Type u_4<VAR>n : ℕ<VAR>β : Type u_3<VAR>xs : Mathlib.Vector α n<VAR>ys : Mathlib.Vector β n<VAR>γ : Type u_1<VAR>ζ : Type u_2<VAR>f₁ : γ → β → ζ<VAR>f₂ : α → γ<GOAL>Mathlib.Vector.map₂ f₁ (Mathlib.Vector.map f₂ xs) ys = Mathlib.Vector.map₂ (fun x y => f₁ (f₂ x) y) xs ys
<VAR>α : Type<VAR>n : ℕ<VAR>β : Type<VAR>xs : Mathlib.Vector α n<VAR>ys : Mathlib.Vector β n<VAR>γ σ₁ ζ σ₂ : Type<VAR>s₂ : σ₂<VAR>s₁ : σ₁<VAR>f₁ : α → γ → σ₁ → σ₁ × ζ<VAR>f₂ : β → σ₂ → σ₂ × γ<GOAL>Mathlib.Vector.mapAccumr₂ f₁ xs (Mathlib.Vector.mapAccumr f₂ ys s₂).2 s₁ = let m := Mathlib.Vector.mapAccumr₂ (fun x y s => let r₂ := f₂ y s.2; let r₁ := f₁ x r₂.2 s.1; ((r₁.1, r₂.1), r₁.2)) xs ys (s₁, s₂); (m.1.1, m.2)
<VAR>α : Type u_3<VAR>n : ℕ<VAR>β : Type u_4<VAR>xs : Mathlib.Vector α n<VAR>ys : Mathlib.Vector β n<VAR>γ : Type u_1<VAR>ζ : Type u_2<VAR>f₁ : α → γ → ζ<VAR>f₂ : β → γ<GOAL>Mathlib.Vector.map₂ f₁ xs (Mathlib.Vector.map f₂ ys) = Mathlib.Vector.map₂ (fun x y => f₁ x (f₂ y)) xs ys
<VAR>α : Type<VAR>n : ℕ<VAR>β : Type<VAR>xs : Mathlib.Vector α n<VAR>ys : Mathlib.Vector β n<VAR>γ σ₁ ζ σ₂ : Type<VAR>s₂ : σ₂<VAR>s₁ : σ₁<VAR>f₁ : γ → σ₁ → σ₁ × ζ<VAR>f₂ : α → β → σ₂ → σ₂ × γ<GOAL>Mathlib.Vector.mapAccumr f₁ (Mathlib.Vector.mapAccumr₂ f₂ xs ys s₂).2 s₁ = let m := Mathlib.Vector.mapAccumr₂ (fun x y s => let r₂ := f₂ x y s.2; let r₁ := f₁ r₂.2 s.1; ((r₁.1, r₂.1), r₁.2)) xs ys (s₁, s₂); (m.1.1, m.2)
<VAR>α : Type u_3<VAR>n : ℕ<VAR>β : Type u_4<VAR>xs : Mathlib.Vector α n<VAR>ys : Mathlib.Vector β n<VAR>γ : Type u_1<VAR>ζ : Type u_2<VAR>f₁ : γ → ζ<VAR>f₂ : α → β → γ<GOAL>Mathlib.Vector.map f₁ (Mathlib.Vector.map₂ f₂ xs ys) = Mathlib.Vector.map₂ (fun x y => f₁ (f₂ x y)) xs ys
<VAR>α : Type<VAR>n : ℕ<VAR>β : Type<VAR>xs : Mathlib.Vector α n<VAR>ys : Mathlib.Vector β n<VAR>γ σ₁ φ σ₂ : Type<VAR>s₂ : σ₂<VAR>s₁ : σ₁<VAR>f₁ : γ → α → σ₁ → σ₁ × φ<VAR>f₂ : α → β → σ₂ → σ₂ × γ<GOAL>Mathlib.Vector.mapAccumr₂ f₁ (Mathlib.Vector.mapAccumr₂ f₂ xs ys s₂).2 xs s₁ = let m := Mathlib.Vector.mapAccumr₂ (fun x y x_1 => match x_1 with | (s₁, s₂) => let r₂ := f₂ x y s₂; let r₁ := f₁ r₂.2 x s₁; ((r₁.1, r₂.1), r₁.2)) xs ys (s₁, s₂); (m.1.1, m.2)
<VAR>α : Type<VAR>n : ℕ<VAR>β : Type<VAR>xs : Mathlib.Vector α n<VAR>ys : Mathlib.Vector β n<VAR>γ σ₁ φ σ₂ : Type<VAR>s₂ : σ₂<VAR>s₁ : σ₁<VAR>f₁ : γ → β → σ₁ → σ₁ × φ<VAR>f₂ : α → β → σ₂ → σ₂ × γ<GOAL>Mathlib.Vector.mapAccumr₂ f₁ (Mathlib.Vector.mapAccumr₂ f₂ xs ys s₂).2 ys s₁ = let m := Mathlib.Vector.mapAccumr₂ (fun x y x_1 => match x_1 with | (s₁, s₂) => let r₂ := f₂ x y s₂; let r₁ := f₁ r₂.2 y s₁; ((r₁.1, r₂.1), r₁.2)) xs ys (s₁, s₂); (m.1.1, m.2)
<VAR>α : Type<VAR>n : ℕ<VAR>β : Type<VAR>xs : Mathlib.Vector α n<VAR>ys : Mathlib.Vector β n<VAR>γ σ₁ φ σ₂ : Type<VAR>s₂ : σ₂<VAR>s₁ : σ₁<VAR>f₁ : α → γ → σ₁ → σ₁ × φ<VAR>f₂ : α → β → σ₂ → σ₂ × γ<GOAL>Mathlib.Vector.mapAccumr₂ f₁ xs (Mathlib.Vector.mapAccumr₂ f₂ xs ys s₂).2 s₁ = let m := Mathlib.Vector.mapAccumr₂ (fun x y x_1 => match x_1 with | (s₁, s₂) => let r₂ := f₂ x y s₂; let r₁ := f₁ x r₂.2 s₁; ((r₁.1, r₂.1), r₁.2)) xs ys (s₁, s₂); (m.1.1, m.2)
<VAR>α : Type<VAR>n : ℕ<VAR>β : Type<VAR>xs : Mathlib.Vector α n<VAR>ys : Mathlib.Vector β n<VAR>γ σ₁ φ σ₂ : Type<VAR>s₂ : σ₂<VAR>s₁ : σ₁<VAR>f₁ : β → γ → σ₁ → σ₁ × φ<VAR>f₂ : α → β → σ₂ → σ₂ × γ<GOAL>Mathlib.Vector.mapAccumr₂ f₁ ys (Mathlib.Vector.mapAccumr₂ f₂ xs ys s₂).2 s₁ = let m := Mathlib.Vector.mapAccumr₂ (fun x y x_1 => match x_1 with | (s₁, s₂) => let r₂ := f₂ x y s₂; let r₁ := f₁ y r₂.2 s₁; ((r₁.1, r₂.1), r₁.2)) xs ys (s₁, s₂); (m.1.1, m.2)
<VAR>α : Type u_2<VAR>n : ℕ<VAR>xs : Mathlib.Vector α n<VAR>σ₁ : Type<VAR>β : Type u_1<VAR>σ₂ : Type<VAR>f₁ : α → σ₁ → σ₁ × β<VAR>f₂ : α → σ₂ → σ₂ × β<VAR>s₁ : σ₁<VAR>s₂ : σ₂<VAR>R : σ₁ → σ₂ → Prop<VAR>h₀ : R s₁ s₂<VAR>hR : ∀ {s : σ₁} {q : σ₂} (a : α), R s q → R (f₁ a s).1 (f₂ a q).1 ∧ (f₁ a s).2 = (f₂ a q).2<GOAL>R (Mathlib.Vector.mapAccumr f₁ xs s₁).1 (Mathlib.Vector.mapAccumr f₂ xs s₂).1 ∧ (Mathlib.Vector.mapAccumr f₁ xs s₁).2 = (Mathlib.Vector.mapAccumr f₂ xs s₂).2
<VAR>α : Type u_2<VAR>n : ℕ<VAR>xs : Mathlib.Vector α n<VAR>σ₁ : Type<VAR>β : Type u_1<VAR>σ₂ : Type<VAR>f₁ : α → σ₁ → σ₁ × β<VAR>f₂ : α → σ₂ → σ₂ × β<VAR>s₁ : σ₁<VAR>s₂ : σ₂<VAR>h : ∃ R, R s₁ s₂ ∧ ∀ {s : σ₁} {q : σ₂} (a : α), R s q → R (f₁ a s).1 (f₂ a q).1 ∧ (f₁ a s).2 = (f₂ a q).2<GOAL>(Mathlib.Vector.mapAccumr f₁ xs s₁).2 = (Mathlib.Vector.mapAccumr f₂ xs s₂).2
<VAR>α : Type<VAR>n : ℕ<VAR>xs : Mathlib.Vector α n<VAR>β σ₁ γ σ₂ : Type<VAR>ys : Mathlib.Vector β n<VAR>f₁ : α → β → σ₁ → σ₁ × γ<VAR>f₂ : α → β → σ₂ → σ₂ × γ<VAR>s₁ : σ₁<VAR>s₂ : σ₂<VAR>R : σ₁ → σ₂ → Prop<VAR>h₀ : R s₁ s₂<VAR>hR : ∀ {s : σ₁} {q : σ₂} (a : α) (b : β), R s q → R (f₁ a b s).1 (f₂ a b q).1 ∧ (f₁ a b s).2 = (f₂ a b q).2<GOAL>R (Mathlib.Vector.mapAccumr₂ f₁ xs ys s₁).1 (Mathlib.Vector.mapAccumr₂ f₂ xs ys s₂).1 ∧ (Mathlib.Vector.mapAccumr₂ f₁ xs ys s₁).2 = (Mathlib.Vector.mapAccumr₂ f₂ xs ys s₂).2
<VAR>α : Type<VAR>n : ℕ<VAR>xs : Mathlib.Vector α n<VAR>β σ₁ γ σ₂ : Type<VAR>ys : Mathlib.Vector β n<VAR>f₁ : α → β → σ₁ → σ₁ × γ<VAR>f₂ : α → β → σ₂ → σ₂ × γ<VAR>s₁ : σ₁<VAR>s₂ : σ₂<VAR>h : ∃ R, R s₁ s₂ ∧ ∀ {s : σ₁} {q : σ₂} (a : α) (b : β), R s q → R (f₁ a b s).1 (f₂ a b q).1 ∧ (f₁ a b s).2 = (f₂ a b q).2<GOAL>(Mathlib.Vector.mapAccumr₂ f₁ xs ys s₁).2 = (Mathlib.Vector.mapAccumr₂ f₂ xs ys s₂).2
<VAR>α : Type u_2<VAR>n : ℕ<VAR>xs : Mathlib.Vector α n<GOAL>∀ {α_1 : Type u_1} {f : α → α_1}, Mathlib.Vector.map f xs = (Mathlib.Vector.mapAccumr (fun x x_1 => ((), f x)) xs ()).2
<VAR>α : Type u_2<VAR>n : ℕ<VAR>β : Type u_1<VAR>xs : Mathlib.Vector α n<VAR>σ : Type<VAR>f : α → σ → σ × β<VAR>s₀ : σ<VAR>S : Set σ<VAR>h₀ : s₀ ∈ S<VAR>closure : ∀ (a : α), ∀ s ∈ S, (f a s).1 ∈ S<VAR>out : ∀ (a : α) (s s' : σ), s ∈ S → s' ∈ S → (f a s).2 = (f a s').2<GOAL>(Mathlib.Vector.mapAccumr f xs s₀).2 = Mathlib.Vector.map (fun x => (f x s₀).2) xs
<VAR>α : Type<VAR>n : ℕ<VAR>β : Type<VAR>xs : Mathlib.Vector α n<VAR>ys : Mathlib.Vector β n<GOAL>∀ {α_1 : Type} {f : α → β → α_1}, Mathlib.Vector.map₂ f xs ys = (Mathlib.Vector.mapAccumr₂ (fun x y x_1 => ((), f x y)) xs ys ()).2
<VAR>α : Type<VAR>n : ℕ<VAR>β : Type<VAR>xs : Mathlib.Vector α n<VAR>ys : Mathlib.Vector β n<VAR>σ γ : Type<VAR>f : α → β → σ → σ × γ<VAR>s₀ : σ<VAR>S : Set σ<VAR>h₀ : s₀ ∈ S<VAR>closure : ∀ (a : α) (b : β), ∀ s ∈ S, (f a b s).1 ∈ S<VAR>out : ∀ (a : α) (b : β) (s s' : σ), s ∈ S → s' ∈ S → (f a b s).2 = (f a b s').2<GOAL>(Mathlib.Vector.mapAccumr₂ f xs ys s₀).2 = Mathlib.Vector.map₂ (fun x x_1 => (f x x_1 s₀).2) xs ys
<VAR>α : Type u_2<VAR>n : ℕ<VAR>β : Type u_1<VAR>xs : Mathlib.Vector α n<VAR>σ : Type<VAR>f : α → σ → σ × β<VAR>s : σ<VAR>h : ∀ (a : α), (f a s).1 = s<GOAL>Mathlib.Vector.mapAccumr f xs s = (s, Mathlib.Vector.map (fun x => (f x s).2) xs)
<VAR>α : Type<VAR>n : ℕ<VAR>β : Type<VAR>xs : Mathlib.Vector α n<VAR>ys : Mathlib.Vector β n<VAR>σ γ : Type<VAR>f : α → β → σ → σ × γ<VAR>s : σ<VAR>h : ∀ (a : α) (b : β), (f a b s).1 = s<GOAL>Mathlib.Vector.mapAccumr₂ f xs ys s = (s, Mathlib.Vector.map₂ (fun x y => (f x y s).2) xs ys)
<VAR>α : Type u_2<VAR>n : ℕ<VAR>β : Type u_1<VAR>xs : Mathlib.Vector α n<VAR>σ : Type<VAR>f : α → σ → σ × β<VAR>s : σ<VAR>h : ∀ (a : α) (s s' : σ), (f a s).2 = (f a s').2<GOAL>(Mathlib.Vector.mapAccumr f xs s).2 = Mathlib.Vector.map (fun x => (f x s).2) xs
<VAR>α : Type<VAR>n : ℕ<VAR>β : Type<VAR>xs : Mathlib.Vector α n<VAR>ys : Mathlib.Vector β n<VAR>σ γ : Type<VAR>f : α → β → σ → σ × γ<VAR>s : σ<VAR>h : ∀ (a : α) (b : β) (s s' : σ), (f a b s).2 = (f a b s').2<GOAL>(Mathlib.Vector.mapAccumr₂ f xs ys s).2 = Mathlib.Vector.map₂ (fun x y => (f x y s).2) xs ys
<VAR>α : Type u_2<VAR>n : ℕ<VAR>β : Type u_1<VAR>xs : Mathlib.Vector α n<VAR>σ : Type<VAR>s : σ<VAR>f : α → σ × σ → (σ × σ) × β<VAR>h : ∀ (x : α) (s : σ), (f x (s, s)).1.1 = (f x (s, s)).1.2<GOAL>(Mathlib.Vector.mapAccumr f xs (s, s)).2 = (Mathlib.Vector.mapAccumr (fun x s => ((f x (s, s)).1.1, (f x (s, s)).2)) xs s).2
<VAR>α : Type<VAR>n : ℕ<VAR>β : Type<VAR>xs : Mathlib.Vector α n<VAR>ys : Mathlib.Vector β n<VAR>σ γ : Type<VAR>s : σ<VAR>f : α → β → σ × σ → (σ × σ) × γ<VAR>h : ∀ (x : α) (y : β) (s : σ), let s' := (f x y (s, s)).1; s'.1 = s'.2<GOAL>(Mathlib.Vector.mapAccumr₂ f xs ys (s, s)).2 = (Mathlib.Vector.mapAccumr₂ (fun x y s => ((f x y (s, s)).1.1, (f x y (s, s)).2)) xs ys s).2
<VAR>α : Type<VAR>n : ℕ<VAR>β : Type<VAR>xs : Mathlib.Vector α n<VAR>ys : Mathlib.Vector β n<VAR>σ γ : Type<VAR>s : σ<VAR>Inhabited α<VAR>f : α → β → σ → σ × γ<VAR>h : ∀ (a : α) (b : β) (s : σ), f default b s = f a b s<GOAL>Mathlib.Vector.mapAccumr₂ f xs ys s = Mathlib.Vector.mapAccumr (fun b s => f default b s) ys s
<VAR>α : Type<VAR>n : ℕ<VAR>β : Type<VAR>xs : Mathlib.Vector α n<VAR>ys : Mathlib.Vector β n<VAR>σ γ : Type<VAR>s : σ<VAR>Inhabited β<VAR>f : α → β → σ → σ × γ<VAR>h : ∀ (a : α) (b : β) (s : σ), f a default s = f a b s<GOAL>Mathlib.Vector.mapAccumr₂ f xs ys s = Mathlib.Vector.mapAccumr (fun a s => f a default s) xs s
<VAR>α : Type u_2<VAR>n : ℕ<VAR>xs ys : Mathlib.Vector α n<VAR>β : Type u_1<VAR>f : α → α → β<VAR>comm : ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁<GOAL>Mathlib.Vector.map₂ f xs ys = Mathlib.Vector.map₂ f ys xs
<VAR>α : Type<VAR>n : ℕ<VAR>xs ys : Mathlib.Vector α n<VAR>σ γ : Type<VAR>s : σ<VAR>f : α → α → σ → σ × γ<VAR>comm : ∀ (a₁ a₂ : α) (s : σ), f a₁ a₂ s = f a₂ a₁ s<GOAL>Mathlib.Vector.mapAccumr₂ f xs ys s = Mathlib.Vector.mapAccumr₂ f ys xs s
<VAR>α : Type u_2<VAR>n : ℕ<VAR>β : Type u_3<VAR>xs : Mathlib.Vector α n<VAR>ys : Mathlib.Vector β n<VAR>γ : Type u_1<VAR>f : α → β → γ<GOAL>Mathlib.Vector.map₂ f xs ys = Mathlib.Vector.map₂ (flip f) ys xs
<VAR>α : Type<VAR>n : ℕ<VAR>β : Type<VAR>xs : Mathlib.Vector α n<VAR>ys : Mathlib.Vector β n<VAR>σ γ : Type<VAR>s : σ<VAR>f : α → β → σ → σ × γ<GOAL>Mathlib.Vector.mapAccumr₂ f xs ys s = Mathlib.Vector.mapAccumr₂ (flip f) ys xs s
<VAR>α : Type u_1<VAR>l : List α<GOAL>(↑l).antidiagonal = ↑(Multiset.powersetAux l).revzip
<VAR>α : Type u_1<VAR>l : List α<GOAL>(↑l).antidiagonal = ↑(Multiset.powersetAux' l).revzip
<VAR>α : Type u_1<VAR>s : Multiset α<VAR>x : Multiset α × Multiset α<GOAL>x ∈ s.antidiagonal ↔ x.1 + x.2 = s
<VAR>α : Type u_1<VAR>s : Multiset α<GOAL>Multiset.map Prod.fst s.antidiagonal = s.powerset
<VAR>α : Type u_1<VAR>s : Multiset α<GOAL>Multiset.map Prod.snd s.antidiagonal = s.powerset
<VAR>α : Type u_1<GOAL>Multiset.antidiagonal 0 = {(0, 0)}
<VAR>α : Type u_1<VAR>a : α<VAR>s : Multiset α<GOAL>(a ::ₘ s).antidiagonal = Multiset.map (Prod.map id (Multiset.cons a)) s.antidiagonal + Multiset.map (Prod.map (Multiset.cons a) id) s.antidiagonal
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Multiset α<GOAL>s.antidiagonal = Multiset.map (fun t => (s - t, t)) s.powerset
<VAR>α : Type u_1<VAR>s : Multiset α<GOAL>Multiset.card s.antidiagonal = 2 ^ Multiset.card s
<VAR>α : Type u_1<GOAL>Multiset.Sections 0 = {0}
<VAR>α : Type u_1<VAR>s : Multiset (Multiset α)<VAR>m : Multiset α<GOAL>(m ::ₘ s).Sections = m.bind fun a => Multiset.map (Multiset.cons a) s.Sections
<VAR>α : Type u_1<VAR>l : List (List α)<GOAL>(↑(List.map (fun l => ↑l) l)).Sections = ↑(List.map (fun l => ↑l) l.sections)
<VAR>α : Type u_1<VAR>s t : Multiset (Multiset α)<GOAL>(s + t).Sections = s.Sections.bind fun m => Multiset.map (fun x => m + x) t.Sections
<VAR>α : Type u_1<VAR>s : Multiset (Multiset α)<VAR>a : Multiset α<GOAL>a ∈ s.Sections ↔ Multiset.Rel (fun s a => a ∈ s) s a
<VAR>α : Type u_1<VAR>s : Multiset (Multiset α)<GOAL>Multiset.card s.Sections = (Multiset.map (⇑Multiset.card) s).prod
<VAR>n : ℕ<VAR>x : ℕ × ℕ<GOAL>x ∈ Multiset.Nat.antidiagonal n ↔ x.1 + x.2 = n
<VAR>n : ℕ<GOAL>Multiset.card (Multiset.Nat.antidiagonal n) = n + 1
<GOAL>Multiset.Nat.antidiagonal 0 = {(0, 0)}
<VAR>n : ℕ<GOAL>(Multiset.Nat.antidiagonal n).Nodup
<VAR>n : ℕ<GOAL>Multiset.Nat.antidiagonal (n + 1) = (0, n + 1) ::ₘ Multiset.map (Prod.map Nat.succ id) (Multiset.Nat.antidiagonal n)
<VAR>n : ℕ<GOAL>Multiset.Nat.antidiagonal (n + 1) = (n + 1, 0) ::ₘ Multiset.map (Prod.map id Nat.succ) (Multiset.Nat.antidiagonal n)
<VAR>n : ℕ<GOAL>Multiset.Nat.antidiagonal (n + 2) = (0, n + 2) ::ₘ (n + 2, 0) ::ₘ Multiset.map (Prod.map Nat.succ Nat.succ) (Multiset.Nat.antidiagonal n)
<VAR>n : ℕ<GOAL>Multiset.map Prod.swap (Multiset.Nat.antidiagonal n) = Multiset.Nat.antidiagonal n
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>DecidableRel r<VAR>IsTrans α r<VAR>IsAntisymm α r<VAR>IsTotal α r<VAR>l : List α<GOAL>Multiset.sort r ↑l = List.mergeSort r l
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>DecidableRel r<VAR>IsTrans α r<VAR>IsAntisymm α r<VAR>IsTotal α r<VAR>s : Multiset α<GOAL>List.Sorted r (Multiset.sort r s)
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>DecidableRel r<VAR>IsTrans α r<VAR>IsAntisymm α r<VAR>IsTotal α r<VAR>s : Multiset α<GOAL>↑(Multiset.sort r s) = s
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>DecidableRel r<VAR>IsTrans α r<VAR>IsAntisymm α r<VAR>IsTotal α r<VAR>s : Multiset α<VAR>a : α<GOAL>a ∈ Multiset.sort r s ↔ a ∈ s