ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>l : List α<GOAL>List.dropWhile p (List.dropWhile p l) = List.dropWhile p l
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>l : List α<GOAL>List.rdropWhile p (List.rdropWhile p l) = List.rdropWhile p l
<VAR>α : Type u_1<VAR>p : α → Bool<GOAL>List.rtakeWhile p [] = []
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>l : List α<VAR>x : α<GOAL>List.rtakeWhile p (l ++ [x]) = if p x = true then List.rtakeWhile p l ++ [x] else []
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>l : List α<VAR>x : α<VAR>h : p x = true<GOAL>List.rtakeWhile p (l ++ [x]) = List.rtakeWhile p l ++ [x]
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>l : List α<VAR>x : α<VAR>h : ¬p x = true<GOAL>List.rtakeWhile p (l ++ [x]) = []
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>l : List α<GOAL>List.rtakeWhile p l <:+ l
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>l : List α<GOAL>List.rtakeWhile p l = l ↔ ∀ (x : α), x ∈ l → p x = true
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>l : List α<GOAL>List.rtakeWhile p l = [] ↔ ∀ (hl : l ≠ []), ¬p (l.getLast hl) = true
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>l : List α<VAR>x : α<VAR>hx : x ∈ List.rtakeWhile p l<GOAL>p x = true
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>l : List α<GOAL>List.rtakeWhile p (List.rtakeWhile p l) = List.rtakeWhile p l
<VAR>α : Type u_1<VAR>l : List α<VAR>i j : ℕ<GOAL>(l.rdrop i).rdrop j = l.rdrop (i + j)
<VAR>α : Type u_1<VAR>l₁ l₂ : List α<GOAL>(l₁ ++ l₂).rdrop l₂.length = l₁
<VAR>α : Type u_1<VAR>l₁ l₂ : List α<VAR>k : ℕ<GOAL>k ≤ l₂.length → (l₁ ++ l₂).rdrop k = l₁ ++ l₂.rdrop k
<VAR>α : Type u_1<VAR>l₁ l₂ : List α<VAR>k : ℕ<GOAL>(l₁ ++ l₂).rdrop (l₂.length + k) = l₁.rdrop k
<VAR>α : Type u_1<VAR>f : α → α<VAR>a : α<VAR>n : ℕ<GOAL>(List.iterate f a n).length = n
<VAR>α : Type u_1<VAR>f : α → α<VAR>a : α<VAR>n : ℕ<GOAL>List.iterate f a n = [] ↔ n = 0
<VAR>α : Type u_1<VAR>f : α → α<VAR>a : α<VAR>n i : ℕ<GOAL>i < n → (List.iterate f a n)[i]? = some (f^[i] a)
<VAR>α : Type u_1<VAR>f : α → α<VAR>a : α<VAR>n i : ℕ<VAR>h : i < n<GOAL>(List.iterate f a n).get? i = some (f^[i] a)
<VAR>α : Type u_1<VAR>f : α → α<VAR>a : α<VAR>n i : ℕ<VAR>h : i < (List.iterate f a n).length<GOAL>(List.iterate f a n)[i] = f^[i] a
<VAR>α : Type u_1<VAR>f : α → α<VAR>a : α<VAR>n : ℕ<VAR>i : Fin (List.iterate f a n).length<GOAL>(List.iterate f a n).get i = f^[↑i] a
<VAR>α : Type u_1<VAR>f : α → α<VAR>a : α<VAR>n : ℕ<VAR>b : α<GOAL>b ∈ List.iterate f a n ↔ ∃ m < n, b = f^[m] a
<VAR>α : Type u_1<VAR>n : ℕ<VAR>f : α → α<VAR>a : α<GOAL>List.map (fun x => f^[x] a) (List.range n) = List.iterate f a n
<VAR>α : Type u_1<VAR>f : α → α<VAR>a : α<VAR>m n : ℕ<GOAL>List.iterate f a (m + n) = List.iterate f a m ++ List.iterate f (f^[m] a) n
<VAR>α : Type u_1<VAR>f : α → α<VAR>a : α<VAR>m n : ℕ<GOAL>List.take m (List.iterate f a n) = List.iterate f a (min m n)
<VAR>X : AlgebraicGeometry.Scheme<VAR>U : X.Opens<VAR>self : ↥U<GOAL>U.ι.val.base self = ↑self
<VAR>X : AlgebraicGeometry.Scheme<VAR>U : X.Opens<GOAL>↑↑(↑U).toPresheafedSpace = ↑↑U
<VAR>X : AlgebraicGeometry.Scheme<VAR>U : X.Opens<VAR>V : (↑U).Opens<GOAL>(↑U).presheaf.obj (Opposite.op V) = X.presheaf.obj (Opposite.op ((AlgebraicGeometry.Scheme.Hom.opensFunctor U.ι).obj V))
<VAR>X : AlgebraicGeometry.Scheme<VAR>U : X.Opens<VAR>V W : (TopologicalSpace.Opens ↑↑(↑U).toPresheafedSpace)ᵒᵖ<VAR>i : V ⟶ W<GOAL>(↑U).presheaf.map i = X.presheaf.map ((AlgebraicGeometry.Scheme.Hom.opensFunctor U.ι).map i.unop).op
<VAR>X : AlgebraicGeometry.Scheme<VAR>U V : X.Opens<GOAL>AlgebraicGeometry.Scheme.Hom.app U.ι V = X.presheaf.map (CategoryTheory.homOfLE ⋯).op
<VAR>X : AlgebraicGeometry.Scheme<VAR>U V : X.Opens<VAR>W : (↑U).Opens<VAR>e : W ≤ (TopologicalSpace.Opens.map U.ι.val.base).obj V<GOAL>AlgebraicGeometry.Scheme.Hom.appLE U.ι V W e = X.presheaf.map (CategoryTheory.homOfLE ⋯).op
<VAR>X : AlgebraicGeometry.Scheme<VAR>U : X.Opens<VAR>V : (↑U).Opens<GOAL>AlgebraicGeometry.Scheme.Hom.appIso U.ι V = CategoryTheory.Iso.refl (X.presheaf.obj (Opposite.op ((AlgebraicGeometry.Scheme.Hom.opensFunctor U.ι).obj V)))
<VAR>X : AlgebraicGeometry.Scheme<VAR>U : X.Opens<GOAL>AlgebraicGeometry.Scheme.Hom.opensRange U.ι = U
<VAR>X : AlgebraicGeometry.Scheme<VAR>U : X.Opens<GOAL>Set.range ⇑U.ι.val.base = ↑U
<VAR>X : AlgebraicGeometry.Scheme<VAR>U : X.Opens<GOAL>(AlgebraicGeometry.Scheme.Hom.opensFunctor U.ι).obj ⊤ = U
<VAR>X : AlgebraicGeometry.Scheme<VAR>U : X.Opens<GOAL>(TopologicalSpace.Opens.map U.ι.val.base).obj U = ⊤
<VAR>X : AlgebraicGeometry.Scheme<VAR>U : X.Opens<GOAL>AlgebraicGeometry.Scheme.Hom.app U.ι U = X.presheaf.map (CategoryTheory.eqToHom ⋯).op
<VAR>X : AlgebraicGeometry.Scheme<VAR>U : X.Opens<VAR>V W : (↑U).Opens<VAR>e : (AlgebraicGeometry.Scheme.Hom.opensFunctor U.ι).obj V = (AlgebraicGeometry.Scheme.Hom.opensFunctor U.ι).obj W<GOAL>X.presheaf.map (CategoryTheory.eqToHom e).op = (↑U).presheaf.map (CategoryTheory.eqToHom ⋯).op
<VAR>X : AlgebraicGeometry.Scheme<VAR>U : X.Opens<GOAL>Nonempty ↑↑(↑U).toPresheafedSpace ↔ (↑U).Nonempty
<VAR>X : AlgebraicGeometry.Scheme<VAR>U : X.Opens<GOAL>U.topIso.inv = X.presheaf.map (CategoryTheory.eqToHom ⋯).op
<VAR>X : AlgebraicGeometry.Scheme<VAR>U : X.Opens<GOAL>U.topIso.hom = X.presheaf.map (CategoryTheory.eqToHom ⋯).op
<VAR>X : AlgebraicGeometry.Scheme<VAR>U : X.Opens<VAR>V : (↑U).Opens<VAR>x : ↥V<GOAL>(↑U).presheaf.germ x ≫ (U.stalkIso ↑x).hom = X.presheaf.germ ⟨↑↑x, ⋯⟩
<VAR>X : AlgebraicGeometry.Scheme<VAR>U : X.Opens<VAR>V : TopologicalSpace.Opens ↑↑(↑U).toPresheafedSpace<VAR>x : ↥U<VAR>hx : x ∈ V<GOAL>(↑U).presheaf.germ ⟨x, hx⟩ ≫ (U.stalkIso x).hom = X.presheaf.germ ⟨↑x, ⋯⟩
<VAR>X : AlgebraicGeometry.Scheme<VAR>U : X.Opens<VAR>V : (↑U).Opens<VAR>x : ↥U<VAR>hx : x ∈ V<GOAL>X.presheaf.germ ⟨↑x, ⋯⟩ ≫ (U.stalkIso x).inv = (↑U).presheaf.germ ⟨x, hx⟩
<VAR>s : Type u_1<VAR>X : AlgebraicGeometry.Scheme<VAR>U : s → X.Opens<VAR>hU : ⨆ i, U i = ⊤<GOAL>(X.openCoverOfISupEqTop U hU).J = s
<VAR>s : Type u_1<VAR>X : AlgebraicGeometry.Scheme<VAR>U : s → X.Opens<VAR>hU : ⨆ i, U i = ⊤<VAR>i : s<GOAL>(X.openCoverOfISupEqTop U hU).obj i = ↑(U i)
<VAR>s : Type u_1<VAR>X : AlgebraicGeometry.Scheme<VAR>U : s → X.Opens<VAR>hU : ⨆ i, U i = ⊤<VAR>i : s<GOAL>(X.openCoverOfISupEqTop U hU).map i = (U i).ι
<VAR>X : AlgebraicGeometry.Scheme<VAR>U : X.Opens<GOAL>∀ (a : (↑U).Opens), ↑↑((AlgebraicGeometry.opensRestrict U) a) = ⇑U.ι.val.base '' ↑a
<VAR>X : AlgebraicGeometry.Scheme<VAR>U : X.Opens<GOAL>∀ (a : { V // V ≤ U }), ↑((AlgebraicGeometry.opensRestrict U).symm a) = ⇑U.ι.val.base ⁻¹' ↑↑((Equiv.subtypeEquivProp ⋯).symm a)
<VAR>X : AlgebraicGeometry.Scheme<VAR>U : X.Opens<VAR>r : ↑((↑U).presheaf.obj (Opposite.op ⊤))<GOAL>(AlgebraicGeometry.Scheme.Hom.opensFunctor U.ι).obj ((↑U).basicOpen r) = X.basicOpen ((X.presheaf.map (CategoryTheory.eqToHom ⋯).op) r)
<VAR>X : AlgebraicGeometry.Scheme<VAR>U : X.Opens<VAR>r : ↑((↑U).presheaf.obj (Opposite.op ⊤))<GOAL>(AlgebraicGeometry.Scheme.Hom.opensFunctor U.ι).obj ((↑U).basicOpen r) = X.basicOpen r
<VAR>X : AlgebraicGeometry.Scheme<VAR>U : X.Opens<VAR>r : ↑(X.presheaf.obj (Opposite.op U))<GOAL>(AlgebraicGeometry.Scheme.Hom.opensFunctor U.ι).obj ((↑U).basicOpen (U.topIso.inv r)) = X.basicOpen r
<VAR>X : AlgebraicGeometry.Scheme<VAR>U : X.Opens<GOAL>(X.restrictFunctor.obj U).left = ↑U
<VAR>X : AlgebraicGeometry.Scheme<VAR>U : X.Opens<GOAL>(X.restrictFunctor.obj U).hom = U.ι
<VAR>X : AlgebraicGeometry.Scheme<VAR>U V : X.Opens<VAR>i : U ⟶ V<GOAL>(X.restrictFunctor.map i).left = AlgebraicGeometry.IsOpenImmersion.lift V.ι U.ι ⋯
<VAR>X : AlgebraicGeometry.Scheme<VAR>U V : X.Opens<VAR>i : U ⟶ V<GOAL>(X.restrictFunctor.map i).left ≫ V.ι = U.ι
<VAR>X : AlgebraicGeometry.Scheme<VAR>U V : X.Opens<VAR>i : U ⟶ V<GOAL>(X.restrictFunctor.map i).left.val.base = (TopologicalSpace.Opens.toTopCat ↑X.toPresheafedSpace).map i
<VAR>X : AlgebraicGeometry.Scheme<VAR>U V : X.Opens<VAR>i : U ⟶ V<VAR>W : (↑V).Opens<GOAL>(AlgebraicGeometry.Scheme.Hom.opensFunctor U.ι).obj ((TopologicalSpace.Opens.map (X.restrictFunctor.map i).left.val.base).obj W) ≤ (AlgebraicGeometry.Scheme.Hom.opensFunctor V.ι).obj W
<VAR>X : AlgebraicGeometry.Scheme<VAR>U V : X.Opens<VAR>i : U ⟶ V<VAR>W : (↑V).Opens<GOAL>AlgebraicGeometry.Scheme.Hom.app (X.restrictFunctor.map i).left W = X.presheaf.map (CategoryTheory.homOfLE ⋯).op
<VAR>X : AlgebraicGeometry.Scheme<GOAL>∀ (X_1 : X.Opensᵒᵖ), AlgebraicGeometry.Scheme.restrictFunctorΓ.inv.app X_1 = X.presheaf.map (CategoryTheory.eqToHom ⋯)
<VAR>X : AlgebraicGeometry.Scheme<GOAL>∀ (X_1 : X.Opensᵒᵖ), AlgebraicGeometry.Scheme.restrictFunctorΓ.hom.app X_1 = X.presheaf.map (CategoryTheory.eqToHom ⋯)
<VAR>X : AlgebraicGeometry.Scheme<VAR>U : X.Opens<VAR>V : (↑U).Opens<GOAL>(X.restrictRestrict U V).hom ≫ ((AlgebraicGeometry.Scheme.Hom.opensFunctor U.ι).obj V).ι = V.ι ≫ U.ι
<VAR>X : AlgebraicGeometry.Scheme<VAR>U : X.Opens<VAR>V : (↑U).Opens<GOAL>(X.restrictRestrict U V).inv ≫ V.ι ≫ U.ι = ((AlgebraicGeometry.Scheme.Hom.opensFunctor U.ι).obj V).ι
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>U : Y.Opens<GOAL>(AlgebraicGeometry.pullbackRestrictIsoRestrict f U).inv ≫ CategoryTheory.Limits.pullback.fst f U.ι = ((TopologicalSpace.Opens.map f.val.base).obj U).ι
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>U : Y.Opens<GOAL>(AlgebraicGeometry.pullbackRestrictIsoRestrict f U).hom ≫ ((TopologicalSpace.Opens.map f.val.base).obj U).ι = CategoryTheory.Limits.pullback.fst f U.ι
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>U : Y.Opens<GOAL>(AlgebraicGeometry.pullbackRestrictIsoRestrict f U).hom ≫ f ∣_ U = CategoryTheory.Limits.pullback.snd f U.ι
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>U : Y.Opens<GOAL>f ∣_ U ≫ U.ι = ((TopologicalSpace.Opens.map f.val.base).obj U).ι ≫ f
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>U : Y.Opens<GOAL>CategoryTheory.IsPullback (f ∣_ U) ((TopologicalSpace.Opens.map f.val.base).obj U).ι U.ι f
<VAR>X : AlgebraicGeometry.Scheme<VAR>U : X.Opens<GOAL>𝟙 X ∣_ U = 𝟙 ↑((TopologicalSpace.Opens.map (𝟙 X).val.base).obj U)
<VAR>X Y Z : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>U : TopologicalSpace.Opens ↑↑Z.toPresheafedSpace<GOAL>(f ≫ g) ∣_ U = f ∣_ (TopologicalSpace.Opens.map g.val.base).obj U ≫ g ∣_ U
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>U : Y.Opens<VAR>x : ↑↑(↑((TopologicalSpace.Opens.map f.val.base).obj U)).toPresheafedSpace<GOAL>Coe.coe ((f ∣_ U).val.base x) = f.val.base ↑x
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>U : Y.Opens<GOAL>⇑(f ∣_ U).val.base = U.carrier.restrictPreimage ⇑f.val.base
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>U : Y.Opens<VAR>V : TopologicalSpace.Opens ↑↑(↑U).toPresheafedSpace<GOAL>(AlgebraicGeometry.Scheme.Hom.opensFunctor ((TopologicalSpace.Opens.map f.val.base).obj U).ι).obj ((TopologicalSpace.Opens.map (f ∣_ U).val.base).obj V) = (TopologicalSpace.Opens.map f.val.base).obj ((AlgebraicGeometry.Scheme.Hom.opensFunctor U.ι).obj V)
<VAR>C : Type u_1<VAR>Preorder C<VAR>X Y : C<VAR>e : X = Y<GOAL>CategoryTheory.eqToHom e = CategoryTheory.homOfLE ⋯
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>U : Y.Opens<VAR>V : (↑U).Opens<GOAL>AlgebraicGeometry.Scheme.Hom.app (f ∣_ U) V = AlgebraicGeometry.Scheme.Hom.app f ((AlgebraicGeometry.Scheme.Hom.opensFunctor U.ι).obj V) ≫ X.presheaf.map (CategoryTheory.eqToHom ⋯).op
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>U : Y.Opens<VAR>V : TopologicalSpace.Opens ↑↑(↑U).toPresheafedSpace<GOAL>AlgebraicGeometry.Scheme.Hom.app (f ∣_ U) V = AlgebraicGeometry.Scheme.Hom.appLE f ((AlgebraicGeometry.Scheme.Hom.opensFunctor U.ι).obj V) ((AlgebraicGeometry.Scheme.Hom.opensFunctor ((TopologicalSpace.Opens.map f.val.base).obj U).ι).obj ((TopologicalSpace.Opens.map (f ∣_ U).val.base).obj V)) ⋯
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>U : Y.Opens<VAR>V : (↑U).Opens<VAR>W : (↑((TopologicalSpace.Opens.map f.val.base).obj U)).Opens<VAR>e : W ≤ (TopologicalSpace.Opens.map (f ∣_ U).val.base).obj V<GOAL>AlgebraicGeometry.Scheme.Hom.appLE (f ∣_ U) V W e = AlgebraicGeometry.Scheme.Hom.appLE f ((AlgebraicGeometry.Scheme.Hom.opensFunctor U.ι).obj V) ((AlgebraicGeometry.Scheme.Hom.opensFunctor ((TopologicalSpace.Opens.map f.val.base).obj U).ι).obj W) ⋯
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>U : Y.Opens<GOAL>AlgebraicGeometry.Scheme.Γ.map (f ∣_ U).op = Y.presheaf.map (CategoryTheory.eqToHom ⋯).op ≫ AlgebraicGeometry.Scheme.Hom.app f U ≫ X.presheaf.map (CategoryTheory.eqToHom ⋯).op
<VAR>X : AlgebraicGeometry.Scheme<VAR>𝒰 : X.OpenCover<VAR>U : X.Opens<GOAL>(𝒰.restrict U).J = 𝒰.J
<VAR>X : AlgebraicGeometry.Scheme<VAR>𝒰 : X.OpenCover<VAR>U : X.Opens<GOAL>∀ (x : 𝒰.J), (𝒰.restrict U).obj x = ↑((TopologicalSpace.Opens.map (𝒰.map x).val.base).obj U)
<VAR>X : AlgebraicGeometry.Scheme<VAR>𝒰 : X.OpenCover<VAR>U : X.Opens<GOAL>∀ (x : 𝒰.J), (𝒰.restrict U).map x = 𝒰.map x ∣_ U
<VAR>α : Type u_1<VAR>l₁ l₂ : List α<VAR>d : l₁.Disjoint l₂<GOAL>l₂.Disjoint l₁
<VAR>α : Type u_1<VAR>l₁ : List α<VAR>a : α<VAR>DecidableEq α<VAR>h : a ∈ l₁<VAR>l₂ : List α<GOAL>a ∈ l₁ ∪ l₂
<VAR>α : Type u_1<VAR>l₂ : List α<VAR>a : α<VAR>DecidableEq α<VAR>l₁ : List α<VAR>h : a ∈ l₂<GOAL>a ∈ l₁ ∪ l₂
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l₁ l₂ : List α<GOAL>∃ t, t.Sublist l₁ ∧ t ++ l₂ = l₁ ∪ l₂
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l₁ l₂ : List α<GOAL>l₂ <:+ l₁ ∪ l₂
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l₁ l₂ : List α<GOAL>(l₁ ∪ l₂).Sublist (l₁ ++ l₂)
<VAR>α : Type u_1<VAR>l₁ l₂ : List α<VAR>p : α → Prop<VAR>DecidableEq α<GOAL>(∀ (x : α), x ∈ l₁ ∪ l₂ → p x) ↔ (∀ (x : α), x ∈ l₁ → p x) ∧ ∀ (x : α), x ∈ l₂ → p x
<VAR>α : Type u_1<VAR>l₁ l₂ : List α<VAR>p : α → Prop<VAR>DecidableEq α<VAR>h : ∀ (x : α), x ∈ l₁ ∪ l₂ → p x<VAR>x : α<GOAL>x ∈ l₁ → p x
<VAR>α : Type u_1<VAR>l₁ l₂ : List α<VAR>p : α → Prop<VAR>DecidableEq α<VAR>h : ∀ (x : α), x ∈ l₁ ∪ l₂ → p x<VAR>x : α<GOAL>x ∈ l₂ → p x
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>xs ys : List α<VAR>h : xs ⊆ ys<GOAL>xs ∪ ys = ys
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<GOAL>[] ∩ l = []
<VAR>α : Type u_1<VAR>l₂ : List α<VAR>a : α<VAR>DecidableEq α<VAR>l₁ : List α<VAR>h : a ∈ l₂<GOAL>(a :: l₁) ∩ l₂ = a :: l₁ ∩ l₂
<VAR>α : Type u_1<VAR>l₂ : List α<VAR>a : α<VAR>DecidableEq α<VAR>l₁ : List α<VAR>h : ¬a ∈ l₂<GOAL>(a :: l₁) ∩ l₂ = l₁ ∩ l₂
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<GOAL>l ∩ [] = []
<VAR>α : Type u_1<VAR>l₁ l₂ : List α<VAR>a : α<VAR>DecidableEq α<GOAL>a ∈ l₁ ∩ l₂ → a ∈ l₁
<VAR>α : Type u_1<VAR>l₁ l₂ : List α<VAR>a : α<VAR>DecidableEq α<VAR>h : a ∈ l₁ ∩ l₂<GOAL>a ∈ l₂
<VAR>α : Type u_1<VAR>l₁ l₂ : List α<VAR>a : α<VAR>DecidableEq α<VAR>h₁ : a ∈ l₁<VAR>h₂ : a ∈ l₂<GOAL>a ∈ l₁ ∩ l₂
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l₁ l₂ : List α<GOAL>l₁ ∩ l₂ ⊆ l₁
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l₁ l₂ : List α<GOAL>l₁ ∩ l₂ ⊆ l₂
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l l₁ l₂ : List α<VAR>h₁ : l ⊆ l₁<VAR>h₂ : l ⊆ l₂<GOAL>l ⊆ l₁ ∩ l₂
<VAR>α : Type u_1<VAR>l₁ l₂ : List α<VAR>DecidableEq α<GOAL>l₁ ∩ l₂ = [] ↔ l₁.Disjoint l₂
<VAR>α : Type u_1<VAR>l₁ : List α<VAR>p : α → Prop<VAR>DecidableEq α<VAR>h : ∀ (x : α), x ∈ l₁ → p x<VAR>l₂ : List α<VAR>x : α<GOAL>x ∈ l₁ ∩ l₂ → p x
<VAR>α : Type u_1<VAR>l₂ : List α<VAR>p : α → Prop<VAR>DecidableEq α<VAR>l₁ : List α<VAR>h : ∀ (x : α), x ∈ l₂ → p x<VAR>x : α<GOAL>x ∈ l₁ ∩ l₂ → p x
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>xs ys : List α<GOAL>xs.inter ys.reverse = xs.inter ys
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>xs ys : List α<VAR>h : xs ⊆ ys<GOAL>xs ∩ ys = xs
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<GOAL>[].bagInter l = []
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<GOAL>l.bagInter [] = []
<VAR>α : Type u_1<VAR>l₂ : List α<VAR>a : α<VAR>DecidableEq α<VAR>l₁ : List α<VAR>h : a ∈ l₂<GOAL>(a :: l₁).bagInter l₂ = a :: l₁.bagInter (l₂.erase a)
<VAR>α : Type u_1<VAR>l₂ : List α<VAR>a : α<VAR>DecidableEq α<VAR>l₁ : List α<VAR>h : ¬a ∈ l₂<GOAL>(a :: l₁).bagInter l₂ = l₁.bagInter l₂
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>l₁ l₂ : List α<GOAL>a ∈ l₁.bagInter l₂ ↔ a ∈ l₁ ∧ a ∈ l₂
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>l₁ l₂ : List α<GOAL>List.count a (l₁.bagInter l₂) = min (List.count a l₁) (List.count a l₂)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l₁ l₂ : List α<GOAL>(l₁.bagInter l₂).Sublist l₁
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l₁ l₂ : List α<GOAL>l₁.bagInter l₂ = [] ↔ l₁ ∩ l₂ = []
<VAR>n : ℕ<GOAL>List.map Fin.val (List.finRange n) = List.range n
<VAR>n : ℕ<GOAL>List.finRange n.succ = 0 :: List.map Fin.succ (List.finRange n)
<VAR>n : ℕ<GOAL>List.finRange n.succ = (List.map Fin.castSucc (List.finRange n)).concat (Fin.last n)
<VAR>α : Type u<VAR>n : ℕ<VAR>f : Fin n → α<GOAL>List.ofFn f = List.pmap (fun i hi => f ⟨i, hi⟩) (List.range n) ⋯
<VAR>n : ℕ<GOAL>List.ofFn id = List.finRange n
<VAR>α : Type u<VAR>n : ℕ<VAR>f : Fin n → α<GOAL>List.ofFn f = List.map f (List.finRange n)
<VAR>α : Type u<VAR>n : ℕ<VAR>f : Fin n → α<VAR>hf : Function.Injective f<GOAL>(List.ofFn f).Nodup
<VAR>α : Type u<VAR>n : ℕ<VAR>f : Fin n → α<GOAL>(List.ofFn f).Nodup ↔ Function.Injective f
<VAR>n : ℕ<VAR>σ : Equiv.Perm (Fin n)<GOAL>List.map (⇑σ) (List.finRange n) ~ List.finRange n
<VAR>n : ℕ<VAR>α : Type u<VAR>σ : Equiv.Perm (Fin n)<VAR>f : Fin n → α<GOAL>List.ofFn (f ∘ ⇑σ) ~ List.ofFn f
<VAR>a b : Prop<VAR>l : List Prop<VAR>h : b ∈ l<GOAL>(a :: l).TFAE ↔ (a ↔ b) ∧ l.TFAE
<VAR>a b : Prop<VAR>l : List Prop<GOAL>(a :: b :: l).TFAE ↔ (a ↔ b) ∧ (b :: l).TFAE
<VAR>b : Prop<VAR>l : List Prop<VAR>h : ∀ (a : Prop), a ∈ l → (a ↔ b)<GOAL>l.TFAE
<VAR>a b : Prop<VAR>l : List Prop<VAR>h_chain : List.Chain (fun x x_1 => x → x_1) a (b :: l)<VAR>h_last : l.getLastD b → a<GOAL>(a :: b :: l).TFAE
<VAR>l : List Prop<VAR>h : l.TFAE<VAR>n₁ n₂ : Nat<VAR>a b : Prop<VAR>h₁ : l.get? n₁ = some a := by rfl<VAR>h₂ : l.get? n₂ = some b := by rfl<GOAL>a ↔ b
<VAR>α : Type u_1<VAR>l : List (α → Prop)<VAR>H : ∀ (a : α), (List.map (fun p => p a) l).TFAE<GOAL>(List.map (fun p => ∀ (a : α), p a) l).TFAE
<VAR>α : Type u_1<VAR>l : List (α → Prop)<VAR>H : ∀ (a : α), (List.map (fun p => p a) l).TFAE<GOAL>(List.map (fun p => ∃ a, p a) l).TFAE
<VAR>l : List Prop<GOAL>(List.map Not l).TFAE ↔ l.TFAE
<VAR>a b : ℤ<GOAL>a ≠ b → a < b ∨ b < a
<VAR>a b : ℤ<GOAL>a < b ∨ b ≤ a
<VAR>a b : ℤ<GOAL>a ≤ b ∨ b < a
<VAR>a b : ℤ<GOAL>a < b → ¬b < a
<VAR>a b : ℤ<VAR>hab : a = b<GOAL>a ≤ b
<VAR>a b : ℤ<VAR>hab : a = b<GOAL>b ≤ a
<VAR>a b : ℤ<GOAL>a = b ↔ a ≤ b ∧ b ≤ a
<VAR>a b : ℤ<GOAL>a ≤ b ↔ a = b ∨ a < b
<VAR>a b : ℤ<GOAL>a ≤ b ↔ a < b ∨ a = b
<VAR>n : ℕ<GOAL>0 ≤ Int.ofNat n
<VAR>a b : ℤ<VAR>h : -a = -b<GOAL>a = b
<VAR>a : ℤ<GOAL>0 < -a ↔ a < 0
<VAR>a : ℤ<GOAL>0 ≤ -a ↔ a ≤ 0
<VAR>a : ℤ<GOAL>-a < 0 ↔ 0 < a
<VAR>a : ℤ<GOAL>-a ≤ 0 ↔ 0 ≤ a
<VAR>a b : ℤ<GOAL>0 < a - b ↔ b < a
<VAR>a b : ℤ<GOAL>0 ≤ a - b ↔ b ≤ a
<VAR>m n : ℕ<GOAL>↑m + ↑n = ↑(m + n)
<VAR>m n : ℕ<GOAL>↑m * ↑n = ↑(m * n)
<VAR>n : ℕ<GOAL>↑n + 1 = ↑n.succ
<VAR>n : ℕ<GOAL>Int.ofNat n = ↑n
<VAR>n : ℕ<GOAL>↑n = Int.ofNat n
<VAR>n : ℕ<GOAL>(↑n).natAbs = n
<VAR>n m : ℕ<GOAL>n ≤ m → ↑(m - n) = ↑m - ↑n
<VAR>n : ℕ<GOAL>↑n ≠ 0 ↔ 0 < n
<VAR>n : ℕ<GOAL>0 < ↑n.succ
<VAR>n : ℕ<GOAL>↑n ≤ 0 ↔ n = 0
<VAR>n : ℕ<GOAL>(↑n + 1).sign = 1
<VAR>n : ℤ<GOAL>2 * n = n + n
<VAR>a b c : ℤ<VAR>ha : 0 < a<GOAL>b * a ≤ c * a ↔ b ≤ c
<VAR>a b : ℤ<VAR>hb : 0 < b<GOAL>0 ≤ a * b ↔ 0 ≤ a
<VAR>n : ℕ<GOAL>↑n.succ = (↑n).succ
<VAR>a : ℤ<GOAL>a.succ.pred = a
<VAR>a : ℤ<GOAL>a.pred.succ = a
<VAR>a : ℤ<GOAL>-a.succ = (-a).pred
<VAR>a : ℤ<GOAL>(-a.succ).succ = -a
<VAR>a : ℤ<GOAL>-a.pred = (-a).succ
<VAR>a : ℤ<GOAL>(-a.pred).pred = -a
<VAR>n : ℕ<GOAL>(↑n.succ).pred = ↑n
<VAR>n : ℕ<GOAL>-↑n.succ = (-↑n).pred
<VAR>n : ℕ<GOAL>(-↑n.succ).succ = -↑n
<VAR>n : ℕ<VAR>h : 0 < n<GOAL>↑(n - 1) = ↑n - 1
<VAR>m n : ℤ<GOAL>m ≤ n + 1 ↔ m ≤ n ∨ m = n + 1
<VAR>m n : ℤ<GOAL>m - 1 < n ↔ m ≤ n
<VAR>m n : ℤ<GOAL>m ≤ n - 1 ↔ m < n
<VAR>a b c : ℤ<GOAL>a + b ≤ c ↔ a ≤ c - b
<VAR>a b c : ℤ<GOAL>a ≤ b + c ↔ a - c ≤ b
<VAR>a b : ℤ<GOAL>a + b ≤ 0 ↔ a ≤ -b
<VAR>a b : ℤ<GOAL>a + b ≤ 0 ↔ b ≤ -a
<VAR>a b : ℤ<GOAL>0 ≤ a + b ↔ -b ≤ a
<VAR>a b : ℤ<GOAL>0 ≤ a + b ↔ -a ≤ b
<VAR>p : ℤ → Prop<VAR>i : ℤ<VAR>hz : p 0<VAR>hp : ∀ (i : ℕ), p ↑i → p (↑i + 1)<VAR>hn : ∀ (i : ℕ), p (-↑i) → p (-↑i - 1)<GOAL>p i
<VAR>C : ℤ → Sort u_1<VAR>b : ℤ<VAR>H0 : C b<VAR>Hs : (k : ℤ) → b ≤ k → C k → C (k + 1)<VAR>Hp : (k : ℤ) → k ≤ b → C k → C (k - 1)<GOAL>b.inductionOn' b H0 Hs Hp = H0
<VAR>C : ℤ → Sort u_1<VAR>z b : ℤ<VAR>H0 : C b<VAR>Hs : (k : ℤ) → b ≤ k → C k → C (k + 1)<VAR>Hp : (k : ℤ) → k ≤ b → C k → C (k - 1)<VAR>hz : b ≤ z<GOAL>(z + 1).inductionOn' b H0 Hs Hp = Hs z hz (z.inductionOn' b H0 Hs Hp)
<VAR>C : ℤ → Sort u_1<VAR>z b : ℤ<VAR>H0 : C b<VAR>Hs : (k : ℤ) → b ≤ k → C k → C (k + 1)<VAR>Hp : (k : ℤ) → k ≤ b → C k → C (k - 1)<VAR>hz : z ≤ b<GOAL>(z - 1).inductionOn' b H0 Hs Hp = Hp z hz (z.inductionOn' b H0 Hs Hp)
<VAR>P : ℤ → Prop<VAR>m : ℤ<VAR>h0 : P m<VAR>h1 : ∀ (n : ℤ), m ≤ n → P n → P (n + 1)<VAR>n : ℤ<GOAL>m ≤ n → P n
<VAR>P : ℤ → Prop<VAR>m : ℤ<VAR>h0 : P m<VAR>h1 : ∀ (n : ℤ), n ≤ m → P n → P (n - 1)<VAR>n : ℤ<GOAL>n ≤ m → P n
<VAR>m n : ℤ<VAR>P : ℤ → Sort u_1<VAR>lt : (n : ℤ) → n < m → P n<VAR>ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → P k) → P n<VAR>hn : n < m<GOAL>Int.strongRec lt ge n = lt n hn
<VAR>m n : ℤ<VAR>P : ℤ → Sort u_1<VAR>lt : (n : ℤ) → n < m → P n<VAR>ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → P k) → P n<VAR>hn : m ≤ n<GOAL>Int.strongRec lt ge n = ge n hn fun k x => Int.strongRec lt ge k
<VAR>n : ℕ<GOAL>(Int.ofNat n).natAbs = n
<VAR>a b : ℤ<GOAL>0 ≤ a → 0 ≤ b → (a + b).natAbs = a.natAbs + b.natAbs
<VAR>a b : ℤ<VAR>ha : a ≤ 0<VAR>hb : b ≤ 0<GOAL>(a + b).natAbs = a.natAbs + b.natAbs
<VAR>n : ℤ<VAR>k : ℕ<GOAL>(n ^ k).natAbs = n.natAbs ^ k
<VAR>a : ℤ<VAR>h : 1 < a.natAbs<GOAL>Function.Injective fun x => a ^ x
<VAR>x : ℤ<GOAL>↑x.natAbs ^ 2 = x ^ 2
<VAR>m n : ℕ<GOAL>↑(m / n) = (↑m).ediv ↑n
<VAR>a b : ℤ<VAR>Ha : a < 0<VAR>Hb : 0 < b<GOAL>a.ediv b = -((-a - 1) / b + 1)
<VAR>m n k : ℤ<VAR>i : ℤ<VAR>H : m % n = k % n<GOAL>(m + i) % n = (k + i) % n
<VAR>i : ℤ<GOAL>-i % 2 = i % 2
<VAR>n : ℤ<GOAL>n % 2 = 0 ∨ n % 2 = 1
<VAR>a b c d : ℤ<GOAL>a ∣ b → c ∣ d → a * c ∣ b * d
<VAR>b c : ℤ<VAR>a : ℤ<VAR>h : b ∣ c<GOAL>a * b ∣ a * c
<VAR>b c : ℤ<VAR>a : ℤ<VAR>h : b ∣ c<GOAL>b * a ∣ c * a
<VAR>a b c : ℤ<VAR>h : b ∣ a<VAR>hdiv : a / b ∣ c<GOAL>a ∣ b * c
<VAR>a b c : ℤ<VAR>h : b ∣ a<VAR>hb : b ≠ 0<GOAL>a / b ∣ c ↔ a ∣ b * c
<VAR>a b c : ℤ<VAR>hcb : c ∣ b<VAR>h : a ∣ b / c<GOAL>c * a ∣ b
<VAR>a b c : ℤ<VAR>h : a * b ∣ c<GOAL>b ∣ c / a
<VAR>a b c : ℤ<VAR>hbc : c ∣ b<GOAL>a ∣ b / c ↔ c * a ∣ b
<VAR>a b c : ℤ<GOAL>a ∣ b → b ∣ c → b / a ∣ c / a
<VAR>n : ℤ<VAR>m : ℤ<VAR>hn : 0 < n<GOAL>(∃ k, n * k < m ∧ m < n * (k + 1)) ↔ ¬n ∣ m
<VAR>m n : ℕ<GOAL>↑m ∣ ↑n ↔ m ∣ n
<VAR>n : ℤ<VAR>m : ℕ<GOAL>↑m ∣ n ↔ m ∣ n.natAbs
<VAR>m : ℤ<VAR>n : ℕ<GOAL>m ∣ ↑n ↔ m.natAbs ∣ n
<VAR>a b : ℤ<VAR>H : b ∣ a<GOAL>(a / b).natAbs = a.natAbs / b.natAbs
<VAR>a m n : ℤ<VAR>ha : a ≠ 0<VAR>h : a * m ∣ a * n<GOAL>m ∣ n
<VAR>a m n : ℤ<VAR>ha : a ≠ 0<VAR>h : m * a ∣ n * a<GOAL>m ∣ n
<VAR>a b c d : ℤ<VAR>hb : b ≠ 0<VAR>hbc : b ∣ c<VAR>h : b * a = c * d<GOAL>a = c / b * d
<VAR>m n : ℤ<VAR>hmn : m ∣ n<VAR>hnm : n.natAbs < m.natAbs<GOAL>n = 0
<VAR>m n : ℤ<VAR>hm : 0 ≤ m<VAR>hmn : m < n<VAR>hnm : n ∣ m<GOAL>m = 0
<VAR>a b c : ℤ<VAR>h1 : a % b = c<VAR>h2 : (a - c).natAbs < b.natAbs<GOAL>a = c
<VAR>m n : ℕ<VAR>h : n.succ ≤ m<GOAL>Int.ofNat m + -[n+1] = Int.ofNat (m - n.succ)
<VAR>m n : ℤ<VAR>hmn : m ∣ n<VAR>hn : n ≠ 0<GOAL>m.natAbs ≤ n.natAbs
<VAR>m n : ℤ<VAR>hmn : m ∣ n<VAR>hnm : n ∣ m<GOAL>m.natAbs = n.natAbs
<VAR>m n : ℤ<VAR>hmn : m ∣ n<GOAL>n / m ∣ n
<VAR>a b : ℤ<VAR>ha : 0 < a<VAR>hab : a ∣ b<GOAL>a ≤ b ↔ 0 < b
<VAR>a b c : ℤ<VAR>ha : 0 < a<VAR>hab : a ∣ c - b<GOAL>a + b ≤ c ↔ b < c
<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>(↑n).sign = 1
<VAR>m n : ℤ<GOAL>m.sign = n.sign → (m + n).sign = n.sign
<VAR>n : ℕ<GOAL>(↑n).toNat = n
<VAR>n : ℕ<GOAL>(↑n + 1).toNat = n + 1
<VAR>m : ℤ<VAR>n : ℕ<GOAL>m.toNat ≤ n ↔ m ≤ ↑n
<VAR>n : ℤ<VAR>m : ℕ<GOAL>m < n.toNat ↔ ↑m < n
<VAR>a b : ℤ<VAR>h : a ≤ b<GOAL>a.toNat ≤ b.toNat
<VAR>a b : ℤ<VAR>hb : 0 < b<GOAL>a.toNat < b.toNat ↔ a < b
<VAR>a b : ℤ<VAR>h : a.toNat < b.toNat<GOAL>a < b
<VAR>i : ℤ<VAR>h : 0 < i<GOAL>↑(i.toNat - 1) = i - 1
<VAR>n : ℤ<GOAL>n.toNat = 0 ↔ n ≤ 0
<VAR>a b : ℤ<VAR>h : b ≤ a<GOAL>↑(a - b).toNat = a - b
<VAR>m : ℤ<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>m.toNat < n ↔ m < ↑n
<VAR>m : ℤ<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>m.natMod ↑n < n
<VAR>m : ℤ<VAR>n : ℕ<GOAL>m.pow n = m ^ n
<VAR>α : Type u_1<VAR>f : α → α<VAR>a : α<VAR>n : ℕ<VAR>l : List α<GOAL>List.iterateTR.loop f a n l = l.reverse ++ List.iterate f a n