ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι✝ : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>K : Set α<VAR>ι : Sort u_2<VAR>U : ι → Set α<VAR>hK : IsCompact K<VAR>hopen : ∀ (i : ι), IsOpen (U i)<VAR>hcover : K ⊆ ⋃ i, U i<VAR>ind : (x : α) → x ∈ K → ι<VAR>W : (x : α) → x ∈ K → Set (α × α)<VAR>hW : ∀ (x : α) (a : x ∈ K), W x a ∈ 𝓤 α<VAR>hWU : ∀ (x : α) (a : x ∈ K), ball x (W x a ○ W x a) ⊆ U (ind x a)<VAR>t : Finset ↑K<VAR>ht : K ⊆ ⋃ x ∈ t, ball (↑x) (W ↑x ⋯)<GOAL>∃ V ∈ 𝓤 α, ∀ x ∈ K, ∃ i, ball x V ⊆ U i
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι✝ : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>K : Set α<VAR>ι : Sort u_2<VAR>U : ι → Set α<VAR>hK : IsCompact K<VAR>hopen : ∀ (i : ι), IsOpen (U i)<VAR>hcover : K ⊆ ⋃ i, U i<VAR>ind : (x : α) → x ∈ K → ι<VAR>W : (x : α) → x ∈ K → Set (α × α)<VAR>hW : ∀ (x : α) (a : x ∈ K), W x a ∈ 𝓤 α<VAR>hWU : ∀ (x : α) (a : x ∈ K), ball x (W x a ○ W x a) ⊆ U (ind x a)<VAR>t : Finset ↑K<VAR>ht : K ⊆ ⋃ x ∈ t, ball (↑x) (W ↑x ⋯)<VAR>x : α<VAR>hx : x ∈ K<GOAL>∃ i, ball x (⋂ x ∈ t, W ↑x ⋯) ⊆ U i
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι✝ : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>K : Set α<VAR>ι : Sort u_2<VAR>U : ι → Set α<VAR>hK : IsCompact K<VAR>hopen : ∀ (i : ι), IsOpen (U i)<VAR>hcover : K ⊆ ⋃ i, U i<VAR>ind : (x : α) → x ∈ K → ι<VAR>W : (x : α) → x ∈ K → Set (α × α)<VAR>hW : ∀ (x : α) (a : x ∈ K), W x a ∈ 𝓤 α<VAR>hWU : ∀ (x : α) (a : x ∈ K), ball x (W x a ○ W x a) ⊆ U (ind x a)<VAR>t : Finset ↑K<VAR>ht : K ⊆ ⋃ x ∈ t, ball (↑x) (W ↑x ⋯)<VAR>x : α<VAR>hx : x ∈ K<VAR>y : ↑K<VAR>hyt : y ∈ t<VAR>hxy : x ∈ ball (↑y) (W ↑y ⋯)<GOAL>∃ i, ball x (⋂ x ∈ t, W ↑x ⋯) ⊆ U i
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝⁶ : EMetricSpace X<VAR>inst✝⁵ : EMetricSpace Y<VAR>C K r : ℝ≥0<VAR>f : X → Y<VAR>s✝ t : Set X<VAR>E : Type u_4<VAR>F : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : FiniteDimensional ℝ E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>s : Set E<VAR>hs : dimH s < ↑(finrank ℝ E)<GOAL>Dense sᶜ
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝⁶ : EMetricSpace X<VAR>inst✝⁵ : EMetricSpace Y<VAR>C K r : ℝ≥0<VAR>f : X → Y<VAR>s✝ t✝ : Set X<VAR>E : Type u_4<VAR>F : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : FiniteDimensional ℝ E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>s : Set E<VAR>hs : dimH s < ↑(finrank ℝ E)<VAR>x : E<VAR>t : Set E<VAR>ht : t ∈ 𝓝 x<VAR>he : t ∩ sᶜ = ∅<GOAL>↑(finrank ℝ E) ≤ dimH s
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝⁶ : EMetricSpace X<VAR>inst✝⁵ : EMetricSpace Y<VAR>C K r : ℝ≥0<VAR>f : X → Y<VAR>s✝ t✝ : Set X<VAR>E : Type u_4<VAR>F : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : FiniteDimensional ℝ E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>s : Set E<VAR>hs : dimH s < ↑(finrank ℝ E)<VAR>x : E<VAR>t : Set E<VAR>ht : t ∈ 𝓝 x<VAR>he : t ⊆ s<GOAL>↑(finrank ℝ E) ≤ dimH s
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝⁶ : EMetricSpace X<VAR>inst✝⁵ : EMetricSpace Y<VAR>C K r : ℝ≥0<VAR>f : X → Y<VAR>s✝ t✝ : Set X<VAR>E : Type u_4<VAR>F : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : FiniteDimensional ℝ E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>s : Set E<VAR>hs : dimH s < ↑(finrank ℝ E)<VAR>x : E<VAR>t : Set E<VAR>ht : t ∈ 𝓝 x<VAR>he : t ⊆ s<GOAL>dimH t ≤ dimH s
<VAR>ι : Type u_1<VAR>F : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>δ : Type u_6<VAR>inst✝⁴ : FunLike F α β<VAR>inst✝³ : Group α<VAR>inst✝² : AddCommSemigroup β<VAR>inst✝¹ : LE β<VAR>inst✝ : MulLEAddHomClass F α β<VAR>f : F<VAR>a b c : α<GOAL>f (a / c) ≤ f (a / b) + f (b / c)
<VAR>M : Type w<VAR>A : Set M<VAR>L : Language<VAR>inst✝ : L.Structure M<VAR>α : Type u₁<VAR>β : Type u_1<VAR>B : Set M<VAR>s✝ : Set (α → M)<VAR>ι : Type u_2<VAR>f : ι → Set (α → M)<VAR>hf : ∀ (i : ι), A.Definable L (f i)<VAR>s : Finset ι<GOAL>A.Definable L (s.inf f)
<GOAL>(1 + √5) * (1 - √5) = -(2 * 2)
<GOAL>1 ^ 2 - √5 ^ 2 = -(2 * 2)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring S<VAR>inst✝ : Algebra R S<VAR>M N : Submodule R S<VAR>hc : ∀ (m : ↥M) (n : ↥N), Commute ↑m ↑n<GOAL>N.mulMap M = M.mulMap N ∘ₗ ↑(TensorProduct.comm R ↥N ↥M)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring S<VAR>inst✝ : Algebra R S<VAR>M N : Submodule R S<VAR>hc : ∀ (m : ↥M) (n : ↥N), Commute ↑m ↑n<VAR>n : ↥N<VAR>m : ↥M<GOAL>(N.mulMap M) (n ⊗ₜ[R] m) = (M.mulMap N ∘ₗ ↑(TensorProduct.comm R ↥N ↥M)) (n ⊗ₜ[R] m)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring S<VAR>inst✝ : Algebra R S<VAR>M N : Submodule R S<VAR>hc : ∀ (m : ↥M) (n : ↥N), Commute ↑m ↑n<VAR>n : ↥N<VAR>m : ↥M<GOAL>↑n * ↑m = ↑m * ↑n
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_2, u_1} C<VAR>inst✝² : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.LeftHomologyData<VAR>h₂ : S₂.LeftHomologyData<VAR>γ : LeftHomologyMapData φ h₁ h₂<VAR>inst✝¹ : S₁.HasLeftHomology<VAR>inst✝ : S₂.HasLeftHomology<GOAL>leftHomologyMap φ = leftHomologyMap' (𝟙 S₁) S₁.leftHomologyData h₁ ≫ γ.φH ≫ leftHomologyMap' (𝟙 S₂) h₂ S₂.leftHomologyData
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_2, u_1} C<VAR>inst✝² : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.LeftHomologyData<VAR>h₂ : S₂.LeftHomologyData<VAR>γ : LeftHomologyMapData φ h₁ h₂<VAR>inst✝¹ : S₁.HasLeftHomology<VAR>inst✝ : S₂.HasLeftHomology<GOAL>leftHomologyMap φ = leftHomologyMap' φ S₁.leftHomologyData S₂.leftHomologyData
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>μ ν : Measure α<VAR>s t N : Set α<VAR>f : α → ℝ≥0∞<VAR>inst✝ : IsFiniteMeasure μ<VAR>hμ : μ ≠ 0<VAR>hf : AEMeasurable f μ<VAR>hN : μ N = 0<GOAL>∃ x ∉ N, f x ≤ ⨍⁻ (a : α), f a ∂μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>μ ν : Measure α<VAR>s t N : Set α<VAR>f : α → ℝ≥0∞<VAR>inst✝ : IsFiniteMeasure μ<VAR>hμ : μ ≠ 0<VAR>hf : AEMeasurable f μ<VAR>hN : μ N = 0<VAR>this : 0 < μ {x | f x ≤ ⨍⁻ (a : α), f a ∂μ}<GOAL>∃ x ∉ N, f x ≤ ⨍⁻ (a : α), f a ∂μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>μ ν : Measure α<VAR>s t N : Set α<VAR>f : α → ℝ≥0∞<VAR>inst✝ : IsFiniteMeasure μ<VAR>hμ : μ ≠ 0<VAR>hf : AEMeasurable f μ<VAR>hN : μ N = 0<VAR>this : 0 < μ ({x | f x ≤ ⨍⁻ (a : α), f a ∂μ} \ N)<GOAL>∃ x ∉ N, f x ≤ ⨍⁻ (a : α), f a ∂μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>μ ν : Measure α<VAR>s t N : Set α<VAR>f : α → ℝ≥0∞<VAR>inst✝ : IsFiniteMeasure μ<VAR>hμ : μ ≠ 0<VAR>hf : AEMeasurable f μ<VAR>hN : μ N = 0<VAR>this : 0 < μ ({x | f x ≤ ⨍⁻ (a : α), f a ∂μ} \ N)<VAR>x : α<VAR>hx : x ∈ {x | f x ≤ ⨍⁻ (a : α), f a ∂μ}<VAR>hxN : x ∉ N<GOAL>∃ x ∉ N, f x ≤ ⨍⁻ (a : α), f a ∂μ
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁵ : CommRing P<VAR>inst✝⁴ : Algebra R P<VAR>loc : IsLocalization S P<VAR>P' : Type u_3<VAR>inst✝³ : CommRing P'<VAR>inst✝² : Algebra R P'<VAR>loc' : IsLocalization S P'<VAR>P'' : Type u_4<VAR>inst✝¹ : CommRing P''<VAR>inst✝ : Algebra R P''<VAR>loc'' : IsLocalization S P''<VAR>I✝ J : FractionalIdeal S P<VAR>g : P →ₐ[R] P'<VAR>I : FractionalIdeal S P<VAR>x : P'<GOAL>x ∈ (canonicalEquiv S P P') I ↔ ∃ y ∈ I, (IsLocalization.map P' (RingHom.id R) ⋯) y = x
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁵ : CommRing P<VAR>inst✝⁴ : Algebra R P<VAR>loc : IsLocalization S P<VAR>P' : Type u_3<VAR>inst✝³ : CommRing P'<VAR>inst✝² : Algebra R P'<VAR>loc' : IsLocalization S P'<VAR>P'' : Type u_4<VAR>inst✝¹ : CommRing P''<VAR>inst✝ : Algebra R P''<VAR>loc'' : IsLocalization S P''<VAR>I✝ J : FractionalIdeal S P<VAR>g : P →ₐ[R] P'<VAR>I : FractionalIdeal S P<VAR>x : P'<GOAL>(∃ x_1 ∈ I, ↑(let __src := ringEquivOfRingEquiv P P' (RingEquiv.refl R) ⋯; { toEquiv := __src.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }) x_1 = x) ↔ ∃ y ∈ I, (IsLocalization.map P' (RingHom.id R) ⋯) y = x
<VAR>α : Type u_1<VAR>inst✝ : LinearOrder α<VAR>s✝ t✝ : Set α<VAR>x✝ y z : α<VAR>s t : Set α<VAR>x : α<GOAL>(s ∩ t).ordConnectedComponent x = s.ordConnectedComponent x ∩ t.ordConnectedComponent x
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>inst✝ : Group G<VAR>hN : Nontrivial G<VAR>tG : IsTorsion G<GOAL>∃ g, g ≠ 1 ∧ IsOfFinOrder g
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>inst✝ : Group G<VAR>hN : Nontrivial G<VAR>tG : IsTorsion G<VAR>x : G<VAR>hx : x ≠ 1<GOAL>∃ g, g ≠ 1 ∧ IsOfFinOrder g
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>h₁ : ∑ x : α, 0 = 0<GOAL>Tendsto (fun p => ∑ i : α, a i * b i ^ p) atTop (𝓝 (∑ x : α, 0))
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>h₁ : ∑ x : α, 0 = 0<VAR>i : α<VAR>x✝ : i ∈ univ<GOAL>Tendsto (fun p => a i * b i ^ p) atTop (𝓝 0)
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>h₁ : ∑ x : α, 0 = 0<VAR>i : α<VAR>x✝ : i ∈ univ<GOAL>Tendsto (fun p => a i * b i ^ p) atTop (𝓝 (a i * 0))
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>h₁ : ∑ x : α, 0 = 0<VAR>i : α<VAR>x✝ : i ∈ univ<GOAL>-1 < b i
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>h₁ : ∑ x : α, 0 = 0<VAR>i : α<VAR>x✝ : i ∈ univ<VAR>this : 0 < b i<GOAL>-1 < b i
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>W✝ : Affine R<VAR>f : R →+* S<VAR>F : Type u<VAR>inst✝ : Field F<VAR>W : Affine F<VAR>x y : F<VAR>h : W.Nonsingular x y<GOAL>↑(XYIdeal W x (C y)) * (↑(XYIdeal W x (C (W.negY x y))) * (↑(XIdeal W x))⁻¹) = 1
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>p : ι → P<VAR>i : ι<GOAL>centroid k {i} p = p i
<VAR>α : Type u_1<VAR>β : α → Type u<VAR>δ : α → Sort v<VAR>inst✝ : DecidableEq α<VAR>s✝ : Finset α<VAR>t : (a : α) → Finset (β a)<VAR>a : α<VAR>b : δ a<VAR>s : Finset α<VAR>hs : a ∉ s<VAR>e₁ e₂ : (a : α) → a ∈ s → δ a<VAR>eq : cons s a b e₁ = cons s a b e₂<VAR>e : α<VAR>h : e ∈ a ::ₘ s.val<GOAL>e ∈ insert a s
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M₂ : Type u_3<VAR>M₁ : ι → Type u_4<VAR>inst✝⁹ : Finite ι<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : AddCommGroup M₂<VAR>inst✝⁶ : Module R M₂<VAR>inst✝⁵ : Module.Finite R M₂<VAR>inst✝⁴ : Module.Free R M₂<VAR>inst✝³ : (i : ι) → AddCommGroup (M₁ i)<VAR>inst✝² : (i : ι) → Module R (M₁ i)<VAR>inst✝¹ : ∀ (i : ι), Module.Finite R (M₁ i)<VAR>inst✝ : ∀ (i : ι), Module.Free R (M₁ i)<GOAL>Module.Free R (MultilinearMap R M₁ M₂) ∧ Module.Finite R (MultilinearMap R M₁ M₂)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M₂ : Type u_3<VAR>M₁ : ι → Type u_4<VAR>inst✝⁹ : Finite ι<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : AddCommGroup M₂<VAR>inst✝⁶ : Module R M₂<VAR>inst✝⁵ : Module.Finite R M₂<VAR>inst✝⁴ : Module.Free R M₂<VAR>inst✝³ : (i : ι) → AddCommGroup (M₁ i)<VAR>inst✝² : (i : ι) → Module R (M₁ i)<VAR>inst✝¹ : ∀ (i : ι), Module.Finite R (M₁ i)<VAR>inst✝ : ∀ (i : ι), Module.Free R (M₁ i)<VAR>val✝ : Fintype ι<GOAL>Module.Free R (MultilinearMap R M₁ M₂) ∧ Module.Finite R (MultilinearMap R M₁ M₂)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M₂ : Type u_3<VAR>M₁ : ι → Type u_4<VAR>inst✝⁹ : Finite ι<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : AddCommGroup M₂<VAR>inst✝⁶ : Module R M₂<VAR>inst✝⁵ : Module.Finite R M₂<VAR>inst✝⁴ : Module.Free R M₂<VAR>inst✝³ : (i : ι) → AddCommGroup (M₁ i)<VAR>inst✝² : (i : ι) → Module R (M₁ i)<VAR>inst✝¹ : ∀ (i : ι), Module.Finite R (M₁ i)<VAR>inst✝ : ∀ (i : ι), Module.Free R (M₁ i)<VAR>val✝ : Fintype ι<VAR>this : ∀ [inst : (i : Fin (Fintype.card ι)) → AddCommGroup (M₁ ((Fintype.equivFin ι).symm i))] [inst_1 : (i : Fin (Fintype.card ι)) → Module R (M₁ ((Fintype.equivFin ι).symm i))] [inst_2 : ∀ (i : Fin (Fintype.card ι)), Module.Finite R (M₁ ((Fintype.equivFin ι).symm i))] [inst_3 : ∀ (i : Fin (Fintype.card ι)), Module.Free R (M₁ ((Fintype.equivFin ι).symm i))], Module.Free R (MultilinearMap R (fun x => M₁ ((Fintype.equivFin ι).symm x)) M₂) ∧ Module.Finite R (MultilinearMap R (fun x => M₁ ((Fintype.equivFin ι).symm x)) M₂)<GOAL>Module.Free R (MultilinearMap R M₁ M₂) ∧ Module.Finite R (MultilinearMap R M₁ M₂)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M₂ : Type u_3<VAR>M₁ : ι → Type u_4<VAR>inst✝⁹ : Finite ι<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : AddCommGroup M₂<VAR>inst✝⁶ : Module R M₂<VAR>inst✝⁵ : Module.Finite R M₂<VAR>inst✝⁴ : Module.Free R M₂<VAR>inst✝³ : (i : ι) → AddCommGroup (M₁ i)<VAR>inst✝² : (i : ι) → Module R (M₁ i)<VAR>inst✝¹ : ∀ (i : ι), Module.Finite R (M₁ i)<VAR>inst✝ : ∀ (i : ι), Module.Free R (M₁ i)<VAR>val✝ : Fintype ι<VAR>this : ∀ [inst : (i : Fin (Fintype.card ι)) → AddCommGroup (M₁ ((Fintype.equivFin ι).symm i))] [inst_1 : (i : Fin (Fintype.card ι)) → Module R (M₁ ((Fintype.equivFin ι).symm i))] [inst_2 : ∀ (i : Fin (Fintype.card ι)), Module.Finite R (M₁ ((Fintype.equivFin ι).symm i))] [inst_3 : ∀ (i : Fin (Fintype.card ι)), Module.Free R (M₁ ((Fintype.equivFin ι).symm i))], Module.Free R (MultilinearMap R (fun x => M₁ ((Fintype.equivFin ι).symm x)) M₂) ∧ Module.Finite R (MultilinearMap R (fun x => M₁ ((Fintype.equivFin ι).symm x)) M₂)<VAR>l : Module.Free R (MultilinearMap R (fun x => M₁ ((Fintype.equivFin ι).symm x)) M₂)<VAR>r : Module.Finite R (MultilinearMap R (fun x => M₁ ((Fintype.equivFin ι).symm x)) M₂)<VAR>e : MultilinearMap R M₁ M₂ ≃ₗ[R] MultilinearMap R (fun i => M₁ ((Fintype.equivFin ι).symm i)) M₂<GOAL>Module.Free R (MultilinearMap R M₁ M₂) ∧ Module.Finite R (MultilinearMap R M₁ M₂)
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ q r p : R[X]<GOAL>∑ i ∈ range (p.natDegree + 1), (monomial i) (p.coeff i) = ∑ i ∈ range (p.natDegree + 1), C (p.coeff i) * X ^ i
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type uX<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x✝ x₀ : E<VAR>c : F<VAR>m✝ n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>h : HasFTaylorSeriesUpTo n f p<VAR>m : ℕ<VAR>hmn : ↑m ≤ n<VAR>x : E<GOAL>p x m = iteratedFDeriv 𝕜 m f x
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type uX<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x✝ x₀ : E<VAR>c : F<VAR>m✝ n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>h : HasFTaylorSeriesUpTo n f p<VAR>m : ℕ<VAR>hmn : ↑m ≤ n<VAR>x : E<GOAL>p x m = iteratedFDerivWithin 𝕜 m f univ x
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type uX<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x✝ x₀ : E<VAR>c : F<VAR>m✝ n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>h : HasFTaylorSeriesUpToOn n f p univ<VAR>m : ℕ<VAR>hmn : ↑m ≤ n<VAR>x : E<GOAL>p x m = iteratedFDerivWithin 𝕜 m f univ x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s s₁ s₂ : Finset α<VAR>t t₁ t₂ : α → Finset β<VAR>inst✝ : DecidableEq β<VAR>s' : Finset β<GOAL>s.biUnion t ⊆ s' ↔ ∀ x ∈ s, t x ⊆ s'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s s₁ s₂ : Finset α<VAR>t t₁ t₂ : α → Finset β<VAR>inst✝ : DecidableEq β<VAR>s' : Finset β<GOAL>(∀ ⦃x : β⦄, (∃ a ∈ s, x ∈ t a) → x ∈ s') ↔ ∀ x ∈ s, ∀ ⦃x_1 : β⦄, x_1 ∈ t x → x_1 ∈ s'
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasProducts C<VAR>X : TopCat<VAR>F : Presheaf C X<VAR>ι : Type v'<VAR>U : ι → Opens ↑X<VAR>c d : Cone (SheafConditionEqualizerProducts.diagram F U)<VAR>f : c ⟶ d<GOAL>f.hom ≫ 𝟙 d.pt = 𝟙 c.pt ≫ f.hom
<VAR>α : Type u_1<VAR>P : α → Prop<VAR>l : Ordnode α<VAR>x : α<VAR>m : Ordnode α<VAR>y : α<VAR>r : Ordnode α<GOAL>All P (l.node3L x m y r) ↔ All P l ∧ P x ∧ All P m ∧ P y ∧ All P r
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>σ : Type u_4<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : SetLike σ M<VAR>inst✝¹ : AddSubmonoidClass σ M<VAR>ℳ : ι → σ<VAR>inst✝ : Decomposition ℳ<VAR>i : ι<VAR>x : ↥(ℳ i)<GOAL>(decompose ℳ) ↑x = (of (fun i => ↥(ℳ i)) i) x
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>inst✝¹ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : Solution hζ<VAR>S' : Solution' hζ<VAR>inst✝ : DecidableRel fun a b => a ∣ b<GOAL>λ ^ 4 ∣ S'.a ^ 3 - 1 ∧ λ ^ 4 ∣ S'.b ^ 3 + 1 ∨ λ ^ 4 ∣ S'.a ^ 3 + 1 ∧ λ ^ 4 ∣ S'.b ^ 3 - 1
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>inst✝¹ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : Solution hζ<VAR>S' : Solution' hζ<VAR>inst✝ : DecidableRel fun a b => a ∣ b<VAR>z : 𝓞 K<VAR>hz : S'.c = λ * z<GOAL>λ ^ 4 ∣ S'.a ^ 3 - 1 ∧ λ ^ 4 ∣ S'.b ^ 3 + 1 ∨ λ ^ 4 ∣ S'.a ^ 3 + 1 ∧ λ ^ 4 ∣ S'.b ^ 3 - 1
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>inst✝¹ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : Solution hζ<VAR>S' : Solution' hζ<VAR>inst✝ : DecidableRel fun a b => a ∣ b<VAR>z : 𝓞 K<VAR>hz : S'.c = λ * z<VAR>x : 𝓞 K<VAR>hx : S'.a ^ 3 - 1 = λ ^ 4 * x<VAR>y : 𝓞 K<VAR>hy : S'.b ^ 3 - 1 = λ ^ 4 * y<GOAL>λ ^ 4 ∣ S'.a ^ 3 - 1 ∧ λ ^ 4 ∣ S'.b ^ 3 + 1 ∨ λ ^ 4 ∣ S'.a ^ 3 + 1 ∧ λ ^ 4 ∣ S'.b ^ 3 - 1
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>inst✝¹ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : Solution hζ<VAR>S' : Solution' hζ<VAR>inst✝ : DecidableRel fun a b => a ∣ b<VAR>z : 𝓞 K<VAR>hz : S'.c = λ * z<VAR>x : 𝓞 K<VAR>hx : S'.a ^ 3 - 1 = λ ^ 4 * x<VAR>y : 𝓞 K<VAR>hy : S'.b ^ 3 + 1 = λ ^ 4 * y<GOAL>λ ^ 4 ∣ S'.a ^ 3 - 1 ∧ λ ^ 4 ∣ S'.b ^ 3 + 1 ∨ λ ^ 4 ∣ S'.a ^ 3 + 1 ∧ λ ^ 4 ∣ S'.b ^ 3 - 1
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>inst✝¹ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : Solution hζ<VAR>S' : Solution' hζ<VAR>inst✝ : DecidableRel fun a b => a ∣ b<VAR>z : 𝓞 K<VAR>hz : S'.c = λ * z<VAR>x : 𝓞 K<VAR>hx : S'.a ^ 3 + 1 = λ ^ 4 * x<VAR>y : 𝓞 K<VAR>hy : S'.b ^ 3 - 1 = λ ^ 4 * y<GOAL>λ ^ 4 ∣ S'.a ^ 3 - 1 ∧ λ ^ 4 ∣ S'.b ^ 3 + 1 ∨ λ ^ 4 ∣ S'.a ^ 3 + 1 ∧ λ ^ 4 ∣ S'.b ^ 3 - 1
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>inst✝¹ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : Solution hζ<VAR>S' : Solution' hζ<VAR>inst✝ : DecidableRel fun a b => a ∣ b<VAR>z : 𝓞 K<VAR>hz : S'.c = λ * z<VAR>x : 𝓞 K<VAR>hx : S'.a ^ 3 + 1 = λ ^ 4 * x<VAR>y : 𝓞 K<VAR>hy : S'.b ^ 3 + 1 = λ ^ 4 * y<GOAL>λ ^ 4 ∣ S'.a ^ 3 - 1 ∧ λ ^ 4 ∣ S'.b ^ 3 + 1 ∨ λ ^ 4 ∣ S'.a ^ 3 + 1 ∧ λ ^ 4 ∣ S'.b ^ 3 - 1
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E'<VAR>inst✝ : NormedSpace 𝕜 E'<VAR>f : E → E'<VAR>s : Set E<VAR>x : E<VAR>f' : TangentSpace 𝓘(𝕜, E) x →L[𝕜] TangentSpace 𝓘(𝕜, E') (f x)<GOAL>HasMFDerivWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E') f s x f' ↔ HasFDerivWithinAt f f' s x
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝ : SemilatticeSup α<VAR>a : α<VAR>f : β → ↑(Ioi a)<VAR>l : Filter β<GOAL>Tendsto f l atTop ↔ Tendsto (fun x => ↑(f x)) l atTop
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>R : Type u_4<VAR>inst✝¹ : Monoid α<VAR>inst✝ : HasDistribNeg α<VAR>a✝ : α<VAR>c : ℕ<VAR>a : α<GOAL>(-a) ^ (2 * c + 1) = -a ^ (2 * c + 1)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>𝕜 : Type u_4<VAR>E : Type u_5<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : CancelCommMonoid α<VAR>s : Finset α<VAR>a : α<GOAL>mulRothNumber (map (mulLeftEmbedding a) s) = mulRothNumber s
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>𝕜 : Type u_4<VAR>E : Type u_5<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : CancelCommMonoid α<VAR>s : Finset α<VAR>a : α<GOAL>mulRothNumber (map (mulLeftEmbedding a) s) ≤ mulRothNumber s
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>𝕜 : Type u_4<VAR>E : Type u_5<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : CancelCommMonoid α<VAR>s : Finset α<VAR>a : α<GOAL>mulRothNumber s ≤ mulRothNumber (map (mulLeftEmbedding a) s)
<VAR>χ : DirichletCharacter ℂ 0<VAR>n : ℕ<GOAL>χ ↑n = δ n
<VAR>χ : DirichletCharacter ℂ 0<GOAL>χ ↑0 = δ 0
<VAR>χ : DirichletCharacter ℂ 0<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>χ ↑n = δ n
<VAR>χ : DirichletCharacter ℂ 0<VAR>hn : 1 ≠ 0<GOAL>χ ↑1 = δ 1
<VAR>χ : DirichletCharacter ℂ 0<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>hn' : n ≠ 1<GOAL>χ ↑n = δ n
<VAR>χ : DirichletCharacter ℂ 0<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>hn' : n ≠ 1<VAR>this : ¬IsUnit ↑n<GOAL>χ ↑n = δ n
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜✝ ℬ : Finset (Finset α)<VAR>s✝ : Finset α<VAR>a✝ a : α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<GOAL>s ∈ memberSubfamily a 𝒜 ∪ nonMemberSubfamily a 𝒜 ↔ s ∈ image (fun s => s.erase a) 𝒜
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜✝ ℬ : Finset (Finset α)<VAR>s✝ : Finset α<VAR>a✝ a : α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<GOAL>insert a s ∈ 𝒜 ∧ a ∉ s ∨ s ∈ 𝒜 ∧ a ∉ s ↔ ∃ a_1 ∈ 𝒜, a_1.erase a = s
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Linear R C<VAR>F G K L : CochainComplex C ℤ<VAR>n m n₁ n₂ n₁₂ : ℤ<VAR>z₁ : Cochain F G n₁<VAR>z₂ : Cochain G K (-n₂)<VAR>z₃ : Cochain K L n₂<VAR>h₁₂ : n₁ + -n₂ = n₁₂<GOAL>n₁₂ + n₂ = n₁
<VAR>α : Type u_1<VAR>N : α → Type u_2<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : (a : α) → DecidableEq (N a)<VAR>inst✝ : (a : α) → AddGroup (N a)<VAR>f f₁ f₂ g g₁ g₂ : Π₀ (a : α), N a<GOAL>f.neLocus g = (f - g).support
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ μ₁ μ₂ ν ν₁ ν₂ : Measure α<VAR>β : Type u_2<VAR>x✝ : MeasurableSpace β<VAR>f : α → β<VAR>hf : MeasurableEmbedding f<VAR>hμν : μ ⟂ₘ ν<GOAL>map f μ ⟂ₘ map f ν
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ μ₁ μ₂ ν ν₁ ν₂ : Measure α<VAR>β : Type u_2<VAR>x✝ : MeasurableSpace β<VAR>f : α → β<VAR>hf : MeasurableEmbedding f<VAR>hμν : μ ⟂ₘ ν<GOAL>(map f μ) (f '' hμν.nullSet) = 0
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ μ₁ μ₂ ν ν₁ ν₂ : Measure α<VAR>β : Type u_2<VAR>x✝ : MeasurableSpace β<VAR>f : α → β<VAR>hf : MeasurableEmbedding f<VAR>hμν : μ ⟂ₘ ν<GOAL>(map f ν) (f '' hμν.nullSet)ᶜ = 0