ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>DecidableEq ι<VAR>(i : ι) → Zero (α i)<VAR>s : Finset ι<VAR>f : Π₀ (i : ι), α i<VAR>(i : ι) → DecidableEq (α i)<VAR>t : Π₀ (i : ι), Finset (α i)<VAR>ht : t.support ⊆ s<GOAL>f ∈ s.dfinsupp ⇑t ↔ ∀ (i : ι), f i ∈ t i
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → Zero (α i)<VAR>f : Π₀ (i : ι), α i<VAR>i : ι<VAR>a : α i<GOAL>a ∈ f.singleton i ↔ a = f i
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → Zero (α i)<VAR>(i : ι) → PartialOrder (α i)<VAR>(i : ι) → LocallyFiniteOrder (α i)<VAR>f g : Π₀ (i : ι), α i<VAR>i : ι<GOAL>(f.rangeIcc g) i = Finset.Icc (f i) (g i)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → Zero (α i)<VAR>(i : ι) → PartialOrder (α i)<VAR>(i : ι) → LocallyFiniteOrder (α i)<VAR>f g : Π₀ (i : ι), α i<VAR>i : ι<VAR>a : α i<GOAL>a ∈ (f.rangeIcc g) i ↔ f i ≤ a ∧ a ≤ g i
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → Zero (α i)<VAR>(i : ι) → PartialOrder (α i)<VAR>(i : ι) → LocallyFiniteOrder (α i)<VAR>f g : Π₀ (i : ι), α i<VAR>DecidableEq ι<VAR>(i : ι) → DecidableEq (α i)<GOAL>(f.rangeIcc g).support ⊆ f.support ∪ g.support
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → Zero (α i)<VAR>DecidableEq ι<VAR>(i : ι) → DecidableEq (α i)<VAR>f : Π₀ (i : ι), Finset (α i)<VAR>g : Π₀ (i : ι), α i<GOAL>g ∈ f.pi ↔ ∀ (i : ι), g i ∈ f i
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → Zero (α i)<VAR>DecidableEq ι<VAR>(i : ι) → DecidableEq (α i)<VAR>f : Π₀ (i : ι), Finset (α i)<GOAL>f.pi.card = f.prod fun i => ↑(f i).card
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>DecidableEq ι<VAR>(i : ι) → DecidableEq (α i)<VAR>(i : ι) → PartialOrder (α i)<VAR>(i : ι) → Zero (α i)<VAR>(i : ι) → LocallyFiniteOrder (α i)<VAR>f g : Π₀ (i : ι), α i<GOAL>Finset.Icc f g = (f.support ∪ g.support).dfinsupp ⇑(f.rangeIcc g)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>DecidableEq ι<VAR>(i : ι) → DecidableEq (α i)<VAR>(i : ι) → PartialOrder (α i)<VAR>(i : ι) → Zero (α i)<VAR>(i : ι) → LocallyFiniteOrder (α i)<VAR>f g : Π₀ (i : ι), α i<GOAL>(Finset.Icc f g).card = ∏ i ∈ f.support ∪ g.support, (Finset.Icc (f i) (g i)).card
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>DecidableEq ι<VAR>(i : ι) → DecidableEq (α i)<VAR>(i : ι) → PartialOrder (α i)<VAR>(i : ι) → Zero (α i)<VAR>(i : ι) → LocallyFiniteOrder (α i)<VAR>f g : Π₀ (i : ι), α i<GOAL>(Finset.Ico f g).card = ∏ i ∈ f.support ∪ g.support, (Finset.Icc (f i) (g i)).card - 1
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>DecidableEq ι<VAR>(i : ι) → DecidableEq (α i)<VAR>(i : ι) → PartialOrder (α i)<VAR>(i : ι) → Zero (α i)<VAR>(i : ι) → LocallyFiniteOrder (α i)<VAR>f g : Π₀ (i : ι), α i<GOAL>(Finset.Ioc f g).card = ∏ i ∈ f.support ∪ g.support, (Finset.Icc (f i) (g i)).card - 1
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>DecidableEq ι<VAR>(i : ι) → DecidableEq (α i)<VAR>(i : ι) → PartialOrder (α i)<VAR>(i : ι) → Zero (α i)<VAR>(i : ι) → LocallyFiniteOrder (α i)<VAR>f g : Π₀ (i : ι), α i<GOAL>(Finset.Ioo f g).card = ∏ i ∈ f.support ∪ g.support, (Finset.Icc (f i) (g i)).card - 2
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>DecidableEq ι<VAR>(i : ι) → DecidableEq (α i)<VAR>(i : ι) → Lattice (α i)<VAR>(i : ι) → Zero (α i)<VAR>(i : ι) → LocallyFiniteOrder (α i)<VAR>f g : Π₀ (i : ι), α i<GOAL>(Finset.uIcc f g).card = ∏ i ∈ f.support ∪ g.support, (Finset.uIcc (f i) (g i)).card
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>DecidableEq ι<VAR>(i : ι) → DecidableEq (α i)<VAR>(i : ι) → CanonicallyOrderedAddCommMonoid (α i)<VAR>(i : ι) → LocallyFiniteOrder (α i)<VAR>f : Π₀ (i : ι), α i<GOAL>(Finset.Iic f).card = ∏ i ∈ f.support, (Finset.Iic (f i)).card
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>DecidableEq ι<VAR>(i : ι) → DecidableEq (α i)<VAR>(i : ι) → CanonicallyOrderedAddCommMonoid (α i)<VAR>(i : ι) → LocallyFiniteOrder (α i)<VAR>f : Π₀ (i : ι), α i<GOAL>(Finset.Iio f).card = ∏ i ∈ f.support, (Finset.Iic (f i)).card - 1
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → Zero (α i)<VAR>(i : ι) → LE (α i)<VAR>f g : Π₀ (i : ι), α i<GOAL>f ≤ g ↔ ∀ (i : ι), f i ≤ g i
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → Zero (α i)<VAR>(i : ι) → LE (α i)<VAR>f g : Π₀ (i : ι), α i<GOAL>⇑f ≤ ⇑g ↔ f ≤ g
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → Zero (α i)<VAR>(i : ι) → LE (α i)<GOAL>⇑DFinsupp.orderEmbeddingToFun = DFunLike.coe
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → Zero (α i)<VAR>(i : ι) → LE (α i)<VAR>f : Π₀ (i : ι), α i<VAR>i : ι<GOAL>DFinsupp.orderEmbeddingToFun f i = f i
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → Zero (α i)<VAR>(i : ι) → Preorder (α i)<VAR>f g : Π₀ (i : ι), α i<GOAL>f < g ↔ f ≤ g ∧ ∃ i, f i < g i
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → Zero (α i)<VAR>(i : ι) → Preorder (α i)<VAR>f g : Π₀ (i : ι), α i<GOAL>⇑f < ⇑g ↔ f < g
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → Zero (α i)<VAR>(i : ι) → Preorder (α i)<GOAL>Monotone DFunLike.coe
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → Zero (α i)<VAR>(i : ι) → SemilatticeInf (α i)<VAR>f g : Π₀ (i : ι), α i<GOAL>⇑(f ⊓ g) = ⇑f ⊓ ⇑g
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → Zero (α i)<VAR>(i : ι) → SemilatticeInf (α i)<VAR>f g : Π₀ (i : ι), α i<VAR>i : ι<GOAL>(f ⊓ g) i = f i ⊓ g i
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → Zero (α i)<VAR>(i : ι) → SemilatticeSup (α i)<VAR>f g : Π₀ (i : ι), α i<GOAL>⇑(f ⊔ g) = ⇑f ⊔ ⇑g
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → Zero (α i)<VAR>(i : ι) → SemilatticeSup (α i)<VAR>f g : Π₀ (i : ι), α i<VAR>i : ι<GOAL>(f ⊔ g) i = f i ⊔ g i
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → Zero (α i)<VAR>(i : ι) → Lattice (α i)<VAR>f g : Π₀ (i : ι), α i<VAR>DecidableEq ι<VAR>(i : ι) → (x : α i) → Decidable (x ≠ 0)<GOAL>(f ⊓ g).support ∪ (f ⊔ g).support = f.support ∪ g.support
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → Zero (α i)<VAR>(i : ι) → Lattice (α i)<VAR>f g : Π₀ (i : ι), α i<VAR>DecidableEq ι<VAR>(i : ι) → (x : α i) → Decidable (x ≠ 0)<GOAL>(f ⊔ g).support ∪ (f ⊓ g).support = f.support ∪ g.support
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → CanonicallyOrderedAddCommMonoid (α i)<GOAL>⊥ = 0
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → CanonicallyOrderedAddCommMonoid (α i)<VAR>f g : Π₀ (i : ι), α i<GOAL>f + g = 0 ↔ f = 0 ∧ g = 0
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → CanonicallyOrderedAddCommMonoid (α i)<VAR>DecidableEq ι<VAR>(i : ι) → (x : α i) → Decidable (x ≠ 0)<VAR>f g : Π₀ (i : ι), α i<VAR>s : Finset ι<VAR>hf : f.support ⊆ s<GOAL>f ≤ g ↔ ∀ i ∈ s, f i ≤ g i
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → CanonicallyOrderedAddCommMonoid (α i)<VAR>DecidableEq ι<VAR>(i : ι) → (x : α i) → Decidable (x ≠ 0)<VAR>f g : Π₀ (i : ι), α i<GOAL>f ≤ g ↔ ∀ i ∈ f.support, f i ≤ g i
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → CanonicallyOrderedAddCommMonoid (α i)<VAR>DecidableEq ι<VAR>(i : ι) → (x : α i) → Decidable (x ≠ 0)<GOAL>Monotone DFinsupp.support
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → CanonicallyOrderedAddCommMonoid (α i)<VAR>DecidableEq ι<VAR>(i : ι) → (x : α i) → Decidable (x ≠ 0)<VAR>f g : Π₀ (i : ι), α i<VAR>hfg : f ≤ g<GOAL>f.support ⊆ g.support
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → CanonicallyOrderedAddCommMonoid (α i)<VAR>DecidableEq ι<VAR>f : Π₀ (i : ι), α i<VAR>i : ι<VAR>a : α i<GOAL>DFinsupp.single i a ≤ f ↔ a ≤ f i
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → CanonicallyOrderedAddCommMonoid (α i)<VAR>(i : ι) → Sub (α i)<VAR>∀ (i : ι), OrderedSub (α i)<VAR>f g : Π₀ (i : ι), α i<VAR>i : ι<GOAL>(f - g) i = f i - g i
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → CanonicallyOrderedAddCommMonoid (α i)<VAR>(i : ι) → Sub (α i)<VAR>∀ (i : ι), OrderedSub (α i)<VAR>f g : Π₀ (i : ι), α i<GOAL>⇑(f - g) = ⇑f - ⇑g
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → CanonicallyOrderedAddCommMonoid (α i)<VAR>(i : ι) → Sub (α i)<VAR>∀ (i : ι), OrderedSub (α i)<VAR>i : ι<VAR>a b : α i<VAR>DecidableEq ι<GOAL>DFinsupp.single i (a - b) = DFinsupp.single i a - DFinsupp.single i b
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → CanonicallyOrderedAddCommMonoid (α i)<VAR>(i : ι) → Sub (α i)<VAR>∀ (i : ι), OrderedSub (α i)<VAR>f g : Π₀ (i : ι), α i<VAR>DecidableEq ι<VAR>(i : ι) → (x : α i) → Decidable (x ≠ 0)<GOAL>(f - g).support ⊆ f.support
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → CanonicallyOrderedAddCommMonoid (α i)<VAR>(i : ι) → Sub (α i)<VAR>∀ (i : ι), OrderedSub (α i)<VAR>f g : Π₀ (i : ι), α i<VAR>DecidableEq ι<VAR>(i : ι) → (x : α i) → Decidable (x ≠ 0)<GOAL>f.support \ g.support ⊆ (f - g).support
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → CanonicallyLinearOrderedAddCommMonoid (α i)<VAR>DecidableEq ι<VAR>f g : Π₀ (i : ι), α i<GOAL>(f ⊓ g).support = f.support ∩ g.support
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → CanonicallyLinearOrderedAddCommMonoid (α i)<VAR>DecidableEq ι<VAR>f g : Π₀ (i : ι), α i<GOAL>(f ⊔ g).support = f.support ∪ g.support
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → CanonicallyLinearOrderedAddCommMonoid (α i)<VAR>DecidableEq ι<VAR>f g : Π₀ (i : ι), α i<GOAL>Disjoint f g ↔ Disjoint f.support g.support
<VAR>α : Type u<VAR>DecidableEq α<GOAL>Finset.antidiagonal 0 = {(0, 0)}
<VAR>α : Type u<VAR>DecidableEq α<VAR>M : Type u_1<VAR>CommMonoid M<VAR>n : α →₀ ℕ<VAR>f : (α →₀ ℕ) → (α →₀ ℕ) → M<GOAL>∏ p ∈ Finset.antidiagonal n, f p.1 p.2 = ∏ p ∈ Finset.antidiagonal n, f p.2 p.1
<VAR>α : Type u<VAR>DecidableEq α<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>n : α →₀ ℕ<VAR>f : (α →₀ ℕ) → (α →₀ ℕ) → M<GOAL>∑ p ∈ Finset.antidiagonal n, f p.1 p.2 = ∑ p ∈ Finset.antidiagonal n, f p.2 p.1
<VAR>α : Type u<VAR>DecidableEq α<VAR>a : α<VAR>n : ℕ<GOAL>Finset.antidiagonal (Finsupp.single a n) = Finset.map ({ toFun := Finsupp.single a, inj' := ⋯ }.prodMap { toFun := Finsupp.single a, inj' := ⋯ }) (Finset.antidiagonal n)
<VAR>α : Type u_1<VAR>σ : Type u_2<VAR>Zero α<VAR>LinearOrder α<VAR>IsWellOrder α fun x x_1 => x < x_1<VAR>Finite σ<VAR>S : Set (σ →₀ α)<GOAL>S.IsPWO
<VAR>n : ℕ<VAR>i : Fin n<VAR>M : Type u_1<VAR>Zero M<VAR>t : Fin (n + 1) →₀ M<GOAL>t.tail i = t i.succ
<VAR>n : ℕ<VAR>M : Type u_1<VAR>Zero M<VAR>y : M<VAR>s : Fin n →₀ M<GOAL>(Finsupp.cons y s) 0 = y
<VAR>n : ℕ<VAR>i : Fin n<VAR>M : Type u_1<VAR>Zero M<VAR>y : M<VAR>s : Fin n →₀ M<GOAL>(Finsupp.cons y s) i.succ = s i
<VAR>n : ℕ<VAR>M : Type u_1<VAR>Zero M<VAR>y : M<VAR>s : Fin n →₀ M<GOAL>(Finsupp.cons y s).tail = s
<VAR>n : ℕ<VAR>M : Type u_1<VAR>Zero M<VAR>t : Fin (n + 1) →₀ M<GOAL>Finsupp.cons (t 0) t.tail = t
<VAR>n : ℕ<VAR>M : Type u_1<VAR>Zero M<GOAL>Finsupp.cons 0 0 = 0
<VAR>n : ℕ<VAR>M : Type u_1<VAR>Zero M<VAR>y : M<VAR>s : Fin n →₀ M<VAR>h : y ≠ 0<GOAL>Finsupp.cons y s ≠ 0
<VAR>n : ℕ<VAR>M : Type u_1<VAR>Zero M<VAR>y : M<VAR>s : Fin n →₀ M<VAR>h : s ≠ 0<GOAL>Finsupp.cons y s ≠ 0
<VAR>n : ℕ<VAR>M : Type u_1<VAR>Zero M<VAR>y : M<VAR>s : Fin n →₀ M<GOAL>Finsupp.cons y s ≠ 0 ↔ y ≠ 0 ∨ s ≠ 0
<VAR>n : ℕ<VAR>M : Type u_1<VAR>Zero M<VAR>y : M<VAR>s : Fin n →₀ M<GOAL>(Finsupp.cons y s).support ⊆ insert 0 (Finset.map (Fin.succEmb n) s.support)
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>Zero M<VAR>f : α →₀ M<GOAL>f.toAList.entries = List.map Prod.toSigma f.graph.toList
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>Zero M<VAR>DecidableEq α<VAR>f : α →₀ M<GOAL>f.toAList.keys.toFinset = f.support
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>Zero M<VAR>f : α →₀ M<VAR>x : α<GOAL>x ∈ f.toAList ↔ f x ≠ 0
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>Zero M<VAR>DecidableEq α<VAR>l : AList fun _x => M<VAR>a : α<GOAL>l.lookupFinsupp a = (AList.lookup a l).getD 0
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>Zero M<VAR>DecidableEq α<VAR>DecidableEq M<VAR>l : AList fun _x => M<GOAL>l.lookupFinsupp.support = (List.filter (fun x => decide (x.snd ≠ 0)) l.entries).keys.toFinset
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>Zero M<VAR>DecidableEq α<VAR>l : AList fun _x => M<VAR>a : α<VAR>x : M<VAR>hx : x ≠ 0<GOAL>l.lookupFinsupp a = x ↔ x ∈ AList.lookup a l
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>Zero M<VAR>DecidableEq α<VAR>l : AList fun _x => M<VAR>a : α<GOAL>l.lookupFinsupp a = 0 ↔ a ∉ l ∨ 0 ∈ AList.lookup a l
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>Zero M<GOAL>∅.lookupFinsupp = 0
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>Zero M<VAR>DecidableEq α<VAR>l : AList fun _x => M<VAR>a : α<VAR>m : M<GOAL>(AList.insert a m l).lookupFinsupp = l.lookupFinsupp.update a m
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>Zero M<VAR>a : α<VAR>m : M<GOAL>(AList.singleton a m).lookupFinsupp = Finsupp.single a m
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>Zero M<VAR>f : α →₀ M<GOAL>f.toAList.lookupFinsupp = f
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>Zero M<GOAL>Function.Surjective AList.lookupFinsupp
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → Zero (α i)<VAR>r : ι → ι → Prop<VAR>s : (i : ι) → α i → α i → Prop<VAR>a b : Π₀ (i : ι), α i<GOAL>Pi.Lex r (fun {i} => s i) ⇑a ⇑b = DFinsupp.Lex r s a b
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → Zero (α i)<VAR>r : ι → ι → Prop<VAR>s : (i : ι) → α i → α i → Prop<VAR>a b : Π₀ (i : ι), α i<GOAL>DFinsupp.Lex r s a b ↔ ∃ j, (∀ (d : ι), r d j → a d = b d) ∧ s j (a j) (b j)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → Zero (α i)<VAR>(i : ι) → Preorder (α i)<VAR>r : ι → ι → Prop<VAR>IsStrictOrder ι r<VAR>x y : Π₀ (i : ι), α i<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>α : ι → Type u_2<VAR>(i : ι) → Zero (α i)<VAR>(i : ι) → PartialOrder (α i)<VAR>r : ι → ι → Prop<VAR>IsStrictOrder ι r<VAR>x y : Π₀ (i : ι), α i<VAR>hlt : x < y<GOAL>Pi.Lex r (fun {i} x x_1 => x < x_1) ⇑x ⇑y
<VAR>ι : Type u_3<VAR>α : ι → Type u_4<VAR>(i : ι) → Zero (α i)<VAR>LinearOrder ι<VAR>(i : ι) → LinearOrder (α i)<GOAL>DFinsupp.Lex.decidableLE = DFinsupp.lt_trichotomy_rec (fun {f g} h => isTrue ⋯) (fun {f g} h => isTrue ⋯) fun {f g} h => isFalse ⋯
<VAR>ι : Type u_3<VAR>α : ι → Type u_4<VAR>(i : ι) → Zero (α i)<VAR>LinearOrder ι<VAR>(i : ι) → LinearOrder (α i)<GOAL>DFinsupp.Lex.decidableLT = DFinsupp.lt_trichotomy_rec (fun {f g} h => isTrue h) (fun {f g} h => isFalse ⋯) fun {f g} h => isFalse ⋯
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → Zero (α i)<VAR>LinearOrder ι<VAR>(i : ι) → PartialOrder (α i)<GOAL>Monotone ⇑toLex
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → Zero (α i)<VAR>LinearOrder ι<VAR>(i : ι) → PartialOrder (α i)<VAR>a b : Lex (Π₀ (i : ι), α i)<VAR>i : ι<GOAL>(∀ j < i, (ofLex a) j = (ofLex b) j) → (ofLex a) i < (ofLex b) i → a < b
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>DecidableEq ι<VAR>AddMonoid M<VAR>l : List (ι →₀ M)<GOAL>l.sum.support ⊆ List.foldr (fun x x_1 => x.support ⊔ x_1) ∅ l
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>DecidableEq ι<VAR>AddCommMonoid M<VAR>s : Multiset (ι →₀ M)<GOAL>s.sum.support ⊆ (Multiset.map Finsupp.support s).sup
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>DecidableEq ι<VAR>AddCommMonoid M<VAR>s : Finset (ι →₀ M)<GOAL>(s.sum id).support ⊆ s.sup Finsupp.support
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>DecidableEq ι<VAR>Zero M<VAR>l : List (ι →₀ M)<VAR>x : ι<GOAL>x ∈ List.foldr (fun x x_1 => x.support ⊔ x_1) ∅ l ↔ ∃ f ∈ l, x ∈ f.support
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>DecidableEq ι<VAR>Zero M<VAR>s : Multiset (ι →₀ M)<VAR>x : ι<GOAL>x ∈ (Multiset.map Finsupp.support s).sup ↔ ∃ f ∈ s, x ∈ f.support
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>DecidableEq ι<VAR>Zero M<VAR>s : Finset (ι →₀ M)<VAR>x : ι<GOAL>x ∈ s.sup Finsupp.support ↔ ∃ f ∈ s, x ∈ f.support
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>DecidableEq ι<VAR>AddMonoid M<VAR>l : List (ι →₀ M)<VAR>hl : List.Pairwise (Disjoint on Finsupp.support) l<GOAL>l.sum.support = List.foldr (fun x x_1 => x.support ⊔ x_1) ∅ l
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>DecidableEq ι<VAR>AddCommMonoid M<VAR>s : Multiset (ι →₀ M)<VAR>hs : Multiset.Pairwise (Disjoint on Finsupp.support) s<GOAL>s.sum.support = (Multiset.map Finsupp.support s).sup
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>DecidableEq ι<VAR>AddCommMonoid M<VAR>s : Finset (ι →₀ M)<VAR>hs : (↑s).PairwiseDisjoint Finsupp.support<GOAL>(s.sum id).support = s.sup Finsupp.support
<VAR>α : Type u_1<VAR>N : Type u_3<VAR>DecidableEq α<VAR>DecidableEq N<VAR>Zero N<VAR>f g : α →₀ N<VAR>a : α<GOAL>a ∈ f.neLocus g ↔ f a ≠ g a
<VAR>α : Type u_1<VAR>N : Type u_3<VAR>DecidableEq α<VAR>DecidableEq N<VAR>Zero N<VAR>f g : α →₀ N<VAR>a : α<GOAL>a ∉ f.neLocus g ↔ f a = g a
<VAR>α : Type u_1<VAR>N : Type u_3<VAR>DecidableEq α<VAR>DecidableEq N<VAR>Zero N<VAR>f g : α →₀ N<GOAL>↑(f.neLocus g) = {x | f x ≠ g x}
<VAR>α : Type u_1<VAR>N : Type u_3<VAR>DecidableEq α<VAR>DecidableEq N<VAR>Zero N<VAR>f g : α →₀ N<GOAL>f.neLocus g = ∅ ↔ f = g
<VAR>α : Type u_1<VAR>N : Type u_3<VAR>DecidableEq α<VAR>DecidableEq N<VAR>Zero N<VAR>f g : α →₀ N<GOAL>(f.neLocus g).Nonempty ↔ f ≠ g
<VAR>α : Type u_1<VAR>N : Type u_3<VAR>DecidableEq α<VAR>DecidableEq N<VAR>Zero N<VAR>f g : α →₀ N<GOAL>f.neLocus g = g.neLocus f
<VAR>α : Type u_1<VAR>N : Type u_3<VAR>DecidableEq α<VAR>DecidableEq N<VAR>Zero N<VAR>f : α →₀ N<GOAL>f.neLocus 0 = f.support
<VAR>α : Type u_1<VAR>N : Type u_3<VAR>DecidableEq α<VAR>DecidableEq N<VAR>Zero N<VAR>f : α →₀ N<GOAL>Finsupp.neLocus 0 f = f.support
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>DecidableEq α<VAR>DecidableEq N<VAR>Zero N<VAR>DecidableEq M<VAR>Zero M<VAR>f g : α →₀ N<VAR>F : N → M<VAR>F0 : F 0 = 0<GOAL>(Finsupp.mapRange F F0 f).neLocus (Finsupp.mapRange F F0 g) ⊆ f.neLocus g
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>DecidableEq α<VAR>DecidableEq N<VAR>Zero M<VAR>DecidableEq P<VAR>Zero P<VAR>Zero N<VAR>F : M → N → P<VAR>F0 : F 0 0 = 0<VAR>f : α →₀ M<VAR>g₁ g₂ : α →₀ N<VAR>hF : ∀ (f : M), Function.Injective fun g => F f g<GOAL>(Finsupp.zipWith F F0 f g₁).neLocus (Finsupp.zipWith F F0 f g₂) = g₁.neLocus g₂
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>DecidableEq α<VAR>DecidableEq M<VAR>Zero M<VAR>DecidableEq P<VAR>Zero P<VAR>Zero N<VAR>F : M → N → P<VAR>F0 : F 0 0 = 0<VAR>f₁ f₂ : α →₀ M<VAR>g : α →₀ N<VAR>hF : ∀ (g : N), Function.Injective fun f => F f g<GOAL>(Finsupp.zipWith F F0 f₁ g).neLocus (Finsupp.zipWith F F0 f₂ g) = f₁.neLocus f₂
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>DecidableEq α<VAR>DecidableEq N<VAR>DecidableEq M<VAR>Zero M<VAR>Zero N<VAR>f g : α →₀ N<VAR>F : N → M<VAR>F0 : F 0 = 0<VAR>hF : Function.Injective F<GOAL>(Finsupp.mapRange F F0 f).neLocus (Finsupp.mapRange F F0 g) = f.neLocus g
<VAR>α : Type u_1<VAR>N : Type u_3<VAR>DecidableEq α<VAR>DecidableEq N<VAR>AddLeftCancelMonoid N<VAR>f g h : α →₀ N<GOAL>(f + g).neLocus (f + h) = g.neLocus h
<VAR>α : Type u_1<VAR>N : Type u_3<VAR>DecidableEq α<VAR>DecidableEq N<VAR>AddRightCancelMonoid N<VAR>f g h : α →₀ N<GOAL>(f + h).neLocus (g + h) = f.neLocus g
<VAR>α : Type u_1<VAR>N : Type u_3<VAR>DecidableEq α<VAR>DecidableEq N<VAR>AddGroup N<VAR>f g : α →₀ N<GOAL>(-f).neLocus (-g) = f.neLocus g
<VAR>α : Type u_1<VAR>N : Type u_3<VAR>DecidableEq α<VAR>DecidableEq N<VAR>AddGroup N<VAR>f g : α →₀ N<GOAL>(-f).neLocus g = f.neLocus (-g)
<VAR>α : Type u_1<VAR>N : Type u_3<VAR>DecidableEq α<VAR>DecidableEq N<VAR>AddGroup N<VAR>f g : α →₀ N<GOAL>f.neLocus g = (f - g).support
<VAR>α : Type u_1<VAR>N : Type u_3<VAR>DecidableEq α<VAR>DecidableEq N<VAR>AddGroup N<VAR>f g₁ g₂ : α →₀ N<GOAL>(f - g₁).neLocus (f - g₂) = g₁.neLocus g₂
<VAR>α : Type u_1<VAR>N : Type u_3<VAR>DecidableEq α<VAR>DecidableEq N<VAR>AddGroup N<VAR>f₁ f₂ g : α →₀ N<GOAL>(f₁ - g).neLocus (f₂ - g) = f₁.neLocus f₂
<VAR>α : Type u_1<VAR>N : Type u_3<VAR>DecidableEq α<VAR>DecidableEq N<VAR>AddGroup N<VAR>f g : α →₀ N<GOAL>f.neLocus (f + g) = g.support
<VAR>α : Type u_1<VAR>N : Type u_3<VAR>DecidableEq α<VAR>DecidableEq N<VAR>AddGroup N<VAR>f g : α →₀ N<GOAL>(f + g).neLocus f = g.support
<VAR>α : Type u_1<VAR>N : Type u_3<VAR>DecidableEq α<VAR>DecidableEq N<VAR>AddGroup N<VAR>f g : α →₀ N<GOAL>f.neLocus (f - g) = g.support
<VAR>α : Type u_1<VAR>N : Type u_3<VAR>DecidableEq α<VAR>DecidableEq N<VAR>AddGroup N<VAR>f g : α →₀ N<GOAL>(f - g).neLocus f = g.support
<VAR>α : Type u_1<VAR>N : Type u_2<VAR>Zero N<VAR>r : α → α → Prop<VAR>s : N → N → Prop<VAR>hbot : ∀ ⦃n : N⦄, ¬s n 0<VAR>hs : WellFounded s<VAR>x : α →₀ N<VAR>h : ∀ a ∈ x.support, Acc (rᶜ ⊓ fun x x_1 => x ≠ x_1) a<GOAL>Acc (Finsupp.Lex r s) x
<VAR>α : Type u_1<VAR>N : Type u_2<VAR>Zero N<VAR>r : α → α → Prop<VAR>s : N → N → Prop<VAR>hbot : ∀ ⦃n : N⦄, ¬s n 0<VAR>hs : WellFounded s<VAR>hr : WellFounded (rᶜ ⊓ fun x x_1 => x ≠ x_1)<GOAL>WellFounded (Finsupp.Lex r s)
<VAR>α : Type u_1<VAR>N : Type u_2<VAR>Zero N<VAR>r : α → α → Prop<VAR>s : N → N → Prop<VAR>hbot : ∀ ⦃n : N⦄, ¬s n 0<VAR>hs : WellFounded s<VAR>IsTrichotomous α r<VAR>hr : WellFounded (Function.swap r)<GOAL>WellFounded (Finsupp.Lex r s)
<VAR>α : Type u_1<VAR>N : Type u_2<VAR>Zero N<VAR>r : α → α → Prop<VAR>s : N → N → Prop<VAR>IsStrictTotalOrder α r<VAR>Finite α<VAR>hs : WellFounded s<GOAL>WellFounded (Finsupp.Lex r s)
<VAR>α : Type u_1<VAR>N : Type u_2<VAR>Zero N<VAR>LinearOrder α<VAR>Finite α<VAR>LT N<VAR>hwf : WellFoundedLT N<GOAL>WellFoundedLT (Lex (α →₀ N))
<VAR>α : Type u_1<VAR>N : Type u_2<VAR>Zero N<VAR>Preorder N<VAR>WellFoundedLT N<VAR>hbot : ∀ (n : N), ¬n < 0<GOAL>WellFoundedLT (α →₀ N)
<VAR>σ : Type u_1<VAR>M : Type u_2<VAR>w : σ → M<VAR>AddCommMonoid M<VAR>f : σ →₀ ℕ<GOAL>(Finsupp.weight w) f = f.sum fun i c => c • w i
<VAR>σ : Type u_1<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>w : σ → M<VAR>self : Finsupp.NonTorsionWeight w<VAR>n : ℕ<VAR>s : σ<VAR>h : n • w s = 0<GOAL>n = 0
<VAR>σ : Type u_1<VAR>M : Type u_2<VAR>w : σ → M<VAR>AddCommMonoid M<VAR>NoZeroSMulDivisors ℕ M<VAR>hw : ∀ (i : σ), w i ≠ 0<GOAL>Finsupp.NonTorsionWeight w
<VAR>σ : Type u_1<VAR>M : Type u_2<VAR>w : σ → M<VAR>AddCommMonoid M<VAR>Finsupp.NonTorsionWeight w<VAR>s : σ<GOAL>w s ≠ 0
<VAR>σ : Type u_1<VAR>w : σ → ℕ<VAR>s : σ<VAR>hs : w s ≠ 0<VAR>f : σ →₀ ℕ<GOAL>f s ≤ (Finsupp.weight w) f
<VAR>σ : Type u_1<VAR>M : Type u_2<VAR>OrderedAddCommMonoid M<VAR>w : σ → M<VAR>hw : ∀ (s : σ), 0 ≤ w s<VAR>s : σ<VAR>f : σ →₀ ℕ<VAR>hs : f s ≠ 0<GOAL>w s ≤ (Finsupp.weight w) f
<VAR>σ : Type u_1<VAR>M : Type u_3<VAR>CanonicallyOrderedAddCommMonoid M<VAR>w : σ → M<VAR>s : σ<VAR>f : σ →₀ ℕ<VAR>hs : f s ≠ 0<GOAL>w s ≤ (Finsupp.weight w) f
<VAR>σ : Type u_1<VAR>M : Type u_3<VAR>CanonicallyOrderedAddCommMonoid M<VAR>w : σ → M<VAR>Finsupp.NonTorsionWeight w<VAR>f : σ →₀ ℕ<GOAL>(Finsupp.weight w) f = 0 ↔ f = 0
<VAR>σ : Type u_1<VAR>d : σ →₀ ℕ<GOAL>d.degree = 0 ↔ d = 0
<VAR>σ : Type u_1<GOAL>Finsupp.degree 0 = 0
<VAR>σ : Type u_1<GOAL>Finsupp.degree = ⇑(Finsupp.weight 1)
<VAR>σ : Type u_1<VAR>s : σ<VAR>f : σ →₀ ℕ<GOAL>f s ≤ f.degree
<VAR>P : EReal → EReal → Prop<VAR>top_top : P ⊤ ⊤<VAR>top_pos : ∀ (x : ℝ), 0 < x → P ⊤ ↑x<VAR>top_zero : P ⊤ 0<VAR>top_neg : ∀ x < 0, P ⊤ ↑x<VAR>top_bot : P ⊤ ⊥<VAR>pos_top : ∀ (x : ℝ), 0 < x → P ↑x ⊤<VAR>pos_bot : ∀ (x : ℝ), 0 < x → P ↑x ⊥<VAR>zero_top : P 0 ⊤<VAR>coe_coe : ∀ (x y : ℝ), P ↑x ↑y<VAR>zero_bot : P 0 ⊥<VAR>neg_top : ∀ x < 0, P ↑x ⊤<VAR>neg_bot : ∀ x < 0, P ↑x ⊥<VAR>bot_top : P ⊥ ⊤<VAR>bot_pos : ∀ (x : ℝ), 0 < x → P ⊥ ↑x<VAR>bot_zero : P ⊥ 0<VAR>bot_neg : ∀ x < 0, P ⊥ ↑x<VAR>bot_bot : P ⊥ ⊥<VAR>x y : EReal<GOAL>P x y
<VAR>P : EReal → EReal → Prop<VAR>symm : ∀ {x y : EReal}, P x y → P y x<VAR>top_top : P ⊤ ⊤<VAR>top_pos : ∀ (x : ℝ), 0 < x → P ⊤ ↑x<VAR>top_zero : P ⊤ 0<VAR>top_neg : ∀ x < 0, P ⊤ ↑x<VAR>top_bot : P ⊤ ⊥<VAR>pos_bot : ∀ (x : ℝ), 0 < x → P ↑x ⊥<VAR>coe_coe : ∀ (x y : ℝ), P ↑x ↑y<VAR>zero_bot : P 0 ⊥<VAR>neg_bot : ∀ x < 0, P ↑x ⊥<VAR>bot_bot : P ⊥ ⊥<VAR>x y : EReal<GOAL>P x y
<VAR>x : ℝ<GOAL>(↑x).toReal = x
<VAR>x : ℝ<GOAL>⊥ < ↑x
<VAR>x : ℝ<GOAL>↑x ≠ ⊥
<VAR>x : ℝ<GOAL>⊥ ≠ ↑x
<VAR>x : ℝ<GOAL>↑x < ⊤
<VAR>x : ℝ<GOAL>↑x ≠ ⊤
<VAR>x : ℝ<GOAL>⊤ ≠ ↑x
<GOAL>Set.range Real.toEReal = {⊥, ⊤}ᶜ
<GOAL>Set.range Real.toEReal = Set.Ioo ⊥ ⊤
<VAR>x : ℝ<GOAL>↑x ≤ 0 ↔ x ≤ 0
<VAR>x : ℝ<GOAL>↑x < 0 ↔ x < 0
<VAR>x : EReal<VAR>hx : x ≠ ⊤<VAR>h'x : x ≠ ⊥<GOAL>↑x.toReal = x
<VAR>x : EReal<VAR>h : x ≠ ⊤<GOAL>x ≤ ↑x.toReal
<VAR>x : EReal<VAR>h : x ≠ ⊥<GOAL>↑x.toReal ≤ x
<VAR>x : EReal<GOAL>x = ⊤ ↔ ∀ (y : ℝ), ↑y < x
<VAR>x : EReal<GOAL>x = ⊥ ↔ ∀ (y : ℝ), x < ↑y
<VAR>x y : ℝ<GOAL>Real.toEReal '' Set.Icc x y = Set.Icc ↑x ↑y
<VAR>x y : ℝ<GOAL>Real.toEReal '' Set.Ico x y = Set.Ico ↑x ↑y
<VAR>x : ℝ<GOAL>Real.toEReal '' Set.Ici x = Set.Ico ↑x ⊤
<VAR>x y : ℝ<GOAL>Real.toEReal '' Set.Ioc x y = Set.Ioc ↑x ↑y
<VAR>x y : ℝ<GOAL>Real.toEReal '' Set.Ioo x y = Set.Ioo ↑x ↑y
<VAR>x : ℝ<GOAL>Real.toEReal '' Set.Ioi x = Set.Ioo ↑x ⊤
<VAR>x : ℝ<GOAL>Real.toEReal '' Set.Iic x = Set.Ioc ⊥ ↑x
<VAR>x : ℝ<GOAL>Real.toEReal '' Set.Iio x = Set.Ioo ⊥ ↑x