ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>e : PartialHomeomorph X Y<VAR>x : X<VAR>p : X → Prop<VAR>hx : x ∈ e.source<GOAL>(∀ᶠ (x : X) in 𝓝 x, p (↑e.symm (↑e x))) ↔ ∀ᶠ (x : X) in 𝓝 x, p 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>e : PartialHomeomorph X Y<VAR>x : X<VAR>p : X → Prop<VAR>hx : x ∈ e.source<VAR>y : X<VAR>hy : ↑e.symm (↑e y) = y<GOAL>p (↑e.symm (↑e y)) ↔ p y
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : DecidableEq β<VAR>inst✝¹ : Group α<VAR>inst✝ : MulAction α β<VAR>s t : Finset β<VAR>a : α<VAR>b : β<GOAL>s ⊆ a • t ↔ a⁻¹ • s ⊆ t
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : DecidableEq β<VAR>inst✝¹ : Group α<VAR>inst✝ : MulAction α β<VAR>s t : Finset β<VAR>a : α<VAR>b : β<GOAL>↑s ⊆ ↑(a • t) ↔ ↑(a⁻¹ • s) ⊆ ↑t
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : DecidableEq β<VAR>inst✝¹ : Group α<VAR>inst✝ : MulAction α β<VAR>s t : Finset β<VAR>a : α<VAR>b : β<GOAL>↑s ⊆ a • ↑t ↔ a⁻¹ • ↑s ⊆ ↑t
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : Invertible 2<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>x✝ y✝ z x y : P<GOAL>(pointReflection (midpoint R x y)) y = x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<GOAL>f'' =o[⊤] g' ↔ ∀ (x : α), f'' x = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F✝ : Type u_3<VAR>ι : Type u_4<VAR>π : ι → Type u_5<VAR>inst✝² : OrderedSemiring 𝕜<VAR>inst✝¹ : AddCommMonoid E<VAR>inst✝ : SMul 𝕜 E<VAR>A B C : Set E<VAR>x : E<VAR>F : Set (Set E)<VAR>hF : F.Nonempty<VAR>hAF : ∀ B ∈ F, IsExtreme 𝕜 A B<GOAL>IsExtreme 𝕜 A (⋂₀ F)
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<VAR>f : Filter X<VAR>H : 𝓝 x ≤ f<GOAL>ClusterPt x f
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g : ι → α<GOAL>(∀ u ∈ 𝓤 β, ∀ᶠ (n : ι) in p, ∀ x ∈ s, (f x, F n x) ∈ u) ↔ ∀ u ∈ 𝓤 β, ∀ᶠ (n : ι × α) in p ×ˢ 𝓟 s, (f n.2, F n.1 n.2) ∈ u
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g : ι → α<GOAL>∀ a ∈ 𝓤 β, (∀ᶠ (n : ι) in p, ∀ x ∈ s, (f x, F n x) ∈ a) ↔ ∀ᶠ (n : ι × α) in p ×ˢ 𝓟 s, (f n.2, F n.1 n.2) ∈ a
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g : ι → α<GOAL>∀ a ∈ 𝓤 β, True
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>n : ℕ<VAR>s : Simplex ℝ P n<VAR>i : Fin (n + 1)<GOAL>dist s.circumcenter (s.points i) = s.circumradius
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>n : ℕ<VAR>s : Simplex ℝ P n<VAR>i : Fin (n + 1)<GOAL>dist (s.points i) s.circumcenter = s.circumradius
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : NonAssocSemiring α<VAR>a : α<VAR>n : ℕ<GOAL>n • a = a * ↑n
<VAR>ι : Sort u_1<VAR>f : ι → ℝ≥0<VAR>inst✝ : Nonempty ι<VAR>a g : ℝ≥0<VAR>h : ι → ℝ≥0<VAR>H : ∀ (j : ι), a ≤ g * h j<GOAL>a ≤ g * iInf h
<VAR>ι : Sort u_1<VAR>f : ι → ℝ≥0<VAR>inst✝ : Nonempty ι<VAR>a g : ℝ≥0<VAR>h : ι → ℝ≥0<VAR>H : ∀ (j : ι), a ≤ g * h j<GOAL>a ≤ ⨅ i, g * h i
<VAR>m n : ℕ<VAR>p : Fin (n + 1)<VAR>i✝ j : Fin n<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>e : Fin n ≃o Fin m<VAR>i : ℕ<VAR>hi : i < n<GOAL>↑(e ⟨i, hi⟩) = i
<VAR>m n : ℕ<VAR>p : Fin (n + 1)<VAR>i✝ j : Fin n<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>e : Fin n ≃o Fin m<VAR>i : ℕ<VAR>h : ∀ m_1 < i, ∀ (hi : m_1 < n), ↑(e ⟨m_1, hi⟩) = m_1<VAR>hi : i < n<GOAL>↑(e ⟨i, hi⟩) = i
<VAR>m n : ℕ<VAR>p : Fin (n + 1)<VAR>i✝ j✝ : Fin n<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>e : Fin n ≃o Fin m<VAR>i : ℕ<VAR>h : ∀ m_1 < i, ∀ (hi : m_1 < n), ↑(e ⟨m_1, hi⟩) = m_1<VAR>hi : i < n<VAR>j : ℕ<VAR>hj : j < ↑(e ⟨i, hi⟩)<GOAL>j < i
<VAR>m n : ℕ<VAR>p : Fin (n + 1)<VAR>i✝ j✝ : Fin n<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>e : Fin n ≃o Fin m<VAR>i : ℕ<VAR>h : ∀ m_1 < i, ∀ (hi : m_1 < n), ↑(e ⟨m_1, hi⟩) = m_1<VAR>hi : i < n<VAR>j : ℕ<VAR>hj : j < i<GOAL>j < ↑(e ⟨i, hi⟩)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>r : R<VAR>x y : M<VAR>inst✝⁵ : Ring R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>p p' : Submodule R M<VAR>R₂ : Type u_3<VAR>M₂ : Type u_4<VAR>inst✝² : Ring R₂<VAR>inst✝¹ : AddCommGroup M₂<VAR>inst✝ : Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<GOAL>map p.mkQ p' = ⊤ ↔ p ⊔ p' = ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>L : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>inst✝⁵ : AddCommMonoid L<VAR>inst✝⁴ : TopologicalSpace L<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : AddCommMonoid N<VAR>inst✝ : TopologicalSpace N<VAR>n : MeasurableSpace α<VAR>v : VectorMeasure α M<VAR>hle : m ≤ n<VAR>i : Set α<VAR>hi : MeasurableSet i<VAR>j : Set α<VAR>hj : MeasurableSet j<GOAL>↑((v.trim hle).restrict i) j = ↑((v.restrict i).trim hle) j
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>L : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>inst✝⁵ : AddCommMonoid L<VAR>inst✝⁴ : TopologicalSpace L<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : AddCommMonoid N<VAR>inst✝ : TopologicalSpace N<VAR>n : MeasurableSpace α<VAR>v : VectorMeasure α M<VAR>hle : m ≤ n<VAR>i : Set α<VAR>hi : MeasurableSet i<VAR>j : Set α<VAR>hj : MeasurableSet j<GOAL>MeasurableSet (j ∩ i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>L : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>inst✝⁵ : AddCommMonoid L<VAR>inst✝⁴ : TopologicalSpace L<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : AddCommMonoid N<VAR>inst✝ : TopologicalSpace N<VAR>n : MeasurableSpace α<VAR>v : VectorMeasure α M<VAR>hle : m ≤ n<VAR>i : Set α<VAR>hi : MeasurableSet i<VAR>j : Set α<VAR>hj : MeasurableSet j<GOAL>MeasurableSet i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>L : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>inst✝⁵ : AddCommMonoid L<VAR>inst✝⁴ : TopologicalSpace L<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : AddCommMonoid N<VAR>inst✝ : TopologicalSpace N<VAR>n : MeasurableSpace α<VAR>v : VectorMeasure α M<VAR>hle : m ≤ n<VAR>i : Set α<VAR>hi : MeasurableSet i<VAR>j : Set α<VAR>hj : MeasurableSet j<GOAL>MeasurableSet j
<VAR>C : Type u₁<VAR>inst✝⁹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝⁸ : Category.{v₂, u₂} D<VAR>W : MorphismProperty C<VAR>M : Type w'<VAR>inst✝⁷ : AddMonoid M<VAR>inst✝⁶ : HasShift C M<VAR>inst✝⁵ : HasShift D M<VAR>inst✝⁴ : W.IsCompatibleWithShift M<VAR>L : C ⥤ D<VAR>inst✝³ : L.IsLocalization W<VAR>inst✝² : HasShift D M<VAR>inst✝¹ : L.CommShift M<VAR>X Y Z T : C<VAR>inst✝ : HasSmallLocalizedShiftedHom W M X Y<VAR>f : X ⟶ Y<GOAL>((L.commShiftIso 0).app Y).homToEquiv ((SmallHom.equiv W L) (SmallHom.mk W (f ≫ (shiftFunctorZero' C 0 ⋯).inv.app Y))) = ShiftedHom.mk₀ 0 ⋯ (L.map f)
<VAR>C : Type u₁<VAR>inst✝⁹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝⁸ : Category.{v₂, u₂} D<VAR>W : MorphismProperty C<VAR>M : Type w'<VAR>inst✝⁷ : AddMonoid M<VAR>inst✝⁶ : HasShift C M<VAR>inst✝⁵ : HasShift D M<VAR>inst✝⁴ : W.IsCompatibleWithShift M<VAR>L : C ⥤ D<VAR>inst✝³ : L.IsLocalization W<VAR>inst✝² : HasShift D M<VAR>inst✝¹ : L.CommShift M<VAR>X Y Z T : C<VAR>inst✝ : HasSmallLocalizedShiftedHom W M X Y<VAR>f : X ⟶ Y<GOAL>(L.map f ≫ L.map ((shiftFunctorZero' C 0 ⋯).inv.app Y)) ≫ ((L.commShiftIso 0).app Y).hom = ShiftedHom.mk₀ 0 ⋯ (L.map f)
<VAR>C : Type u₁<VAR>inst✝⁹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝⁸ : Category.{v₂, u₂} D<VAR>W : MorphismProperty C<VAR>M : Type w'<VAR>inst✝⁷ : AddMonoid M<VAR>inst✝⁶ : HasShift C M<VAR>inst✝⁵ : HasShift D M<VAR>inst✝⁴ : W.IsCompatibleWithShift M<VAR>L : C ⥤ D<VAR>inst✝³ : L.IsLocalization W<VAR>inst✝² : HasShift D M<VAR>inst✝¹ : L.CommShift M<VAR>X Y Z T : C<VAR>inst✝ : HasSmallLocalizedShiftedHom W M X Y<VAR>f : X ⟶ Y<GOAL>(L.map f ≫ L.map ((shiftFunctorZero C M).inv.app Y ≫ 𝟙 ((shiftFunctor C 0).obj Y))) ≫ (L.commShiftIso 0).hom.app Y = L.map f ≫ (shiftFunctorZero D M).inv.app (L.obj Y) ≫ 𝟙 ((shiftFunctor D 0).obj (L.obj Y))
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>h e f : L<VAR>t : IsSl2Triple h e f<GOAL>e ≠ 0
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>h e f : L<VAR>t : IsSl2Triple h e f<VAR>this : h ≠ 0<GOAL>e ≠ 0
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>h e f : L<VAR>t : IsSl2Triple h e f<VAR>this : e = 0<GOAL>h = 0
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝¹ : Group α<VAR>inst✝ : MulAction α β<VAR>s✝ t✝ A B : Set β<VAR>a : α<VAR>x✝ : β<VAR>s t : Set α<VAR>x : α<GOAL>x • s ∩ t ≠ ∅ ↔ ∃ a b, (a ∈ t ∧ b ∈ s) ∧ a / b = x
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝ : CommRing R<VAR>x : 𝕎 (ZMod p)<GOAL>verschiebung x = x * ↑p
<VAR>α : Type u_1<VAR>inst✝¹ : DistribLattice α<VAR>inst✝ : BoundedOrder α<VAR>a b : Complementeds α<GOAL>Disjoint ↑a ↑b ↔ Disjoint a b
<VAR>ι : Type u_1<VAR>μ : Type u_2<VAR>μ' : Type u_3<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<VAR>m n : ℕ<VAR>hn : n ≠ 0<GOAL>map { toFun := fun x => n • x, inj' := ⋯ } (univ.piAntidiag m) = filter (fun f => ∀ (i : ι), n ∣ f i) (univ.piAntidiag (n * m))
<VAR>V : Type u_1<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>P : Type u_2<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>a b c d p : P<VAR>h : Cospherical {a, b, c, d}<VAR>hab : a ≠ b<VAR>hcd : c ≠ d<VAR>hapb : ∠ a p b = 0<VAR>hcpd : ∠ c p d = 0<GOAL>dist a p * dist b p = dist c p * dist d p
<VAR>V : Type u_1<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>P : Type u_2<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>a b c d p : P<VAR>h : Cospherical {a, b, c, d}<VAR>hab : a ≠ b<VAR>hcd : c ≠ d<VAR>hapb : ∠ a p b = 0<VAR>hcpd : ∠ c p d = 0<VAR>k₁ : ℝ<VAR>hab₁ : b -ᵥ p = k₁ • (a -ᵥ p)<GOAL>dist a p * dist b p = dist c p * dist d p
<VAR>V : Type u_1<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>P : Type u_2<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>a b c d p : P<VAR>h : Cospherical {a, b, c, d}<VAR>hab : a ≠ b<VAR>hcd : c ≠ d<VAR>hapb : ∠ a p b = 0<VAR>hcpd : ∠ c p d = 0<VAR>k₁ : ℝ<VAR>hab₁ : b -ᵥ p = k₁ • (a -ᵥ p)<VAR>k₂ : ℝ<VAR>hcd₁ : d -ᵥ p = k₂ • (c -ᵥ p)<GOAL>dist a p * dist b p = dist c p * dist d p
<VAR>V : Type u_1<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>P : Type u_2<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>a b c d p : P<VAR>h : Cospherical {a, b, c, d}<VAR>hab : a ≠ b<VAR>hcd : c ≠ d<VAR>hapb : ∠ a p b = 0<VAR>hcpd : ∠ c p d = 0<VAR>k₁ k₂ : ℝ<VAR>hab₁ : b -ᵥ p = a -ᵥ p<VAR>hcd₁ : d -ᵥ p = k₂ • (c -ᵥ p)<VAR>hnot : k₁ = 1<GOAL>False
<VAR>V : Type u_1<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>P : Type u_2<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>a b c d p : P<VAR>h : Cospherical {a, b, c, d}<VAR>hab : a ≠ b<VAR>hcd : c ≠ d<VAR>hapb : ∠ a p b = 0<VAR>hcpd : ∠ c p d = 0<VAR>k₁ : ℝ<VAR>hab₁ : b -ᵥ p = k₁ • (a -ᵥ p)<VAR>k₂ : ℝ<VAR>hcd₁ : d -ᵥ p = c -ᵥ p<VAR>hnot : k₂ = 1<GOAL>False
<VAR>α : Type u<VAR>t : TopologicalSpace α<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>Y : Type u_2<VAR>inst✝ : TopologicalSpace Y<VAR>π : X → Y<VAR>V : Set (Set X)<VAR>hV : IsTopologicalBasis V<VAR>h' : QuotientMap π<VAR>h : IsOpenMap π<GOAL>IsTopologicalBasis (image π '' V)
<VAR>α : Type u<VAR>t : TopologicalSpace α<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>Y : Type u_2<VAR>inst✝ : TopologicalSpace Y<VAR>π : X → Y<VAR>V : Set (Set X)<VAR>hV : IsTopologicalBasis V<VAR>h' : QuotientMap π<VAR>h : IsOpenMap π<GOAL>∀ u ∈ image π '' V, IsOpen u
<VAR>α : Type u<VAR>t : TopologicalSpace α<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>Y : Type u_2<VAR>inst✝ : TopologicalSpace Y<VAR>π : X → Y<VAR>V : Set (Set X)<VAR>hV : IsTopologicalBasis V<VAR>h' : QuotientMap π<VAR>h : IsOpenMap π<GOAL>∀ (a : Y) (u : Set Y), a ∈ u → IsOpen u → ∃ v ∈ image π '' V, a ∈ v ∧ v ⊆ u
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>P : R[X]<VAR>x : S<VAR>h : IsUnit ((aeval x) (derivative P))<GOAL>IsFixedPt P.newtonMap x ↔ (aeval x) P = 0
<VAR>R : Type r<VAR>S : Type s<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : WeierstrassCurve R<GOAL>W.ΨSq 3 = W.Ψ₃ ^ 2
<VAR>α : Type u_1<VAR>n : PosNum<GOAL>↑n = pos n
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>β : ι → Type u_3<VAR>s s₁ s₂ : Set ι<VAR>t t₁ t₂ : (i : ι) → Set (α i)<VAR>i : ι<GOAL>s.pi t = ∅ ↔ ∃ i, IsEmpty (α i) ∨ i ∈ s ∧ t i = ∅
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>β : ι → Type u_3<VAR>s s₁ s₂ : Set ι<VAR>t t₁ t₂ : (i : ι) → Set (α i)<VAR>i : ι<GOAL>(¬∀ (i : ι), ∃ x, i ∈ s → x ∈ t i) ↔ ∃ i, IsEmpty (α i) ∨ i ∈ s ∧ t i = ∅
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>β : ι → Type u_3<VAR>s s₁ s₂ : Set ι<VAR>t t₁ t₂ : (i : ι) → Set (α i)<VAR>i : ι<GOAL>(∃ i, ∀ (x : α i), i ∈ s ∧ x ∉ t i) ↔ ∃ i, IsEmpty (α i) ∨ i ∈ s ∧ t i = ∅
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>β : ι → Type u_3<VAR>s s₁ s₂ : Set ι<VAR>t t₁ t₂ : (i : ι) → Set (α i)<VAR>i✝ i : ι<GOAL>(∀ (x : α i), i ∈ s ∧ x ∉ t i) ↔ IsEmpty (α i) ∨ i ∈ s ∧ t i = ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>κ : Sort u_6<VAR>r p q : α → α → Prop<VAR>inst✝ : Frame α<VAR>s : Set ι<VAR>t : Set ι'<VAR>f : ι × ι' → α<GOAL>(s ×ˢ t).PairwiseDisjoint f ↔ (s.PairwiseDisjoint fun i => ⨆ i' ∈ t, f (i, i')) ∧ t.PairwiseDisjoint fun i' => ⨆ i ∈ s, f (i, i')
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>κ : Sort u_6<VAR>r p q : α → α → Prop<VAR>inst✝ : Frame α<VAR>s : Set ι<VAR>t : Set ι'<VAR>f : ι × ι' → α<VAR>h : (s ×ˢ t).PairwiseDisjoint f<VAR>i : ι<VAR>hi : i ∈ s<VAR>j : ι<VAR>hj : j ∈ s<VAR>hij : i ≠ j<VAR>i' : ι'<VAR>hi' : i' ∈ t<VAR>j' : ι'<VAR>hj' : j' ∈ t<GOAL>Disjoint (f (i, i')) (f (j, j'))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>κ : Sort u_6<VAR>r p q : α → α → Prop<VAR>inst✝ : Frame α<VAR>s : Set ι<VAR>t : Set ι'<VAR>f : ι × ι' → α<VAR>h : (s ×ˢ t).PairwiseDisjoint f<VAR>i : ι'<VAR>hi : i ∈ t<VAR>j : ι'<VAR>hj : j ∈ t<VAR>hij : i ≠ j<VAR>i' : ι<VAR>hi' : i' ∈ s<VAR>j' : ι<VAR>hj' : j' ∈ s<GOAL>Disjoint (f (i', i)) (f (j', j))
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>X✝ : SimplicialObject C<VAR>s✝ : Splitting X✝<VAR>inst✝ : Preadditive C<VAR>X : SimplicialObject C<VAR>s : Splitting X<VAR>n : ℕ<VAR>A : IndexSet (op [n])<VAR>hA : ¬A.EqId<GOAL>(s.cofan (op [n])).inj A ≫ PInfty.f n = 0
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>X✝ : SimplicialObject C<VAR>s✝ : Splitting X✝<VAR>inst✝ : Preadditive C<VAR>X : SimplicialObject C<VAR>s : Splitting X<VAR>n : ℕ<VAR>A : IndexSet (op [n])<VAR>hA : ¬Mono A.e<GOAL>(s.cofan (op [n])).inj A ≫ PInfty.f n = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝ : CompleteBooleanAlgebra α<VAR>f : Filter β<VAR>u : β → α<GOAL>(liminf u f)ᶜ = limsup (compl ∘ u) f
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝¹ : Field F<VAR>W : Jacobian F<VAR>inst✝ : NoZeroDivisors R<VAR>P Q : Fin 3 → R<VAR>hQz : Q z ≠ 0<VAR>hx : P x * Q z ^ 2 = Q x * P z ^ 2<VAR>hy : P y * Q z ^ 3 = Q y * P z ^ 3<VAR>hy' : P y * Q z ^ 3 = W'.negY Q * P z ^ 3<GOAL>W'.dblXYZ P = ![W'.dblU P ^ 2, W'.dblU P ^ 3, 0]
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>u v w : V<VAR>p : G.Walk u v<VAR>q : G.Walk v w<GOAL>(p.append q).length = p.length + q.length
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort uι<VAR>s t u : Set α<VAR>m : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>f : α → β × γ<VAR>hf₁ : Measurable fun a => (f a).1<VAR>hf₂ : Measurable fun a => (f a).2<GOAL>MeasurableSpace.comap Prod.fst mβ ≤ MeasurableSpace.map f m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort uι<VAR>s t u : Set α<VAR>m : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>f : α → β × γ<VAR>hf₁ : Measurable fun a => (f a).1<VAR>hf₂ : Measurable fun a => (f a).2<GOAL>mβ ≤ MeasurableSpace.map (Prod.fst ∘ f) m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort uι<VAR>s t u : Set α<VAR>m : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>f : α → β × γ<VAR>hf₁ : Measurable fun a => (f a).1<VAR>hf₂ : Measurable fun a => (f a).2<GOAL>MeasurableSpace.comap Prod.snd mγ ≤ MeasurableSpace.map f m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort uι<VAR>s t u : Set α<VAR>m : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>f : α → β × γ<VAR>hf₁ : Measurable fun a => (f a).1<VAR>hf₂ : Measurable fun a => (f a).2<GOAL>mγ ≤ MeasurableSpace.map (Prod.snd ∘ f) m
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>A : Type u_3<VAR>S✝ : Type u_4<VAR>inst✝¹ : Group G<VAR>inst✝ : AddGroup A<VAR>s S : Set G<GOAL>(closure S).toSubmonoid = Submonoid.closure (S ∪ S⁻¹)
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>A : Type u_3<VAR>S✝ : Type u_4<VAR>inst✝¹ : Group G<VAR>inst✝ : AddGroup A<VAR>s S : Set G<VAR>x : G<VAR>hx : x ∈ (closure S).toSubmonoid<GOAL>x ∈ Submonoid.closure (S ∪ S⁻¹)
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>A : Type u_3<VAR>S✝ : Type u_4<VAR>inst✝¹ : Group G<VAR>inst✝ : AddGroup A<VAR>s S : Set G<GOAL>S ∪ S⁻¹ ⊆ ↑(closure S).toSubmonoid
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝³ : Fintype α✝<VAR>p✝ : α✝ → Prop<VAR>inst✝² : DecidablePred p✝<VAR>α : Type u_4<VAR>p : α → Prop<VAR>inst✝¹ : Fintype { a // p a }<VAR>inst✝ : DecidableEq α<VAR>x y : { a // p a }<VAR>hy : (fun a => ↑a = ↑x) y<GOAL>y = x
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝³ : Fintype α✝<VAR>p✝ : α✝ → Prop<VAR>inst✝² : DecidablePred p✝<VAR>α : Type u_4<VAR>p : α → Prop<VAR>inst✝¹ : Fintype { a // p a }<VAR>inst✝ : DecidableEq α<VAR>x : { a // p a }<VAR>h : optParam (∃! a, ↑a = ↑x) ⋯<GOAL>choose (fun y => ↑y = ↑x) h = x
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>κ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>r : α → β → Prop<VAR>inst✝ : (a : α) → DecidablePred (r a)<VAR>s✝ s₁ s₂ : Finset α<VAR>t✝ t₁ t₂ : Finset β<VAR>a : α<VAR>b : β<VAR>δ : 𝕜<VAR>s : Finset α<VAR>t : Finset β<GOAL>edgeDensity r s t ≤ 1
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>κ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>r : α → β → Prop<VAR>inst✝ : (a : α) → DecidablePred (r a)<VAR>s✝ s₁ s₂ : Finset α<VAR>t✝ t₁ t₂ : Finset β<VAR>a : α<VAR>b : β<VAR>δ : 𝕜<VAR>s : Finset α<VAR>t : Finset β<GOAL>↑(interedges r s t).card ≤ ↑s.card * ↑t.card
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>κ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>r : α → β → Prop<VAR>inst✝ : (a : α) → DecidablePred (r a)<VAR>s✝ s₁ s₂ : Finset α<VAR>t✝ t₁ t₂ : Finset β<VAR>a : α<VAR>b : β<VAR>δ : 𝕜<VAR>s : Finset α<VAR>t : Finset β<GOAL>0 ≤ ↑s.card * ↑t.card
<VAR>R : Type u_1<VAR>inst✝⁶ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁵ : CommSemiring S<VAR>inst✝⁴ : Algebra R S<VAR>P : Type u_3<VAR>inst✝³ : CommSemiring P<VAR>A : Type u_4<VAR>inst✝² : CommRing A<VAR>inst✝¹ : IsDomain A<VAR>I : Ideal R<VAR>hI : I.IsPrime<VAR>inst✝ : IsLocalization.AtPrime S I<VAR>x : R<VAR>y : ↥I.primeCompl<VAR>h : optParam (LocalRing S) ⋯<GOAL>mk' S x y ∉ LocalRing.maximalIdeal S ↔ x ∉ I
<VAR>n m : ℕ<VAR>i : Fin (n + 1)<VAR>hi : i ≠ last n<VAR>j : Fin n<VAR>h : i.castPred hi = j<GOAL>i = j.castSucc
<VAR>n m : ℕ<VAR>i : Fin (n + 1)<VAR>hi : i ≠ last n<VAR>j : Fin n<VAR>h : i = j.castSucc<GOAL>i.castPred hi = j
<VAR>D : GlueData<VAR>i : D.J<VAR>x y : ↑(D.U i)<VAR>h : (D.ι i) x = (D.ι i) y<GOAL>x = y
<VAR>D : GlueData<VAR>i : D.J<VAR>x : ↑(D.U i)<VAR>h : (D.ι i) x = (D.ι i) x<GOAL>x = x
<VAR>D : GlueData<VAR>i : D.J<VAR>x y : ↑(D.U i)<VAR>h : (D.ι i) x = (D.ι i) y<VAR>w✝ : ↑(D.V (⟨i, x⟩.fst, ⟨i, y⟩.fst))<VAR>e₁ : (D.f ⟨i, x⟩.fst ⟨i, y⟩.fst) w✝ = ⟨i, x⟩.snd<VAR>e₂ : (D.f ⟨i, y⟩.fst ⟨i, x⟩.fst) ((D.t ⟨i, x⟩.fst ⟨i, y⟩.fst) w✝) = ⟨i, y⟩.snd<GOAL>x = y
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁷ : MeasurableSpace α<VAR>inst✝⁶ : MeasurableSpace α'<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace β'<VAR>inst✝³ : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : SFinite ν<VAR>f : α → β → E<VAR>hf : StronglyMeasurable (uncurry f)<VAR>hE : CompleteSpace E<VAR>this✝¹ : MeasurableSpace E := borel E<VAR>this✝ : BorelSpace E<GOAL>StronglyMeasurable fun x => ∫ (y : β), f x y ∂ν
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁷ : MeasurableSpace α<VAR>inst✝⁶ : MeasurableSpace α'<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace β'<VAR>inst✝³ : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : SFinite ν<VAR>f : α → β → E<VAR>hf : StronglyMeasurable (uncurry f)<VAR>hE : CompleteSpace E<VAR>this✝¹ : MeasurableSpace E := borel E<VAR>this✝ : BorelSpace E<VAR>this : SeparableSpace ↑(range (uncurry f) ∪ {0})<GOAL>StronglyMeasurable fun x => ∫ (y : β), f x y ∂ν