ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>CanonicallyOrderedAddCommMonoid α<VAR>f g : ι →₀ α<GOAL>f ≤ g ↔ ∀ i ∈ f.support, f i ≤ g i
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>CanonicallyOrderedAddCommMonoid α<GOAL>Monotone Finsupp.support
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>CanonicallyOrderedAddCommMonoid α<VAR>f g : ι →₀ α<VAR>hfg : f ≤ g<GOAL>f.support ⊆ g.support
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>CanonicallyOrderedAddCommMonoid α<VAR>i : ι<VAR>x : α<VAR>f : ι →₀ α<GOAL>Finsupp.single i x ≤ f ↔ x ≤ f i
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>CanonicallyOrderedAddCommMonoid α<VAR>Sub α<VAR>OrderedSub α<VAR>f g : ι →₀ α<GOAL>⇑(f - g) = ⇑f - ⇑g
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>CanonicallyOrderedAddCommMonoid α<VAR>Sub α<VAR>OrderedSub α<VAR>f g : ι →₀ α<VAR>a : ι<GOAL>(f - g) a = f a - g a
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>CanonicallyOrderedAddCommMonoid α<VAR>Sub α<VAR>OrderedSub α<VAR>i : ι<VAR>a b : α<GOAL>Finsupp.single i (a - b) = Finsupp.single i a - Finsupp.single i b
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>CanonicallyOrderedAddCommMonoid α<VAR>Sub α<VAR>OrderedSub α<VAR>f1 f2 : ι →₀ α<GOAL>(f1 - f2).support ⊆ f1.support
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>CanonicallyOrderedAddCommMonoid α<VAR>Sub α<VAR>OrderedSub α<VAR>DecidableEq ι<VAR>f1 f2 : ι →₀ α<GOAL>f1.support \ f2.support ⊆ (f1 - f2).support
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>CanonicallyLinearOrderedAddCommMonoid α<VAR>DecidableEq ι<VAR>f g : ι →₀ α<GOAL>(f ⊓ g).support = f.support ∩ g.support
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>CanonicallyLinearOrderedAddCommMonoid α<VAR>DecidableEq ι<VAR>f g : ι →₀ α<GOAL>(f ⊔ g).support = f.support ∪ g.support
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>CanonicallyLinearOrderedAddCommMonoid α<VAR>f g : ι →₀ α<GOAL>Disjoint f g ↔ Disjoint f.support g.support
<VAR>ι : Type u_1<VAR>a : ι<VAR>u u' : ι →₀ ℕ<VAR>h : u a ≠ 0<GOAL>u - Finsupp.single a 1 + u' = u + u' - Finsupp.single a 1
<VAR>ι : Type u_1<VAR>a : ι<VAR>u u' : ι →₀ ℕ<VAR>h : u' a ≠ 0<GOAL>u + (u' - Finsupp.single a 1) = u + u' - Finsupp.single a 1
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>Fintype ι<VAR>DecidableEq ι<VAR>(i : ι) → DecidableEq (α i)<VAR>(i : ι) → PartialOrder (α i)<VAR>(i : ι) → LocallyFiniteOrder (α i)<VAR>a b : (i : ι) → α i<GOAL>Finset.Icc a b = Fintype.piFinset fun i => Finset.Icc (a i) (b i)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>Fintype ι<VAR>DecidableEq ι<VAR>(i : ι) → DecidableEq (α i)<VAR>(i : ι) → PartialOrder (α i)<VAR>(i : ι) → LocallyFiniteOrder (α i)<VAR>a b : (i : ι) → α i<GOAL>(Finset.Icc a b).card = ∏ i : ι, (Finset.Icc (a i) (b i)).card
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>Fintype ι<VAR>DecidableEq ι<VAR>(i : ι) → DecidableEq (α i)<VAR>(i : ι) → PartialOrder (α i)<VAR>(i : ι) → LocallyFiniteOrder (α i)<VAR>a b : (i : ι) → α i<GOAL>(Finset.Ico a b).card = ∏ i : ι, (Finset.Icc (a i) (b i)).card - 1
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>Fintype ι<VAR>DecidableEq ι<VAR>(i : ι) → DecidableEq (α i)<VAR>(i : ι) → PartialOrder (α i)<VAR>(i : ι) → LocallyFiniteOrder (α i)<VAR>a b : (i : ι) → α i<GOAL>(Finset.Ioc a b).card = ∏ i : ι, (Finset.Icc (a i) (b i)).card - 1
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>Fintype ι<VAR>DecidableEq ι<VAR>(i : ι) → DecidableEq (α i)<VAR>(i : ι) → PartialOrder (α i)<VAR>(i : ι) → LocallyFiniteOrder (α i)<VAR>a b : (i : ι) → α i<GOAL>(Finset.Ioo a b).card = ∏ i : ι, (Finset.Icc (a i) (b i)).card - 2
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>Fintype ι<VAR>DecidableEq ι<VAR>(i : ι) → DecidableEq (α i)<VAR>(i : ι) → PartialOrder (α i)<VAR>(i : ι) → LocallyFiniteOrderBot (α i)<VAR>b : (i : ι) → α i<GOAL>(Finset.Iic b).card = ∏ i : ι, (Finset.Iic (b i)).card
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>Fintype ι<VAR>DecidableEq ι<VAR>(i : ι) → DecidableEq (α i)<VAR>(i : ι) → PartialOrder (α i)<VAR>(i : ι) → LocallyFiniteOrderBot (α i)<VAR>b : (i : ι) → α i<GOAL>(Finset.Iio b).card = ∏ i : ι, (Finset.Iic (b i)).card - 1
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>Fintype ι<VAR>DecidableEq ι<VAR>(i : ι) → DecidableEq (α i)<VAR>(i : ι) → PartialOrder (α i)<VAR>(i : ι) → LocallyFiniteOrderTop (α i)<VAR>a : (i : ι) → α i<GOAL>(Finset.Ici a).card = ∏ i : ι, (Finset.Ici (a i)).card
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>Fintype ι<VAR>DecidableEq ι<VAR>(i : ι) → DecidableEq (α i)<VAR>(i : ι) → PartialOrder (α i)<VAR>(i : ι) → LocallyFiniteOrderTop (α i)<VAR>a : (i : ι) → α i<GOAL>(Finset.Ioi a).card = ∏ i : ι, (Finset.Ici (a i)).card - 1
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>Fintype ι<VAR>DecidableEq ι<VAR>(i : ι) → DecidableEq (α i)<VAR>(i : ι) → Lattice (α i)<VAR>(i : ι) → LocallyFiniteOrder (α i)<VAR>a b : (i : ι) → α i<GOAL>Finset.uIcc a b = Fintype.piFinset fun i => Finset.uIcc (a i) (b i)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>Fintype ι<VAR>DecidableEq ι<VAR>(i : ι) → DecidableEq (α i)<VAR>(i : ι) → Lattice (α i)<VAR>(i : ι) → LocallyFiniteOrder (α i)<VAR>a b : (i : ι) → α i<GOAL>(Finset.uIcc a b).card = ∏ i : ι, (Finset.uIcc (a i) (b i)).card
<VAR>α : Type u₁<VAR>β : Type u₂<VAR>MulZeroClass β<VAR>g₁ g₂ : α →₀ β<GOAL>⇑(g₁ * g₂) = ⇑g₁ * ⇑g₂
<VAR>α : Type u₁<VAR>β : Type u₂<VAR>MulZeroClass β<VAR>g₁ g₂ : α →₀ β<VAR>a : α<GOAL>(g₁ * g₂) a = g₁ a * g₂ a
<VAR>α : Type u₁<VAR>β : Type u₂<VAR>MulZeroClass β<VAR>a : α<VAR>b₁ b₂ : β<GOAL>Finsupp.single a (b₁ * b₂) = Finsupp.single a b₁ * Finsupp.single a b₂
<VAR>α : Type u₁<VAR>β : Type u₂<VAR>MulZeroClass β<VAR>DecidableEq α<VAR>g₁ g₂ : α →₀ β<GOAL>(g₁ * g₂).support ⊆ g₁.support ∩ g₂.support
<VAR>α : Type u₁<VAR>β : Type u₂<VAR>Semiring β<VAR>f : α → β<VAR>g : α →₀ β<GOAL>⇑(f • g) = f • ⇑g
<VAR>α : Type u_1<VAR>N : Type u_2<VAR>Zero N<VAR>r : α → α → Prop<VAR>s : N → N → Prop<VAR>a b : α →₀ N<GOAL>Pi.Lex r (fun {i} => s) ⇑a ⇑b = Finsupp.Lex r s a b
<VAR>α : Type u_1<VAR>N : Type u_2<VAR>Zero N<VAR>r : α → α → Prop<VAR>s : N → N → Prop<VAR>a b : α →₀ N<GOAL>Finsupp.Lex r s a b ↔ ∃ j, (∀ (d : α), r d j → a d = b d) ∧ s (a j) (b j)
<VAR>α : Type u_1<VAR>N : Type u_2<VAR>Zero N<VAR>r : α → α → Prop<VAR>s : N → N → Prop<GOAL>Finsupp.Lex r s = InvImage (DFinsupp.Lex r fun x => s) Finsupp.toDFinsupp
<VAR>α : Type u_1<VAR>N : Type u_2<VAR>Zero N<VAR>Preorder N<VAR>r : α → α → Prop<VAR>IsStrictOrder α r<VAR>x y : α →₀ N<VAR>hlt : x < y<GOAL>∃ i, (∀ (j : α), r j i → x j ≤ y j ∧ y j ≤ x j) ∧ x i < y i
<VAR>α : Type u_1<VAR>N : Type u_2<VAR>Zero N<VAR>PartialOrder N<VAR>r : α → α → Prop<VAR>IsStrictOrder α r<VAR>x y : α →₀ N<VAR>hlt : x < y<GOAL>Pi.Lex r (fun {i} x x_1 => x < x_1) ⇑x ⇑y
<VAR>α : Type u_1<VAR>N : Type u_2<VAR>Zero N<VAR>LinearOrder α<VAR>PartialOrder N<GOAL>Monotone ⇑toLex
<VAR>α : Type u_1<VAR>N : Type u_2<VAR>Zero N<VAR>LinearOrder α<VAR>PartialOrder N<VAR>a b : Lex (α →₀ N)<VAR>i : α<GOAL>(∀ j < i, (ofLex a) j = (ofLex b) j) → (ofLex a) i < (ofLex b) i → a < b
<VAR>α : Type u_1<VAR>DivisionRing α<VAR>n : ℕ<GOAL>↑(↑n)⁻¹ = (↑n)⁻¹
<VAR>α : Type u_1<VAR>DivisionRing α<VAR>n : ℤ<GOAL>↑(↑n)⁻¹ = (↑n)⁻¹
<VAR>K : Type u_2<VAR>DivisionRing K<VAR>q : ℚ≥0<GOAL>↑↑q = ↑q
<VAR>K : Type u_2<VAR>DivisionRing K<VAR>m : ℕ<VAR>s : Bool<VAR>e : ℕ<GOAL>↑(OfScientific.ofScientific m s e) = OfScientific.ofScientific m s e
<VAR>K : Type u_1<VAR>DivisionSemiring K<VAR>q : ℚ≥0<VAR>n : ℕ<GOAL>↑(q ^ n) = ↑q ^ n
<VAR>K : Type u_1<VAR>DivisionSemiring K<VAR>q : ℚ≥0<VAR>z : ℤ<VAR>hq : ↑q.num ≠ 0<GOAL>↑(q ^ z) = ↑q ^ z
<VAR>K : Type u_1<VAR>LinearOrderedField K<VAR>m : ℕ<VAR>s : Bool<VAR>e : ℕ<GOAL>↑(OfScientific.ofScientific m s e) = OfScientific.ofScientific m s e
<VAR>α : Type u_2<VAR>DivisionRing α<VAR>CharZero α<VAR>s : List ℚ<GOAL>↑s.sum = (List.map Rat.cast s).sum
<VAR>α : Type u_2<VAR>DivisionRing α<VAR>CharZero α<VAR>s : Multiset ℚ<GOAL>↑s.sum = (Multiset.map Rat.cast s).sum
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>DivisionRing α<VAR>CharZero α<VAR>s : Finset ι<VAR>f : ι → ℚ<GOAL>↑(∑ i ∈ s, f i) = ∑ i ∈ s, ↑(f i)
<VAR>α : Type u_2<VAR>DivisionRing α<VAR>CharZero α<VAR>s : List ℚ<GOAL>↑s.prod = (List.map Rat.cast s).prod
<VAR>α : Type u_2<VAR>Field α<VAR>CharZero α<VAR>s : Multiset ℚ<GOAL>↑s.prod = (Multiset.map Rat.cast s).prod
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>Field α<VAR>CharZero α<VAR>s : Finset ι<VAR>f : ι → ℚ<GOAL>↑(∏ i ∈ s, f i) = ∏ i ∈ s, ↑(f i)
<VAR>q : ℚ<VAR>hq : 0 ≤ q<GOAL>NNRat.num ⟨q, hq⟩ = q.num.natAbs
<VAR>q : ℚ<VAR>hq : 0 ≤ q<GOAL>NNRat.den ⟨q, hq⟩ = q.den
<VAR>n : ℚ≥0<GOAL>↑n = n
<VAR>α : Type u_3<VAR>DivisionRing α<VAR>CharZero α<VAR>m n : ℚ<GOAL>↑m = ↑n ↔ m = n
<VAR>α : Type u_3<VAR>DivisionRing α<VAR>CharZero α<GOAL>Function.Injective Rat.cast
<VAR>α : Type u_3<VAR>DivisionRing α<VAR>CharZero α<VAR>n : ℚ<GOAL>↑n = 0 ↔ n = 0
<VAR>α : Type u_3<VAR>DivisionRing α<VAR>CharZero α<VAR>n : ℚ<GOAL>↑n ≠ 0 ↔ n ≠ 0
<VAR>α : Type u_3<VAR>DivisionRing α<VAR>CharZero α<VAR>m n : ℚ<GOAL>↑(m + n) = ↑m + ↑n
<VAR>α : Type u_3<VAR>DivisionRing α<VAR>CharZero α<VAR>m n : ℚ<GOAL>↑(m - n) = ↑m - ↑n
<VAR>α : Type u_3<VAR>DivisionRing α<VAR>CharZero α<VAR>m n : ℚ<GOAL>↑(m * n) = ↑m * ↑n
<VAR>α : Type u_3<VAR>DivisionRing α<VAR>CharZero α<GOAL>⇑(Rat.castHom α) = Rat.cast
<VAR>α : Type u_3<VAR>DivisionRing α<VAR>CharZero α<VAR>n : ℚ<GOAL>↑n⁻¹ = (↑n)⁻¹
<VAR>α : Type u_3<VAR>DivisionRing α<VAR>CharZero α<VAR>m n : ℚ<GOAL>↑(m / n) = ↑m / ↑n
<VAR>α : Type u_3<VAR>DivisionRing α<VAR>CharZero α<VAR>q : ℚ<VAR>n : ℤ<GOAL>↑(q ^ n) = ↑q ^ n
<VAR>α : Type u_3<VAR>DivisionRing α<VAR>CharZero α<VAR>a b : ℤ<GOAL>↑(Rat.divInt a b) = ↑a / ↑b
<VAR>α : Type u_3<VAR>DivisionRing α<VAR>CharZero α<VAR>q : ℚ<VAR>k : ℕ<GOAL>↑(q ^ k) = ↑q ^ k
<VAR>q : ℚ<GOAL>Rat.sqrt (q * q) = |q|
<VAR>x : ℚ<GOAL>(∃ q, q * q = x) ↔ Rat.sqrt x * Rat.sqrt x = x
<VAR>q : ℚ<GOAL>0 ≤ Rat.sqrt q
<VAR>z : ℤ<GOAL>Rat.sqrt ↑z = ↑(Int.sqrt z)
<VAR>n : ℕ<GOAL>Rat.sqrt ↑n = ↑n.sqrt
<VAR>n : ℕ<GOAL>Rat.sqrt (OfNat.ofNat n) = ↑(Nat.sqrt (OfNat.ofNat n))
<GOAL>Rat.castHom ℚ = RingHom.id ℚ
<VAR>q : ℚ<VAR>K : Type u_5<VAR>LinearOrderedField K<VAR>hq : 0 < q<GOAL>0 < ↑q
<VAR>K : Type u_5<VAR>LinearOrderedField K<GOAL>StrictMono Rat.cast
<VAR>K : Type u_5<VAR>LinearOrderedField K<GOAL>Monotone Rat.cast
<VAR>K : Type u_5<VAR>LinearOrderedField K<GOAL>∀ (a : ℚ), Rat.castOrderEmbedding a = ↑a
<VAR>p q : ℚ<VAR>K : Type u_5<VAR>LinearOrderedField K<GOAL>↑p ≤ ↑q ↔ p ≤ q
<VAR>p q : ℚ<VAR>K : Type u_5<VAR>LinearOrderedField K<GOAL>↑p < ↑q ↔ p < q
<VAR>q : ℚ<VAR>K : Type u_5<VAR>LinearOrderedField K<GOAL>0 ≤ ↑q ↔ 0 ≤ q
<VAR>q : ℚ<VAR>K : Type u_5<VAR>LinearOrderedField K<GOAL>↑q ≤ 0 ↔ q ≤ 0
<VAR>q : ℚ<VAR>K : Type u_5<VAR>LinearOrderedField K<GOAL>0 < ↑q ↔ 0 < q
<VAR>q : ℚ<VAR>K : Type u_5<VAR>LinearOrderedField K<GOAL>↑q < 0 ↔ q < 0
<VAR>K : Type u_5<VAR>LinearOrderedField K<VAR>p q : ℚ<GOAL>↑(min p q) = min ↑p ↑q
<VAR>K : Type u_5<VAR>LinearOrderedField K<VAR>p q : ℚ<GOAL>↑(max p q) = max ↑p ↑q
<VAR>K : Type u_5<VAR>LinearOrderedField K<VAR>q : ℚ<GOAL>↑|q| = |↑q|
<VAR>K : Type u_5<VAR>LinearOrderedField K<VAR>p q : ℚ<GOAL>Rat.cast ⁻¹' Set.Icc ↑p ↑q = Set.Icc p q
<VAR>K : Type u_5<VAR>LinearOrderedField K<VAR>p q : ℚ<GOAL>Rat.cast ⁻¹' Set.Ico ↑p ↑q = Set.Ico p q
<VAR>K : Type u_5<VAR>LinearOrderedField K<VAR>p q : ℚ<GOAL>Rat.cast ⁻¹' Set.Ioc ↑p ↑q = Set.Ioc p q
<VAR>K : Type u_5<VAR>LinearOrderedField K<VAR>p q : ℚ<GOAL>Rat.cast ⁻¹' Set.Ioo ↑p ↑q = Set.Ioo p q
<VAR>K : Type u_5<VAR>LinearOrderedField K<VAR>q : ℚ<GOAL>Rat.cast ⁻¹' Set.Ici ↑q = Set.Ici q
<VAR>K : Type u_5<VAR>LinearOrderedField K<VAR>q : ℚ<GOAL>Rat.cast ⁻¹' Set.Iic ↑q = Set.Iic q
<VAR>K : Type u_5<VAR>LinearOrderedField K<VAR>q : ℚ<GOAL>Rat.cast ⁻¹' Set.Ioi ↑q = Set.Ioi q
<VAR>K : Type u_5<VAR>LinearOrderedField K<VAR>q : ℚ<GOAL>Rat.cast ⁻¹' Set.Iio ↑q = Set.Iio q
<VAR>K : Type u_5<VAR>LinearOrderedField K<VAR>p q : ℚ<GOAL>Rat.cast ⁻¹' Set.uIcc ↑p ↑q = Set.uIcc p q
<VAR>K : Type u_5<VAR>LinearOrderedField K<VAR>p q : ℚ<GOAL>Rat.cast ⁻¹' Ι ↑p ↑q = Ι p q
<VAR>K : Type u_5<VAR>LinearOrderedSemifield K<GOAL>StrictMono NNRat.cast
<VAR>K : Type u_5<VAR>LinearOrderedSemifield K<GOAL>Monotone NNRat.cast
<VAR>K : Type u_5<VAR>LinearOrderedSemifield K<GOAL>∀ (a : ℚ≥0), NNRat.castOrderEmbedding a = ↑a
<VAR>K : Type u_5<VAR>LinearOrderedSemifield K<VAR>p q : ℚ≥0<GOAL>↑p ≤ ↑q ↔ p ≤ q
<VAR>K : Type u_5<VAR>LinearOrderedSemifield K<VAR>p q : ℚ≥0<GOAL>↑p < ↑q ↔ p < q
<VAR>K : Type u_5<VAR>LinearOrderedSemifield K<VAR>q : ℚ≥0<GOAL>↑q ≤ 0 ↔ q ≤ 0
<VAR>K : Type u_5<VAR>LinearOrderedSemifield K<VAR>q : ℚ≥0<GOAL>0 < ↑q ↔ 0 < q
<VAR>K : Type u_5<VAR>LinearOrderedSemifield K<VAR>q : ℚ≥0<GOAL>↑q < 0 ↔ q < 0
<VAR>K : Type u_5<VAR>LinearOrderedSemifield K<VAR>q : ℚ≥0<GOAL>¬↑q < 0
<VAR>K : Type u_5<VAR>LinearOrderedSemifield K<VAR>p q : ℚ≥0<GOAL>↑(min p q) = min ↑p ↑q
<VAR>K : Type u_5<VAR>LinearOrderedSemifield K<VAR>p q : ℚ≥0<GOAL>↑(max p q) = max ↑p ↑q
<VAR>K : Type u_5<VAR>LinearOrderedSemifield K<VAR>p q : ℚ≥0<GOAL>NNRat.cast ⁻¹' Set.Icc ↑p ↑q = Set.Icc p q
<VAR>K : Type u_5<VAR>LinearOrderedSemifield K<VAR>p q : ℚ≥0<GOAL>NNRat.cast ⁻¹' Set.Ico ↑p ↑q = Set.Ico p q
<VAR>K : Type u_5<VAR>LinearOrderedSemifield K<VAR>p q : ℚ≥0<GOAL>NNRat.cast ⁻¹' Set.Ioc ↑p ↑q = Set.Ioc p q
<VAR>K : Type u_5<VAR>LinearOrderedSemifield K<VAR>p q : ℚ≥0<GOAL>NNRat.cast ⁻¹' Set.Ioo ↑p ↑q = Set.Ioo p q
<VAR>K : Type u_5<VAR>LinearOrderedSemifield K<VAR>p : ℚ≥0<GOAL>NNRat.cast ⁻¹' Set.Ici ↑p = Set.Ici p
<VAR>K : Type u_5<VAR>LinearOrderedSemifield K<VAR>p : ℚ≥0<GOAL>NNRat.cast ⁻¹' Set.Iic ↑p = Set.Iic p
<VAR>K : Type u_5<VAR>LinearOrderedSemifield K<VAR>p : ℚ≥0<GOAL>NNRat.cast ⁻¹' Set.Ioi ↑p = Set.Ioi p
<VAR>K : Type u_5<VAR>LinearOrderedSemifield K<VAR>p : ℚ≥0<GOAL>NNRat.cast ⁻¹' Set.Iio ↑p = Set.Iio p
<VAR>K : Type u_5<VAR>LinearOrderedSemifield K<VAR>p q : ℚ≥0<GOAL>NNRat.cast ⁻¹' Set.uIcc ↑p ↑q = Set.uIcc p q
<VAR>K : Type u_5<VAR>LinearOrderedSemifield K<VAR>p q : ℚ≥0<GOAL>NNRat.cast ⁻¹' Ι ↑p ↑q = Ι p q
<VAR>α : Type u<VAR>s : Stream'.Seq α<VAR>x : α<GOAL>↑(Stream'.Seq.cons x s) = Stream'.cons (some x) ↑s
<VAR>α : Type u<VAR>f : Stream' (Option α)<VAR>hf : f.IsSeq<GOAL>Stream'.Seq.get? ⟨f, hf⟩ = f
<VAR>α : Type u<VAR>n : ℕ<GOAL>Stream'.Seq.nil.get? n = none
<VAR>α : Type u<VAR>a : α<VAR>s : Stream'.Seq α<GOAL>(Stream'.Seq.cons a s).get? 0 = some a
<VAR>α : Type u<VAR>a : α<VAR>s : Stream'.Seq α<VAR>n : ℕ<GOAL>(Stream'.Seq.cons a s).get? (n + 1) = s.get? n
<VAR>α : Type u<VAR>s t : Stream'.Seq α<VAR>h : ∀ (n : ℕ), s.get? n = t.get? n<GOAL>s = t
<VAR>α : Type u<GOAL>Function.Injective2 Stream'.Seq.cons
<VAR>α : Type u<VAR>s : Stream'.Seq α<GOAL>Function.Injective fun x => Stream'.Seq.cons x s
<VAR>α : Type u<VAR>x : α<GOAL>Function.Injective (Stream'.Seq.cons x)
<VAR>α : Type u<VAR>s : Stream'.Seq α<GOAL>¬s.Terminates ↔ ∀ (n : ℕ), (s.get? n).isSome = true
<VAR>α : Type u<VAR>s : Stream'.Seq α<VAR>m n : ℕ<VAR>h : m ≤ n<GOAL>s.get? m = none → s.get? n = none
<VAR>α : Type u<VAR>s : Stream'.Seq α<VAR>m n : ℕ<GOAL>m ≤ n → s.TerminatedAt m → s.TerminatedAt n
<VAR>α : Type u<VAR>s : Stream'.Seq α<VAR>aₙ : α<VAR>n m : ℕ<VAR>m_le_n : m ≤ n<VAR>s_nth_eq_some : s.get? n = some aₙ<GOAL>∃ aₘ, s.get? m = some aₘ
<VAR>α : Type u<VAR>a : α<GOAL>¬a ∈ Stream'.Seq.nil
<VAR>α : Type u<VAR>a : α<VAR>s : Stream'.Seq α<GOAL>a ∈ Stream'.Seq.cons a s
<VAR>α : Type u<VAR>y : α<VAR>a : α<VAR>s : Stream'.Seq α<GOAL>a ∈ s → a ∈ Stream'.Seq.cons y s
<VAR>α : Type u<VAR>a b : α<VAR>s : Stream'.Seq α<GOAL>a ∈ Stream'.Seq.cons b s → a = b ∨ a ∈ s
<VAR>α : Type u<VAR>a b : α<VAR>s : Stream'.Seq α<GOAL>a ∈ Stream'.Seq.cons b s ↔ a = b ∨ a ∈ s
<VAR>α : Type u<VAR>s : Stream'.Seq α<GOAL>s.destruct = none → s = Stream'.Seq.nil
<VAR>α : Type u<VAR>s : Stream'.Seq α<VAR>a : α<VAR>s' : Stream'.Seq α<GOAL>s.destruct = some (a, s') → s = Stream'.Seq.cons a s'
<VAR>α : Type u<GOAL>Stream'.Seq.nil.destruct = none
<VAR>α : Type u<VAR>a : α<VAR>s : Stream'.Seq α<GOAL>(Stream'.Seq.cons a s).destruct = some (a, s)
<VAR>α : Type u<VAR>s : Stream'.Seq α<GOAL>s.head = Prod.fst <$> s.destruct
<VAR>α : Type u<GOAL>Stream'.Seq.nil.head = none
<VAR>α : Type u<VAR>a : α<VAR>s : Stream'.Seq α<GOAL>(Stream'.Seq.cons a s).head = some a
<VAR>α : Type u<GOAL>Stream'.Seq.nil.tail = Stream'.Seq.nil
<VAR>α : Type u<VAR>a : α<VAR>s : Stream'.Seq α<GOAL>(Stream'.Seq.cons a s).tail = s
<VAR>α : Type u<VAR>s : Stream'.Seq α<VAR>n : ℕ<GOAL>s.tail.get? n = s.get? (n + 1)
<VAR>α : Type u<VAR>C : Stream'.Seq α → Prop<VAR>a : α<VAR>s : Stream'.Seq α<VAR>M : a ∈ s<VAR>h1 : ∀ (b : α) (s' : Stream'.Seq α), a = b ∨ C s' → C (Stream'.Seq.cons b s')<GOAL>C s
<VAR>α : Type u<VAR>β : Type v<VAR>f : β → Option (α × β)<VAR>b : β<GOAL>(Stream'.Seq.corec f b).destruct = Stream'.Seq.omap (Stream'.Seq.corec f) (f b)
<VAR>α : Type u<VAR>R : Stream'.Seq α → Stream'.Seq α → Prop<VAR>bisim : Stream'.Seq.IsBisimulation R<VAR>s₁ s₂ : Stream'.Seq α<VAR>r : R s₁ s₂<GOAL>s₁ = s₂
<VAR>α : Type u<VAR>s₁ s₂ : Stream'.Seq α<GOAL>s₁.head = s₂.head → (∀ (β : Type u) (fr : Stream'.Seq α → β), fr s₁ = fr s₂ → fr s₁.tail = fr s₂.tail) → s₁ = s₂
<VAR>α : Type u<VAR>β : Type v<VAR>s : Stream'.Seq α<VAR>f g : Stream'.Seq α → Stream'.Seq β<VAR>H : ∀ (s : Stream'.Seq α), Stream'.Seq.BisimO (fun s1 s2 => ∃ s, s1 = f s ∧ s2 = g s) (f s).destruct (g s).destruct<GOAL>f s = g s
<VAR>α : Type u<GOAL>↑[] = Stream'.Seq.nil
<VAR>α : Type u<VAR>l : List α<VAR>n : ℕ<GOAL>(↑l).get? n = l.get? n
<VAR>α : Type u<VAR>a : α<VAR>l : List α<GOAL>↑(a :: l) = Stream'.Seq.cons a ↑l
<VAR>n : ℕ<GOAL>Stream'.Seq.nats.get? n = some n
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : α → β → γ<VAR>s : Stream'.Seq α<VAR>s' : Stream'.Seq β<VAR>n : ℕ<GOAL>(Stream'.Seq.zipWith f s s').get? n = Option.map₂ f (s.get? n) (s'.get? n)
<VAR>α : Type u<VAR>β : Type v<VAR>s : Stream'.Seq α<VAR>t : Stream'.Seq β<VAR>n : ℕ<GOAL>(s.zip t).get? n = Option.map₂ Prod.mk (s.get? n) (t.get? n)
<VAR>α : Type u<VAR>s : Stream'.Seq α<VAR>n : ℕ<GOAL>s.enum.get? n = Option.map (Prod.mk n) (s.get? n)
<VAR>α : Type u<GOAL>Stream'.Seq.nil.enum = Stream'.Seq.nil
<VAR>α : Type u<VAR>s : Stream'.Seq α<GOAL>Stream'.Seq.nil.append s = s
<VAR>α : Type u<VAR>a : α<VAR>s t : Stream'.Seq α<GOAL>(Stream'.Seq.cons a s).append t = Stream'.Seq.cons a (s.append t)
<VAR>α : Type u<VAR>s : Stream'.Seq α<GOAL>s.append Stream'.Seq.nil = s
<VAR>α : Type u<VAR>s t u : Stream'.Seq α<GOAL>(s.append t).append u = s.append (t.append u)
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<GOAL>Stream'.Seq.map f Stream'.Seq.nil = Stream'.Seq.nil
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>a : α<VAR>s : Stream'.Seq α<GOAL>Stream'.Seq.map f (Stream'.Seq.cons a s) = Stream'.Seq.cons (f a) (Stream'.Seq.map f s)
<VAR>α : Type u<VAR>s : Stream'.Seq α<GOAL>Stream'.Seq.map id s = s
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>s : Stream'.Seq α<GOAL>Stream'.Seq.map f s.tail = (Stream'.Seq.map f s).tail
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : α → β<VAR>g : β → γ<VAR>s : Stream'.Seq α<GOAL>Stream'.Seq.map (g ∘ f) s = Stream'.Seq.map g (Stream'.Seq.map f s)
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>s t : Stream'.Seq α<GOAL>Stream'.Seq.map f (s.append t) = (Stream'.Seq.map f s).append (Stream'.Seq.map f t)
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>s : Stream'.Seq α<VAR>n : ℕ<GOAL>(Stream'.Seq.map f s).get? n = Option.map f (s.get? n)
<VAR>α : Type u<GOAL>Stream'.Seq.nil.join = Stream'.Seq.nil
<VAR>α : Type u<VAR>a : α<VAR>S : Stream'.Seq (Stream'.Seq1 α)<GOAL>(Stream'.Seq.cons (a, Stream'.Seq.nil) S).join = Stream'.Seq.cons a S.join
<VAR>α : Type u<VAR>a b : α<VAR>s : Stream'.Seq α<VAR>S : Stream'.Seq (Stream'.Seq1 α)<GOAL>(Stream'.Seq.cons (a, Stream'.Seq.cons b s) S).join = Stream'.Seq.cons a (Stream'.Seq.cons (b, s) S).join
<VAR>α : Type u<VAR>a : α<VAR>s : Stream'.Seq α<VAR>S : Stream'.Seq (Stream'.Seq1 α)<GOAL>(Stream'.Seq.cons (a, s) S).join = Stream'.Seq.cons a (s.append S.join)
<VAR>α : Type u<VAR>S T : Stream'.Seq (Stream'.Seq1 α)<GOAL>(S.append T).join = S.join.append T.join
<VAR>α : Type u<VAR>a : α<VAR>s : Stream' α<GOAL>↑(Stream'.cons a s) = Stream'.Seq.cons a ↑s
<VAR>α : Type u<VAR>l l' : List α<GOAL>↑(l ++ l') = (↑l).append ↑l'
<VAR>α : Type u<VAR>l : List α<VAR>s : Stream' α<GOAL>↑(l ++ₛ s) = (↑l).append ↑s
<VAR>α : Type u<VAR>s : Stream'.Seq α<VAR>m n : ℕ<GOAL>s.drop (m + n) = (s.drop m).drop n
<VAR>α : Type u<VAR>s : Stream'.Seq α<VAR>n : ℕ<GOAL>s.tail.drop n = s.drop (n + 1)
<VAR>α : Type u<VAR>s : Stream'.Seq α<VAR>n : ℕ<GOAL>(s.drop n).head = s.get? n
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>a : α<VAR>s : Stream'.Seq α<GOAL>a ∈ s → f a ∈ Stream'.Seq.map f s
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>b : β<VAR>s : Stream'.Seq α<GOAL>b ∈ Stream'.Seq.map f s → ∃ a, a ∈ s ∧ f a = b
<VAR>α : Type u<VAR>s₁ s₂ : Stream'.Seq α<VAR>a : α<VAR>h : a ∈ s₁.append s₂<GOAL>a ∈ s₁ ∨ a ∈ s₂
<VAR>α : Type u<VAR>s₁ s₂ : Stream'.Seq α<VAR>a : α<VAR>h : a ∈ s₁<GOAL>a ∈ s₁.append s₂
<VAR>α : Type u<VAR>s : Stream'.Seq α<VAR>x : α<GOAL>(Stream'.Seq.cons x s).enum = Stream'.Seq.cons (0, x) (Stream'.Seq.map (Prod.map Nat.succ id) s.enum)
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>a : α<VAR>s : Stream'.Seq α<GOAL>Stream'.Seq1.map f (a, s) = (f a, Stream'.Seq.map f s)
<VAR>α : Type u<VAR>s : Stream'.Seq1 α<GOAL>Stream'.Seq1.map id s = s
<VAR>α : Type u<VAR>a : α<VAR>S : Stream'.Seq (Stream'.Seq1 α)<GOAL>Stream'.Seq1.join ((a, Stream'.Seq.nil), S) = (a, S.join)
<VAR>α : Type u<VAR>a b : α<VAR>s : Stream'.Seq α<VAR>S : Stream'.Seq (Stream'.Seq1 α)<GOAL>Stream'.Seq1.join ((a, Stream'.Seq.cons b s), S) = (a, (Stream'.Seq.cons (b, s) S).join)
<VAR>α : Type u<VAR>s : Stream'.Seq α<GOAL>(Stream'.Seq.map Stream'.Seq1.ret s).join = s
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>s : Stream'.Seq1 α<GOAL>s.bind (Stream'.Seq1.ret ∘ f) = Stream'.Seq1.map f s
<VAR>α : Type u<VAR>β : Type v<VAR>a : α<VAR>f : α → Stream'.Seq1 β<GOAL>(Stream'.Seq1.ret a).bind f = f a
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>S : Stream'.Seq (Stream'.Seq1 α)<GOAL>Stream'.Seq.map f S.join = (Stream'.Seq.map (Stream'.Seq1.map f) S).join
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>S : Stream'.Seq1 (Stream'.Seq1 α)<GOAL>Stream'.Seq1.map f S.join = (Stream'.Seq1.map (Stream'.Seq1.map f) S).join
<VAR>α : Type u<VAR>SS : Stream'.Seq (Stream'.Seq1 (Stream'.Seq1 α))<GOAL>SS.join.join = (Stream'.Seq.map Stream'.Seq1.join SS).join
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : Stream'.Seq1 α<VAR>f : α → Stream'.Seq1 β<VAR>g : β → Stream'.Seq1 γ<GOAL>(s.bind f).bind g = s.bind fun x => (f x).bind g
<VAR>α : Type u_1<GOAL>Finsupp.toMultiset 0 = 0
<VAR>α : Type u_1<VAR>m n : α →₀ ℕ<GOAL>Finsupp.toMultiset (m + n) = Finsupp.toMultiset m + Finsupp.toMultiset n
<VAR>α : Type u_1<VAR>f : α →₀ ℕ<GOAL>Finsupp.toMultiset f = f.sum fun a n => n • {a}
<VAR>α : Type u_1<VAR>a : α<VAR>n : ℕ<GOAL>Finsupp.toMultiset (Finsupp.single a n) = n • {a}
<VAR>α : Type u_1<VAR>ι : Type u_3<VAR>f : ι → α →₀ ℕ<VAR>s : Finset ι<GOAL>Finsupp.toMultiset (∑ i ∈ s, f i) = ∑ i ∈ s, Finsupp.toMultiset (f i)
<VAR>ι : Type u_3<VAR>s : Finset ι<VAR>n : ℕ<GOAL>Finsupp.toMultiset (∑ i ∈ s, Finsupp.single i n) = n • s.val
<VAR>α : Type u_1<VAR>f : α →₀ ℕ<GOAL>Multiset.card (Finsupp.toMultiset f) = f.sum fun x => id
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α →₀ ℕ<VAR>g : α → β<GOAL>Multiset.map g (Finsupp.toMultiset f) = Finsupp.toMultiset (Finsupp.mapDomain g f)
<VAR>α : Type u_1<VAR>AddCommMonoid α<VAR>f : α →₀ ℕ<GOAL>(Finsupp.toMultiset f).sum = f.sum fun a n => n • a
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>f : α →₀ ℕ<GOAL>(Finsupp.toMultiset f).prod = f.prod fun a n => a ^ n
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>f : α →₀ ℕ<GOAL>(Finsupp.toMultiset f).toFinset = f.support
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>f : α →₀ ℕ<VAR>a : α<GOAL>Multiset.count a (Finsupp.toMultiset f) = f a
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>f g : α →₀ ℕ<GOAL>Finsupp.toMultiset (f ⊔ g) = Finsupp.toMultiset f ∪ Finsupp.toMultiset g
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>f g : α →₀ ℕ<GOAL>Finsupp.toMultiset (f ⊓ g) = Finsupp.toMultiset f ∩ Finsupp.toMultiset g
<VAR>α : Type u_1<VAR>f : α →₀ ℕ<VAR>i : α<GOAL>i ∈ Finsupp.toMultiset f ↔ i ∈ f.support
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>f : α →₀ ℕ<GOAL>Multiset.toFinsupp.symm f = Finsupp.toMultiset f
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Multiset α<GOAL>(Multiset.toFinsupp s).support = s.toFinset
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Multiset α<VAR>a : α<GOAL>(Multiset.toFinsupp s) a = Multiset.count a s
<VAR>α : Type u_1<VAR>DecidableEq α<GOAL>Multiset.toFinsupp 0 = 0
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Multiset α<GOAL>Multiset.toFinsupp (s + t) = Multiset.toFinsupp s + Multiset.toFinsupp t