ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>hf : Function.Bijective f<VAR>s : Set β<VAR>t : Set α<GOAL>f ⁻¹' s = t ↔ s = f '' t
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>hf : Function.Bijective f<VAR>s : Set α<VAR>t : Set β<GOAL>s = f ⁻¹' t ↔ f '' s = t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s t : Set β<VAR>h : Disjoint s t<GOAL>Disjoint (f ⁻¹' s) (f ⁻¹' t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s t : Set β<VAR>h : Codisjoint s t<GOAL>Codisjoint (f ⁻¹' s) (f ⁻¹' t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s t : Set β<VAR>h : IsCompl s t<GOAL>IsCompl (f ⁻¹' s) (f ⁻¹' t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : β → α<VAR>g : γ → α<VAR>s : Set β<VAR>t : Set γ<VAR>h : ∀ b ∈ s, ∀ c ∈ t, f b ≠ g c<GOAL>Disjoint (f '' s) (g '' t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>hf : Function.Injective f<VAR>s t : Set α<VAR>hd : Disjoint s t<GOAL>Disjoint (f '' s) (f '' t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s t : Set α<VAR>h : Disjoint (f '' s) (f '' t)<GOAL>Disjoint s t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s t : Set α<VAR>hf : Function.Injective f<GOAL>Disjoint (f '' s) (f '' t) ↔ Disjoint s t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>hf : Function.Surjective f<VAR>s t : Set β<VAR>h : Disjoint (f ⁻¹' s) (f ⁻¹' t)<GOAL>Disjoint s t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>hf : Function.Surjective f<VAR>s t : Set β<GOAL>Disjoint (f ⁻¹' s) (f ⁻¹' t) ↔ Disjoint s t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s : Set β<VAR>h : Disjoint s (Set.range f)<GOAL>f ⁻¹' s = ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s : Set β<GOAL>f ⁻¹' s = ∅ ↔ Disjoint s (Set.range f)
<VAR>α : Type u_1<VAR>β : α → Type u_2<VAR>i j : α<VAR>s : Set (β i)<VAR>h : i ≠ j<GOAL>Sigma.mk j ⁻¹' (Sigma.mk i '' s) = ∅
<VAR>α : Type u_1<VAR>β : α → Type u_2<VAR>i : α<VAR>s : Set (β i)<GOAL>Sigma.mk i ⁻¹' (Sigma.mk i '' s) = s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : Multiset β<GOAL>Multiset.disjSum 0 t = Multiset.map Sum.inr t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Multiset α<GOAL>s.disjSum 0 = Multiset.map Sum.inl s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Multiset α<VAR>t : Multiset β<GOAL>Multiset.card (s.disjSum t) = Multiset.card s + Multiset.card t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Multiset α<VAR>t : Multiset β<VAR>x : α ⊕ β<GOAL>x ∈ s.disjSum t ↔ (∃ a ∈ s, Sum.inl a = x) ∨ ∃ b ∈ t, Sum.inr b = x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Multiset α<VAR>t : Multiset β<VAR>a : α<GOAL>Sum.inl a ∈ s.disjSum t ↔ a ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Multiset α<VAR>t : Multiset β<VAR>b : β<GOAL>Sum.inr b ∈ s.disjSum t ↔ b ∈ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s₁ s₂ : Multiset α<VAR>t₁ t₂ : Multiset β<VAR>hs : s₁ ≤ s₂<VAR>ht : t₁ ≤ t₂<GOAL>s₁.disjSum t₁ ≤ s₂.disjSum t₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : Multiset β<GOAL>Monotone fun s => s.disjSum t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Multiset α<GOAL>Monotone s.disjSum
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s₁ s₂ : Multiset α<VAR>t₁ t₂ : Multiset β<VAR>hs : s₁ < s₂<VAR>ht : t₁ ≤ t₂<GOAL>s₁.disjSum t₁ < s₂.disjSum t₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s₁ s₂ : Multiset α<VAR>t₁ t₂ : Multiset β<VAR>hs : s₁ ≤ s₂<VAR>ht : t₁ < t₂<GOAL>s₁.disjSum t₁ < s₂.disjSum t₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : Multiset β<GOAL>StrictMono fun s => s.disjSum t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Multiset α<GOAL>StrictMono s.disjSum
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Multiset α<VAR>t : Multiset β<VAR>hs : s.Nodup<VAR>ht : t.Nodup<GOAL>(s.disjSum t).Nodup
<VAR>α : Type u_1<VAR>op : α → α → α<VAR>hc : Std.Commutative op<VAR>ha : Std.Associative op<VAR>b : α<VAR>s : Multiset α<GOAL>Multiset.fold op b s = Multiset.foldr op ⋯ b s
<VAR>α : Type u_1<VAR>op : α → α → α<VAR>hc : Std.Commutative op<VAR>ha : Std.Associative op<VAR>b : α<VAR>l : List α<GOAL>Multiset.fold op b ↑l = List.foldr op b l
<VAR>α : Type u_1<VAR>op : α → α → α<VAR>hc : Std.Commutative op<VAR>ha : Std.Associative op<VAR>b : α<VAR>l : List α<GOAL>Multiset.fold op b ↑l = List.foldl op b l
<VAR>α : Type u_1<VAR>op : α → α → α<VAR>hc : Std.Commutative op<VAR>ha : Std.Associative op<VAR>b : α<VAR>s : Multiset α<GOAL>Multiset.fold op b s = Multiset.foldl op ⋯ b s
<VAR>α : Type u_1<VAR>op : α → α → α<VAR>hc : Std.Commutative op<VAR>ha : Std.Associative op<VAR>b : α<GOAL>Multiset.fold op b 0 = b
<VAR>α : Type u_1<VAR>op : α → α → α<VAR>hc : Std.Commutative op<VAR>ha : Std.Associative op<VAR>b a : α<VAR>s : Multiset α<GOAL>Multiset.fold op b (a ::ₘ s) = op a (Multiset.fold op b s)
<VAR>α : Type u_1<VAR>op : α → α → α<VAR>hc : Std.Commutative op<VAR>ha : Std.Associative op<VAR>b a : α<VAR>s : Multiset α<GOAL>Multiset.fold op b (a ::ₘ s) = op (Multiset.fold op b s) a
<VAR>α : Type u_1<VAR>op : α → α → α<VAR>hc : Std.Commutative op<VAR>ha : Std.Associative op<VAR>b a : α<VAR>s : Multiset α<GOAL>Multiset.fold op b (a ::ₘ s) = Multiset.fold op (op b a) s
<VAR>α : Type u_1<VAR>op : α → α → α<VAR>hc : Std.Commutative op<VAR>ha : Std.Associative op<VAR>b a : α<VAR>s : Multiset α<GOAL>Multiset.fold op b (a ::ₘ s) = Multiset.fold op (op a b) s
<VAR>α : Type u_1<VAR>op : α → α → α<VAR>hc : Std.Commutative op<VAR>ha : Std.Associative op<VAR>b₁ b₂ : α<VAR>s₁ s₂ : Multiset α<GOAL>Multiset.fold op (op b₁ b₂) (s₁ + s₂) = op (Multiset.fold op b₁ s₁) (Multiset.fold op b₂ s₂)
<VAR>α : Type u_1<VAR>op : α → α → α<VAR>hc : Std.Commutative op<VAR>ha : Std.Associative op<VAR>ι : Type u_3<VAR>s : Multiset ι<VAR>t : ι → Multiset α<VAR>b : ι → α<VAR>b₀ : α<GOAL>Multiset.fold op (Multiset.fold op b₀ (Multiset.map b s)) (s.bind t) = Multiset.fold op b₀ (Multiset.map (fun i => Multiset.fold op (b i) (t i)) s)
<VAR>α : Type u_1<VAR>op : α → α → α<VAR>hc : Std.Commutative op<VAR>ha : Std.Associative op<VAR>b a : α<GOAL>Multiset.fold op b {a} = op a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>op : α → α → α<VAR>hc : Std.Commutative op<VAR>ha : Std.Associative op<VAR>f g : β → α<VAR>u₁ u₂ : α<VAR>s : Multiset β<GOAL>Multiset.fold op (op u₁ u₂) (Multiset.map (fun x => op (f x) (g x)) s) = op (Multiset.fold op u₁ (Multiset.map f s)) (Multiset.fold op u₂ (Multiset.map g s))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>op : α → α → α<VAR>hc : Std.Commutative op<VAR>ha : Std.Associative op<VAR>op' : β → β → β<VAR>Std.Commutative op'<VAR>Std.Associative op'<VAR>m : α → β<VAR>hm : ∀ (x y : α), m (op x y) = op' (m x) (m y)<VAR>b : α<VAR>s : Multiset α<GOAL>Multiset.fold op' (m b) (Multiset.map m s) = m (Multiset.fold op b s)
<VAR>α : Type u_1<VAR>op : α → α → α<VAR>hc : Std.Commutative op<VAR>ha : Std.Associative op<VAR>DecidableEq α<VAR>s₁ s₂ : Multiset α<VAR>b₁ b₂ : α<GOAL>op (Multiset.fold op b₁ (s₁ ∪ s₂)) (Multiset.fold op b₂ (s₁ ∩ s₂)) = op (Multiset.fold op b₁ s₁) (Multiset.fold op b₂ s₂)
<VAR>α : Type u_1<VAR>op : α → α → α<VAR>hc : Std.Commutative op<VAR>ha : Std.Associative op<VAR>DecidableEq α<VAR>hi : Std.IdempotentOp op<VAR>s : Multiset α<VAR>b : α<GOAL>Multiset.fold op b s.dedup = Multiset.fold op b s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Multiset α<GOAL>∃ n, s ≤ n • s.dedup
<VAR>q : ℚ≥0<GOAL>↑q = ↑q
<VAR>p q : ℚ≥0<GOAL>↑p = ↑q → p = q
<VAR>p q : ℚ≥0<GOAL>↑p = ↑q ↔ p = q
<VAR>p q : ℚ≥0<GOAL>p = q ↔ ↑p = ↑q
<VAR>x y : ℚ≥0<GOAL>↑x ≠ ↑y ↔ x ≠ y
<VAR>q : ℚ<VAR>hq : 0 ≤ q<GOAL>↑⟨q, hq⟩ = q
<VAR>p : ℚ≥0 → Prop<GOAL>(∀ (q : ℚ≥0), p q) ↔ ∀ (q : ℚ) (hq : 0 ≤ q), p ⟨q, hq⟩
<VAR>p : ℚ≥0 → Prop<GOAL>(∃ q, p q) ↔ ∃ q, ∃ (hq : 0 ≤ q), p ⟨q, hq⟩
<VAR>q : ℚ<VAR>hq : 0 ≤ q<GOAL>↑q.toNNRat = q
<VAR>q : ℚ<GOAL>q ≤ ↑q.toNNRat
<VAR>q : ℚ≥0<GOAL>0 ≤ ↑q
<VAR>p q : ℚ≥0<GOAL>↑(p + q) = ↑p + ↑q
<VAR>p q : ℚ≥0<GOAL>↑(p * q) = ↑p * ↑q
<VAR>q : ℚ≥0<VAR>n : ℕ<GOAL>↑(q ^ n) = ↑q ^ n
<VAR>q : ℚ≥0<VAR>n : ℕ<GOAL>(q ^ n).num = q.num ^ n
<VAR>q : ℚ≥0<VAR>n : ℕ<GOAL>(q ^ n).den = q.den ^ n
<VAR>p q : ℚ≥0<VAR>h : q ≤ p<GOAL>↑(p - q) = ↑p - ↑q
<VAR>q : ℚ≥0<GOAL>↑q = 0 ↔ q = 0
<VAR>q : ℚ≥0<GOAL>↑q ≠ 0 ↔ q ≠ 0
<VAR>p q : ℚ≥0<GOAL>↑p ≤ ↑q ↔ p ≤ q
<VAR>p q : ℚ≥0<GOAL>↑p < ↑q ↔ p < q
<VAR>q : ℚ≥0<GOAL>0 < ↑q ↔ 0 < q
<VAR>q : ℚ≥0<GOAL>(↑q).toNNRat = q
<VAR>n : ℕ<GOAL>(↑n).toNNRat = ↑n
<VAR>n : ℕ<GOAL>⟨↑n, ⋯⟩ = ↑n
<GOAL>⇑NNRat.coeHom = NNRat.cast
<VAR>q : ℚ≥0<VAR>n : ℕ<GOAL>↑(n • q) = n • ↑q
<VAR>s : Set ℚ≥0<GOAL>BddAbove (NNRat.cast '' s) ↔ BddAbove s
<VAR>s : Set ℚ≥0<GOAL>BddBelow (NNRat.cast '' s)
<VAR>x y : ℚ≥0<GOAL>↑(max x y) = max ↑x ↑y
<VAR>x y : ℚ≥0<GOAL>↑(min x y) = min ↑x ↑y
<VAR>p q : ℚ≥0<GOAL>p - q = (↑p - ↑q).toNNRat
<VAR>q : ℚ≥0<GOAL>|↑q| = ↑q
<VAR>q : ℚ<GOAL>0 < q.toNNRat ↔ 0 < q
<VAR>q : ℚ<GOAL>q.toNNRat = 0 ↔ q ≤ 0
<VAR>p q : ℚ<VAR>h : 0 < p<GOAL>q.toNNRat < p.toNNRat ↔ q < p
<VAR>p q : ℚ<VAR>hq : 0 ≤ q<GOAL>q.toNNRat < p.toNNRat ↔ q < p
<VAR>p q : ℚ<VAR>hq : 0 ≤ q<VAR>hp : 0 ≤ p<GOAL>(q + p).toNNRat = q.toNNRat + p.toNNRat
<VAR>p q : ℚ<GOAL>(q + p).toNNRat ≤ q.toNNRat + p.toNNRat
<VAR>q : ℚ<VAR>p : ℚ≥0<GOAL>q.toNNRat ≤ p ↔ q ≤ ↑p
<VAR>p : ℚ<VAR>q : ℚ≥0<VAR>hp : 0 ≤ p<GOAL>q ≤ p.toNNRat ↔ ↑q ≤ p
<VAR>p : ℚ<VAR>q : ℚ≥0<VAR>hq : 0 < q<GOAL>q ≤ p.toNNRat ↔ ↑q ≤ p
<VAR>q : ℚ<VAR>p : ℚ≥0<VAR>hq : 0 ≤ q<GOAL>q.toNNRat < p ↔ q < ↑p
<VAR>p : ℚ<VAR>q : ℚ≥0<GOAL>q < p.toNNRat ↔ ↑q < p
<VAR>x : ℚ<GOAL>↑(Rat.nnabs x) = |x|
<VAR>q : ℚ≥0<GOAL>(↑q).num = ↑q.num
<VAR>q : ℚ≥0<GOAL>(↑q).num.natAbs = q.num
<VAR>q : ℚ≥0<GOAL>(↑q).den = q.den
<VAR>q : ℚ≥0<GOAL>q.num ≠ 0 ↔ q ≠ 0
<VAR>q : ℚ≥0<GOAL>0 < q.num ↔ 0 < q
<VAR>q : ℚ≥0<GOAL>0 < q.den
<VAR>q : ℚ≥0<GOAL>q.den ≠ 0
<VAR>q : ℚ≥0<GOAL>q.num.Coprime q.den
<VAR>n : ℕ<GOAL>(↑n).num = n
<VAR>n : ℕ<GOAL>(↑n).den = 1
<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>(OfNat.ofNat n).num = OfNat.ofNat n
<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>(OfNat.ofNat n).den = 1
<VAR>p q : ℚ≥0<GOAL>p = q ↔ p.num = q.num ∧ p.den = q.den
<VAR>n d : ℕ<GOAL>↑(NNRat.divNat n d) = Rat.divInt ↑n ↑d
<VAR>n d : ℕ<GOAL>⟨Rat.divInt ↑n ↑d, ⋯⟩ = NNRat.divNat n d
<VAR>n₁ n₂ d₁ d₂ : ℕ<VAR>h₁ : d₁ ≠ 0<VAR>h₂ : d₂ ≠ 0<GOAL>NNRat.divNat n₁ d₁ = NNRat.divNat n₂ d₂ ↔ n₁ * d₂ = n₂ * d₁
<VAR>n : ℕ<GOAL>NNRat.divNat n 0 = 0
<VAR>q : ℚ≥0<GOAL>NNRat.divNat q.num q.den = q
<VAR>n : ℕ<GOAL>↑n = NNRat.divNat n 1
<VAR>n₁ n₂ : ℕ<VAR>d₁ d₂ : ℕ<VAR>hd₁ : d₁ ≠ 0<VAR>hd₂ : d₂ ≠ 0<GOAL>NNRat.divNat n₁ d₁ * NNRat.divNat n₂ d₂ = NNRat.divNat (n₁ * n₂) (d₁ * d₂)
<VAR>a : ℕ<VAR>ha : a ≠ 0<VAR>n d : ℕ<GOAL>NNRat.divNat (a * n) (a * d) = NNRat.divNat n d
<VAR>a : ℕ<VAR>ha : a ≠ 0<VAR>n d : ℕ<GOAL>NNRat.divNat (n * a) (d * a) = NNRat.divNat n d
<VAR>q : ℚ≥0<GOAL>q * ↑q.den = ↑q.num
<VAR>q : ℚ≥0<GOAL>↑q.den * q = ↑q.num
<VAR>q r : ℚ≥0<GOAL>q + r = NNRat.divNat (q.num * r.den + r.num * q.den) (q.den * r.den)
<VAR>q r : ℚ≥0<GOAL>q * r = NNRat.divNat (q.num * r.num) (q.den * r.den)
<VAR>p q : ℚ≥0<GOAL>p < q ↔ p.num * q.den < q.num * p.den
<VAR>p q : ℚ≥0<GOAL>p ≤ q ↔ p.num * q.den ≤ q.num * p.den
<VAR>α : Type u_1<VAR>Mul α<VAR>Preorder α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass α α (Function.swap HMul.hMul) LE.le<VAR>a b c d : α<GOAL>Set.Icc a b * Set.Icc c d ⊆ Set.Icc (a * c) (b * d)
<VAR>α : Type u_1<VAR>Add α<VAR>Preorder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass α α (Function.swap HAdd.hAdd) LE.le<VAR>a b c d : α<GOAL>Set.Icc a b + Set.Icc c d ⊆ Set.Icc (a + c) (b + d)
<VAR>α : Type u_1<VAR>Mul α<VAR>Preorder α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass α α (Function.swap HMul.hMul) LE.le<VAR>a b : α<GOAL>Set.Iic a * Set.Iic b ⊆ Set.Iic (a * b)
<VAR>α : Type u_1<VAR>Add α<VAR>Preorder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass α α (Function.swap HAdd.hAdd) LE.le<VAR>a b : α<GOAL>Set.Iic a + Set.Iic b ⊆ Set.Iic (a + b)
<VAR>α : Type u_1<VAR>Mul α<VAR>Preorder α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass α α (Function.swap HMul.hMul) LE.le<VAR>a b : α<GOAL>Set.Ici a * Set.Ici b ⊆ Set.Ici (a * b)
<VAR>α : Type u_1<VAR>Add α<VAR>Preorder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass α α (Function.swap HAdd.hAdd) LE.le<VAR>a b : α<GOAL>Set.Ici a + Set.Ici b ⊆ Set.Ici (a + b)
<VAR>α : Type u_1<VAR>Mul α<VAR>PartialOrder α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>CovariantClass α α (Function.swap HMul.hMul) LT.lt<VAR>a b c d : α<GOAL>Set.Icc a b * Set.Ico c d ⊆ Set.Ico (a * c) (b * d)
<VAR>α : Type u_1<VAR>Add α<VAR>PartialOrder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>CovariantClass α α (Function.swap HAdd.hAdd) LT.lt<VAR>a b c d : α<GOAL>Set.Icc a b + Set.Ico c d ⊆ Set.Ico (a + c) (b + d)
<VAR>α : Type u_1<VAR>Add α<VAR>PartialOrder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>CovariantClass α α (Function.swap HAdd.hAdd) LT.lt<VAR>a b c d : α<GOAL>Set.Ico a b + Set.Icc c d ⊆ Set.Ico (a + c) (b + d)
<VAR>α : Type u_1<VAR>Mul α<VAR>PartialOrder α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>CovariantClass α α (Function.swap HMul.hMul) LT.lt<VAR>a b c d : α<GOAL>Set.Ico a b * Set.Icc c d ⊆ Set.Ico (a * c) (b * d)
<VAR>α : Type u_1<VAR>Add α<VAR>PartialOrder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>CovariantClass α α (Function.swap HAdd.hAdd) LT.lt<VAR>a b c d : α<GOAL>Set.Ioc a b + Set.Ico c d ⊆ Set.Ioo (a + c) (b + d)
<VAR>α : Type u_1<VAR>Mul α<VAR>PartialOrder α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>CovariantClass α α (Function.swap HMul.hMul) LT.lt<VAR>a b c d : α<GOAL>Set.Ioc a b * Set.Ico c d ⊆ Set.Ioo (a * c) (b * d)
<VAR>α : Type u_1<VAR>Mul α<VAR>PartialOrder α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>CovariantClass α α (Function.swap HMul.hMul) LT.lt<VAR>a b c d : α<GOAL>Set.Ico a b * Set.Ioc c d ⊆ Set.Ioo (a * c) (b * d)
<VAR>α : Type u_1<VAR>Add α<VAR>PartialOrder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>CovariantClass α α (Function.swap HAdd.hAdd) LT.lt<VAR>a b c d : α<GOAL>Set.Ico a b + Set.Ioc c d ⊆ Set.Ioo (a + c) (b + d)
<VAR>α : Type u_1<VAR>Mul α<VAR>PartialOrder α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>CovariantClass α α (Function.swap HMul.hMul) LT.lt<VAR>a b : α<GOAL>Set.Iic a * Set.Iio b ⊆ Set.Iio (a * b)
<VAR>α : Type u_1<VAR>Add α<VAR>PartialOrder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>CovariantClass α α (Function.swap HAdd.hAdd) LT.lt<VAR>a b : α<GOAL>Set.Iic a + Set.Iio b ⊆ Set.Iio (a + b)
<VAR>α : Type u_1<VAR>Add α<VAR>PartialOrder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>CovariantClass α α (Function.swap HAdd.hAdd) LT.lt<VAR>a b : α<GOAL>Set.Iio a + Set.Iic b ⊆ Set.Iio (a + b)
<VAR>α : Type u_1<VAR>Mul α<VAR>PartialOrder α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>CovariantClass α α (Function.swap HMul.hMul) LT.lt<VAR>a b : α<GOAL>Set.Iio a * Set.Iic b ⊆ Set.Iio (a * b)
<VAR>α : Type u_1<VAR>Add α<VAR>PartialOrder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>CovariantClass α α (Function.swap HAdd.hAdd) LT.lt<VAR>a b : α<GOAL>Set.Ioi a + Set.Ici b ⊆ Set.Ioi (a + b)
<VAR>α : Type u_1<VAR>Mul α<VAR>PartialOrder α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>CovariantClass α α (Function.swap HMul.hMul) LT.lt<VAR>a b : α<GOAL>Set.Ioi a * Set.Ici b ⊆ Set.Ioi (a * b)
<VAR>α : Type u_1<VAR>Mul α<VAR>PartialOrder α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>CovariantClass α α (Function.swap HMul.hMul) LT.lt<VAR>a b : α<GOAL>Set.Ici a * Set.Ioi b ⊆ Set.Ioi (a * b)
<VAR>α : Type u_1<VAR>Add α<VAR>PartialOrder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>CovariantClass α α (Function.swap HAdd.hAdd) LT.lt<VAR>a b : α<GOAL>Set.Ici a + Set.Ioi b ⊆ Set.Ioi (a + b)
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>a b : α<GOAL>(fun x => a + x) ⁻¹' Set.Ici b = Set.Ici (b - a)
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>a b : α<GOAL>(fun x => a + x) ⁻¹' Set.Ioi b = Set.Ioi (b - a)
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>a b : α<GOAL>(fun x => a + x) ⁻¹' Set.Iic b = Set.Iic (b - a)
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>a b : α<GOAL>(fun x => a + x) ⁻¹' Set.Iio b = Set.Iio (b - a)
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>a b c : α<GOAL>(fun x => a + x) ⁻¹' Set.Icc b c = Set.Icc (b - a) (c - a)
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>a b c : α<GOAL>(fun x => a + x) ⁻¹' Set.Ico b c = Set.Ico (b - a) (c - a)
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>a b c : α<GOAL>(fun x => a + x) ⁻¹' Set.Ioc b c = Set.Ioc (b - a) (c - a)
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>a b c : α<GOAL>(fun x => a + x) ⁻¹' Set.Ioo b c = Set.Ioo (b - a) (c - a)
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>a b : α<GOAL>(fun x => x + a) ⁻¹' Set.Ici b = Set.Ici (b - a)
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>a b : α<GOAL>(fun x => x + a) ⁻¹' Set.Ioi b = Set.Ioi (b - a)
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>a b : α<GOAL>(fun x => x + a) ⁻¹' Set.Iic b = Set.Iic (b - a)
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>a b : α<GOAL>(fun x => x + a) ⁻¹' Set.Iio b = Set.Iio (b - a)
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>a b c : α<GOAL>(fun x => x + a) ⁻¹' Set.Icc b c = Set.Icc (b - a) (c - a)
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>a b c : α<GOAL>(fun x => x + a) ⁻¹' Set.Ico b c = Set.Ico (b - a) (c - a)
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>a b c : α<GOAL>(fun x => x + a) ⁻¹' Set.Ioc b c = Set.Ioc (b - a) (c - a)
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>a b c : α<GOAL>(fun x => x + a) ⁻¹' Set.Ioo b c = Set.Ioo (b - a) (c - a)
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>a : α<GOAL>-Set.Ici a = Set.Iic (-a)
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>a : α<GOAL>-Set.Iic a = Set.Ici (-a)
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>a : α<GOAL>-Set.Ioi a = Set.Iio (-a)
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>a : α<GOAL>-Set.Iio a = Set.Ioi (-a)
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>a b : α<GOAL>-Set.Icc a b = Set.Icc (-b) (-a)
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>a b : α<GOAL>-Set.Ico a b = Set.Ioc (-b) (-a)
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>a b : α<GOAL>-Set.Ioc a b = Set.Ico (-b) (-a)
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>a b : α<GOAL>-Set.Ioo a b = Set.Ioo (-b) (-a)
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>a b : α<GOAL>(fun x => x - a) ⁻¹' Set.Ici b = Set.Ici (b + a)
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>a b : α<GOAL>(fun x => x - a) ⁻¹' Set.Ioi b = Set.Ioi (b + a)
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>a b : α<GOAL>(fun x => x - a) ⁻¹' Set.Iic b = Set.Iic (b + a)
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>a b : α<GOAL>(fun x => x - a) ⁻¹' Set.Iio b = Set.Iio (b + a)
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>a b c : α<GOAL>(fun x => x - a) ⁻¹' Set.Icc b c = Set.Icc (b + a) (c + a)
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>a b c : α<GOAL>(fun x => x - a) ⁻¹' Set.Ico b c = Set.Ico (b + a) (c + a)
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>a b c : α<GOAL>(fun x => x - a) ⁻¹' Set.Ioc b c = Set.Ioc (b + a) (c + a)
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>a b c : α<GOAL>(fun x => x - a) ⁻¹' Set.Ioo b c = Set.Ioo (b + a) (c + a)
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>a b : α<GOAL>(fun x => a - x) ⁻¹' Set.Ici b = Set.Iic (a - b)
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>a b : α<GOAL>(fun x => a - x) ⁻¹' Set.Iic b = Set.Ici (a - b)
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>a b : α<GOAL>(fun x => a - x) ⁻¹' Set.Ioi b = Set.Iio (a - b)
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>a b : α<GOAL>(fun x => a - x) ⁻¹' Set.Iio b = Set.Ioi (a - b)
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>a b c : α<GOAL>(fun x => a - x) ⁻¹' Set.Icc b c = Set.Icc (a - c) (a - b)
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>a b c : α<GOAL>(fun x => a - x) ⁻¹' Set.Ico b c = Set.Ioc (a - c) (a - b)
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>a b c : α<GOAL>(fun x => a - x) ⁻¹' Set.Ioc b c = Set.Ico (a - c) (a - b)
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>a b c : α<GOAL>(fun x => a - x) ⁻¹' Set.Ioo b c = Set.Ioo (a - c) (a - b)
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>a b : α<GOAL>(fun x => a + x) '' Set.Iic b = Set.Iic (a + b)
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>a b : α<GOAL>(fun x => a + x) '' Set.Iio b = Set.Iio (a + b)
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>a b : α<GOAL>(fun x => x + a) '' Set.Iic b = Set.Iic (b + a)
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>a b : α<GOAL>(fun x => x + a) '' Set.Iio b = Set.Iio (b + a)
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>a : α<GOAL>Neg.neg '' Set.Ici a = Set.Iic (-a)
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>a : α<GOAL>Neg.neg '' Set.Iic a = Set.Ici (-a)
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>a : α<GOAL>Neg.neg '' Set.Ioi a = Set.Iio (-a)
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>a : α<GOAL>Neg.neg '' Set.Iio a = Set.Ioi (-a)
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>a b : α<GOAL>Neg.neg '' Set.Icc a b = Set.Icc (-b) (-a)
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>a b : α<GOAL>Neg.neg '' Set.Ico a b = Set.Ioc (-b) (-a)
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>a b : α<GOAL>Neg.neg '' Set.Ioc a b = Set.Ico (-b) (-a)
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>a b : α<GOAL>Neg.neg '' Set.Ioo a b = Set.Ioo (-b) (-a)
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>a b : α<GOAL>(fun x => a - x) '' Set.Ici b = Set.Iic (a - b)
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>a b : α<GOAL>(fun x => a - x) '' Set.Iic b = Set.Ici (a - b)
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>a b : α<GOAL>(fun x => a - x) '' Set.Ioi b = Set.Iio (a - b)
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>a b : α<GOAL>(fun x => a - x) '' Set.Iio b = Set.Ioi (a - b)
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>a b c : α<GOAL>(fun x => a - x) '' Set.Icc b c = Set.Icc (a - c) (a - b)
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>a b c : α<GOAL>(fun x => a - x) '' Set.Ico b c = Set.Ioc (a - c) (a - b)
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>a b c : α<GOAL>(fun x => a - x) '' Set.Ioc b c = Set.Ico (a - c) (a - b)
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>a b c : α<GOAL>(fun x => a - x) '' Set.Ioo b c = Set.Ioo (a - c) (a - b)
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>a b : α<GOAL>(fun x => x - a) '' Set.Ici b = Set.Ici (b - a)
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>a b : α<GOAL>(fun x => x - a) '' Set.Iic b = Set.Iic (b - a)
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>a b : α<GOAL>(fun x => x - a) '' Set.Ioi b = Set.Ioi (b - a)
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>a b : α<GOAL>(fun x => x - a) '' Set.Iio b = Set.Iio (b - a)
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>a b c : α<GOAL>(fun x => x - a) '' Set.Icc b c = Set.Icc (b - a) (c - a)
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>a b c : α<GOAL>(fun x => x - a) '' Set.Ico b c = Set.Ico (b - a) (c - a)
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>a b c : α<GOAL>(fun x => x - a) '' Set.Ioc b c = Set.Ioc (b - a) (c - a)
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>a b c : α<GOAL>(fun x => x - a) '' Set.Ioo b c = Set.Ioo (b - a) (c - a)
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>a b : α<GOAL>Set.BijOn (fun x => x + a) (Set.Iic b) (Set.Iic (b + a))
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>a b : α<GOAL>Set.BijOn (fun x => x + a) (Set.Iio b) (Set.Iio (b + a))
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>a b c : α<GOAL>(fun x => a + x) ⁻¹' [[b, c]] = [[b - a, c - a]]
<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>-[[a, b]] = [[-a, -b]]
<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 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 => 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]]