ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>s✝ t u✝ v✝ s : Set α<VAR>h : ∀ (t t' : Set α), IsClosed t → IsClosed t' → s ⊆ t ∪ t' → (s ∩ t).Nonempty → (s ∩ t').Nonempty → (s ∩ (t ∩ t')).Nonempty<VAR>u v : Set α<VAR>hu : IsOpen u<VAR>hv : IsOpen v<VAR>huv : s ⊆ u ∪ v<VAR>x : α<VAR>xs : x ∈ s<VAR>xu : x ∈ u<VAR>y : α<VAR>ys : y ∈ s<VAR>yv : y ∈ v<VAR>h' : s ⊆ uᶜ ∪ vᶜ<GOAL>False
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>s✝ t u✝ v✝ s : Set α<VAR>h : ∀ (t t' : Set α), IsClosed t → IsClosed t' → s ⊆ t ∪ t' → (s ∩ t).Nonempty → (s ∩ t').Nonempty → (s ∩ (t ∩ t')).Nonempty<VAR>u v : Set α<VAR>hu : IsOpen u<VAR>hv : IsOpen v<VAR>huv : s ⊆ u ∪ v<VAR>x : α<VAR>xs : x ∈ s<VAR>xu : x ∈ u<VAR>y : α<VAR>ys : y ∈ s<VAR>yv : y ∈ v<VAR>h' : s ⊆ uᶜ ∪ vᶜ<VAR>xv : x ∉ v<GOAL>False
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>s✝ t u✝ v✝ s : Set α<VAR>h : ∀ (t t' : Set α), IsClosed t → IsClosed t' → s ⊆ t ∪ t' → (s ∩ t).Nonempty → (s ∩ t').Nonempty → (s ∩ (t ∩ t')).Nonempty<VAR>u v : Set α<VAR>hu : IsOpen u<VAR>hv : IsOpen v<VAR>huv : s ⊆ u ∪ v<VAR>x : α<VAR>xs : x ∈ s<VAR>xu : x ∈ u<VAR>y : α<VAR>ys : y ∈ s<VAR>yv : y ∈ v<VAR>h' : s ⊆ uᶜ ∪ vᶜ<VAR>xv : x ∉ v<VAR>yu : y ∉ u<GOAL>False
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>s✝ t u✝ v✝ s : Set α<VAR>h : ∀ (t t' : Set α), IsClosed t → IsClosed t' → s ⊆ t ∪ t' → (s ∩ t).Nonempty → (s ∩ t').Nonempty → (s ∩ (t ∩ t')).Nonempty<VAR>u v : Set α<VAR>hu : IsOpen u<VAR>hv : IsOpen v<VAR>huv : s ⊆ u ∪ v<VAR>x : α<VAR>xs : x ∈ s<VAR>xu : x ∈ u<VAR>y : α<VAR>ys : y ∈ s<VAR>yv : y ∈ v<VAR>h' : s ⊆ uᶜ ∪ vᶜ<VAR>xv : x ∉ v<VAR>yu : y ∉ u<VAR>this : (s ∩ (uᶜ ∩ vᶜ)).Nonempty<GOAL>False
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>s✝ t u✝ v✝ s : Set α<VAR>h : ∀ (t t' : Set α), IsClosed t → IsClosed t' → s ⊆ t ∪ t' → (s ∩ t).Nonempty → (s ∩ t').Nonempty → (s ∩ (t ∩ t')).Nonempty<VAR>u v : Set α<VAR>hu : IsOpen u<VAR>hv : IsOpen v<VAR>huv : s ⊆ u ∪ v<VAR>x : α<VAR>xs : x ∈ s<VAR>xu : x ∈ u<VAR>y : α<VAR>ys : y ∈ s<VAR>yv : y ∈ v<VAR>h' : s ⊆ uᶜ ∪ vᶜ<VAR>xv : x ∉ v<VAR>yu : y ∉ u<VAR>this : (s ∩ (u ∪ v)ᶜ).Nonempty<GOAL>False
<VAR>α : Type u<VAR>i : Nat<VAR>a : Array α<GOAL>a.extract i i = #[]
<VAR>α : Type u<VAR>i : Nat<VAR>a : Array α<GOAL>i ≤ i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>s s₁ s₂ : LowerSet α<VAR>t t₁ t₂ : LowerSet β<VAR>x : α × β<GOAL>Disjoint (s₁ ×ˢ t₁) (s₂ ×ˢ t₂) ↔ Disjoint s₁ s₂ ∨ Disjoint t₁ t₂
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>a b : ℝ<VAR>f✝ g : ℝ → E<VAR>μ : Measure ℝ<VAR>f : ℝ → E<GOAL>‖∫ (x : ℝ) in min a b..max a b, f x ∂μ‖ = ‖∫ (x : ℝ) in a..b, f x ∂μ‖
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>inst✝³ : FunLike F α β<VAR>inst✝² : BooleanAlgebra α<VAR>inst✝¹ : BooleanAlgebra β<VAR>inst✝ : BoundedLatticeHomClass F α β<VAR>f : F<VAR>a b : α<GOAL>f (a ⇨ b) = f a ⇨ f b
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>inst✝³ : FunLike F α β<VAR>inst✝² : BooleanAlgebra α<VAR>inst✝¹ : BooleanAlgebra β<VAR>inst✝ : BoundedLatticeHomClass F α β<VAR>f : F<VAR>a b : α<GOAL>f (a \ b) = f a \ f b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : PartialOrder β<VAR>f : α → β<VAR>𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)<VAR>s t u : Finset α<VAR>a b : α<VAR>inst✝ : DecidableEq α<GOAL>{ ofColex := s \ t } ≤ { ofColex := t \ s } ↔ { ofColex := s } ≤ { ofColex := t }
<VAR>𝕜 : Type u<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace 𝕜 E<VAR>G : Type u_1<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedSpace 𝕜 G<VAR>f✝ f₀ f₁ g : 𝕜 → F<VAR>f'✝ f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>ι : Type u_2<VAR>inst✝² : DecidableEq ι<VAR>𝔸' : Type u_3<VAR>inst✝¹ : NormedCommRing 𝔸'<VAR>inst✝ : NormedAlgebra 𝕜 𝔸'<VAR>u : Finset ι<VAR>f : ι → 𝕜 → 𝔸'<VAR>f' : ι → 𝔸'<VAR>hf : ∀ i ∈ u, HasDerivAt (f i) (f' i) x<GOAL>HasDerivAt (fun x => ∏ i ∈ u, f i x) (∑ i ∈ u, (∏ j ∈ u.erase i, f j x) • f' i) x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>E' : Type u_5<VAR>M' : Type u_6<VAR>H' : Type u_7<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : TopologicalSpace H<VAR>inst✝⁵ : TopologicalSpace M<VAR>f f' : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>inst✝⁴ : NormedAddCommGroup E'<VAR>inst✝³ : NormedSpace 𝕜 E'<VAR>inst✝² : TopologicalSpace H'<VAR>inst✝¹ : TopologicalSpace M'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>s t : Set M<VAR>inst✝ : I.Boundaryless<VAR>x : M<VAR>hx : x ∈ f.source<GOAL>map (↑(f.extend I)) (𝓝 x) = 𝓝 (↑(f.extend I) x)
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁✝ l₂✝ : List α<VAR>f : α → β<VAR>l₁ l₂ : List α<GOAL>map f (l₁.reverseAux l₂) = (map f l₁).reverseAux (map f l₂)
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>J : GrothendieckTopology C<VAR>R₀ : Cᵒᵖ ⥤ RingCat<VAR>R : Sheaf J RingCat<VAR>α : R₀ ⟶ R.val<VAR>inst✝³ : Presheaf.IsLocallyInjective J α<VAR>inst✝² : Presheaf.IsLocallySurjective J α<VAR>M₀ : PresheafOfModules R₀<VAR>A : Sheaf J AddCommGrp<VAR>φ : M₀.presheaf ⟶ A.val<VAR>inst✝¹ : Presheaf.IsLocallyInjective J φ<VAR>inst✝ : Presheaf.IsLocallySurjective J φ<VAR>X Y : Cᵒᵖ<VAR>π : X ⟶ Y<VAR>r r' : ↑(R.val.obj X)<VAR>m m' : ↑(A.val.obj X)<VAR>S : Sieve (Opposite.unop X) := Presheaf.imageSieve α r ⊓ Presheaf.imageSieve φ m ⊓ Presheaf.imageSieve φ m'<GOAL>smul α φ r (m + m') = smul α φ r m + smul α φ r m'
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>J : GrothendieckTopology C<VAR>R₀ : Cᵒᵖ ⥤ RingCat<VAR>R : Sheaf J RingCat<VAR>α : R₀ ⟶ R.val<VAR>inst✝³ : Presheaf.IsLocallyInjective J α<VAR>inst✝² : Presheaf.IsLocallySurjective J α<VAR>M₀ : PresheafOfModules R₀<VAR>A : Sheaf J AddCommGrp<VAR>φ : M₀.presheaf ⟶ A.val<VAR>inst✝¹ : Presheaf.IsLocallyInjective J φ<VAR>inst✝ : Presheaf.IsLocallySurjective J φ<VAR>X Y : Cᵒᵖ<VAR>π : X ⟶ Y<VAR>r r' : ↑(R.val.obj X)<VAR>m m' : ↑(A.val.obj X)<VAR>S : Sieve (Opposite.unop X) := Presheaf.imageSieve α r ⊓ Presheaf.imageSieve φ m ⊓ Presheaf.imageSieve φ m'<VAR>hS : S ∈ J.sieves (Opposite.unop X)<GOAL>smul α φ r (m + m') = smul α φ r m + smul α φ r m'
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>J : GrothendieckTopology C<VAR>R₀ : Cᵒᵖ ⥤ RingCat<VAR>R : Sheaf J RingCat<VAR>α : R₀ ⟶ R.val<VAR>inst✝³ : Presheaf.IsLocallyInjective J α<VAR>inst✝² : Presheaf.IsLocallySurjective J α<VAR>M₀ : PresheafOfModules R₀<VAR>A : Sheaf J AddCommGrp<VAR>φ : M₀.presheaf ⟶ A.val<VAR>inst✝¹ : Presheaf.IsLocallyInjective J φ<VAR>inst✝ : Presheaf.IsLocallySurjective J φ<VAR>X Y : Cᵒᵖ<VAR>π : X ⟶ Y<VAR>r r' : ↑(R.val.obj X)<VAR>m m' : ↑(A.val.obj X)<VAR>S : Sieve (Opposite.unop X) := Presheaf.imageSieve α r ⊓ Presheaf.imageSieve φ m ⊓ Presheaf.imageSieve φ m'<VAR>hS : S ∈ J.sieves (Opposite.unop X)<GOAL>∀ (Y : C) (f : Y ⟶ Opposite.unop X), S.arrows f → (A.val.map f.op) (smul α φ r (m + m')) = (A.val.map f.op) (smul α φ r m + smul α φ r m')
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>J : GrothendieckTopology C<VAR>R₀ : Cᵒᵖ ⥤ RingCat<VAR>R : Sheaf J RingCat<VAR>α : R₀ ⟶ R.val<VAR>inst✝³ : Presheaf.IsLocallyInjective J α<VAR>inst✝² : Presheaf.IsLocallySurjective J α<VAR>M₀ : PresheafOfModules R₀<VAR>A : Sheaf J AddCommGrp<VAR>φ : M₀.presheaf ⟶ A.val<VAR>inst✝¹ : Presheaf.IsLocallyInjective J φ<VAR>inst✝ : Presheaf.IsLocallySurjective J φ<VAR>X Y✝ : Cᵒᵖ<VAR>π : X ⟶ Y✝<VAR>r r' : ↑(R.val.obj X)<VAR>m m' : ↑(A.val.obj X)<VAR>S : Sieve (Opposite.unop X) := Presheaf.imageSieve α r ⊓ Presheaf.imageSieve φ m ⊓ Presheaf.imageSieve φ m'<VAR>hS : S ∈ J.sieves (Opposite.unop X)<VAR>Y : C<VAR>f : Y ⟶ Opposite.unop X<VAR>r₀ : (forget RingCat).obj (R₀.obj (Opposite.op Y))<VAR>hr₀ : (α.app (Opposite.op Y)) r₀ = (R.val.map f.op) r<VAR>m₀ : ↑(M₀.presheaf.obj (Opposite.op Y))<VAR>hm₀ : (φ.app (Opposite.op Y)) m₀ = (A.val.map f.op) m<VAR>m₀' : ↑(M₀.presheaf.obj (Opposite.op Y))<VAR>hm₀' : (φ.app (Opposite.op Y)) m₀' = (A.val.map f.op) m'<GOAL>(A.val.map f.op) (smul α φ r (m + m')) = (A.val.map f.op) (smul α φ r m + smul α φ r m')
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>inst✝ : Category.{v₃, u₃} E<VAR>F : C ⥤ D<VAR>G : D ⥤ C<VAR>adj : F ⊣ G<VAR>X Y : D<VAR>f : X ⟶ Y<VAR>hf : Mono f<VAR>Z : C<VAR>g h : Z ⟶ G.obj X<VAR>H : (adj.homEquiv Z Y).symm (g ≫ G.map f) = (adj.homEquiv Z Y).symm (h ≫ G.map f)<GOAL>g = h
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>X✝ : SimplicialObject C<VAR>q n : ℕ<VAR>X Y : SimplicialObject C<VAR>f : X ⟶ Y<GOAL>f.app (op [n]) ≫ (Q q).f n = (Q q).f n ≫ f.app (op [n])
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>X✝ : SimplicialObject C<VAR>q n : ℕ<VAR>X Y : SimplicialObject C<VAR>f : X ⟶ Y<GOAL>f.app (op [n]) ≫ 𝟙 (K[Y].X n) = 𝟙 (K[X].X n) ≫ f.app (op [n])
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>X✝ : SimplicialObject C<VAR>q n : ℕ<VAR>X Y : SimplicialObject C<VAR>f : X ⟶ Y<GOAL>f.app (op [n]) ≫ 𝟙 (Y _[n]) = 𝟙 (X _[n]) ≫ f.app (op [n])
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>f : α → β<VAR>hs : autoParam s.Finite _auto✝<VAR>ht : autoParam t.Finite _auto✝<GOAL>s.ncard = t.ncard ↔ (s \ t).ncard = (t \ s).ncard
<VAR>R : Type u<VAR>inst✝³ : CommRing R<VAR>n G : Type v<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype n<VAR>α β : Type v<VAR>inst✝ : DecidableEq α<VAR>M✝ M : Matrix n n R<VAR>e : Matrix n n R ≃ₗ[R] Matrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) R := reindexLinearEquiv R R (Fintype.equivFin n) (Fintype.equivFin n)<GOAL>eval 0 (derivative (1 + X • M.map ⇑C).det) = M.trace
<VAR>R : Type u<VAR>inst✝³ : CommRing R<VAR>n G : Type v<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype n<VAR>α β : Type v<VAR>inst✝ : DecidableEq α<VAR>M✝ M : Matrix n n R<VAR>e : Matrix n n R ≃ₗ[R] Matrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) R := reindexLinearEquiv R R (Fintype.equivFin n) (Fintype.equivFin n)<GOAL>eval 0 (derivative ((reindexLinearEquiv R[X] R[X] (Fintype.equivFin n) (Fintype.equivFin n)) (1 + X • M.map ⇑C)).det) = M.trace
<VAR>R : Type u<VAR>inst✝³ : CommRing R<VAR>n G : Type v<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype n<VAR>α β : Type v<VAR>inst✝ : DecidableEq α<VAR>M✝ M : Matrix n n R<VAR>e : Matrix n n R ≃ₗ[R] Matrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) R := reindexLinearEquiv R R (Fintype.equivFin n) (Fintype.equivFin n)<GOAL>(reindexLinearEquiv R[X] R[X] (Fintype.equivFin n) (Fintype.equivFin n)) (1 + X • M.map ⇑C) = 1 + X • (e M).map ⇑C
<VAR>R : Type u<VAR>inst✝³ : CommRing R<VAR>n G : Type v<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype n<VAR>α β : Type v<VAR>inst✝ : DecidableEq α<VAR>M✝ M : Matrix n n R<VAR>e : Matrix n n R ≃ₗ[R] Matrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) R := reindexLinearEquiv R R (Fintype.equivFin n) (Fintype.equivFin n)<GOAL>M.trace = (e M).trace
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>G : SimpleGraph α<VAR>inst✝ : MulZeroOneClass R<VAR>a b : α<VAR>e : Sym2 α<GOAL>incMatrix R G a e * incMatrix R G b e = (G.incidenceSet a ∩ G.incidenceSet b).indicator 1 e
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝⁴ : Category.{v, u} V<VAR>inst✝³ : HasZeroMorphisms V<VAR>α : Type u_2<VAR>inst✝² : AddRightCancelSemigroup α<VAR>inst✝¹ : One α<VAR>inst✝ : DecidableEq α<VAR>X : α → V<VAR>d : (n : α) → X n ⟶ X (n + 1)<VAR>sq : ∀ (n : α), d n ≫ d (n + 1) = 0<VAR>i j : α<VAR>h : i + 1 ≠ j<GOAL>(if h : i + 1 = j then d i ≫ eqToHom ⋯ else 0) = 0
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℝ → E<VAR>T : ℝ<VAR>hf : Periodic f T<VAR>t s : ℝ<GOAL>∫ (x : ℝ) in t..t + T, f x = ∫ (x : ℝ) in s..s + T, f x
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℝ → E<VAR>T : ℝ<VAR>hf : Periodic f T<VAR>t s : ℝ<VAR>hT : 0 < T<GOAL>∫ (x : ℝ) in t..t + T, f x = ∫ (x : ℝ) in s..s + T, f x
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℝ → E<VAR>t s : ℝ<VAR>hf : Periodic f 0<GOAL>∫ (x : ℝ) in t..t + 0, f x = ∫ (x : ℝ) in s..s + 0, f x
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℝ → E<VAR>T : ℝ<VAR>hf : Periodic f T<VAR>t s : ℝ<VAR>hT : T < 0<GOAL>∫ (x : ℝ) in t..t + T, f x = ∫ (x : ℝ) in s..s + T, f x
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f : ArithmeticFunction R<GOAL>f.ppow 0 = ↑ζ
<VAR>L : Language<VAR>α : Type w<VAR>M : Type w'<VAR>n : ℕ<VAR>inst✝ : Preorder M<GOAL>M ⊨ Language.order.denselyOrderedSentence ↔ DenselyOrdered M
<VAR>L : Language<VAR>α : Type w<VAR>M : Type w'<VAR>n : ℕ<VAR>inst✝ : Preorder M<GOAL>(∀ (a a_1 : M), Fin.snoc (Fin.snoc default a) a_1 0 < Fin.snoc (Fin.snoc default a) a_1 1 → ∃ a_3, Fin.snoc (Fin.snoc (Fin.snoc default a) a_1) a_3 0 < Fin.snoc (Fin.snoc (Fin.snoc default a) a_1) a_3 2 ∧ Fin.snoc (Fin.snoc (Fin.snoc default a) a_1) a_3 2 < Fin.snoc (Fin.snoc (Fin.snoc default a) a_1) a_3 1) ↔ DenselyOrdered M
<VAR>L : Language<VAR>α : Type w<VAR>M : Type w'<VAR>n : ℕ<VAR>inst✝ : Preorder M<VAR>h : DenselyOrdered M<VAR>a b : M<VAR>ab : Fin.snoc (Fin.snoc default a) b 0 < Fin.snoc (Fin.snoc default a) b 1<GOAL>∃ a_1, Fin.snoc (Fin.snoc (Fin.snoc default a) b) a_1 0 < Fin.snoc (Fin.snoc (Fin.snoc default a) b) a_1 2 ∧ Fin.snoc (Fin.snoc (Fin.snoc default a) b) a_1 2 < Fin.snoc (Fin.snoc (Fin.snoc default a) b) a_1 1
<VAR>u : ℂ<VAR>hu : 0 < u.re<VAR>v : ℂ<GOAL>IntervalIntegrable (fun x => ↑x ^ (u - 1) * (1 - ↑x) ^ (v - 1)) volume 0 (1 / 2)
<VAR>u : ℂ<VAR>hu : 0 < u.re<VAR>v : ℂ<GOAL>IntervalIntegrable (fun x => ↑x ^ (u - 1)) volume 0 (1 / 2)
<VAR>u : ℂ<VAR>hu : 0 < u.re<VAR>v : ℂ<GOAL>ContinuousOn (fun x => (1 - ↑x) ^ (v - 1)) (uIcc 0 (1 / 2))
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>ι : Type u_5<VAR>π✝ : ι → Type u_6<VAR>κ : Type u_7<VAR>inst✝¹ : TopologicalSpace X<VAR>T : (i : ι) → TopologicalSpace (π✝ i)<VAR>f : X → (i : ι) → π✝ i<VAR>π : ι → Type u_8<VAR>g : (a : ι) → Set (Set (π a))<VAR>inst✝ : Finite ι<VAR>hg : ∀ (a : ι), ⋃₀ g a = univ<GOAL>Pi.topologicalSpace = generateFrom {t | ∃ s, (∀ (a : ι), s a ∈ g a) ∧ t = univ.pi s}
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>ι : Type u_5<VAR>π✝ : ι → Type u_6<VAR>κ : Type u_7<VAR>inst✝¹ : TopologicalSpace X<VAR>T : (i : ι) → TopologicalSpace (π✝ i)<VAR>f : X → (i : ι) → π✝ i<VAR>π : ι → Type u_8<VAR>g : (a : ι) → Set (Set (π a))<VAR>inst✝ : Finite ι<VAR>hg : ∀ (a : ι), ⋃₀ g a = univ<VAR>val✝ : Fintype ι<GOAL>Pi.topologicalSpace = generateFrom {t | ∃ s, (∀ (a : ι), s a ∈ g a) ∧ t = univ.pi s}
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>ι : Type u_5<VAR>π✝ : ι → Type u_6<VAR>κ : Type u_7<VAR>inst✝¹ : TopologicalSpace X<VAR>T : (i : ι) → TopologicalSpace (π✝ i)<VAR>f : X → (i : ι) → π✝ i<VAR>π : ι → Type u_8<VAR>g : (a : ι) → Set (Set (π a))<VAR>inst✝ : Finite ι<VAR>hg : ∀ (a : ι), ⋃₀ g a = univ<VAR>val✝ : Fintype ι<GOAL>generateFrom {t | ∃ s i, (∀ a ∈ i, s a ∈ g a) ∧ t = (↑i).pi s} = generateFrom {t | ∃ s, (∀ (a : ι), s a ∈ g a) ∧ t = univ.pi s}
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>ι : Type u_5<VAR>π✝ : ι → Type u_6<VAR>κ : Type u_7<VAR>inst✝¹ : TopologicalSpace X<VAR>T : (i : ι) → TopologicalSpace (π✝ i)<VAR>f : X → (i : ι) → π✝ i<VAR>π : ι → Type u_8<VAR>g : (a : ι) → Set (Set (π a))<VAR>inst✝ : Finite ι<VAR>hg : ∀ (a : ι), ⋃₀ g a = univ<VAR>val✝ : Fintype ι<GOAL>{t | ∃ s, (∀ (a : ι), s a ∈ g a) ∧ t = univ.pi s} ⊆ {t | ∃ s i, (∀ a ∈ i, s a ∈ g a) ∧ t = (↑i).pi s}
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>ι : Type u_5<VAR>π✝ : ι → Type u_6<VAR>κ : Type u_7<VAR>inst✝¹ : TopologicalSpace X<VAR>T : (i : ι) → TopologicalSpace (π✝ i)<VAR>f : X → (i : ι) → π✝ i<VAR>π : ι → Type u_8<VAR>g : (a : ι) → Set (Set (π a))<VAR>inst✝ : Finite ι<VAR>hg : ∀ (a : ι), ⋃₀ g a = univ<VAR>val✝ : Fintype ι<GOAL>∀ s ∈ {t | ∃ s i, (∀ a ∈ i, s a ∈ g a) ∧ t = (↑i).pi s}, IsOpen s
<VAR>R✝ : Type u<VAR>S : Type v<VAR>a b : R✝<VAR>n✝ m : ℕ<VAR>inst✝¹ : Semiring R✝<VAR>p q r : R✝[X]<VAR>n : ℕ<VAR>R : Type u_1<VAR>inst✝ : Semiring R<GOAL>(↑n).coeff 0 = ↑n
<VAR>n d : ℕ<VAR>hnd : d ∣ n<GOAL>φ (n / d) = (filter (fun k => n.gcd k = d) (range n)).card
<VAR>n : ℕ<VAR>hnd : 0 ∣ n<GOAL>φ (n / 0) = (filter (fun k => n.gcd k = 0) (range n)).card
<VAR>n d : ℕ<VAR>hnd : d ∣ n<VAR>hd0 : d > 0<GOAL>φ (n / d) = (filter (fun k => n.gcd k = d) (range n)).card
<VAR>d : ℕ<VAR>hd0 : d > 0<VAR>x : ℕ<GOAL>φ (d * x / d) = (filter (fun k => (d * x).gcd k = d) (range (d * x))).card
<VAR>d : ℕ<VAR>hd0 : d > 0<VAR>x : ℕ<GOAL>φ x = (filter (fun k => (d * x).gcd k = d) (range (d * x))).card
<VAR>d : ℕ<VAR>hd0 : d > 0<VAR>x : ℕ<GOAL>∀ a ∈ filter x.Coprime (range x), d * a ∈ filter (fun k => (d * x).gcd k = d) (range (d * x))
<VAR>d : ℕ<VAR>hd0 : d > 0<VAR>x : ℕ<GOAL>∀ a₁ ∈ filter x.Coprime (range x), ∀ a₂ ∈ filter x.Coprime (range x), d * a₁ = d * a₂ → a₁ = a₂
<VAR>d : ℕ<VAR>hd0 : d > 0<VAR>x : ℕ<GOAL>∀ b ∈ filter (fun k => (d * x).gcd k = d) (range (d * x)), ∃ a, ∃ (_ : a ∈ filter x.Coprime (range x)), d * a = b
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝² : SeminormedRing 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : SMul 𝕜 E<VAR>p✝ : Seminorm 𝕜 E<VAR>x y : E<VAR>r✝ : ℝ<VAR>p : ι → Seminorm 𝕜 E<VAR>s : Finset ι<VAR>H : s.Nonempty<VAR>e : E<VAR>r : ℝ<GOAL>(s.sup' H p).closedBall e r = s.inf' H fun i => (p i).closedBall e r
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedCommGroup α<VAR>a b : α<VAR>hab : a ≤ b<GOAL>mabs (a * b) = mabs a * mabs b ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedCommGroup α<VAR>a b : α<VAR>hab : a ≤ b<VAR>ha : 1 ≤ a<VAR>hb : 1 ≤ b<GOAL>mabs (a * b) = mabs a * mabs b ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedCommGroup α<VAR>a b : α<VAR>hab : a ≤ b<VAR>ha : 1 ≤ a<VAR>hb : b < 1<GOAL>mabs (a * b) = mabs a * mabs b ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedCommGroup α<VAR>a b : α<VAR>hab : a ≤ b<VAR>ha : a < 1<VAR>hb : 1 ≤ b<GOAL>mabs (a * b) = mabs a * mabs b ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedCommGroup α<VAR>a b : α<VAR>hab : a ≤ b<VAR>ha : a < 1<VAR>hb : b < 1<GOAL>mabs (a * b) = mabs a * mabs b ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedCommGroup α<VAR>a b : α<VAR>hab : a ≤ b<VAR>ha : a < 1<VAR>hb : 1 ≤ b<VAR>this : (mabs (a * b) = a⁻¹ * b ↔ b ≤ 1) ↔ (mabs (a * b) = mabs a * mabs b ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1)<GOAL>mabs (a * b) = mabs a * mabs b ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedCommGroup α<VAR>a b : α<VAR>hab : a ≤ b<VAR>ha : a < 1<VAR>hb : 1 ≤ b<VAR>this : (mabs (a * b) = a⁻¹ * b ↔ b ≤ 1) ↔ (mabs (a * b) = mabs a * mabs b ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1)<VAR>h : mabs (a * b) = a⁻¹ * b<GOAL>b ≤ 1
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedCommGroup α<VAR>a b : α<VAR>hab : a ≤ b<VAR>ha : a < 1<VAR>hb : 1 ≤ b<VAR>this : (mabs (a * b) = a⁻¹ * b ↔ b ≤ 1) ↔ (mabs (a * b) = mabs a * mabs b ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1)<VAR>h : mabs (a * b) = a⁻¹ * b<VAR>ab : a * b ≤ 1<GOAL>b ≤ 1
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedCommGroup α<VAR>a b : α<VAR>hab : a ≤ b<VAR>ha : a < 1<VAR>hb : 1 ≤ b<VAR>this : (mabs (a * b) = a⁻¹ * b ↔ b ≤ 1) ↔ (mabs (a * b) = mabs a * mabs b ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1)<VAR>h : mabs (a * b) = a⁻¹ * b<VAR>ab : 1 < a * b<GOAL>b ≤ 1
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : SemilatticeSup α<VAR>b c : α<VAR>inst✝ : OrderBot α<VAR>s : Finset ι<VAR>f : ι → α<VAR>ha : SupIrred ⊥<GOAL>False
<VAR>E : Type u_1<VAR>f✝ : ℝ → E<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f f' : ℝ → ℝ<VAR>g : ℝ → E<VAR>a : ℝ<VAR>hf : ContinuousOn f (Ici a)<VAR>hft : Tendsto f atTop atTop<VAR>hff' : ∀ x ∈ Ioi a, HasDerivWithinAt f (f' x) (Ioi x) x<VAR>hg_cont : ContinuousOn g (f '' Ioi a)<VAR>hg1 : IntegrableOn g (f '' Ici a) volume<VAR>hg2 : IntegrableOn (fun x => f' x • (g ∘ f) x) (Ici a) volume<VAR>eq : ∀ (b : ℝ), a < b → ∫ (x : ℝ) in a..b, f' x • (g ∘ f) x = ∫ (u : ℝ) in f a..f b, g u<GOAL>∫ (x : ℝ) in Ioi a, f' x • (g ∘ f) x = ∫ (u : ℝ) in Ioi (f a), g u
<VAR>E : Type u_1<VAR>f✝ : ℝ → E<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f f' : ℝ → ℝ<VAR>g : ℝ → E<VAR>a : ℝ<VAR>hf : ContinuousOn f (Ici a)<VAR>hft : Tendsto f atTop atTop<VAR>hff' : ∀ x ∈ Ioi a, HasDerivWithinAt f (f' x) (Ioi x) x<VAR>hg_cont : ContinuousOn g (f '' Ioi a)<VAR>hg1 : IntegrableOn g (f '' Ici a) volume<VAR>hg2 : IntegrableOn (fun x => f' x • (g ∘ f) x) (Ioi a) volume<VAR>eq : ∀ (b : ℝ), a < b → ∫ (x : ℝ) in a..b, f' x • (g ∘ f) x = ∫ (u : ℝ) in f a..f b, g u<GOAL>∫ (x : ℝ) in Ioi a, f' x • (g ∘ f) x = ∫ (u : ℝ) in Ioi (f a), g u
<VAR>E : Type u_1<VAR>f✝ : ℝ → E<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f f' : ℝ → ℝ<VAR>g : ℝ → E<VAR>a : ℝ<VAR>hf : ContinuousOn f (Ici a)<VAR>hft : Tendsto f atTop atTop<VAR>hff' : ∀ x ∈ Ioi a, HasDerivWithinAt f (f' x) (Ioi x) x<VAR>hg_cont : ContinuousOn g (f '' Ioi a)<VAR>hg1 : IntegrableOn g (f '' Ici a) volume<VAR>hg2 : IntegrableOn (fun x => f' x • (g ∘ f) x) (Ioi a) volume<VAR>eq : ∀ (b : ℝ), a < b → ∫ (x : ℝ) in a..b, f' x • (g ∘ f) x = ∫ (u : ℝ) in f a..f b, g u<VAR>t2 : Tendsto (fun i => ∫ (x : ℝ) in a..id i, f' x • (g ∘ f) x) atTop (𝓝 (∫ (x : ℝ) in Ioi a, f' x • (g ∘ f) x ∂volume))<GOAL>∫ (x : ℝ) in Ioi a, f' x • (g ∘ f) x = ∫ (u : ℝ) in Ioi (f a), g u
<VAR>E : Type u_1<VAR>f✝ : ℝ → E<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f f' : ℝ → ℝ<VAR>g : ℝ → E<VAR>a : ℝ<VAR>hf : ContinuousOn f (Ici a)<VAR>hft : Tendsto f atTop atTop<VAR>hff' : ∀ x ∈ Ioi a, HasDerivWithinAt f (f' x) (Ioi x) x<VAR>hg_cont : ContinuousOn g (f '' Ioi a)<VAR>hg1 : IntegrableOn g (f '' Ici a) volume<VAR>hg2 : IntegrableOn (fun x => f' x • (g ∘ f) x) (Ioi a) volume<VAR>eq : ∀ (b : ℝ), a < b → ∫ (x : ℝ) in a..b, f' x • (g ∘ f) x = ∫ (u : ℝ) in f a..f b, g u<VAR>t2 : Tendsto (fun i => ∫ (x : ℝ) in a..id i, f' x • (g ∘ f) x) atTop (𝓝 (∫ (x : ℝ) in Ioi a, f' x • (g ∘ f) x ∂volume))<VAR>this : Ioi (f a) ⊆ f '' Ici a<GOAL>∫ (x : ℝ) in Ioi a, f' x • (g ∘ f) x = ∫ (u : ℝ) in Ioi (f a), g u
<VAR>E : Type u_1<VAR>f✝ : ℝ → E<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f f' : ℝ → ℝ<VAR>g : ℝ → E<VAR>a : ℝ<VAR>hf : ContinuousOn f (Ici a)<VAR>hft : Tendsto f atTop atTop<VAR>hff' : ∀ x ∈ Ioi a, HasDerivWithinAt f (f' x) (Ioi x) x<VAR>hg_cont : ContinuousOn g (f '' Ioi a)<VAR>hg1 : IntegrableOn g (f '' Ici a) volume<VAR>hg2 : IntegrableOn (fun x => f' x • (g ∘ f) x) (Ioi a) volume<VAR>eq : ∀ (b : ℝ), a < b → ∫ (x : ℝ) in a..b, f' x • (g ∘ f) x = ∫ (u : ℝ) in f a..f b, g u<VAR>t2 : Tendsto (fun i => ∫ (x : ℝ) in a..id i, f' x • (g ∘ f) x) atTop (𝓝 (∫ (x : ℝ) in Ioi a, f' x • (g ∘ f) x ∂volume))<VAR>this : Ioi (f a) ⊆ f '' Ici a<VAR>t1 : Tendsto ((fun i => ∫ (x : ℝ) in f a..id i, g x) ∘ f) atTop (𝓝 (∫ (x : ℝ) in Ioi (f a), g x ∂volume))<GOAL>∫ (x : ℝ) in Ioi a, f' x • (g ∘ f) x = ∫ (u : ℝ) in Ioi (f a), g u
<VAR>G : PGame<VAR>inst✝ : G.Impartial<VAR>H : PGame<GOAL>H ≈ G ↔ H + G ≈ 0
<VAR>G : PGame<VAR>inst✝ : G.Impartial<VAR>H : PGame<GOAL>⟦H + G⟧ = 0 ↔ ⟦H + G⟧ = ⟦0⟧