ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>s : Finset α<VAR>f : α → ℝ<VAR>hf : ∀ a ∈ s, 0 ≤ f a<GOAL>(∑ a ∈ s, f a).toNNReal = ∑ a ∈ s, (f a).toNNReal
<VAR>α : Type u_1<VAR>s : Finset α<VAR>f : α → ℝ<VAR>hf : ∀ a ∈ s, 0 ≤ f a<GOAL>(∏ a ∈ s, f a).toNNReal = ∏ a ∈ s, (f a).toNNReal
<VAR>r : ℝ≥0<VAR>n : ℕ<GOAL>↑(n • r) = n • ↑r
<VAR>m : ℕ<VAR>s : Bool<VAR>e : ℕ<GOAL>↑(OfScientific.ofScientific m s e) = OfScientific.ofScientific m s e
<GOAL>⇑(algebraMap ℝ≥0 ℝ) = NNReal.toReal
<VAR>r₁ r₂ : ℝ≥0<GOAL>↑r₁ ≤ ↑r₂ ↔ r₁ ≤ r₂
<VAR>r₁ r₂ : ℝ≥0<GOAL>↑r₁ < ↑r₂ ↔ r₁ < r₂
<VAR>r : ℝ≥0<GOAL>1 < ↑r ↔ 1 < r
<VAR>r : ℝ≥0<GOAL>↑r < 1 ↔ r < 1
<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>(OfNat.ofNat n).toNNReal = OfNat.ofNat n
<VAR>a : ℝ≥0<VAR>b : ↑(Set.Icc 0 ↑a)<GOAL>↑↑(a.orderIsoIccZeroCoe b) = ↑b
<VAR>a : ℝ≥0<VAR>b : ↑(Set.Iic a)<GOAL>↑(a.orderIsoIccZeroCoe.symm b) = ↑↑b
<VAR>s : Set ℝ≥0<GOAL>NNReal.toReal '' s = {x | ∃ (h : 0 ≤ x), ⟨x, h⟩ ∈ s}
<VAR>s : Set ℝ≥0<GOAL>BddAbove (NNReal.toReal '' s) ↔ BddAbove s
<VAR>s : Set ℝ≥0<GOAL>BddBelow (NNReal.toReal '' s)
<VAR>s : Set ℝ≥0<GOAL>↑(sSup s) = sSup (NNReal.toReal '' s)
<VAR>ι : Sort u_1<VAR>s : ι → ℝ≥0<GOAL>↑(⨆ i, s i) = ⨆ i, ↑(s i)
<VAR>s : Set ℝ≥0<GOAL>↑(sInf s) = sInf (NNReal.toReal '' s)
<VAR>ι : Sort u_1<VAR>s : ι → ℝ≥0<GOAL>↑(⨅ i, s i) = ⨅ i, ↑(s i)
<VAR>ι : Sort u_1<VAR>ι' : Sort u_2<VAR>Nonempty ι<VAR>Nonempty ι'<VAR>f : ι → ℝ≥0<VAR>g : ι' → ℝ≥0<VAR>a : ℝ≥0<VAR>h : ∀ (i : ι) (j : ι'), a ≤ f i + g j<GOAL>a ≤ (⨅ i, f i) + ⨅ j, g j
<VAR>a b : ℝ≥0<VAR>h : ∀ (ε : ℝ≥0), 0 < ε → a ≤ b + ε<GOAL>a ≤ b
<VAR>a b : ℝ≥0<GOAL>a < b ↔ ∃ q, 0 ≤ q ∧ a < (↑q).toNNReal ∧ (↑q).toNNReal < b
<VAR>a b c : ℝ≥0<GOAL>a * (b ⊔ c) = a * b ⊔ a * c
<VAR>a b c : ℝ≥0<GOAL>(a ⊔ b) * c = a * c ⊔ b * c
<VAR>α : Type u_1<VAR>r : ℝ≥0<VAR>s : Finset α<VAR>f : α → ℝ≥0<GOAL>r * s.sup f = s.sup fun a => r * f a
<VAR>α : Type u_1<VAR>s : Finset α<VAR>f : α → ℝ≥0<VAR>r : ℝ≥0<GOAL>s.sup f * r = s.sup fun a => f a * r
<VAR>α : Type u_1<VAR>f : α → ℝ≥0<VAR>s : Finset α<VAR>r : ℝ≥0<GOAL>s.sup f / r = s.sup fun a => f a / r
<VAR>x y : ℝ≥0<GOAL>↑(max x y) = max ↑x ↑y
<VAR>x y : ℝ≥0<GOAL>↑(min x y) = min ↑x ↑y
<VAR>q : ℝ≥0<GOAL>0 ≤ ↑q
<VAR>r : ℝ<GOAL>↑r.toNNReal = max r 0
<VAR>r : ℝ<GOAL>0 < r.toNNReal ↔ 0 < r
<VAR>r : ℝ<GOAL>r ≤ 0 → r.toNNReal = 0
<VAR>r : ℝ<VAR>p : ℝ≥0<VAR>hp : p ≠ 0<GOAL>r.toNNReal = p ↔ r = ↑p
<VAR>r : ℝ<GOAL>r.toNNReal = 1 ↔ r = 1
<VAR>r : ℝ<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>r.toNNReal = ↑n ↔ r = ↑n
<VAR>r : ℝ<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>r.toNNReal = OfNat.ofNat n ↔ r = OfNat.ofNat n
<VAR>r : ℝ<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>r.toNNReal ≤ OfNat.ofNat n ↔ r ≤ ↑n
<VAR>r : ℝ<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>OfNat.ofNat n < r.toNNReal ↔ ↑n < r
<VAR>r p : ℝ<GOAL>r.toNNReal < p.toNNReal ↔ r < p ∧ 0 < p
<VAR>r p : ℝ<VAR>h : 0 < p<GOAL>r.toNNReal < p.toNNReal ↔ r < p
<VAR>r p : ℝ<VAR>h : r.toNNReal < p.toNNReal<GOAL>r < p
<VAR>r p : ℝ<VAR>hr : 0 ≤ r<GOAL>r.toNNReal < p.toNNReal ↔ r < p
<VAR>n : ℕ<VAR>r : ℝ<GOAL>↑n ≤ r.toNNReal ↔ ↑n ≤ r ∨ n = 0
<VAR>n : ℕ<VAR>r : ℝ<VAR>hn : n ≠ 0<GOAL>↑n ≤ r.toNNReal ↔ ↑n ≤ r
<VAR>r : ℝ<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>r.toNNReal < ↑n ↔ r < ↑n
<VAR>r : ℝ<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>r.toNNReal < OfNat.ofNat n ↔ r < OfNat.ofNat n
<VAR>n : ℕ<VAR>r : ℝ<VAR>n.AtLeastTwo<GOAL>OfNat.ofNat n ≤ r.toNNReal ↔ OfNat.ofNat n ≤ r
<VAR>r p : ℝ<VAR>hr : 0 ≤ r<VAR>hp : 0 ≤ p<GOAL>(r + p).toNNReal = r.toNNReal + p.toNNReal
<VAR>r p : ℝ<VAR>hr : 0 ≤ r<VAR>hp : 0 ≤ p<GOAL>r.toNNReal + p.toNNReal = (r + p).toNNReal
<VAR>r p : ℝ<VAR>h : r ≤ p<GOAL>r.toNNReal ≤ p.toNNReal
<VAR>r p : ℝ<GOAL>(r + p).toNNReal ≤ r.toNNReal + p.toNNReal
<VAR>r : ℝ<VAR>p : ℝ≥0<GOAL>r.toNNReal ≤ p ↔ r ≤ ↑p
<VAR>r : ℝ≥0<VAR>p : ℝ<VAR>hr : 0 < r<GOAL>r ≤ p.toNNReal ↔ ↑r ≤ p
<VAR>r : ℝ≥0<VAR>p : ℝ<GOAL>r < p.toNNReal ↔ ↑r < p
<VAR>p q : ℝ<VAR>hp : 0 ≤ p<GOAL>(p * q).toNNReal = p.toNNReal * q.toNNReal
<VAR>a : ℝ≥0<VAR>m n : ℕ<VAR>mn : m ≤ n<VAR>a1 : a ≤ 1<GOAL>a ^ n ≤ a ^ m
<VAR>x y : ℝ≥0<VAR>hx : x ≠ 0<VAR>hy : 1 < y<GOAL>∃ n, x ∈ Set.Ico (y ^ n) (y ^ (n + 1))
<VAR>x y : ℝ≥0<VAR>hx : x ≠ 0<VAR>hy : 1 < y<GOAL>∃ n, x ∈ Set.Ioc (y ^ n) (y ^ (n + 1))
<VAR>r p : ℝ≥0<GOAL>r - p = (↑r - ↑p).toNNReal
<VAR>r p : ℝ≥0<GOAL>↑(r - p) = max (↑r - ↑p) 0
<VAR>a b c : ℝ≥0<GOAL>(a - b) / c = a / c - b / c
<VAR>a b r : ℝ≥0<VAR>hr : r ≠ 0<GOAL>a ≤ b / r ↔ a * r ≤ b
<VAR>a b r : ℝ≥0<VAR>hr : r ≠ 0<GOAL>a / r ≤ b ↔ a ≤ b * r
<VAR>a b r : ℝ≥0<VAR>hr : r ≠ 0<GOAL>a / r ≤ b ↔ a ≤ r * b
<VAR>a b c : ℝ≥0<VAR>h : a ≤ b * c<GOAL>a / c ≤ b
<VAR>a b c : ℝ≥0<VAR>h : a ≤ b * c<GOAL>a / b ≤ c
<VAR>a b r : ℝ≥0<VAR>hr : r ≠ 0<GOAL>a ≤ b / r ↔ r * a ≤ b
<VAR>a b r : ℝ≥0<VAR>hr : r ≠ 0<GOAL>a / r < b ↔ a < b * r
<VAR>a b r : ℝ≥0<VAR>hr : r ≠ 0<GOAL>a / r < b ↔ a < r * b
<VAR>a b r : ℝ≥0<VAR>hr : r ≠ 0<GOAL>a < b / r ↔ a * r < b
<VAR>a b r : ℝ≥0<VAR>hr : r ≠ 0<GOAL>a < b / r ↔ r * a < b
<VAR>a b r : ℝ≥0<VAR>h : a < b / r<GOAL>a * r < b
<VAR>a b c : ℝ≥0<VAR>c0 : c ≠ 0<VAR>cb : c ≤ b<GOAL>a / b ≤ a / c
<VAR>a b c : ℝ≥0<VAR>a0 : 0 < a<VAR>b0 : 0 < b<VAR>c0 : 0 < c<GOAL>a / b ≤ a / c ↔ c ≤ b
<VAR>x y : ℝ≥0<VAR>h : ∀ a < 1, a * x ≤ y<GOAL>x ≤ y
<VAR>a : ℝ≥0<GOAL>a / 2 ≤ a
<VAR>a : ℝ≥0<VAR>h : a ≠ 0<GOAL>a / 2 < a
<VAR>x : ℝ≥0<VAR>hx : x ≠ 0<VAR>n : ℤ<GOAL>0 < x ^ n
<VAR>x y : ℝ≥0<VAR>hx : x ≠ 0<VAR>h : x < y<GOAL>y⁻¹ < x⁻¹
<VAR>x : ℝ≥0<GOAL>|↑x| = ↑x
<VAR>x : ℝ≥0<VAR>y : ℝ<VAR>h : ↑x ≤ y<GOAL>x ≤ y.toNNReal
<VAR>s : Set ℝ≥0<VAR>hs : ¬BddAbove s<GOAL>sSup s = 0
<VAR>ι : Sort u_1<VAR>f : ι → ℝ≥0<VAR>hf : ¬BddAbove (Set.range f)<GOAL>⨆ i, f i = 0
<VAR>ι : Sort u_1<VAR>IsEmpty ι<VAR>f : ι → ℝ≥0<GOAL>⨆ i, f i = 0
<VAR>ι : Sort u_1<VAR>IsEmpty ι<VAR>f : ι → ℝ≥0<GOAL>⨅ i, f i = 0
<VAR>α : Sort u_2<GOAL>⨅ x, 0 = 0
<VAR>ι : Sort u_1<VAR>f : ι → ℝ≥0<VAR>a : ℝ≥0<GOAL>iInf f * a = ⨅ i, f i * a
<VAR>ι : Sort u_1<VAR>f : ι → ℝ≥0<VAR>a : ℝ≥0<GOAL>a * iInf f = ⨅ i, a * f i
<VAR>ι : Sort u_1<VAR>f : ι → ℝ≥0<VAR>a : ℝ≥0<GOAL>a * ⨆ i, f i = ⨆ i, a * f i
<VAR>ι : Sort u_1<VAR>f : ι → ℝ≥0<VAR>a : ℝ≥0<GOAL>(⨆ i, f i) * a = ⨆ i, f i * a
<VAR>ι : Sort u_1<VAR>f : ι → ℝ≥0<VAR>a : ℝ≥0<GOAL>(⨆ i, f i) / a = ⨆ i, f i / a
<VAR>ι : Sort u_1<VAR>a g : ℝ≥0<VAR>h : ι → ℝ≥0<VAR>H : ∀ (j : ι), g * h j ≤ a<GOAL>g * iSup h ≤ a
<VAR>ι : Sort u_1<VAR>a : ℝ≥0<VAR>g : ι → ℝ≥0<VAR>h : ℝ≥0<VAR>H : ∀ (i : ι), g i * h ≤ a<GOAL>iSup g * h ≤ a
<VAR>ι : Sort u_1<VAR>a : ℝ≥0<VAR>g h : ι → ℝ≥0<VAR>H : ∀ (i j : ι), g i * h j ≤ a<GOAL>iSup g * iSup h ≤ a
<VAR>ι : Sort u_1<VAR>Nonempty ι<VAR>a g : ℝ≥0<VAR>h : ι → ℝ≥0<VAR>H : ∀ (j : ι), a ≤ g * h j<GOAL>a ≤ g * iInf h
<VAR>ι : Sort u_1<VAR>Nonempty ι<VAR>a : ℝ≥0<VAR>g : ι → ℝ≥0<VAR>h : ℝ≥0<VAR>H : ∀ (i : ι), a ≤ g i * h<GOAL>a ≤ iInf g * h
<VAR>ι : Sort u_1<VAR>Nonempty ι<VAR>a : ℝ≥0<VAR>g h : ι → ℝ≥0<VAR>H : ∀ (i j : ι), a ≤ g i * h j<GOAL>a ≤ iInf g * iInf h
<VAR>s : Set ℝ<VAR>h : s.OrdConnected<GOAL>(NNReal.toReal ⁻¹' s).OrdConnected
<VAR>t : Set ℝ≥0<VAR>h : t.OrdConnected<GOAL>(NNReal.toReal '' t).OrdConnected
<VAR>s : Set ℝ<VAR>h : s.OrdConnected<GOAL>(Real.toNNReal '' s).OrdConnected
<VAR>t : Set ℝ≥0<VAR>h : t.OrdConnected<GOAL>(Real.toNNReal ⁻¹' t).OrdConnected
<VAR>x : ℝ<GOAL>↑(Real.nnabs x) = |x|
<VAR>x : ℝ<VAR>h : 0 ≤ x<GOAL>Real.nnabs x = x.toNNReal
<VAR>x : ℝ≥0<GOAL>Real.nnabs ↑x = x
<VAR>x : ℝ<GOAL>↑x.toNNReal ≤ |x|
<VAR>x : ℝ<GOAL>|x|.toNNReal = Real.nnabs x
<VAR>n : ℤ<GOAL>↑n.natAbs = Real.nnabs ↑n
<VAR>Γ₀ : Type u_1<VAR>LinearOrderedCommGroupWithZero Γ₀<VAR>h : Nontrivial Γ₀ˣ<VAR>f : Γ₀ →*₀ ℝ≥0<VAR>hf : StrictMono ⇑f<VAR>r : ℝ≥0<VAR>hr : 0 < r<GOAL>∃ d, f ↑d < r
<VAR>Γ₀ : Type u_1<VAR>LinearOrderedCommGroupWithZero Γ₀<VAR>h : Nontrivial Γ₀ˣ<VAR>f : Γ₀ →*₀ ℝ≥0<VAR>hf : StrictMono ⇑f<VAR>r : ℝ<VAR>hr : 0 < r<GOAL>∃ d, ↑(f ↑d) < r
<VAR>c : Char<VAR>cs₁ cs₂ : List Char<VAR>i₁ i₂ : String.Pos<GOAL>String.ltb { s := { data := c :: cs₁ }, i := i₁ + c } { s := { data := c :: cs₂ }, i := i₂ + c } = String.ltb { s := { data := cs₁ }, i := i₁ } { s := { data := cs₂ }, i := i₂ }
<VAR>s₁ s₂ : String<GOAL>s₁ < s₂ ↔ s₁.toList < s₂.toList
<VAR>s₁ s₂ : String<GOAL>s₁ ≤ s₂ ↔ s₁.toList ≤ s₂.toList
<VAR>s₁ s₂ : String<GOAL>s₁.toList = s₂.toList ↔ s₁ = s₂
<VAR>s : String<GOAL>s ≠ "" → s.toList = s.head :: (s.drop 1).toList
<VAR>l : List Char<GOAL>l.asString.toList = l
<VAR>l : List Char<GOAL>l.asString.length = l.length
<VAR>l l' : List Char<GOAL>l.asString = l'.asString ↔ l = l'
<VAR>f : ℕ → ℚ<GOAL>IsCauSeq abs f ↔ IsCauSeq abs fun i => ↑(f i)
<VAR>f : ℕ → ℚ<VAR>x : ℝ<VAR>h : ∀ ε > 0, ∃ i, ∀ j ≥ i, |↑(f j) - x| < ε<GOAL>∃ (h' : IsCauSeq abs f), Real.mk ⟨f, h'⟩ = x
<VAR>x : ℝ<GOAL>∃ ub, ↑ub ≤ x ∧ ∀ (z : ℤ), ↑z ≤ x → z ≤ ub
<VAR>S : Set ℝ<VAR>hne : S.Nonempty<VAR>hbdd : BddAbove S<GOAL>∃ x, IsLUB S x
<VAR>S : Set ℝ<GOAL>sSup S = if h : S.Nonempty ∧ BddAbove S then Classical.choose ⋯ else 0
<VAR>S : Set ℝ<GOAL>sInf S = -sSup (-S)
<VAR>s : Set ℝ<VAR>h : s.Nonempty<VAR>ε : ℝ<VAR>hε : 0 < ε<GOAL>∃ a ∈ s, a < sInf s + ε
<VAR>s : Set ℝ<VAR>h : s.Nonempty<VAR>ε : ℝ<VAR>hε : ε < 0<GOAL>∃ a ∈ s, sSup s + ε < a
<VAR>α : Sort u_1<VAR>IsEmpty α<VAR>f : α → ℝ<GOAL>⨆ i, f i = 0
<VAR>s : Set ℝ<VAR>hs : ¬BddAbove s<GOAL>sSup s = 0
<VAR>α : Sort u_1<VAR>f : α → ℝ<VAR>hf : ¬BddAbove (Set.range f)<GOAL>⨆ i, f i = 0
<VAR>α : Sort u_1<VAR>IsEmpty α<VAR>f : α → ℝ<GOAL>⨅ i, f i = 0
<VAR>s : Set ℝ<VAR>hs : ¬BddBelow s<GOAL>sInf s = 0
<VAR>α : Sort u_1<VAR>f : α → ℝ<VAR>hf : ¬BddBelow (Set.range f)<GOAL>⨅ i, f i = 0
<VAR>ι : Sort u_1<VAR>f : ι → ℝ<VAR>hf : ∀ (i : ι), 0 ≤ f i<GOAL>0 ≤ ⨆ i, f i
<VAR>S : Set ℝ<VAR>a : ℝ<VAR>hS : ∀ x ∈ S, x ≤ a<VAR>ha : 0 ≤ a<GOAL>sSup S ≤ a
<VAR>ι : Sort u_1<VAR>f : ι → ℝ<VAR>a : ℝ<VAR>hS : ∀ (i : ι), f i ≤ a<VAR>ha : 0 ≤ a<GOAL>⨆ i, f i ≤ a
<VAR>S : Set ℝ<VAR>hS : ∀ x ∈ S, x ≤ 0<GOAL>sSup S ≤ 0
<VAR>ι : Sort u_1<VAR>f : ι → ℝ<VAR>hf : ∀ (i : ι), 0 ≤ f i<GOAL>0 ≤ iInf f
<VAR>f : CauSeq ℝ abs<GOAL>∃ x, f ≈ CauSeq.const abs x
<VAR>f : ℝ → ℝ<VAR>x : ℝ<VAR>hf : BddBelow (f '' Set.Ioi x)<VAR>hf_mono : Monotone f<GOAL>⨅ r, f ↑r = ⨅ q, f ↑↑q
<GOAL>¬BddAbove (Set.range fun x => ↑x)
<GOAL>¬BddBelow (Set.range fun x => ↑x)
<GOAL>⋃ r, Set.Iic ↑r = Set.univ
<GOAL>⋂ r, Set.Iic ↑r = ∅
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>n : ℕ<GOAL>DFinsupp.toMultiset (DFinsupp.single a n) = Multiset.replicate n a
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Multiset α<VAR>a : α<GOAL>(Multiset.toDFinsupp s) a = Multiset.count a s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Multiset α<GOAL>(Multiset.toDFinsupp s).support = s.toFinset
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>n : ℕ<GOAL>Multiset.toDFinsupp (Multiset.replicate n a) = DFinsupp.single a n
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<GOAL>Multiset.toDFinsupp {a} = DFinsupp.single a 1
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : Π₀ (x : α), ℕ<GOAL>Multiset.equivDFinsupp.symm a = DFinsupp.toMultiset a
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : Multiset α<GOAL>Multiset.equivDFinsupp a = Multiset.toDFinsupp a
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Multiset α<GOAL>DFinsupp.toMultiset (Multiset.toDFinsupp s) = s
<VAR>α : Type u_1<VAR>DecidableEq α<GOAL>Function.Injective ⇑Multiset.toDFinsupp
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Multiset α<GOAL>Multiset.toDFinsupp s = Multiset.toDFinsupp t ↔ s = t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Multiset α<GOAL>Multiset.toDFinsupp s ≤ Multiset.toDFinsupp t ↔ s ≤ t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Multiset α<GOAL>Multiset.toDFinsupp s < Multiset.toDFinsupp t ↔ s < t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Multiset α<GOAL>Multiset.toDFinsupp (s ∩ t) = Multiset.toDFinsupp s ⊓ Multiset.toDFinsupp t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Multiset α<GOAL>Multiset.toDFinsupp (s ∪ t) = Multiset.toDFinsupp s ⊔ Multiset.toDFinsupp t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>f : Π₀ (x : α), ℕ<GOAL>Multiset.toDFinsupp (DFinsupp.toMultiset f) = f
<VAR>α : Type u_1<VAR>DecidableEq α<GOAL>Function.Injective ⇑DFinsupp.toMultiset
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>f g : Π₀ (_a : α), ℕ<GOAL>DFinsupp.toMultiset f = DFinsupp.toMultiset g ↔ f = g
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>f g : Π₀ (_a : α), ℕ<GOAL>DFinsupp.toMultiset f ≤ DFinsupp.toMultiset g ↔ f ≤ g
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>f g : Π₀ (_a : α), ℕ<GOAL>DFinsupp.toMultiset f < DFinsupp.toMultiset g ↔ f < g
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>f g : Π₀ (_a : α), ℕ<GOAL>DFinsupp.toMultiset (f ⊓ g) = DFinsupp.toMultiset f ∩ DFinsupp.toMultiset g
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>f g : Π₀ (_a : α), ℕ<GOAL>DFinsupp.toMultiset (f ⊔ g) = DFinsupp.toMultiset f ∪ DFinsupp.toMultiset g
<VAR>α : Type u_1<VAR>N : α → Type u_2<VAR>DecidableEq α<VAR>(a : α) → DecidableEq (N a)<VAR>(a : α) → Zero (N a)<VAR>f g : Π₀ (a : α), N a<VAR>a : α<GOAL>a ∈ f.neLocus g ↔ f a ≠ g a
<VAR>α : Type u_1<VAR>N : α → Type u_2<VAR>DecidableEq α<VAR>(a : α) → DecidableEq (N a)<VAR>(a : α) → Zero (N a)<VAR>f g : Π₀ (a : α), N a<VAR>a : α<GOAL>a ∉ f.neLocus g ↔ f a = g a
<VAR>α : Type u_1<VAR>N : α → Type u_2<VAR>DecidableEq α<VAR>(a : α) → DecidableEq (N a)<VAR>(a : α) → Zero (N a)<VAR>f g : Π₀ (a : α), N a<GOAL>↑(f.neLocus g) = {x | f x ≠ g x}
<VAR>α : Type u_1<VAR>N : α → Type u_2<VAR>DecidableEq α<VAR>(a : α) → DecidableEq (N a)<VAR>(a : α) → Zero (N a)<VAR>f g : Π₀ (a : α), N a<GOAL>f.neLocus g = ∅ ↔ f = g
<VAR>α : Type u_1<VAR>N : α → Type u_2<VAR>DecidableEq α<VAR>(a : α) → DecidableEq (N a)<VAR>(a : α) → Zero (N a)<VAR>f g : Π₀ (a : α), N a<GOAL>(f.neLocus g).Nonempty ↔ f ≠ g
<VAR>α : Type u_1<VAR>N : α → Type u_2<VAR>DecidableEq α<VAR>(a : α) → DecidableEq (N a)<VAR>(a : α) → Zero (N a)<VAR>f g : Π₀ (a : α), N a<GOAL>f.neLocus g = g.neLocus f
<VAR>α : Type u_1<VAR>N : α → Type u_2<VAR>DecidableEq α<VAR>(a : α) → DecidableEq (N a)<VAR>(a : α) → Zero (N a)<VAR>f : Π₀ (a : α), N a<GOAL>f.neLocus 0 = f.support
<VAR>α : Type u_1<VAR>N : α → Type u_2<VAR>DecidableEq α<VAR>(a : α) → DecidableEq (N a)<VAR>(a : α) → Zero (N a)<VAR>f : Π₀ (a : α), N a<GOAL>DFinsupp.neLocus 0 f = f.support
<VAR>α : Type u_1<VAR>N : α → Type u_2<VAR>DecidableEq α<VAR>M : α → Type u_3<VAR>(a : α) → Zero (N a)<VAR>(a : α) → Zero (M a)<VAR>(a : α) → DecidableEq (N a)<VAR>(a : α) → DecidableEq (M a)<VAR>f g : Π₀ (a : α), N a<VAR>F : (a : α) → N a → M a<VAR>F0 : ∀ (a : α), F a 0 = 0<GOAL>(DFinsupp.mapRange F F0 f).neLocus (DFinsupp.mapRange F F0 g) ⊆ f.neLocus g
<VAR>α : Type u_1<VAR>N : α → Type u_2<VAR>DecidableEq α<VAR>M : α → Type u_3<VAR>P : α → Type u_4<VAR>(a : α) → Zero (N a)<VAR>(a : α) → Zero (M a)<VAR>(a : α) → Zero (P a)<VAR>(a : α) → DecidableEq (N a)<VAR>(a : α) → DecidableEq (P a)<VAR>F : (a : α) → M a → N a → P a<VAR>F0 : ∀ (a : α), F a 0 0 = 0<VAR>f : Π₀ (a : α), M a<VAR>g₁ g₂ : Π₀ (a : α), N a<VAR>hF : ∀ (a : α) (f : M a), Function.Injective fun g => F a f g<GOAL>(DFinsupp.zipWith F F0 f g₁).neLocus (DFinsupp.zipWith F F0 f g₂) = g₁.neLocus g₂
<VAR>α : Type u_1<VAR>N : α → Type u_2<VAR>DecidableEq α<VAR>M : α → Type u_3<VAR>P : α → Type u_4<VAR>(a : α) → Zero (N a)<VAR>(a : α) → Zero (M a)<VAR>(a : α) → Zero (P a)<VAR>(a : α) → DecidableEq (M a)<VAR>(a : α) → DecidableEq (P a)<VAR>F : (a : α) → M a → N a → P a<VAR>F0 : ∀ (a : α), F a 0 0 = 0<VAR>f₁ f₂ : Π₀ (a : α), M a<VAR>g : Π₀ (a : α), N a<VAR>hF : ∀ (a : α) (g : N a), Function.Injective fun f => F a f g<GOAL>(DFinsupp.zipWith F F0 f₁ g).neLocus (DFinsupp.zipWith F F0 f₂ g) = f₁.neLocus f₂
<VAR>α : Type u_1<VAR>N : α → Type u_2<VAR>DecidableEq α<VAR>M : α → Type u_3<VAR>(a : α) → Zero (N a)<VAR>(a : α) → Zero (M a)<VAR>(a : α) → DecidableEq (N a)<VAR>(a : α) → DecidableEq (M a)<VAR>f g : Π₀ (a : α), N a<VAR>F : (a : α) → N a → M a<VAR>F0 : ∀ (a : α), F a 0 = 0<VAR>hF : ∀ (a : α), Function.Injective (F a)<GOAL>(DFinsupp.mapRange F F0 f).neLocus (DFinsupp.mapRange F F0 g) = f.neLocus g
<VAR>α : Type u_1<VAR>N : α → Type u_2<VAR>DecidableEq α<VAR>(a : α) → DecidableEq (N a)<VAR>(a : α) → AddLeftCancelMonoid (N a)<VAR>f g h : Π₀ (a : α), N a<GOAL>(f + g).neLocus (f + h) = g.neLocus h
<VAR>α : Type u_1<VAR>N : α → Type u_2<VAR>DecidableEq α<VAR>(a : α) → DecidableEq (N a)<VAR>(a : α) → AddRightCancelMonoid (N a)<VAR>f g h : Π₀ (a : α), N a<GOAL>(f + h).neLocus (g + h) = f.neLocus g
<VAR>α : Type u_1<VAR>N : α → Type u_2<VAR>DecidableEq α<VAR>(a : α) → DecidableEq (N a)<VAR>(a : α) → AddGroup (N a)<VAR>f g : Π₀ (a : α), N a<GOAL>(-f).neLocus (-g) = f.neLocus g
<VAR>α : Type u_1<VAR>N : α → Type u_2<VAR>DecidableEq α<VAR>(a : α) → DecidableEq (N a)<VAR>(a : α) → AddGroup (N a)<VAR>f g : Π₀ (a : α), N a<GOAL>(-f).neLocus g = f.neLocus (-g)
<VAR>α : Type u_1<VAR>N : α → Type u_2<VAR>DecidableEq α<VAR>(a : α) → DecidableEq (N a)<VAR>(a : α) → AddGroup (N a)<VAR>f g : Π₀ (a : α), N a<GOAL>f.neLocus g = (f - g).support
<VAR>α : Type u_1<VAR>N : α → Type u_2<VAR>DecidableEq α<VAR>(a : α) → DecidableEq (N a)<VAR>(a : α) → AddGroup (N a)<VAR>f g₁ g₂ : Π₀ (a : α), N a<GOAL>(f - g₁).neLocus (f - g₂) = g₁.neLocus g₂
<VAR>α : Type u_1<VAR>N : α → Type u_2<VAR>DecidableEq α<VAR>(a : α) → DecidableEq (N a)<VAR>(a : α) → AddGroup (N a)<VAR>f₁ f₂ g : Π₀ (a : α), N a<GOAL>(f₁ - g).neLocus (f₂ - g) = f₁.neLocus f₂
<VAR>α : Type u_1<VAR>N : α → Type u_2<VAR>DecidableEq α<VAR>(a : α) → DecidableEq (N a)<VAR>(a : α) → AddGroup (N a)<VAR>f g : Π₀ (a : α), N a<GOAL>f.neLocus (f + g) = g.support
<VAR>α : Type u_1<VAR>N : α → Type u_2<VAR>DecidableEq α<VAR>(a : α) → DecidableEq (N a)<VAR>(a : α) → AddGroup (N a)<VAR>f g : Π₀ (a : α), N a<GOAL>(f + g).neLocus f = g.support
<VAR>α : Type u_1<VAR>N : α → Type u_2<VAR>DecidableEq α<VAR>(a : α) → DecidableEq (N a)<VAR>(a : α) → AddGroup (N a)<VAR>f g : Π₀ (a : α), N a<GOAL>f.neLocus (f - g) = g.support
<VAR>α : Type u_1<VAR>N : α → Type u_2<VAR>DecidableEq α<VAR>(a : α) → DecidableEq (N a)<VAR>(a : α) → AddGroup (N a)<VAR>f g : Π₀ (a : α), N a<GOAL>(f - g).neLocus f = g.support
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r s : Rel α β<GOAL>(∀ (a : α), r a = s a) → r = s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : Rel α β<VAR>x : α<VAR>y : β<GOAL>r.inv y x ↔ r x y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : Rel α β<GOAL>r.inv.inv = r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r s : Rel α β<VAR>h : r ≤ s<GOAL>r.dom ⊆ s.dom
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : Rel α β<GOAL>r.inv.codom = r.dom
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : Rel α β<GOAL>r.inv.dom = r.codom
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>r : Rel α β<VAR>s : Rel β γ<VAR>t : Rel γ δ<GOAL>(r.comp s).comp t = r.comp (s.comp t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : Rel α β<GOAL>r.comp Eq = r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : Rel α β<GOAL>Rel.comp Eq r = r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : Rel α β<GOAL>r.comp ⊥ = ⊥
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : Rel α β<GOAL>⊥.comp r = ⊥
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : Rel α β<GOAL>r.comp ⊤ = fun x x_1 => x ∈ r.dom
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : Rel α β<GOAL>⊤.comp r = fun x y => y ∈ r.codom
<VAR>α : Type u_1<GOAL>Rel.inv Eq = Eq
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : Rel α β<VAR>s : Rel β γ<GOAL>(r.comp s).inv = s.inv.comp r.inv
<VAR>α : Type u_1<VAR>β : Type u_2<GOAL>⊥.inv = ⊥
<VAR>α : Type u_1<VAR>β : Type u_2<GOAL>⊤.inv = ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : Rel α β<VAR>y : β<VAR>s : Set α<GOAL>y ∈ r.image s ↔ ∃ x ∈ s, r x y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : Rel α β<GOAL>((fun x x_1 => x ⊆ x_1) ⇒ fun x x_1 => x ⊆ x_1) r.image r.image
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : Rel α β<GOAL>Monotone r.image
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : Rel α β<VAR>s t : Set α<GOAL>r.image (s ∩ t) ⊆ r.image s ∩ r.image t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : Rel α β<VAR>s t : Set α<GOAL>r.image (s ∪ t) = r.image s ∪ r.image t
<VAR>α : Type u_1<VAR>s : Set α<GOAL>Rel.image Eq s = s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : Rel α β<VAR>s : Rel β γ<VAR>t : Set α<GOAL>(r.comp s).image t = s.image (r.image t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : Rel α β<GOAL>r.image Set.univ = r.codom
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : Rel α β<GOAL>r.image ∅ = ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<GOAL>⊥.image s = ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>h : s.Nonempty<GOAL>⊤.image s = Set.univ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : Rel α β<VAR>x : α<VAR>s : Set β<GOAL>x ∈ r.preimage s ↔ ∃ y ∈ s, r x y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : Rel α β<VAR>s : Set β<GOAL>r.preimage s = {x | ∃ y ∈ s, r x y}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : Rel α β<VAR>s t : Set β<VAR>h : s ⊆ t<GOAL>r.preimage s ⊆ r.preimage t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : Rel α β<VAR>s t : Set β<GOAL>r.preimage (s ∩ t) ⊆ r.preimage s ∩ r.preimage t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : Rel α β<VAR>s t : Set β<GOAL>r.preimage (s ∪ t) = r.preimage s ∪ r.preimage t
<VAR>α : Type u_1<VAR>s : Set α<GOAL>Rel.preimage Eq s = s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : Rel α β<VAR>s : Rel β γ<VAR>t : Set γ<GOAL>(r.comp s).preimage t = r.preimage (s.preimage t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : Rel α β<GOAL>r.preimage Set.univ = r.dom
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : Rel α β<GOAL>r.preimage ∅ = ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : Rel α β<VAR>s : Set α<GOAL>r.inv.preimage s = r.image s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set β<GOAL>⊥.preimage s = ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set β<VAR>h : s.Nonempty<GOAL>⊤.preimage s = Set.univ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : Rel α β<VAR>s : Set β<VAR>h : r.codom ⊆ s<GOAL>r.preimage s = r.dom
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : Rel α β<VAR>s : Set α<VAR>h : r.dom ⊆ s<GOAL>r.image s = r.codom
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : Rel α β<VAR>s : Set α<GOAL>r.image (s ∩ r.dom) = r.image s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : Rel α β<VAR>s : Set β<GOAL>r.preimage (s ∩ r.codom) = r.preimage s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : Rel α β<VAR>s : Set α<GOAL>s ∩ r.dom ⊆ r.preimage (r.image s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : Rel α β<VAR>s : Set β<GOAL>s ∩ r.codom ⊆ r.image (r.preimage s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : Rel α β<VAR>x : α<VAR>s : Set β<GOAL>x ∈ r.core s ↔ ∀ (y : β), r x y → y ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : Rel α β<GOAL>((fun x x_1 => x ⊆ x_1) ⇒ fun x x_1 => x ⊆ x_1) r.core r.core
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : Rel α β<GOAL>Monotone r.core
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : Rel α β<VAR>s t : Set β<GOAL>r.core (s ∩ t) = r.core s ∩ r.core t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : Rel α β<VAR>s t : Set β<GOAL>r.core s ∪ r.core t ⊆ r.core (s ∪ t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : Rel α β<GOAL>r.core Set.univ = Set.univ
<VAR>α : Type u_1<VAR>s : Set α<GOAL>Rel.core Eq s = s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : Rel α β<VAR>s : Rel β γ<VAR>t : Set γ<GOAL>(r.comp s).core t = r.core (s.core t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : Rel α β<VAR>s : Set α<VAR>t : Set β<GOAL>r.image s ⊆ t ↔ s ⊆ r.core t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : Rel α β<GOAL>GaloisConnection r.image r.core
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>x : α<VAR>y : β<GOAL>Function.graph f x y ↔ f x = y
<VAR>α : Type u_1<VAR>β : Type u_2<GOAL>Function.Injective Function.graph
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f g : α → β<GOAL>Function.graph f = Function.graph g ↔ f = g
<VAR>α : Type u_1<GOAL>Function.graph id = Eq
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : β → γ<VAR>g : α → β<GOAL>Function.graph (f ∘ g) = (Function.graph g).comp (Function.graph f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α ≃ β<GOAL>Function.graph ⇑f.symm = (Function.graph ⇑f).inv
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : Rel α β<GOAL>(∃! f, Function.graph f = r) ↔ ∀ (x : α), ∃! y, r x y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s : Set α<GOAL>f '' s = (Function.graph f).image s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s : Set β<GOAL>f ⁻¹' s = (Function.graph f).preimage s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s : Set β<GOAL>f ⁻¹' s = (Function.graph f).core s
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>DecidableEq ι<VAR>(i : ι) → Zero (α i)<VAR>s : Finset ι<VAR>t : (i : ι) → Finset (α i)<GOAL>(s.dfinsupp t).card = ∏ i ∈ s, (t i).card
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>DecidableEq ι<VAR>(i : ι) → Zero (α i)<VAR>s : Finset ι<VAR>f : Π₀ (i : ι), α i<VAR>t : (i : ι) → Finset (α i)<VAR>(i : ι) → DecidableEq (α i)<GOAL>f ∈ s.dfinsupp t ↔ f.support ⊆ s ∧ ∀ i ∈ s, f i ∈ t i