ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>xl xr : Type u<VAR>x y : PGame<VAR>L : x.LeftMoves ≃ y.LeftMoves<VAR>R : x.RightMoves ≃ y.RightMoves<VAR>hl : ∀ (i : x.LeftMoves), x.moveLeft i ≈ y.moveLeft (L i)<VAR>hr : ∀ (j : x.RightMoves), x.moveRight j ≈ y.moveRight (R j)<GOAL>(∀ (i : x.LeftMoves), (∃ i', x.moveLeft i ≤ y.moveLeft i') ∨ ∃ j, (x.moveLeft i).moveRight j ≤ y) ∧ ∀ (j : y.RightMoves), (∃ i, x ≤ (y.moveRight j).moveLeft i) ∨ ∃ j', x.moveRight j' ≤ y.moveRight j
<VAR>xl xr : Type u<VAR>x y : PGame<VAR>L : x.LeftMoves ≃ y.LeftMoves<VAR>R : x.RightMoves ≃ y.RightMoves<VAR>hl : ∀ (i : x.LeftMoves), x.moveLeft i ≈ y.moveLeft (L i)<VAR>hr : ∀ (j : x.RightMoves), x.moveRight j ≈ y.moveRight (R j)<GOAL>(∀ (i : y.LeftMoves), (∃ i', y.moveLeft i ≤ x.moveLeft i') ∨ ∃ j, (y.moveLeft i).moveRight j ≤ x) ∧ ∀ (j : x.RightMoves), (∃ i, y ≤ (x.moveRight j).moveLeft i) ∨ ∃ j', y.moveRight j' ≤ x.moveRight j
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u<VAR>B : Type u_3<VAR>inst✝¹⁸ : CommRing A<VAR>inst✝¹⁷ : Field K<VAR>inst✝¹⁶ : CommRing B<VAR>inst✝¹⁵ : Field L<VAR>inst✝¹⁴ : Algebra A K<VAR>inst✝¹³ : Algebra B L<VAR>inst✝¹² : Algebra A B<VAR>inst✝¹¹ : Algebra K L<VAR>inst✝¹⁰ : Algebra A L<VAR>inst✝⁹ : IsScalarTower A K L<VAR>inst✝⁸ : IsScalarTower A B L<VAR>inst✝⁷ : IsDomain A<VAR>inst✝⁶ : IsFractionRing A K<VAR>inst✝⁵ : IsIntegralClosure B A L<VAR>inst✝⁴ : IsFractionRing B L<VAR>inst✝³ : FiniteDimensional K L<VAR>inst✝² : Algebra.IsSeparable K L<VAR>inst✝¹ : IsIntegrallyClosed A<VAR>inst✝ : IsDedekindDomain B<VAR>I J : FractionalIdeal B⁰ L<VAR>hI✝ : I ≠ 0<VAR>hJ : J ≠ 0<VAR>hI : ¬I = 0<GOAL>I ≤ dual A K J ↔ I * J ≤ dual A K 1
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : AddCommMonoid A<VAR>inst✝¹ : Module R A<VAR>inst✝ : Module (MvPolynomial σ R) A<VAR>D : Derivation R (MvPolynomial σ R) A<VAR>a : R<VAR>f : MvPolynomial σ R<VAR>this : C a • D f = D (C a * f)<GOAL>C a • D f = a • D f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s t u : Set α<VAR>inst✝⁹ : TopologicalSpace α<VAR>inst✝⁸ : MeasurableSpace α<VAR>inst✝⁷ : BorelSpace α<VAR>inst✝⁶ : TopologicalSpace β<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : BorelSpace β<VAR>inst✝³ : MeasurableSpace δ<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : SecondCountableTopology α<VAR>f : δ → α<VAR>hf : ∀ (x : α), MeasurableSet (f ⁻¹' Ici x)<GOAL>Measurable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s t u : Set α<VAR>inst✝⁹ : TopologicalSpace α<VAR>inst✝⁸ : MeasurableSpace α<VAR>inst✝⁷ : BorelSpace α<VAR>inst✝⁶ : TopologicalSpace β<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : BorelSpace β<VAR>inst✝³ : MeasurableSpace δ<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : SecondCountableTopology α<VAR>f : δ → α<VAR>hf : ∀ (x : α), MeasurableSet (f ⁻¹' Ici x)<GOAL>∀ (x : α), MeasurableSet (f ⁻¹' Iio x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s t u : Set α<VAR>inst✝⁹ : TopologicalSpace α<VAR>inst✝⁸ : MeasurableSpace α<VAR>inst✝⁷ : BorelSpace α<VAR>inst✝⁶ : TopologicalSpace β<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : BorelSpace β<VAR>inst✝³ : MeasurableSpace δ<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : SecondCountableTopology α<VAR>f : δ → α<VAR>hf : ∀ (x : α), MeasurableSet (f ⁻¹' Ici x)<GOAL>∀ (x : α), MeasurableSet (f ⁻¹' Ici x)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>f✝ f : Perm α<GOAL>f.cycleFactorsFinset = {f} ↔ f.IsCycle
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x y : α<VAR>c : ℝ≥0<GOAL>edist x y ≤ ↑c ↔ nndist x y ≤ c
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} C<VAR>inst✝⁴ : Preadditive C<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : HasShift C ℤ<VAR>inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝ : Pretriangulated C<VAR>t : TStructure C<VAR>A : C<VAR>n₀ n₁ : ℤ<VAR>h : n₀ + 1 = n₁<GOAL>∃ X Y, ∃ (_ : t.LE n₀ X) (_ : t.GE n₁ Y), ∃ f g h, Triangle.mk f g h ∈ distinguishedTriangles
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} C<VAR>inst✝⁴ : Preadditive C<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : HasShift C ℤ<VAR>inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝ : Pretriangulated C<VAR>t : TStructure C<VAR>A : C<VAR>n₀ n₁ : ℤ<VAR>h✝ : n₀ + 1 = n₁<VAR>X Y : C<VAR>hX : t.LE 0 X<VAR>hY : t.GE 1 Y<VAR>f : X ⟶ (shiftFunctor C n₀).obj A<VAR>g : (shiftFunctor C n₀).obj A ⟶ Y<VAR>h : Y ⟶ (shiftFunctor C 1).obj X<VAR>mem : Triangle.mk f g h ∈ distinguishedTriangles<GOAL>∃ X Y, ∃ (_ : t.LE n₀ X) (_ : t.GE n₁ Y), ∃ f g h, Triangle.mk f g h ∈ distinguishedTriangles
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} C<VAR>inst✝⁴ : Preadditive C<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : HasShift C ℤ<VAR>inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝ : Pretriangulated C<VAR>t : TStructure C<VAR>A : C<VAR>n₀ n₁ : ℤ<VAR>h✝ : n₀ + 1 = n₁<VAR>X Y : C<VAR>hX : t.LE 0 X<VAR>hY : t.GE 1 Y<VAR>f : X ⟶ (shiftFunctor C n₀).obj A<VAR>g : (shiftFunctor C n₀).obj A ⟶ Y<VAR>h : Y ⟶ (shiftFunctor C 1).obj X<VAR>mem : Triangle.mk f g h ∈ distinguishedTriangles<VAR>T : Triangle C := (Triangle.shiftFunctor C (-n₀)).obj (Triangle.mk f g h)<VAR>e : ((shiftEquiv C n₀).functor ⋙ (shiftEquiv C n₀).inverse).obj A ≅ (𝟭 C).obj A := (shiftEquiv C n₀).unitIso.symm.app A<GOAL>∃ X Y, ∃ (_ : t.LE n₀ X) (_ : t.GE n₁ Y), ∃ f g h, Triangle.mk f g h ∈ distinguishedTriangles
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} C<VAR>inst✝⁴ : Preadditive C<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : HasShift C ℤ<VAR>inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝ : Pretriangulated C<VAR>t : TStructure C<VAR>A : C<VAR>n₀ n₁ : ℤ<VAR>h✝ : n₀ + 1 = n₁<VAR>X Y : C<VAR>hX : t.LE 0 X<VAR>hY : t.GE 1 Y<VAR>f : X ⟶ (shiftFunctor C n₀).obj A<VAR>g : (shiftFunctor C n₀).obj A ⟶ Y<VAR>h : Y ⟶ (shiftFunctor C 1).obj X<VAR>mem : Triangle.mk f g h ∈ distinguishedTriangles<VAR>T : Triangle C := (Triangle.shiftFunctor C (-n₀)).obj (Triangle.mk f g h)<VAR>e : ((shiftEquiv C n₀).functor ⋙ (shiftEquiv C n₀).inverse).obj A ≅ (𝟭 C).obj A := (shiftEquiv C n₀).unitIso.symm.app A<VAR>hT' : Triangle.mk (T.mor₁ ≫ e.hom) (e.inv ≫ T.mor₂) T.mor₃ ∈ distinguishedTriangles<GOAL>∃ X Y, ∃ (_ : t.LE n₀ X) (_ : t.GE n₁ Y), ∃ f g h, Triangle.mk f g h ∈ distinguishedTriangles
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : Semiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>s : Set M<VAR>hs : s.Finite<GOAL>span R ↑hs.toFinset = span R s
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>f : Filter X<GOAL>Disjoint f (cocompact X) ↔ ∃ K ∈ f, IsCompact K
<GOAL>(fun n => ↑(Nat.fib n)) = fun n => (φ ^ n - ψ ^ n) / √5
<GOAL>Set.EqOn (fun n => ↑(Nat.fib n)) (fun n => (φ ^ n - ψ ^ n) / √5) ↑(Finset.range fibRec.order)
<GOAL>fibRec.IsSolution fun n => ↑(Nat.fib n)
<GOAL>fibRec.IsSolution fun n => (φ ^ n - ψ ^ n) / √5
<VAR>α β : BoolAlg<VAR>e : ↑α ≃o ↑β<VAR>x✝ : (forget BoolAlg).obj α<GOAL>((let __src := { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯ }; { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ }) ≫ let __src := { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯ }; { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ }) x✝ = (𝟙 α) x✝
<VAR>α β : BoolAlg<VAR>e : ↑α ≃o ↑β<VAR>x✝ : (forget BoolAlg).obj β<GOAL>((let __src := { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯ }; { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ }) ≫ let __src := { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯ }; { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ }) x✝ = (𝟙 β) x✝
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>inst✝¹ : FiniteDimensional F E<VAR>inst✝ : Algebra.IsSeparable F E<GOAL>∃ α, F⟮α⟯ = ⊤
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>inst✝¹ : FiniteDimensional F E<VAR>inst✝ : Algebra.IsSeparable F E<VAR>F_inf : IsEmpty (Fintype F)<GOAL>∃ α, F⟮α⟯ = ⊤
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>inst✝¹ : FiniteDimensional F E<VAR>inst✝ : Algebra.IsSeparable F E<VAR>F_finite : Fintype F<GOAL>∃ α, F⟮α⟯ = ⊤
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X : TopCat<VAR>F : Presheaf C X<VAR>ι : Type w<VAR>U : ι → Opens ↑X<VAR>Y : Opens ↑X<VAR>hY : Y = iSup U<GOAL>F.IsSheaf ↔ F.IsSheafOpensLeCover
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X : TopCat<VAR>F : Presheaf C X<VAR>ι : Type w<VAR>U : ι → Opens ↑X<VAR>Y : Opens ↑X<VAR>hY : Y = iSup U<GOAL>(∀ ⦃X_1 : Opens ↑X⦄, ∀ S ∈ (Opens.grothendieckTopology ↑X).sieves X_1, Nonempty (IsLimit (Functor.mapCone F S.arrows.cocone.op))) ↔ F.IsSheafOpensLeCover
<VAR>α : Type u<VAR>β : Type v<VAR>R✝ r : α → α → Prop<VAR>l l₁ l₂ : List α<VAR>a✝ b✝ : α<VAR>R : α → α → Prop<VAR>a b : α<VAR>t : List α<GOAL>Chain' R (a :: b :: t) ↔ ∀ (i : ℕ) (h : i < (a :: b :: t).length - 1), R ((a :: b :: t).get ⟨i, ⋯⟩) ((a :: b :: t).get ⟨i + 1, ⋯⟩)
<VAR>α : Type u<VAR>β : Type v<VAR>R✝ r : α → α → Prop<VAR>l l₁ l₂ : List α<VAR>a✝ b✝ : α<VAR>R : α → α → Prop<VAR>a b : α<VAR>t : List α<GOAL>(R a b ∧ ∀ (i : ℕ) (h : i < (b :: t).length - 1), R ((b :: t).get ⟨i, ⋯⟩) ((b :: t).get ⟨i + 1, ⋯⟩)) ↔ (∀ (h : 0 < (a :: b :: t).length - 1), R ((a :: b :: t).get ⟨0, ⋯⟩) ((a :: b :: t).get ⟨0 + 1, ⋯⟩)) ∧ ∀ (n : ℕ) (h : n + 1 < (a :: b :: t).length - 1), R ((a :: b :: t).get ⟨n + 1, ⋯⟩) ((a :: b :: t).get ⟨n + 1 + 1, ⋯⟩)
<VAR>α : Type u<VAR>β : Type v<VAR>R✝ r : α → α → Prop<VAR>l l₁ l₂ : List α<VAR>a✝ b✝ : α<VAR>R : α → α → Prop<VAR>a b : α<VAR>t : List α<GOAL>R a b → ((∀ (i : ℕ) (h : i < t.length), R ((b :: t).get ⟨i, ⋯⟩) (t.get ⟨i, ⋯⟩)) ↔ ∀ (n : ℕ) (h : n + 1 < t.length + 1), R ((b :: t).get ⟨n, ⋯⟩) (t.get ⟨n, ⋯⟩))
<VAR>α : Type u<VAR>β : Type v<VAR>R✝ r : α → α → Prop<VAR>l l₁ l₂ : List α<VAR>a✝ b✝ : α<VAR>R : α → α → Prop<VAR>a b : α<VAR>t : List α<GOAL>R a b → ((∀ (i : ℕ) (h : i < t.length), R (b :: t)[i] t[i]) ↔ ∀ (n : ℕ) (h : n + 1 < t.length + 1), R (b :: t)[n] t[n])
<VAR>α✝ : Type u<VAR>β : Type u_1<VAR>t : TopologicalSpace α✝<VAR>B : Set (Set α✝)<VAR>s✝ : Set α✝<VAR>ι : Type u_2<VAR>inst✝¹ : Countable ι<VAR>α : ι → Type u_3<VAR>s : (i : ι) → Set (α i)<VAR>inst✝ : (i : ι) → TopologicalSpace (α i)<VAR>h : ∀ (i : ι), IsSeparable (s i)<GOAL>IsSeparable {f | ∀ (i : ι), f i ∈ s i}
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>s✝ : Set α<VAR>inst✝¹ : Bornology α<VAR>inst✝ : Finite ι<VAR>s : ι → Set α<GOAL>IsBounded (⋃ i, s i) ↔ ∀ (i : ι), IsBounded (s i)
<VAR>k : ℕ<VAR>IH : multichoose 2 k = k + 1<GOAL>multichoose 1 (k + 1) + (k + 1) = k + 1 + 1
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>R : Type u_3<VAR>α : Type u_4<VAR>inst✝² : DivisionSemiring α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSemiring α<VAR>f g : ι → α<VAR>a a₁ a₂ : α<VAR>h : a₂ ≠ 0<VAR>H : HasSum (fun i => f i * a₂) (a₁ * a₂)<GOAL>HasSum f a₁
<VAR>k : Type u_1<VAR>V₁ : Type u_2<VAR>P₁ : Type u_3<VAR>V₂ : Type u_4<VAR>P₂ : Type u_5<VAR>V₃ : Type u_6<VAR>P₃ : Type u_7<VAR>inst✝⁹ : Ring k<VAR>inst✝⁸ : AddCommGroup V₁<VAR>inst✝⁷ : Module k V₁<VAR>inst✝⁶ : AffineSpace V₁ P₁<VAR>inst✝⁵ : AddCommGroup V₂<VAR>inst✝⁴ : Module k V₂<VAR>inst✝³ : AffineSpace V₂ P₂<VAR>inst✝² : AddCommGroup V₃<VAR>inst✝¹ : Module k V₃<VAR>inst✝ : AffineSpace V₃ P₃<VAR>f : P₁ →ᵃ[k] P₂<VAR>s : Set P₁<GOAL>Submodule.map f.linear (vectorSpan k s) = vectorSpan k (⇑f '' s)
<VAR>α : Type u<VAR>σ σ' : Type v<VAR>M✝ : εNFA α σ<VAR>S : Set σ<VAR>x : List α<VAR>s : σ<VAR>a : α<VAR>M : NFA α σ<VAR>start : Set σ<GOAL>M.toεNFA.evalFrom start = M.evalFrom start
<VAR>α : Type u<VAR>σ σ' : Type v<VAR>M✝ : εNFA α σ<VAR>S : Set σ<VAR>x : List α<VAR>s : σ<VAR>a : α<VAR>M : NFA α σ<VAR>start : Set σ<GOAL>List.foldl M.toεNFA.stepSet start = List.foldl M.stepSet start
<VAR>α : Type u<VAR>σ σ' : Type v<VAR>M✝ : εNFA α σ<VAR>S✝ : Set σ<VAR>x : List α<VAR>s✝ : σ<VAR>a : α<VAR>M : NFA α σ<VAR>start S : Set σ<VAR>s : α<VAR>x✝ : σ<GOAL>x✝ ∈ M.toεNFA.stepSet S s ↔ x✝ ∈ M.stepSet S s
<VAR>α : Type u<VAR>σ σ' : Type v<VAR>M✝ : εNFA α σ<VAR>S✝ : Set σ<VAR>x : List α<VAR>s✝ : σ<VAR>a : α<VAR>M : NFA α σ<VAR>start S : Set σ<VAR>s : α<VAR>x✝ : σ<GOAL>(∃ i ∈ S, x✝ ∈ M.toεNFA.εClosure (M.toεNFA.step i (some s))) ↔ ∃ i ∈ S, x✝ ∈ M.step i s
<VAR>α : Type u<VAR>σ σ' : Type v<VAR>M✝ : εNFA α σ<VAR>S✝ : Set σ<VAR>x : List α<VAR>s✝ : σ<VAR>a : α<VAR>M : NFA α σ<VAR>start S : Set σ<VAR>s : α<VAR>x✝ : σ<GOAL>∀ (a : σ), a ∈ S ∧ x✝ ∈ M.toεNFA.εClosure (M.toεNFA.step a (some s)) ↔ a ∈ S ∧ x✝ ∈ M.step a s
<VAR>α : Type u<VAR>σ σ' : Type v<VAR>M✝ : εNFA α σ<VAR>S✝ : Set σ<VAR>x : List α<VAR>s✝ : σ<VAR>a : α<VAR>M : NFA α σ<VAR>start S : Set σ<VAR>s : α<VAR>x✝ : σ<GOAL>∀ a ∈ S, x✝ ∈ M.toεNFA.εClosure (M.toεNFA.step a (some s)) ↔ x✝ ∈ M.step a s
<VAR>α : Type u<VAR>σ σ' : Type v<VAR>M✝ : εNFA α σ<VAR>S✝ : Set σ<VAR>x : List α<VAR>s✝ : σ<VAR>a : α<VAR>M : NFA α σ<VAR>start S : Set σ<VAR>s : α<VAR>x✝ a✝¹ : σ<VAR>a✝ : a✝¹ ∈ S<GOAL>x✝ ∈ M.toεNFA.εClosure (M.toεNFA.step a✝¹ (some s)) ↔ x✝ ∈ M.step a✝¹ s
<VAR>α : Type u<VAR>σ σ' : Type v<VAR>M✝ : εNFA α σ<VAR>S✝ : Set σ<VAR>x : List α<VAR>s✝ : σ<VAR>a : α<VAR>M : NFA α σ<VAR>start S : Set σ<VAR>s : α<VAR>x✝ a✝¹ : σ<VAR>a✝ : a✝¹ ∈ S<GOAL>x✝ ∈ M.toεNFA.step a✝¹ (some s) ↔ x✝ ∈ M.step a✝¹ s
<VAR>F : Type u → Type u<VAR>inst✝¹ : Applicative F<VAR>inst✝ : CommApplicative F<VAR>α' β' : Type u<VAR>f : α' → F β'<VAR>α : Type u_1<VAR>x : Multiset α<GOAL>traverse pure x = x
<VAR>F : Type u → Type u<VAR>inst✝¹ : Applicative F<VAR>inst✝ : CommApplicative F<VAR>α' β' : Type u<VAR>f : α' → F β'<VAR>α : Type u_1<VAR>x : Multiset α<GOAL>∀ (a : List α), traverse pure ⟦a⟧ = ⟦a⟧
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>s : Set α<VAR>C : Set (Set β)<GOAL>s ×ˢ ⋃₀ C = ⋃₀ ((fun t => s ×ˢ t) '' C)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>hs : autoParam s.Finite _auto✝<GOAL>0 < s.ncard ↔ s.Nonempty
<VAR>X : Type u_1<VAR>X' : Type u_2<VAR>Y : Type u_3<VAR>Y' : Type u_4<VAR>Z : Type u_5<VAR>Z' : Type u_6<VAR>inst✝⁶ : TopologicalSpace X<VAR>inst✝⁵ : TopologicalSpace X'<VAR>inst✝⁴ : TopologicalSpace Y<VAR>inst✝³ : TopologicalSpace Y'<VAR>inst✝² : TopologicalSpace Z<VAR>inst✝¹ : TopologicalSpace Z'<VAR>f : X → Y<VAR>h : OpenEmbedding f<VAR>inst✝ : Nonempty X<VAR>x : Y<VAR>hx : x ∈ range f<GOAL>f (↑(toPartialHomeomorph f h).symm x) = x
<VAR>X : Type u_1<VAR>X' : Type u_2<VAR>Y : Type u_3<VAR>Y' : Type u_4<VAR>Z : Type u_5<VAR>Z' : Type u_6<VAR>inst✝⁶ : TopologicalSpace X<VAR>inst✝⁵ : TopologicalSpace X'<VAR>inst✝⁴ : TopologicalSpace Y<VAR>inst✝³ : TopologicalSpace Y'<VAR>inst✝² : TopologicalSpace Z<VAR>inst✝¹ : TopologicalSpace Z'<VAR>f : X → Y<VAR>h : OpenEmbedding f<VAR>inst✝ : Nonempty X<VAR>x : Y<VAR>hx : x ∈ range f<GOAL>x ∈ (toPartialHomeomorph f h).target
<VAR>k : Type u_1<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>α : Type v<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Zero α<VAR>inst✝ : One α<VAR>i✝ j✝ : n<GOAL>(PEquiv.refl n).toMatrix i✝ j✝ = 1 i✝ j✝
<VAR>u✝ : Lean.Level<VAR>arg : Q(Type u✝)<VAR>sα✝ : Q(CommSemiring «$arg»)<VAR>u : Lean.Level<VAR>α : Q(Type u)<VAR>sα : Q(CommSemiring «$α»)<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>a a' a₁ a₂ a₃ b b' b₁ b₂ b₃ c₁ c₂ : R<VAR>h : IsNat (a₁ + b₁) 0<GOAL>a₁ + a₂ + (b₁ + b₂) = a₂ + b₂
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>p : ℝ<VAR>hp0 : 0 ≤ p<VAR>f g : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>hf_zero : ∫⁻ (a : α), f a ^ p ∂μ = 0<GOAL>∫⁻ (a : α), (f * g) a ∂μ = 0
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>p : ℝ<VAR>hp0 : 0 ≤ p<VAR>f g : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>hf_zero : ∫⁻ (a : α), f a ^ p ∂μ = 0<GOAL>∫⁻ (a : α), (f * g) a ∂μ = lintegral μ 0
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>p : ℝ<VAR>hp0 : 0 ≤ p<VAR>f g : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>hf_zero : ∫⁻ (a : α), f a ^ p ∂μ = 0<GOAL>f * g =ᶠ[ae μ] 0
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>p : ℝ<VAR>hp0 : 0 ≤ p<VAR>f g : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>hf_zero : ∫⁻ (a : α), f a ^ p ∂μ = 0<GOAL>f * g =ᶠ[ae μ] 0 * g
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>p : ℝ<VAR>hp0 : 0 ≤ p<VAR>f g : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>hf_zero : ∫⁻ (a : α), f a ^ p ∂μ = 0<VAR>hf_eq_zero : f =ᶠ[ae μ] 0<GOAL>f * g =ᶠ[ae μ] 0 * g
<VAR>m n : ℕ<VAR>h : m ≤ n<GOAL>n.Coprime (n - m) ↔ n.Coprime m
<VAR>R : Type u<VAR>E : Type v<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Ring R<VAR>inst✝² : Module R E<VAR>inst✝¹ : Nontrivial E<VAR>inst✝ : NoZeroSMulDivisors R E<GOAL>lift.{v, u} #R ≤ lift.{u, v} #E
<VAR>R : Type u<VAR>E : Type v<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Ring R<VAR>inst✝² : Module R E<VAR>inst✝¹ : Nontrivial E<VAR>inst✝ : NoZeroSMulDivisors R E<VAR>x : E<VAR>hx : x ≠ 0<GOAL>lift.{v, u} #R ≤ lift.{u, v} #E
<VAR>R : Type u<VAR>E : Type v<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Ring R<VAR>inst✝² : Module R E<VAR>inst✝¹ : Nontrivial E<VAR>inst✝ : NoZeroSMulDivisors R E<VAR>x : E<VAR>hx : x ≠ 0<VAR>this : Injective fun k => k • x<GOAL>lift.{v, u} #R ≤ lift.{u, v} #E
<VAR>α : Type u<VAR>o n m : ℕ<VAR>m' : Type uₘ<VAR>n' : Type uₙ<VAR>o' : Type uₒ<VAR>a b : ℕ<VAR>R : Type u_1<VAR>inst✝ : SMul R α<VAR>x : R<VAR>a₀ a₁ a₂ : α<GOAL>x • ![a₀, a₁, a₂] = ![x • a₀, x • a₁, x • a₂]
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>R : Type u_3<VAR>s✝ t u : Finset α✝<VAR>f : α✝ → β<VAR>n : ℕ<VAR>ι : Type u_4<VAR>α : ι → Type u_5<VAR>inst✝ : (i : ι) → DecidableEq (α i)<VAR>s : Finset ((i : ι) → α i)<VAR>h : 1 < s.card<GOAL>∃ i, 1 < (image (fun x => x i) s).card ∧ ∀ (ai : α i), filter (fun x => x i = ai) s ⊂ s
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>R : Type u_3<VAR>s✝ t u : Finset α✝<VAR>f : α✝ → β<VAR>n : ℕ<VAR>ι : Type u_4<VAR>α : ι → Type u_5<VAR>inst✝ : (i : ι) → DecidableEq (α i)<VAR>s : Finset ((i : ι) → α i)<VAR>h : ∃ a b, a ∈ s ∧ b ∈ s ∧ ∃ a_1, a a_1 ≠ b a_1<GOAL>∃ i, (∃ a b, a ∈ image (fun x => x i) s ∧ b ∈ image (fun x => x i) s ∧ a ≠ b) ∧ ∀ (ai : α i), filter (fun x => x i = ai) s ⊂ s
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>R : Type u_3<VAR>s✝ t u : Finset α✝<VAR>f : α✝ → β<VAR>n : ℕ<VAR>ι : Type u_4<VAR>α : ι → Type u_5<VAR>inst✝ : (i : ι) → DecidableEq (α i)<VAR>s : Finset ((i : ι) → α i)<VAR>a1 a2 : (i : ι) → α i<VAR>h1 : a1 ∈ s<VAR>h2 : a2 ∈ s<VAR>i : ι<VAR>hne : a1 i ≠ a2 i<GOAL>∃ i, (∃ a b, a ∈ image (fun x => x i) s ∧ b ∈ image (fun x => x i) s ∧ a ≠ b) ∧ ∀ (ai : α i), filter (fun x => x i = ai) s ⊂ s
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>R : Type u_3<VAR>s✝ t u : Finset α✝<VAR>f : α✝ → β<VAR>n : ℕ<VAR>ι : Type u_4<VAR>α : ι → Type u_5<VAR>inst✝ : (i : ι) → DecidableEq (α i)<VAR>s : Finset ((i : ι) → α i)<VAR>a1 a2 : (i : ι) → α i<VAR>h1 : a1 ∈ s<VAR>h2 : a2 ∈ s<VAR>i : ι<VAR>hne : a1 i ≠ a2 i<VAR>ai : α i<GOAL>filter (fun x => x i = ai) s ⊂ s
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>R : Type u_3<VAR>s✝ t u : Finset α✝<VAR>f : α✝ → β<VAR>n : ℕ<VAR>ι : Type u_4<VAR>α : ι → Type u_5<VAR>inst✝ : (i : ι) → DecidableEq (α i)<VAR>s : Finset ((i : ι) → α i)<VAR>a1 a2 : (i : ι) → α i<VAR>h1 : a1 ∈ s<VAR>h2 : a2 ∈ s<VAR>i : ι<VAR>hne : a1 i ≠ a2 i<VAR>ai : α i<GOAL>∃ x ∈ s, ¬x i = ai
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>R : Type u_3<VAR>s✝ t u : Finset α✝<VAR>f : α✝ → β<VAR>n : ℕ<VAR>ι : Type u_4<VAR>α : ι → Type u_5<VAR>inst✝ : (i : ι) → DecidableEq (α i)<VAR>s : Finset ((i : ι) → α i)<VAR>a1 a2 : (i : ι) → α i<VAR>h1 : a1 ∈ s<VAR>h2 : a2 ∈ s<VAR>i : ι<VAR>hne : a1 i ≠ a2 i<GOAL>∃ x ∈ s, ¬x i = a2 i
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>R : Type u_3<VAR>s✝ t u : Finset α✝<VAR>f : α✝ → β<VAR>n : ℕ<VAR>ι : Type u_4<VAR>α : ι → Type u_5<VAR>inst✝ : (i : ι) → DecidableEq (α i)<VAR>s : Finset ((i : ι) → α i)<VAR>a1 a2 : (i : ι) → α i<VAR>h1 : a1 ∈ s<VAR>h2 : a2 ∈ s<VAR>i : ι<VAR>hne✝ : a1 i ≠ a2 i<VAR>ai : α i<VAR>hne : a2 i ≠ ai<GOAL>∃ x ∈ s, ¬x i = ai
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasColimits C<VAR>X Y Z : TopCat<VAR>F : Presheaf C X<VAR>U V : Opens ↑X<VAR>i : U ⟶ V<VAR>x : ↥U<VAR>inst✝ : ConcreteCategory C<VAR>s : (forget C).obj (F.obj (op V))<GOAL>(F.germ x) ((F.map i.op) s) = (F.germ ((fun x => ⟨↑x, ⋯⟩) x)) s
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasureSpace Ω<VAR>inst✝ : IsProbabilityMeasure ℙ<VAR>X : ℕ → Ω → ℝ<VAR>hint : Integrable (X 0) ℙ<VAR>hindep : Pairwise fun i j => IndepFun (X i) (X j) ℙ<VAR>hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ<VAR>hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω<VAR>c : ℝ<VAR>c_one : 1 < c<GOAL>∀ᵐ (ω : Ω), Tendsto (fun n => (∑ i ∈ range ⌊c ^ n⌋₊, X i ω) / ↑⌊c ^ n⌋₊) atTop (𝓝 (∫ (a : Ω), X 0 a))
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasureSpace Ω<VAR>inst✝ : IsProbabilityMeasure ℙ<VAR>X : ℕ → Ω → ℝ<VAR>hint : Integrable (X 0) ℙ<VAR>hindep : Pairwise fun i j => IndepFun (X i) (X j) ℙ<VAR>hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ<VAR>hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω<VAR>c : ℝ<VAR>c_one : 1 < c<VAR>H : ∀ (n : ℕ), 0 < ↑⌊c ^ n⌋₊<GOAL>∀ᵐ (ω : Ω), Tendsto (fun n => (∑ i ∈ range ⌊c ^ n⌋₊, X i ω) / ↑⌊c ^ n⌋₊) atTop (𝓝 (∫ (a : Ω), X 0 a))
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasureSpace Ω<VAR>inst✝ : IsProbabilityMeasure ℙ<VAR>X : ℕ → Ω → ℝ<VAR>hint : Integrable (X 0) ℙ<VAR>hindep : Pairwise fun i j => IndepFun (X i) (X j) ℙ<VAR>hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ<VAR>hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω<VAR>c : ℝ<VAR>c_one : 1 < c<VAR>H : ∀ (n : ℕ), 0 < ↑⌊c ^ n⌋₊<VAR>ω : Ω<VAR>hω : (fun n => ∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω - ↑⌊c ^ n⌋₊ * ∫ (a : Ω), X 0 a) =o[atTop] fun n => ↑⌊c ^ n⌋₊<VAR>h'ω : (fun n => ∑ i ∈ range n, truncation (X i) (↑i) ω - ∑ i ∈ range n, X i ω) =o[atTop] fun n => ↑n<GOAL>Tendsto (fun n => (∑ i ∈ range ⌊c ^ n⌋₊, X i ω) / ↑⌊c ^ n⌋₊) atTop (𝓝 (∫ (a : Ω), X 0 a))
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasureSpace Ω<VAR>inst✝ : IsProbabilityMeasure ℙ<VAR>X : ℕ → Ω → ℝ<VAR>hint : Integrable (X 0) ℙ<VAR>hindep : Pairwise fun i j => IndepFun (X i) (X j) ℙ<VAR>hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ<VAR>hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω<VAR>c : ℝ<VAR>c_one : 1 < c<VAR>H : ∀ (n : ℕ), 0 < ↑⌊c ^ n⌋₊<VAR>ω : Ω<VAR>hω : (fun n => ∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω - ↑⌊c ^ n⌋₊ * ∫ (a : Ω), X 0 a) =o[atTop] fun n => ↑⌊c ^ n⌋₊<VAR>h'ω : (fun n => ∑ i ∈ range n, truncation (X i) (↑i) ω - ∑ i ∈ range n, X i ω) =o[atTop] fun n => ↑n<GOAL>(fun x => (∑ i ∈ range ⌊c ^ x⌋₊, X i ω) / ↑⌊c ^ x⌋₊ - ∫ (a : Ω), X 0 a) =o[atTop] fun _x => 1
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasureSpace Ω<VAR>inst✝ : IsProbabilityMeasure ℙ<VAR>X : ℕ → Ω → ℝ<VAR>hint : Integrable (X 0) ℙ<VAR>hindep : Pairwise fun i j => IndepFun (X i) (X j) ℙ<VAR>hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ<VAR>hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω<VAR>c : ℝ<VAR>c_one : 1 < c<VAR>H : ∀ (n : ℕ), 0 < ↑⌊c ^ n⌋₊<VAR>ω : Ω<VAR>hω : (fun n => ∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω - ↑⌊c ^ n⌋₊ * ∫ (a : Ω), X 0 a) =o[atTop] fun n => ↑⌊c ^ n⌋₊<VAR>h'ω : (fun n => ∑ i ∈ range n, truncation (X i) (↑i) ω - ∑ i ∈ range n, X i ω) =o[atTop] fun n => ↑n<VAR>L : (fun n => ∑ i ∈ range ⌊c ^ n⌋₊, X i ω - ↑⌊c ^ n⌋₊ * ∫ (a : Ω), X 0 a) =o[atTop] fun n => ↑⌊c ^ n⌋₊<GOAL>(fun x => (∑ i ∈ range ⌊c ^ x⌋₊, X i ω) / ↑⌊c ^ x⌋₊ - ∫ (a : Ω), X 0 a) =o[atTop] fun _x => 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p : PMF α<VAR>f✝ : (a : α) → a ∈ p.support → PMF β<VAR>a : α<VAR>f : (a' : α) → a' ∈ (pure a).support → PMF β<GOAL>(pure a).bindOnSupport f = f a ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p : PMF α<VAR>f✝ : (a : α) → a ∈ p.support → PMF β<VAR>a : α<VAR>f : (a' : α) → a' ∈ (pure a).support → PMF β<VAR>b : β<GOAL>((pure a).bindOnSupport f) b = (f a ⋯) b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p : PMF α<VAR>f✝ : (a : α) → a ∈ p.support → PMF β<VAR>a : α<VAR>f : (a' : α) → a' ∈ (pure a).support → PMF β<VAR>b : β<GOAL>(∑' (a_1 : α), (if a_1 = a then 1 else 0) * if h : (if a_1 = a then 1 else 0) = 0 then 0 else (f a_1 h) b) = (f a ⋯) b