ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>X : AlgebraicGeometry.LocallyRingedSpace<VAR>R : Type u<VAR>CommRing R<VAR>f : CommRingCat.of R ⟶ AlgebraicGeometry.LocallyRingedSpace.Γ.obj (Opposite.op X)<GOAL>(AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction.homEquiv X (Opposite.op (CommRingCat.of R))) (Opposite.op f) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.identityToΓSpec.app X) (AlgebraicGeometry.Spec.locallyRingedSpaceMap f)
<VAR>X : AlgebraicGeometry.LocallyRingedSpace<VAR>R : Type u<VAR>CommRing R<VAR>f : AlgebraicGeometry.LocallyRingedSpace.Γ.rightOp.obj X ⟶ Opposite.op (CommRingCat.of R)<VAR>U : (TopologicalSpace.Opens ↑↑(AlgebraicGeometry.Spec.toLocallyRingedSpace.obj (Opposite.op (CommRingCat.of R))).toPresheafedSpace)ᵒᵖ<GOAL>CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.StructureSheaf.toOpen R (Opposite.unop U)) (((AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction.homEquiv X (Opposite.op (CommRingCat.of R))) f).val.c.app U) = CategoryTheory.CategoryStruct.comp f.unop (X.presheaf.map (CategoryTheory.homOfLE ⋯).op)
<VAR>X : AlgebraicGeometry.Scheme<VAR>R : CommRingCatᵒᵖ<VAR>f : Opposite.op (AlgebraicGeometry.Scheme.Γ.obj (Opposite.op X)) ⟶ R<GOAL>(AlgebraicGeometry.ΓSpec.adjunction.homEquiv X R) f = (AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction.homEquiv X.toLocallyRingedSpace R) f
<VAR>X : AlgebraicGeometry.Scheme<VAR>R : CommRingCatᵒᵖ<GOAL>AlgebraicGeometry.ΓSpec.adjunction.homEquiv X R = AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction.homEquiv X.toLocallyRingedSpace R
<VAR>X : AlgebraicGeometry.Scheme<VAR>R : CommRingCatᵒᵖ<VAR>f : X ⟶ AlgebraicGeometry.Scheme.Spec.obj R<GOAL>(AlgebraicGeometry.ΓSpec.adjunction.homEquiv X R).symm f = (AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction.homEquiv X.toLocallyRingedSpace R).symm f
<VAR>R : CommRingCatᵒᵖ<GOAL>AlgebraicGeometry.ΓSpec.adjunction.counit.app R = AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction.counit.app R
<VAR>R : CommRingCatᵒᵖ<GOAL>AlgebraicGeometry.ΓSpec.adjunction.counit.app R = (AlgebraicGeometry.Scheme.ΓSpecIso (Opposite.unop R)).inv.op
<VAR>X : AlgebraicGeometry.Scheme<GOAL>AlgebraicGeometry.ΓSpec.adjunction.unit.app X = AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction.unit.app X.toLocallyRingedSpace
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<GOAL>CategoryTheory.CategoryStruct.comp f (AlgebraicGeometry.ΓSpec.adjunction.unit.app Y) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.ΓSpec.adjunction.unit.app X) (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.Hom.app f ⊤))
<VAR>X : AlgebraicGeometry.Scheme<GOAL>AlgebraicGeometry.Scheme.Hom.app (AlgebraicGeometry.ΓSpec.adjunction.unit.app X) ⊤ = (AlgebraicGeometry.Scheme.ΓSpecIso (X.presheaf.obj (Opposite.op ⊤))).hom
<VAR>R : CommRingCat<GOAL>AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.ΓSpecIso R).hom = AlgebraicGeometry.ΓSpec.adjunction.unit.app (AlgebraicGeometry.Spec R)
<VAR>X : AlgebraicGeometry.Scheme<VAR>r : ↑(X.presheaf.obj (Opposite.op ⊤))<GOAL>(TopologicalSpace.Opens.map (AlgebraicGeometry.ΓSpec.adjunction.unit.app X).val.base).obj (PrimeSpectrum.basicOpen r) = X.basicOpen r
<VAR>X : AlgebraicGeometry.Scheme<VAR>U : (TopologicalSpace.Opens ↑↑((AlgebraicGeometry.Scheme.Γ.rightOp.comp AlgebraicGeometry.Scheme.Spec).obj X).toPresheafedSpace)ᵒᵖ<GOAL>CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.StructureSheaf.toOpen (↑(Opposite.unop (AlgebraicGeometry.Scheme.Γ.rightOp.obj X))) (Opposite.unop U)) ((AlgebraicGeometry.ΓSpec.adjunction.unit.app X).val.c.app U) = X.presheaf.map (CategoryTheory.homOfLE ⋯).op
<VAR>X : AlgebraicGeometry.Scheme<VAR>U : TopologicalSpace.Opens (PrimeSpectrum ↑(X.presheaf.obj (Opposite.op ⊤)))<GOAL>CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.StructureSheaf.toOpen (↑(X.presheaf.obj (Opposite.op ⊤))) U) (AlgebraicGeometry.Scheme.Hom.app (AlgebraicGeometry.ΓSpec.adjunction.unit.app X) U) = X.presheaf.map (CategoryTheory.homOfLE ⋯).op
<VAR>X : AlgebraicGeometry.Scheme<VAR>U : X.Opens<GOAL>(AlgebraicGeometry.Scheme.ΓSpecIso (X.presheaf.obj (Opposite.op U))).hom = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.app (AlgebraicGeometry.Spec.map U.topIso.inv) ⊤) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.app (AlgebraicGeometry.ΓSpec.adjunction.unit.app ↑U) ⊤) U.topIso.hom)
<VAR>R S : CommRingCat<VAR>φ ψ : R ⟶ S<GOAL>AlgebraicGeometry.Spec.map φ = AlgebraicGeometry.Spec.map ψ ↔ φ = ψ
<VAR>R S : CommRingCat<GOAL>Function.Injective AlgebraicGeometry.Spec.map
<VAR>R S : CommRingCat<VAR>f : AlgebraicGeometry.Spec S ⟶ AlgebraicGeometry.Spec R<GOAL>AlgebraicGeometry.Spec.map (AlgebraicGeometry.Spec.preimage f) = f
<VAR>R S : CommRingCat<VAR>φ : R ⟶ S<GOAL>AlgebraicGeometry.Spec.preimage (AlgebraicGeometry.Spec.map φ) = φ
<VAR>R S : CommRingCat<VAR>f : R ⟶ S<GOAL>AlgebraicGeometry.Spec.homEquiv.symm f = AlgebraicGeometry.Spec.map f
<VAR>R S : CommRingCat<VAR>f : AlgebraicGeometry.Spec S ⟶ AlgebraicGeometry.Spec R<GOAL>AlgebraicGeometry.Spec.homEquiv f = AlgebraicGeometry.Spec.preimage f
<VAR>a b : ℤ<VAR>r : ℤ<VAR>hr : 0 < r<GOAL>Finset.filter (fun x => r ∣ x) (Finset.Ico a b) = Finset.map { toFun := fun x => x * r, inj' := ⋯ } (Finset.Ico ⌈↑a / ↑r⌉ ⌈↑b / ↑r⌉)
<VAR>a b : ℤ<VAR>r : ℤ<VAR>hr : 0 < r<GOAL>Finset.filter (fun x => r ∣ x) (Finset.Ioc a b) = Finset.map { toFun := fun x => x * r, inj' := ⋯ } (Finset.Ioc ⌊↑a / ↑r⌋ ⌊↑b / ↑r⌋)
<VAR>a b : ℤ<VAR>r : ℤ<VAR>hr : 0 < r<GOAL>↑(Finset.filter (fun x => r ∣ x) (Finset.Ico a b)).card = max (⌈↑b / ↑r⌉ - ⌈↑a / ↑r⌉) 0
<VAR>a b : ℤ<VAR>r : ℤ<VAR>hr : 0 < r<GOAL>↑(Finset.filter (fun x => r ∣ x) (Finset.Ioc a b)).card = max (⌊↑b / ↑r⌋ - ⌊↑a / ↑r⌋) 0
<VAR>a b : ℤ<VAR>r : ℤ<VAR>v : ℤ<GOAL>Finset.filter (fun x => x ≡ v [ZMOD r]) (Finset.Ico a b) = Finset.map { toFun := fun x => x + v, inj' := ⋯ } (Finset.filter (fun x => r ∣ x) (Finset.Ico (a - v) (b - v)))
<VAR>a b : ℤ<VAR>r : ℤ<VAR>v : ℤ<GOAL>Finset.filter (fun x => x ≡ v [ZMOD r]) (Finset.Ioc a b) = Finset.map { toFun := fun x => x + v, inj' := ⋯ } (Finset.filter (fun x => r ∣ x) (Finset.Ioc (a - v) (b - v)))
<VAR>a b : ℤ<VAR>r : ℤ<VAR>hr : 0 < r<VAR>v : ℤ<GOAL>↑(Finset.filter (fun x => x ≡ v [ZMOD r]) (Finset.Ico a b)).card = max (⌈(↑b - ↑v) / ↑r⌉ - ⌈(↑a - ↑v) / ↑r⌉) 0
<VAR>a b : ℤ<VAR>r : ℤ<VAR>hr : 0 < r<VAR>v : ℤ<GOAL>↑(Finset.filter (fun x => x ≡ v [ZMOD r]) (Finset.Ioc a b)).card = max (⌊(↑b - ↑v) / ↑r⌋ - ⌊(↑a - ↑v) / ↑r⌋) 0
<VAR>a b : ℕ<VAR>r v : ℕ<GOAL>Finset.map Nat.castEmbedding (Finset.filter (fun x => x ≡ v [MOD r]) (Finset.Ico a b)) = Finset.filter (fun x => x ≡ ↑v [ZMOD ↑r]) (Finset.Ico ↑a ↑b)
<VAR>a b : ℕ<VAR>r v : ℕ<GOAL>Finset.map Nat.castEmbedding (Finset.filter (fun x => x ≡ v [MOD r]) (Finset.Ioc a b)) = Finset.filter (fun x => x ≡ ↑v [ZMOD ↑r]) (Finset.Ioc ↑a ↑b)
<VAR>a b : ℕ<VAR>r : ℕ<VAR>hr : 0 < r<VAR>v : ℕ<GOAL>↑(Finset.filter (fun x => x ≡ v [MOD r]) (Finset.Ico a b)).card = max (⌈(↑b - ↑v) / ↑r⌉ - ⌈(↑a - ↑v) / ↑r⌉) 0
<VAR>a b : ℕ<VAR>r : ℕ<VAR>hr : 0 < r<VAR>v : ℕ<GOAL>↑(Finset.filter (fun x => x ≡ v [MOD r]) (Finset.Ioc a b)).card = max (⌊(↑b - ↑v) / ↑r⌋ - ⌊(↑a - ↑v) / ↑r⌋) 0
<VAR>b : ℕ<VAR>r : ℕ<VAR>hr : 0 < r<VAR>v : ℕ<GOAL>↑(Nat.count (fun x => x ≡ v [MOD r]) b) = ⌈(↑b - ↑(v % r)) / ↑r⌉
<VAR>b : ℕ<VAR>r : ℕ<VAR>hr : 0 < r<VAR>v : ℕ<GOAL>Nat.count (fun x => x ≡ v [MOD r]) b = b / r + if v % r < b % r then 1 else 0
<VAR>α : Type u_1<VAR>l : List α<VAR>p : l.Palindrome<GOAL>l.reverse = l
<VAR>α : Type u_1<VAR>l : List α<GOAL>l.reverse = l → l.Palindrome
<VAR>α : Type u_1<VAR>l : List α<GOAL>l.Palindrome ↔ l.reverse = l
<VAR>α : Type u_1<VAR>l : List α<GOAL>(l ++ l.reverse).Palindrome
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : List α<VAR>f : α → β<VAR>p : l.Palindrome<GOAL>(List.map f l).Palindrome
<VAR>α : Type u_1<VAR>x : α<VAR>l : List (Option α)<GOAL>(some x :: l).reduceOption = x :: l.reduceOption
<VAR>α : Type u_1<VAR>l : List (Option α)<GOAL>(none :: l).reduceOption = l.reduceOption
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : List (Option α)<VAR>f : α → β<GOAL>(List.map (Option.map f) l).reduceOption = List.map f l.reduceOption
<VAR>α : Type u_1<VAR>l l' : List (Option α)<GOAL>(l ++ l').reduceOption = l.reduceOption ++ l'.reduceOption
<VAR>α : Type u_1<VAR>l : List (Option α)<GOAL>l.reduceOption.length = (List.filter Option.isSome l).length
<VAR>α : Type u_1<VAR>l : List (Option α)<GOAL>l.length = l.reduceOption.length + (List.filter Option.isNone l).length
<VAR>α : Type u_1<VAR>l : List (Option α)<GOAL>l.reduceOption.length ≤ l.length
<VAR>α : Type u_1<VAR>l : List (Option α)<GOAL>l.reduceOption.length = l.length ↔ ∀ (x : Option α), x ∈ l → x.isSome = true
<VAR>α : Type u_1<VAR>l : List (Option α)<GOAL>l.reduceOption.length < l.length ↔ none ∈ l
<VAR>α : Type u_1<VAR>x : Option α<GOAL>[x].reduceOption = x.toList
<VAR>α : Type u_1<VAR>l : List (Option α)<VAR>x : Option α<GOAL>(l.concat x).reduceOption = l.reduceOption ++ x.toList
<VAR>α : Type u_1<VAR>l : List (Option α)<VAR>x : α<GOAL>(l.concat (some x)).reduceOption = l.reduceOption.concat x
<VAR>α : Type u_1<VAR>l : List (Option α)<VAR>x : α<GOAL>x ∈ l.reduceOption ↔ some x ∈ l
<VAR>α : Type u_1<VAR>l : List (Option α)<VAR>x : α<GOAL>(∃ i, l.get? i = some (some x)) ↔ ∃ i, l.reduceOption.get? i = some x
<VAR>α : Type u_1<VAR>a : α<VAR>l : List α<GOAL>l <+: l.concat a
<VAR>α : Type u_1<VAR>l₁ l₂ : List α<VAR>a : α<GOAL>l₁ <+: l₂ ++ [a] ↔ l₁ = l₂ ++ [a] ∨ l₁ <+: l₂
<VAR>α : Type u_1<VAR>l₁ l₂ : List α<VAR>h : l₁ <:+: l₂<GOAL>l₁.length = l₂.length → l₁ = l₂
<VAR>α : Type u_1<VAR>l₁ l₂ : List α<VAR>h : l₁ <+: l₂<GOAL>l₁.length = l₂.length → l₁ = l₂
<VAR>α : Type u_1<VAR>l₁ l₂ : List α<VAR>h : l₁ <:+ l₂<GOAL>l₁.length = l₂.length → l₁ = l₂
<VAR>α : Type u_1<VAR>n m : ℕ<VAR>l : List α<GOAL>(List.dropSlice n m l).Sublist l
<VAR>α : Type u_1<VAR>n m : ℕ<VAR>l : List α<GOAL>List.dropSlice n m l ⊆ l
<VAR>α : Type u_1<VAR>n m : ℕ<VAR>l : List α<VAR>a : α<VAR>h : a ∈ List.dropSlice n m l<GOAL>a ∈ l
<VAR>α : Type u_1<VAR>l : List α<VAR>p : α → Bool<GOAL>List.takeWhile p l <+: l
<VAR>α : Type u_1<VAR>l : List α<VAR>p : α → Bool<GOAL>List.dropWhile p l <:+ l
<VAR>α : Type u_1<VAR>l : List α<GOAL>l.dropLast <+: l
<VAR>α : Type u_1<VAR>l : List α<GOAL>l.tail <:+ l
<VAR>α : Type u_1<VAR>l : List α<GOAL>l.dropLast.Sublist l
<VAR>α : Type u_1<VAR>l : List α<VAR>m n : ℕ<VAR>h : m ≤ n<GOAL>(List.drop n l).Sublist (List.drop m l)
<VAR>α : Type u_1<VAR>l : List α<GOAL>l.dropLast ⊆ l
<VAR>α : Type u_1<VAR>l : List α<GOAL>l.tail ⊆ l
<VAR>α : Type u_1<VAR>l : List α<VAR>a : α<VAR>h : a ∈ l.dropLast<GOAL>a ∈ l
<VAR>α : Type u_1<VAR>l : List α<VAR>a : α<VAR>h : a ∈ l.tail<GOAL>a ∈ l
<VAR>α : Type u_1<VAR>l₁ l₂ : List α<GOAL>l₁.Sublist l₂ → ∀ (n : ℕ), (List.drop n l₁).Sublist (List.drop n l₂)
<VAR>α : Type u_1<VAR>l₁ l₂ : List α<GOAL>l₁ <+: l₂ ↔ l₁ ++ List.drop l₁.length l₂ = l₂
<VAR>α : Type u_1<VAR>l₁ l₂ : List α<GOAL>l₁ <:+ l₂ ↔ List.take (l₂.length - l₁.length) l₂ ++ l₁ = l₂
<VAR>α : Type u_1<VAR>l₁ l₂ : List α<GOAL>l₁ <+: l₂ ↔ l₁ = List.take l₁.length l₂
<VAR>α : Type u_1<VAR>x y : List α<VAR>n : ℕ<GOAL>x <+: List.take n y ↔ x <+: y ∧ x.length ≤ n
<VAR>α : Type u_1<VAR>x y : List α<VAR>h : x <+: y<VAR>hl : x.length < y.length<GOAL>x ++ [y.get ⟨x.length, hl⟩] <+: y
<VAR>α : Type u_1<VAR>l₁ l₂ : List α<GOAL>l₁ <:+ l₂ ↔ l₁ = List.drop (l₂.length - l₁.length) l₂
<VAR>α : Type u_1<VAR>m n : ℕ<VAR>L : List (List (Option α))<VAR>hm : m < L.length<GOAL>List.take m L <+: List.take n L ↔ m ≤ n
<VAR>α : Type u_1<VAR>l₁ l₂ : List α<VAR>a b : α<GOAL>a :: l₁ <+: b :: l₂ ↔ a = b ∧ l₁ <+: l₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l₁ l₂ : List α<VAR>h : l₁ <+: l₂<VAR>f : α → β<GOAL>List.map f l₁ <+: List.map f l₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l₁ l₂ : List α<VAR>h : l₁ <+: l₂<VAR>f : α → Option β<GOAL>List.filterMap f l₁ <+: List.filterMap f l₂
<VAR>α : Type u_1<VAR>l₁ l₂ : List (Option α)<VAR>h : l₁ <+: l₂<GOAL>l₁.reduceOption <+: l₂.reduceOption
<VAR>α : Type u_1<VAR>s t : List α<GOAL>s ∈ t.inits ↔ s <+: t
<VAR>α : Type u_1<VAR>s t : List α<GOAL>s ∈ t.tails ↔ s <:+ t
<VAR>α : Type u_1<VAR>a : α<VAR>l : List α<GOAL>(a :: l).inits = [] :: List.map (fun t => a :: t) l.inits
<VAR>α : Type u_1<VAR>a : α<VAR>l : List α<GOAL>(a :: l).tails = (a :: l) :: l.tails
<VAR>α : Type u_1<VAR>s t : List α<GOAL>(s ++ t).inits = s.inits ++ List.map (fun l => s ++ l) t.inits.tail
<VAR>α : Type u_1<VAR>s t : List α<GOAL>(s ++ t).tails = List.map (fun l => l ++ t) s.tails ++ t.tails.tail
<VAR>α : Type u_1<VAR>l : List α<GOAL>l.inits = (List.map List.reverse l.reverse.tails).reverse
<VAR>α : Type u_1<VAR>l : List α<GOAL>l.tails = (List.map List.reverse l.reverse.inits).reverse
<VAR>α : Type u_1<VAR>l : List α<GOAL>l.reverse.inits = (List.map List.reverse l.tails).reverse
<VAR>α : Type u_1<VAR>l : List α<GOAL>l.reverse.tails = (List.map List.reverse l.inits).reverse
<VAR>α : Type u_1<VAR>l : List α<GOAL>List.map List.reverse l.inits = l.reverse.tails.reverse
<VAR>α : Type u_1<VAR>l : List α<GOAL>List.map List.reverse l.tails = l.reverse.inits.reverse
<VAR>α : Type u_1<VAR>l : List α<GOAL>l.tails.length = l.length + 1
<VAR>α : Type u_1<VAR>l : List α<GOAL>l.inits.length = l.length + 1
<VAR>α : Type u_1<VAR>l : List α<VAR>n : ℕ<VAR>h : n < l.tails.length<GOAL>l.tails[n] = List.drop n l
<VAR>α : Type u_1<VAR>l : List α<VAR>n : Fin l.tails.length<GOAL>l.tails.get n = List.drop (↑n) l
<VAR>α : Type u_1<VAR>l : List α<VAR>n : ℕ<VAR>h : n < l.inits.length<GOAL>l.inits[n] = List.take n l
<VAR>α : Type u_1<VAR>l : List α<VAR>n : Fin l.inits.length<GOAL>l.inits.get n = List.take (↑n) l
<VAR>α : Type u_1<VAR>l : List α<VAR>n : ℕ<VAR>hn : n < l.tails.length<GOAL>l.tails.nthLe n hn = List.drop n l
<VAR>α : Type u_1<VAR>l : List α<VAR>n : ℕ<VAR>hn : n < l.inits.length<GOAL>l.inits.nthLe n hn = List.take n l
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>l : List α<GOAL>insert a l = if a ∈ l then l else a :: l
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>l : List α<GOAL>l <:+ List.insert a l
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>l : List α<GOAL>l <:+: List.insert a l
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>l : List α<GOAL>l.Sublist (List.insert a l)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>l : List α<GOAL>l ⊆ List.insert a l
<VAR>α : Type u_1<VAR>l₁ l₂ : List α<VAR>a : α<VAR>hx : a ∈ l₁<VAR>hl : l₁ <:+ l₂<GOAL>a ∈ l₂
<VAR>α : Type u_1<VAR>x y : List α<VAR>h : x <+: y<VAR>hx : x ≠ []<GOAL>y ≠ []
<VAR>α : Type u_1<VAR>x y : List α<VAR>h : x <+: y<VAR>n : ℕ<VAR>hn : n < x.length<GOAL>x[n] = y[n]
<VAR>α : Type u_1<VAR>x y : List α<VAR>h : x <+: y<VAR>n : ℕ<VAR>hn : n < x.length<GOAL>x.get ⟨n, hn⟩ = y.get ⟨n, ⋯⟩
<VAR>α : Type u_1<VAR>x y : List α<VAR>h : x <+: y<VAR>hx : x ≠ []<GOAL>x.head hx = y.head ⋯
<VAR>α : Type u_1<VAR>L : List (List α)<VAR>f : List α<GOAL>f ∈ L.sections ↔ List.Forall₂ (fun x x_1 => x ∈ x_1) f L
<VAR>α : Type u_1<VAR>L : List (List α)<VAR>f : List α<VAR>h : f ∈ L.sections<GOAL>f.length = L.length
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → β → Prop<GOAL>(List.Forall₂ (List.Forall₂ r) ⇒ List.Forall₂ (List.Forall₂ r)) List.sections List.sections
<VAR>α : Type u<VAR>a : α<VAR>l : List α<GOAL>(∀ a' ∈ l, ¬a = a') ↔ a ∉ l
<VAR>α : Type u<VAR>a : α<VAR>l : List α<GOAL>(a :: l).Nodup ↔ a ∉ l ∧ l.Nodup
<VAR>α : Type u<VAR>l : List α<VAR>r : α → α → Prop<VAR>IsIrrefl α r<VAR>h : List.Pairwise r l<GOAL>l.Nodup
<VAR>α : Type u<VAR>β : Type v<VAR>r : α → β → Prop<VAR>hr : Relator.BiUnique r<GOAL>(List.Forall₂ r ⇒ fun x x_1 => x ↔ x_1) List.Nodup List.Nodup
<VAR>α : Type u<VAR>l : List α<VAR>a : α<VAR>ha : a ∉ l<VAR>hl : l.Nodup<GOAL>(a :: l).Nodup
<VAR>α : Type u<VAR>a : α<GOAL>[a].Nodup
<VAR>α : Type u<VAR>l : List α<VAR>a : α<VAR>h : (a :: l).Nodup<GOAL>l.Nodup
<VAR>α : Type u<VAR>l : List α<VAR>a : α<VAR>h : (a :: l).Nodup<GOAL>a ∉ l
<VAR>α : Type u<VAR>l : List α<VAR>a : α<GOAL>a ∈ l → ¬(a :: l).Nodup
<VAR>α : Type u<VAR>l₁ l₂ : List α<GOAL>l₁.Sublist l₂ → l₂.Nodup → l₁.Nodup
<VAR>α : Type u<VAR>a : α<GOAL>¬[a, a].Nodup
<VAR>α : Type u<VAR>l : List α<GOAL>l.Nodup ↔ ∀ (a : α), ¬[a, a].Sublist l
<VAR>α : Type u<VAR>l : List α<GOAL>l.Nodup ↔ Function.Injective fun i => l[↑i]
<VAR>α : Type u<VAR>l : List α<GOAL>l.Nodup ↔ Function.Injective l.get
<VAR>α : Type u<VAR>l : List α<GOAL>l.Nodup ↔ ∀ (i j : ℕ) (h₁ : i < l.length) (h₂ : j < l.length), l.nthLe i h₁ = l.nthLe j h₂ → i = j
<VAR>α : Type u<VAR>l : List α<VAR>h : l.Nodup<VAR>i j : Fin l.length<GOAL>l.get i = l.get j ↔ i = j
<VAR>α : Type u<VAR>l : List α<VAR>h : l.Nodup<VAR>i : ℕ<VAR>hi : i < l.length<VAR>j : ℕ<VAR>hj : j < l.length<GOAL>l[i] = l[j] ↔ i = j
<VAR>α : Type u<VAR>l : List α<VAR>h : l.Nodup<VAR>i j : ℕ<VAR>hi : i < l.length<VAR>hj : j < l.length<GOAL>l.nthLe i hi = l.nthLe j hj ↔ i = j
<VAR>α : Type u<VAR>l : List α<GOAL>l.Nodup ↔ ∀ (i j : ℕ), i < j → j < l.length → l[i]? ≠ l[j]?
<VAR>α : Type u<VAR>l : List α<GOAL>l.Nodup ↔ ∀ (i j : ℕ), i < j → j < l.length → l.get? i ≠ l.get? j
<VAR>α : Type u<VAR>l : List α<VAR>h : l.Nodup<VAR>x : α<GOAL>l ≠ [x] ↔ l = [] ∨ ∃ y ∈ l, y ≠ x
<VAR>α : Type u<VAR>xs : List α<VAR>n m : Fin xs.length<VAR>h : xs.get n = xs.get m<VAR>hne : n ≠ m<GOAL>¬xs.Nodup
<VAR>α : Type u<VAR>DecidableEq α<VAR>l : List α<VAR>H : l.Nodup<VAR>i : ℕ<VAR>h : i < l.length<GOAL>List.indexOf l[i] l = i
<VAR>α : Type u<VAR>DecidableEq α<VAR>l : List α<VAR>H : l.Nodup<VAR>i : Fin l.length<GOAL>List.indexOf (l.get i) l = ↑i
<VAR>α : Type u<VAR>DecidableEq α<VAR>l : List α<GOAL>l.Nodup ↔ ∀ (a : α), List.count a l ≤ 1
<VAR>α : Type u<VAR>l : List α<VAR>DecidableEq α<GOAL>l.Nodup ↔ ∀ a ∈ l, List.count a l = 1
<VAR>α : Type u<VAR>a : α<VAR>n : ℕ<GOAL>(List.replicate n a).Nodup ↔ n ≤ 1
<VAR>α : Type u<VAR>DecidableEq α<VAR>a : α<VAR>l : List α<VAR>d : l.Nodup<VAR>h : a ∈ l<GOAL>List.count a l = 1
<VAR>α : Type u<VAR>DecidableEq α<VAR>a : α<VAR>l : List α<VAR>d : l.Nodup<GOAL>List.count a l = if a ∈ l then 1 else 0
<VAR>α : Type u<VAR>l₁ l₂ : List α<GOAL>(l₁ ++ l₂).Nodup → l₁.Nodup
<VAR>α : Type u<VAR>l₁ l₂ : List α<GOAL>(l₁ ++ l₂).Nodup → l₂.Nodup
<VAR>α : Type u<VAR>l₁ l₂ : List α<GOAL>(l₁ ++ l₂).Nodup ↔ l₁.Nodup ∧ l₂.Nodup ∧ l₁.Disjoint l₂
<VAR>α : Type u<VAR>l₁ l₂ : List α<VAR>d : (l₁ ++ l₂).Nodup<GOAL>l₁.Disjoint l₂
<VAR>α : Type u<VAR>l₁ l₂ : List α<VAR>d₁ : l₁.Nodup<VAR>d₂ : l₂.Nodup<VAR>dj : l₁.Disjoint l₂<GOAL>(l₁ ++ l₂).Nodup
<VAR>α : Type u<VAR>l₁ l₂ : List α<GOAL>(l₁ ++ l₂).Nodup ↔ (l₂ ++ l₁).Nodup
<VAR>α : Type u<VAR>a : α<VAR>l₁ l₂ : List α<GOAL>(l₁ ++ a :: l₂).Nodup ↔ (a :: (l₁ ++ l₂)).Nodup
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>l : List α<GOAL>(List.map f l).Nodup → l.Nodup
<VAR>α : Type u<VAR>β : Type v<VAR>l : List α<VAR>f : α → β<VAR>H : ∀ x ∈ l, ∀ y ∈ l, f x = f y → x = y<VAR>d : l.Nodup<GOAL>(List.map f l).Nodup
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>l : List α<VAR>d : (List.map f l).Nodup<VAR>x : α<GOAL>x ∈ l → ∀ ⦃y : α⦄, y ∈ l → f x = f y → x = y
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>l : List α<VAR>d : l.Nodup<GOAL>(List.map f l).Nodup ↔ ∀ x ∈ l, ∀ y ∈ l, f x = f y → x = y
<VAR>α : Type u<VAR>β : Type v<VAR>l : List α<VAR>f : α → β<VAR>hf : Function.Injective f<GOAL>l.Nodup → (List.map f l).Nodup
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>l : List α<VAR>hf : Function.Injective f<GOAL>(List.map f l).Nodup ↔ l.Nodup
<VAR>α : Type u<VAR>l : List α<GOAL>l.attach.Nodup ↔ l.Nodup
<VAR>α : Type u<VAR>β : Type v<VAR>p : α → Prop<VAR>f : (a : α) → p a → β<VAR>l : List α<VAR>H : ∀ a ∈ l, p a<VAR>hf : ∀ (a : α) (ha : p a) (b : α) (hb : p b), f a ha = f b hb → a = b<VAR>h : l.Nodup<GOAL>(List.pmap f l H).Nodup
<VAR>α : Type u<VAR>p : α → Bool<VAR>l : List α<GOAL>l.Nodup → (List.filter p l).Nodup
<VAR>α : Type u<VAR>l : List α<GOAL>l.reverse.Nodup ↔ l.Nodup
<VAR>α : Type u<VAR>DecidableEq α<VAR>l : List α<VAR>d : l.Nodup<VAR>a : α<GOAL>l.erase a = List.filter (fun x => decide (x ≠ a)) l
<VAR>α : Type u<VAR>l : List α<VAR>DecidableEq α<VAR>a : α<GOAL>l.Nodup → (l.erase a).Nodup
<VAR>α : Type u<VAR>DecidableEq α<VAR>l : List α<VAR>hl : l.Nodup<VAR>i : ℕ<VAR>h : i < l.length<GOAL>l.erase l[i] = l.eraseIdx i
<VAR>α : Type u<VAR>DecidableEq α<VAR>l : List α<VAR>hl : l.Nodup<VAR>i : Fin l.length<GOAL>l.erase (l.get i) = l.eraseIdx ↑i
<VAR>α : Type u<VAR>l₁ l₂ : List α<VAR>DecidableEq α<GOAL>l₁.Nodup → (l₁.diff l₂).Nodup
<VAR>α : Type u<VAR>l : List α<VAR>a b : α<VAR>DecidableEq α<VAR>d : l.Nodup<GOAL>a ∈ l.erase b ↔ a ≠ b ∧ a ∈ l
<VAR>α : Type u<VAR>l : List α<VAR>a : α<VAR>DecidableEq α<VAR>h : l.Nodup<GOAL>a ∉ l.erase a
<VAR>α : Type u<VAR>L : List (List α)<GOAL>L.join.Nodup ↔ (∀ l ∈ L, l.Nodup) ∧ List.Pairwise List.Disjoint L
<VAR>α : Type u<VAR>β : Type v<VAR>l₁ : List α<VAR>f : α → List β<GOAL>(l₁.bind f).Nodup ↔ (∀ x ∈ l₁, (f x).Nodup) ∧ List.Pairwise (fun a b => (f a).Disjoint (f b)) l₁
<VAR>α : Type u<VAR>β : Type v<VAR>l₁ : List α<VAR>l₂ : List β<VAR>d₁ : l₁.Nodup<VAR>d₂ : l₂.Nodup<GOAL>(l₁ ×ˢ l₂).Nodup
<VAR>α : Type u<VAR>l₁ : List α<VAR>σ : α → Type u_1<VAR>l₂ : (a : α) → List (σ a)<VAR>d₁ : l₁.Nodup<VAR>d₂ : ∀ (a : α), (l₂ a).Nodup<GOAL>(l₁.sigma l₂).Nodup
<VAR>α : Type u<VAR>β : Type v<VAR>l : List α<VAR>f : α → Option β<VAR>h : ∀ (a a' : α), ∀ b ∈ f a, b ∈ f a' → a = a'<GOAL>l.Nodup → (List.filterMap f l).Nodup
<VAR>α : Type u<VAR>l : List α<VAR>a : α<VAR>h : a ∉ l<VAR>h' : l.Nodup<GOAL>(l.concat a).Nodup
<VAR>α : Type u<VAR>l : List α<VAR>a : α<VAR>DecidableEq α<VAR>h : l.Nodup<GOAL>(List.insert a l).Nodup
<VAR>α : Type u<VAR>l₂ : List α<VAR>DecidableEq α<VAR>l₁ : List α<VAR>h : l₂.Nodup<GOAL>(l₁ ∪ l₂).Nodup
<VAR>α : Type u<VAR>l₁ : List α<VAR>DecidableEq α<VAR>l₂ : List α<GOAL>l₁.Nodup → (l₁ ∩ l₂).Nodup
<VAR>α : Type u<VAR>DecidableEq α<VAR>l₁ l₂ : List α<GOAL>l₁.Nodup → l₁.diff l₂ = List.filter (fun x => decide (x ∉ l₂)) l₁
<VAR>α : Type u<VAR>l₁ l₂ : List α<VAR>a : α<VAR>DecidableEq α<VAR>hl₁ : l₁.Nodup<GOAL>a ∈ l₁.diff l₂ ↔ a ∈ l₁ ∧ a ∉ l₂
<VAR>α : Type u<VAR>l : List α<VAR>n : ℕ<VAR>a : α<GOAL>l.Nodup → a ∉ l → (l.set n a).Nodup
<VAR>α : Type u<VAR>β : Type v<VAR>DecidableEq α<VAR>l : List α<VAR>hl : l.Nodup<VAR>f : α → β<VAR>x : α<VAR>y : β<GOAL>List.map (Function.update f x y) l = if x ∈ l then (List.map f l).set (List.indexOf x l) y else List.map f l
<VAR>α : Type u<VAR>l : List α<VAR>r : α → α → Prop<VAR>hl : l.Nodup<VAR>h : ∀ a ∈ l, ∀ b ∈ l, a ≠ b → r a b<GOAL>List.Pairwise r l
<VAR>α : Type u<VAR>l : List α<VAR>r : α → α → Prop<VAR>hl : l.Nodup<VAR>h : {x | x ∈ l}.Pairwise r<GOAL>List.Pairwise r l
<VAR>α : Type u<VAR>l : List α<VAR>r : α → α → Prop<VAR>IsSymm α r<VAR>hl : l.Nodup<GOAL>{a | a ∈ l}.Pairwise r ↔ List.Pairwise r l
<VAR>α : Type u<VAR>DecidableEq α<VAR>l : List α<VAR>n : ℕ<GOAL>l.Nodup → List.take n l = List.filter (fun a => List.elem a (List.take n l)) l
<VAR>α : Type u<VAR>o : Option α<GOAL>o.toList.Nodup
<VAR>α : Type u_1<VAR>n : ℕ<GOAL>[].rdrop n = []
<VAR>α : Type u_1<VAR>l : List α<GOAL>l.rdrop 0 = l
<VAR>α : Type u_1<VAR>l : List α<VAR>n : ℕ<GOAL>l.rdrop n = (List.drop n l.reverse).reverse
<VAR>α : Type u_1<VAR>l : List α<VAR>n : ℕ<VAR>x : α<GOAL>(l ++ [x]).rdrop (n + 1) = l.rdrop n
<VAR>α : Type u_1<VAR>n : ℕ<GOAL>[].rtake n = []
<VAR>α : Type u_1<VAR>l : List α<GOAL>l.rtake 0 = []
<VAR>α : Type u_1<VAR>l : List α<VAR>n : ℕ<GOAL>l.rtake n = (List.take n l.reverse).reverse
<VAR>α : Type u_1<VAR>l : List α<VAR>n : ℕ<VAR>x : α<GOAL>(l ++ [x]).rtake (n + 1) = l.rtake n ++ [x]
<VAR>α : Type u_1<VAR>p : α → Bool<GOAL>List.rdropWhile p [] = []
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>l : List α<VAR>x : α<GOAL>List.rdropWhile p (l ++ [x]) = if p x = true then List.rdropWhile p l else l ++ [x]
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>l : List α<VAR>x : α<VAR>h : p x = true<GOAL>List.rdropWhile p (l ++ [x]) = List.rdropWhile p l
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>l : List α<VAR>x : α<VAR>h : ¬p x = true<GOAL>List.rdropWhile p (l ++ [x]) = l ++ [x]
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>x : α<GOAL>List.rdropWhile p [x] = if p x = true then [] else [x]
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>l : List α<VAR>hl : List.rdropWhile p l ≠ []<GOAL>¬p ((List.rdropWhile p l).getLast hl) = true
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>l : List α<GOAL>List.rdropWhile p l <+: l
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>l : List α<GOAL>List.rdropWhile p l = [] ↔ ∀ (x : α), x ∈ l → p x = true
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>l : List α<GOAL>List.dropWhile p l = l ↔ ∀ (hl : 0 < l.length), ¬p (l.get ⟨0, hl⟩) = true
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>l : List α<GOAL>List.rdropWhile p l = l ↔ ∀ (hl : l ≠ []), ¬p (l.getLast hl) = true