ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : SimplicialCategory C<VAR>K L L' L'' : C<VAR>g : L ⟶ L'<VAR>g' : L' ⟶ L''<GOAL>(ρ_ (sHom K L)).inv ≫ sHom K L ◁ (λ_ (𝟙_ SSet)).inv ≫ sHom K L ◁ ((homEquiv L L') g ⊗ (homEquiv L' L'') g') ≫ (α_ (EnrichedCategory.Hom K L) (EnrichedCategory.Hom L L') (EnrichedCategory.Hom L' L'')).inv ≫ eComp SSet K L L' ▷ EnrichedCategory.Hom L' L'' ≫ eComp SSet K L' L'' = (ρ_ (sHom K L)).inv ≫ sHom K L ◁ (homEquiv L L') g ≫ sHomComp K L L' ≫ (ρ_ (sHom K L')).inv ≫ sHom K L' ◁ (homEquiv L' L'') g' ≫ sHomComp K L' L''
<VAR>o : Ordinal.{u}<VAR>f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}<VAR>i : Ordinal.{u}<VAR>hi : i < o<VAR>H : IsNormal (f i hi)<VAR>a : Ordinal.{max v u}<GOAL>f i hi (o.nfpBFamily f a) = o.nfpBFamily f a
<VAR>o : Ordinal.{u}<VAR>f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}<VAR>i : Ordinal.{u}<VAR>hi : i < o<VAR>H : IsNormal (f i hi)<VAR>a : Ordinal.{max v u}<GOAL>o.familyOfBFamily f (enum (fun x x_1 => x < x_1) i ⋯) (o.nfpBFamily f a) = o.nfpBFamily f a
<VAR>o : Ordinal.{u}<VAR>f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}<VAR>i : Ordinal.{u}<VAR>hi : i < o<VAR>H : IsNormal (f i hi)<VAR>a : Ordinal.{max v u}<GOAL>IsNormal (o.familyOfBFamily f (enum (fun x x_1 => x < x_1) i ⋯))
<VAR>o : Ordinal.{u}<VAR>f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}<VAR>i : Ordinal.{u}<VAR>hi : i < o<VAR>H : IsNormal (f i hi)<VAR>a : Ordinal.{max v u}<GOAL>IsNormal (f i ?H.hi)
<VAR>o : Ordinal.{u}<VAR>f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}<VAR>i : Ordinal.{u}<VAR>hi : i < o<VAR>H : IsNormal (f i hi)<VAR>a : Ordinal.{max v u}<GOAL>i < o
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W : WeierstrassCurve R<VAR>inst✝ : Invertible 2<GOAL>IsUnit W.twoTorsionPolynomial.disc ↔ IsUnit W.Δ
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W : WeierstrassCurve R<VAR>inst✝ : Invertible 2<GOAL>IsUnit (2 ^ 4) ∧ IsUnit W.Δ ↔ IsUnit W.Δ
<VAR>α : Type u<VAR>β : Type u_1<VAR>inst✝⁵ : Semiring α<VAR>inst✝⁴ : Preorder α<VAR>a b c d : α<VAR>inst✝³ : ExistsAddOfLE α<VAR>inst✝² : PosMulMono α<VAR>inst✝¹ : CovariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : ContravariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>ha : a ≤ 0<VAR>h : b ≤ 1<GOAL>a ≤ a * b
<VAR>p : ℝ≥0∞<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>α : ι → Type u_3<VAR>β : ι → Type u_4<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : (i : ι) → PseudoEMetricSpace (β i)<VAR>f : PiLp p β<GOAL>edist f f = 0
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>α : ι → Type u_3<VAR>β : ι → Type u_4<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : (i : ι) → PseudoEMetricSpace (β i)<VAR>f : PiLp 0 β<GOAL>edist f f = 0
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>α : ι → Type u_3<VAR>β : ι → Type u_4<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : (i : ι) → PseudoEMetricSpace (β i)<VAR>f : PiLp ⊤ β<GOAL>edist f f = 0
<VAR>p : ℝ≥0∞<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>α : ι → Type u_3<VAR>β : ι → Type u_4<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : (i : ι) → PseudoEMetricSpace (β i)<VAR>f : PiLp p β<VAR>h : 0 < p.toReal<GOAL>edist f f = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : Semiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>N₁ N₂ : Submodule R M<VAR>hN₁ : N₁.FG<VAR>hN₂ : N₂.FG<VAR>t₁ : Set M<VAR>ht₁ : t₁.Finite ∧ span R t₁ = N₁<VAR>t₂ : Set M<VAR>ht₂ : t₂.Finite ∧ span R t₂ = N₂<GOAL>span R (t₁ ∪ t₂) = N₁ ⊔ N₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>s✝ s₁ s₂ : Set α<VAR>t✝ t₁ t₂ : Set β<VAR>p : Set γ<VAR>f✝ f₁ f₂ f₃ : α → β<VAR>g g₁ g₂ : β → γ<VAR>f' f₁' f₂' : β → α<VAR>g' : γ → β<VAR>a : α<VAR>b : β<VAR>inst✝ : Nonempty β<VAR>s : Set (α × β)<VAR>x✝ : ∃ f t, s = graphOn f t<VAR>f : α → β<VAR>t : Set α<VAR>hs : s = graphOn f t<GOAL>s = graphOn f (Prod.fst '' s)
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>m n : ℕ<GOAL>pellZd a1 (m + (n + 1)) = pellZd a1 m * pellZd a1 (n + 1)
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>s✝ t✝ u v : Set α<VAR>inst✝ : TopologicalSpace β<VAR>s : Set α<VAR>t : Set β<VAR>hs : IsPreconnected s<VAR>ht : IsPreconnected t<GOAL>IsPreconnected (s ×ˢ t)
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>s✝ t✝ u v : Set α<VAR>inst✝ : TopologicalSpace β<VAR>s : Set α<VAR>t : Set β<VAR>hs : IsPreconnected s<VAR>ht : IsPreconnected t<GOAL>∀ x ∈ s ×ˢ t, ∀ y ∈ s ×ˢ t, ∃ t_1 ⊆ s ×ˢ t, x ∈ t_1 ∧ y ∈ t_1 ∧ IsPreconnected t_1
<VAR>R : Type u_1<VAR>N : Type u_2<VAR>M : Type u_3<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid N<VAR>inst✝² : Module R N<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>f i : N →ₗ[R] M<VAR>K : Submodule R N<VAR>h : map f K ≤ map i K<VAR>n : ℕ<GOAL>f.iterateMapComap i n K ≤ (fun K => comap f (map i K))^[n + 1] K
<VAR>R : Type u_1<VAR>N : Type u_2<VAR>M : Type u_3<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid N<VAR>inst✝² : Module R N<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>f i : N →ₗ[R] M<VAR>K : Submodule R N<VAR>h : map f K ≤ map i K<VAR>n : ℕ<GOAL>map f (f.iterateMapComap i n K) ≤ map i (f.iterateMapComap i n K)
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝³ : Ring R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>ι : Type w<VAR>ι' : Type w'<VAR>inst✝ : StrongRankCondition R<VAR>v : Basis ι R M<GOAL>lift.{v, w} #ι = lift.{w, v} (Module.rank R M)
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝³ : Ring R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>ι : Type w<VAR>ι' : Type w'<VAR>inst✝ : StrongRankCondition R<VAR>v : Basis ι R M<VAR>this : Nontrivial R<GOAL>lift.{v, w} #ι = lift.{w, v} (Module.rank R M)
<VAR>x y : ℝ<GOAL>AntitoneOn (fun x => log x / x) {x | rexp 1 ≤ x}
<VAR>x y : ℝ<GOAL>∀ ⦃a : ℝ⦄, rexp 1 ≤ a → ∀ ⦃b : ℝ⦄, rexp 1 ≤ b → a ≤ b → log b / b ≤ log a / a
<VAR>x✝ y✝ x : ℝ<VAR>hex : rexp 1 ≤ x<VAR>y : ℝ<VAR>hey : rexp 1 ≤ y<VAR>hxy : x ≤ y<GOAL>log y / y ≤ log x / x
<VAR>x✝ y✝ x : ℝ<VAR>hex : rexp 1 ≤ x<VAR>y : ℝ<VAR>hey : rexp 1 ≤ y<VAR>hxy : x ≤ y<VAR>x_pos : 0 < x<GOAL>log y / y ≤ log x / x
<VAR>x✝ y✝ x : ℝ<VAR>hex : rexp 1 ≤ x<VAR>y : ℝ<VAR>hey : rexp 1 ≤ y<VAR>hxy : x ≤ y<VAR>x_pos : 0 < x<VAR>y_pos : 0 < y<GOAL>log y / y ≤ log x / x
<VAR>x✝ y✝ x : ℝ<VAR>hex : rexp 1 ≤ x<VAR>y : ℝ<VAR>hey : rexp 1 ≤ y<VAR>hxy : x ≤ y<VAR>x_pos : 0 < x<VAR>y_pos : 0 < y<VAR>hlogx : 1 ≤ log x<GOAL>log y / y ≤ log x / x
<VAR>x✝ y✝ x : ℝ<VAR>hex : rexp 1 ≤ x<VAR>y : ℝ<VAR>hey : rexp 1 ≤ y<VAR>hxy : x ≤ y<VAR>x_pos : 0 < x<VAR>y_pos : 0 < y<VAR>hlogx : 1 ≤ log x<VAR>hyx : 0 ≤ y / x - 1<GOAL>log y / y ≤ log x / x
<VAR>x✝ y✝ x : ℝ<VAR>hex : rexp 1 ≤ x<VAR>y : ℝ<VAR>hey : rexp 1 ≤ y<VAR>hxy : x ≤ y<VAR>x_pos : 0 < x<VAR>y_pos : 0 < y<VAR>hlogx : 1 ≤ log x<VAR>hyx : 0 ≤ y / x - 1<GOAL>log y - log x ≤ log x / x * y - log x
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : BooleanAlgebra α<GOAL>xᶜ ≤ x ↔ x = ⊤
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>c₁ c₂ : R<VAR>q : ℍ[R,c₁,c₂]<GOAL>CliffordAlgebraQuaternion.equiv (ofQuaternion (star q)) = CliffordAlgebraQuaternion.equiv (star (ofQuaternion q))
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>inst✝ : BraidedCategory C<VAR>X Y : Mon_ C<VAR>f : X ⟶ Y<VAR>Z : Mon_ C<GOAL>(f ▷ Z).hom = f.hom ▷ Z.X
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>inst✝ : BraidedCategory C<VAR>X Y : Mon_ C<VAR>f : X ⟶ Y<VAR>Z : Mon_ C<GOAL>(f ▷ Z).hom = f.hom ⊗ 𝟙 Z.X
<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>p p₀ p₁ p₂ p1 p2 p3 : P<VAR>h : InnerProductGeometry.angle (p1 -ᵥ p2) (p3 -ᵥ p2) = π<GOAL>∠ p2 p1 p3 = 0
<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>p p₀ p₁ p₂ p1 p2 p3 : P<VAR>h : p1 -ᵥ p2 ≠ 0 ∧ ∃ r < 0, p3 -ᵥ p2 = r • (p1 -ᵥ p2)<GOAL>∠ p2 p1 p3 = 0
<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>p p₀ p₁ p₂ p1 p2 p3 : P<VAR>hp1p2 : p1 -ᵥ p2 ≠ 0<VAR>r : ℝ<VAR>hr : r < 0<VAR>hpr : p3 -ᵥ p2 = r • (p1 -ᵥ p2)<GOAL>InnerProductGeometry.angle (p2 -ᵥ p1) (p3 -ᵥ p1) = 0
<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>p p₀ p₁ p₂ p1 p2 p3 : P<VAR>hp1p2 : p1 -ᵥ p2 ≠ 0<VAR>r : ℝ<VAR>hr : r < 0<VAR>hpr : p3 -ᵥ p2 = r • (p1 -ᵥ p2)<GOAL>p2 -ᵥ p1 ≠ 0 ∧ ∃ r, 0 < r ∧ p3 -ᵥ p1 = r • (p2 -ᵥ p1)
<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>p p₀ p₁ p₂ p1 p2 p3 : P<VAR>hp1p2 : p2 -ᵥ p1 ≠ 0<VAR>r : ℝ<VAR>hr : r < 0<VAR>hpr : p3 -ᵥ p2 = r • (p1 -ᵥ p2)<GOAL>p2 -ᵥ p1 ≠ 0 ∧ ∃ r, 0 < r ∧ p3 -ᵥ p1 = r • (p2 -ᵥ p1)
<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>p p₀ p₁ p₂ p1 p2 p3 : P<VAR>hp1p2 : p2 -ᵥ p1 ≠ 0<VAR>r : ℝ<VAR>hr : r < 0<VAR>hpr : p3 -ᵥ p2 = r • (p1 -ᵥ p2)<GOAL>p3 -ᵥ p1 = (-r + 1) • (p2 -ᵥ p1)
<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>p p₀ p₁ p₂ p1 p2 p3 : P<VAR>hp1p2 : p2 -ᵥ p1 ≠ 0<VAR>r : ℝ<VAR>hr : r < 0<VAR>hpr : p3 -ᵥ p2 = r • (p1 -ᵥ p2)<GOAL>p3 -ᵥ p1 = -(-r • (p1 -ᵥ p2)) + 1 • -(p1 -ᵥ p2)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>s : Set (β × γ)<VAR>κ : Kernel α β<VAR>η : Kernel (α × β) γ<VAR>h : ¬IsSFiniteKernel η<GOAL>κ ⊗ₖ η = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>s : Set (β × γ)<VAR>κ : Kernel α β<VAR>η : Kernel (α × β) γ<VAR>h : ¬IsSFiniteKernel η<GOAL>¬(IsSFiniteKernel κ ∧ IsSFiniteKernel η)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>n : Type w<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : Fintype n<VAR>p : R[X]<VAR>M : Matrix n n R[X]<GOAL>matPolyEquiv (p • M) = Polynomial.map (algebraMap R (Matrix n n R)) p * matPolyEquiv M
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : TopologicalSpace 𝕜<VAR>inst✝ : OrderTopology 𝕜<VAR>p q✝ : 𝕜<VAR>hp : Fact (0 < p)<VAR>q : ℚ<GOAL>addOrderOf ↑(↑q * p) = q.den
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : TopologicalSpace 𝕜<VAR>inst✝ : OrderTopology 𝕜<VAR>p q✝ : 𝕜<VAR>hp : Fact (0 < p)<VAR>q : ℚ<VAR>this : ↑↑q.den ≠ 0<GOAL>addOrderOf ↑(↑q * p) = q.den
<VAR>Ω : Type u_1<VAR>Ω' : Type u_2<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : MeasurableSpace Ω'<VAR>ν : FiniteMeasure Ω<VAR>f : Ω → Ω'<VAR>f_aemble : AEMeasurable f ↑ν<VAR>A : Set Ω'<VAR>A_mble : MeasurableSet A<GOAL>(ν.map f) A = ν (f ⁻¹' A)
<VAR>Ω : Type u_1<VAR>Ω' : Type u_2<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : MeasurableSpace Ω'<VAR>ν : FiniteMeasure Ω<VAR>f : Ω → Ω'<VAR>f_aemble : AEMeasurable f ↑ν<VAR>A : Set Ω'<VAR>A_mble : MeasurableSet A<VAR>this : ↑(ν.map f) A = ↑ν (f ⁻¹' A)<GOAL>(ν.map f) A = ν (f ⁻¹' A)
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : HasShift C ℤ<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : Pretriangulated C<VAR>T : Triangle C<VAR>hT : T ∈ distinguishedTriangles<GOAL>T.mor₁ = 0 ↔ Epi T.mor₃
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : HasShift C ℤ<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : Pretriangulated C<VAR>T : Triangle C<VAR>hT : T ∈ distinguishedTriangles<VAR>h : T.rotate.mor₃ = 0 ↔ Epi T.rotate.mor₂<GOAL>T.mor₁ = 0 ↔ Epi T.mor₃
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : HasShift C ℤ<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : Pretriangulated C<VAR>T : Triangle C<VAR>hT : T ∈ distinguishedTriangles<VAR>h : -(CategoryTheory.shiftFunctor C 1).map T.mor₁ = 0 ↔ Epi T.mor₃<GOAL>T.mor₁ = 0 ↔ Epi T.mor₃
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : HasShift C ℤ<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : Pretriangulated C<VAR>T : Triangle C<VAR>hT : T ∈ distinguishedTriangles<VAR>h : -(CategoryTheory.shiftFunctor C 1).map T.mor₁ = 0 ↔ Epi T.mor₃<GOAL>T.mor₁ = 0 ↔ (CategoryTheory.shiftFunctor C 1).map T.mor₁ = 0
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : (i : ι) → TopologicalSpace (π i)<VAR>x✝ y✝ z : X<VAR>s : Set X<VAR>f✝ g : X → Y<VAR>t : Set (SeparationQuotient X)<VAR>f : X → Y → α<VAR>hf : ∀ (a : X) (b : Y) (c : X) (d : Y), (a ~ᵢ c) → (b ~ᵢ d) → f a b = f c d<VAR>x : X<VAR>y : Y<VAR>l : Filter α<GOAL>Tendsto (uncurry (lift₂ f hf)) (𝓝 (mk x, mk y)) l ↔ Tendsto (uncurry f) (𝓝 (x, y)) l
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : (i : ι) → TopologicalSpace (π i)<VAR>x✝ y✝ z : X<VAR>s : Set X<VAR>f✝ g : X → Y<VAR>t : Set (SeparationQuotient X)<VAR>f : X → Y → α<VAR>hf : ∀ (a : X) (b : Y) (c : X) (d : Y), (a ~ᵢ c) → (b ~ᵢ d) → f a b = f c d<VAR>x : X<VAR>y : Y<VAR>l : Filter α<GOAL>Tendsto (uncurry (lift₂ f hf) ∘ Prod.map mk mk) (𝓝 (x, y)) l ↔ Tendsto (uncurry f) (𝓝 (x, y)) l
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : PseudoEMetricSpace α<VAR>inst✝¹ : PseudoEMetricSpace β<VAR>inst✝ : PseudoEMetricSpace γ<VAR>f : α → β<VAR>x✝ y✝ z : α<VAR>s : Set α<VAR>h : Isometry f<VAR>x : α<VAR>r : ℝ≥0∞<VAR>y : α<GOAL>y ∈ f ⁻¹' EMetric.closedBall (f x) r ↔ y ∈ EMetric.closedBall x r
<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R S<VAR>P : Type u_3<VAR>inst✝ : CommRing P<VAR>x : R<GOAL>coeSubmodule S (Ideal.span {x}) = Submodule.span R {(algebraMap R S) x}
<VAR>C✝ : Type u<VAR>inst✝¹ : Category.{v, u} C✝<VAR>X✝ Y✝ : PresheafedSpace C✝<VAR>f✝ : X✝ ⟶ Y✝<VAR>H : IsOpenImmersion f✝<VAR>C : Type u_1<VAR>inst✝ : Category.{u_2, u_1} C<VAR>X : PresheafedSpace C<VAR>Y : TopCat<VAR>f : Y ⟶ TopCat.of ↑↑X<VAR>h : OpenEmbedding ⇑f<VAR>U : Opens ↑↑(X.restrict h)<GOAL>(X.restrict h).presheaf.map (eqToHom ⋯) ≫ inv ((X.ofRestrict h).c.app (op ((opensFunctor (X.ofRestrict h)).obj U))) = 𝟙 ((X.restrict h).presheaf.obj (op U))
<VAR>C✝ : Type u<VAR>inst✝¹ : Category.{v, u} C✝<VAR>X✝ Y✝ : PresheafedSpace C✝<VAR>f✝ : X✝ ⟶ Y✝<VAR>H : IsOpenImmersion f✝<VAR>C : Type u_1<VAR>inst✝ : Category.{u_2, u_1} C<VAR>X : PresheafedSpace C<VAR>Y : TopCat<VAR>f : Y ⟶ TopCat.of ↑↑X<VAR>h : OpenEmbedding ⇑f<VAR>U : Opens ↑↑(X.restrict h)<GOAL>(X.restrict h).presheaf.map (eqToHom ⋯) = (X.ofRestrict h).c.app (op ((opensFunctor (X.ofRestrict h)).obj U))
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{?u.40064, u_1} C<VAR>inst✝³ : Category.{?u.40068, u_2} D<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : Preadditive D<VAR>S : ShortComplex C<VAR>hS : S.Exact<VAR>inst✝ : HasZeroObject C<VAR>kf : KernelFork S.g<VAR>hkf : IsLimit kf<GOAL>Epi ((hkf.ofIsoLimit (Fork.ext (Iso.refl kf.pt) ⋯)).lift (KernelFork.ofι S.f ⋯))
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{?u.40064, u_1} C<VAR>inst✝³ : Category.{?u.40068, u_2} D<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : Preadditive D<VAR>S : ShortComplex C<VAR>hS : S.Exact<VAR>inst✝ : HasZeroObject C<VAR>kf : KernelFork S.g<VAR>hkf : IsLimit kf<VAR>this : S.HasHomology<GOAL>Epi ((hkf.ofIsoLimit (Fork.ext (Iso.refl kf.pt) ⋯)).lift (KernelFork.ofι S.f ⋯))
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{?u.40064, u_1} C<VAR>inst✝³ : Category.{?u.40068, u_2} D<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : Preadditive D<VAR>S : ShortComplex C<VAR>hS : S.Exact<VAR>inst✝ : HasZeroObject C<VAR>kf : KernelFork S.g<VAR>hkf : IsLimit kf<VAR>this : S.HasHomology<GOAL>Arrow.mk S.toCycles ≅ Arrow.mk ((hkf.ofIsoLimit (Fork.ext (Iso.refl kf.pt) ⋯)).lift (KernelFork.ofι S.f ⋯))
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{?u.40064, u_1} C<VAR>inst✝³ : Category.{?u.40068, u_2} D<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : Preadditive D<VAR>S : ShortComplex C<VAR>hS : S.Exact<VAR>inst✝ : HasZeroObject C<VAR>kf : KernelFork S.g<VAR>hkf : IsLimit kf<VAR>this : S.HasHomology<GOAL>(Iso.refl (Arrow.mk S.toCycles).left).hom ≫ (Arrow.mk ((hkf.ofIsoLimit (Fork.ext (Iso.refl kf.pt) ⋯)).lift (KernelFork.ofι S.f ⋯))).hom = (Arrow.mk S.toCycles).hom ≫ (S.cyclesIsKernel.conePointUniqueUpToIso hkf).hom
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{?u.40064, u_1} C<VAR>inst✝³ : Category.{?u.40068, u_2} D<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : Preadditive D<VAR>S : ShortComplex C<VAR>hS : S.Exact<VAR>inst✝ : HasZeroObject C<VAR>kf : KernelFork S.g<VAR>hkf : IsLimit kf<VAR>this : S.HasHomology<GOAL>((Iso.refl (Arrow.mk S.toCycles).left).hom ≫ (Arrow.mk ((hkf.ofIsoLimit (Fork.ext (Iso.refl kf.pt) ⋯)).lift (KernelFork.ofι S.f ⋯))).hom) ≫ Fork.ι kf = ((Arrow.mk S.toCycles).hom ≫ (S.cyclesIsKernel.conePointUniqueUpToIso hkf).hom) ≫ Fork.ι kf
<VAR>k m : Nat<VAR>H : k.Coprime m<VAR>d : k ∣ m<GOAL>k = 1
<VAR>p : ℕ → Prop<VAR>h₀ : ¬p 0<VAR>a b : ℕ<VAR>hab : a ≤ b<VAR>ha : nth p a = 0<GOAL>nth p b = 0
<VAR>p : ℕ → Prop<VAR>h₀ : ¬p 0<VAR>a b : ℕ<VAR>hab : a ≤ b<VAR>ha : ∃ (hf : (setOf p).Finite), hf.toFinset.card ≤ a<GOAL>∃ (hf : (setOf p).Finite), hf.toFinset.card ≤ b
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝ : MetricSpace P<VAR>p₁ p₂ : P<VAR>s : Sphere P<VAR>hp₁ : p₁ ∈ s<VAR>hp₂ : p₂ ∈ s<GOAL>dist s.center p₁ = dist s.center p₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a b : α<VAR>h✝ : a ≤ b<VAR>x : α<VAR>h : a < b<GOAL>projIcc a b ⋯ x = ⟨a, ⋯⟩ ↔ x ≤ a
<VAR>a b : ℝ<VAR>n : ℕ<GOAL>∫ (x : ℝ) in a..b, sin x * cos x ^ 2 = (cos a ^ 3 - cos b ^ 3) / 3
<VAR>a b : ℝ<VAR>n : ℕ<VAR>this : ∫ (x : ℝ) in a..b, sin x ^ (2 * 0 + 1) * cos x ^ 2 = ∫ (u : ℝ) in cos b..cos a, u ^ 2 * (1 - u ^ 2) ^ 0<GOAL>∫ (x : ℝ) in a..b, sin x * cos x ^ 2 = (cos a ^ 3 - cos b ^ 3) / 3
<VAR>a q m : ℤ<VAR>b' r : ℕ<VAR>hm : q * ↑b' = m<VAR>h₂ : r.blt b' = true<VAR>h : ↑r + m = a<GOAL>a / ↑b' = ↑q
<VAR>a q m : ℤ<VAR>b' r : ℕ<VAR>hm : q * ↑b' = m<VAR>h : ↑r + m = a<VAR>h₂ : r < b'<GOAL>a / ↑b' = ↑q
<VAR>a q m : ℤ<VAR>b' r : ℕ<VAR>hm : q * ↑b' = m<VAR>h : ↑r + m = a<VAR>h₂ : r < b'<GOAL>(↑r + q * ↑b') / ↑b' = q
<VAR>a q m : ℤ<VAR>b' r : ℕ<VAR>hm : q * ↑b' = m<VAR>h : ↑r + m = a<VAR>h₂ : r < b'<GOAL>↑r / ↑b' + q = q
<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 x y : V<VAR>q : G.Walk v w<VAR>hadj : G.Adj u v<GOAL>notNilRec (fun x u x_1 x x => u) (cons hadj q) ⋯ = v
<VAR>A : Type u_1<VAR>inst✝⁷ : TopologicalSpace A<VAR>inst✝⁶ : NonUnitalRing A<VAR>inst✝⁵ : StarRing A<VAR>inst✝⁴ : Module ℂ A<VAR>inst✝³ : IsScalarTower ℂ A A<VAR>inst✝² : SMulCommClass ℂ A A<VAR>inst✝¹ : StarModule ℂ A<VAR>inst✝ : NonUnitalContinuousFunctionalCalculus ℂ IsStarNormal<VAR>a : A<GOAL>IsSelfAdjoint a ↔ IsStarNormal a ∧ QuasispectrumRestricts a ⇑Complex.reCLM
<VAR>A : Type u_1<VAR>inst✝⁷ : TopologicalSpace A<VAR>inst✝⁶ : NonUnitalRing A<VAR>inst✝⁵ : StarRing A<VAR>inst✝⁴ : Module ℂ A<VAR>inst✝³ : IsScalarTower ℂ A A<VAR>inst✝² : SMulCommClass ℂ A A<VAR>inst✝¹ : StarModule ℂ A<VAR>inst✝ : NonUnitalContinuousFunctionalCalculus ℂ IsStarNormal<VAR>a : A<VAR>ha : IsSelfAdjoint a<VAR>x : ℂ<VAR>hx : x ∈ σₙ ℂ a<GOAL>(algebraMap ℝ ℂ) (Complex.reCLM x) = x
<VAR>A : Type u_1<VAR>inst✝⁷ : TopologicalSpace A<VAR>inst✝⁶ : NonUnitalRing A<VAR>inst✝⁵ : StarRing A<VAR>inst✝⁴ : Module ℂ A<VAR>inst✝³ : IsScalarTower ℂ A A<VAR>inst✝² : SMulCommClass ℂ A A<VAR>inst✝¹ : StarModule ℂ A<VAR>inst✝ : NonUnitalContinuousFunctionalCalculus ℂ IsStarNormal<VAR>a : A<GOAL>IsStarNormal a ∧ QuasispectrumRestricts a ⇑Complex.reCLM → IsSelfAdjoint a
<VAR>α : Type u_1<VAR>m n : ZNum<VAR>h : m = n<GOAL>↑m < ↑n ↔ Ordering.eq = Ordering.lt
<VAR>α : Type u_1<VAR>m n : ZNum<VAR>h : Ordering.casesOn Ordering.gt (↑m < ↑n) (m = n) (↑n < ↑m)<GOAL>↑m < ↑n ↔ Ordering.gt = Ordering.lt
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>inst✝ : Monoid G<VAR>X Y : Action (Type u) (MonCat.of G)<VAR>f : X ⟶ Y<VAR>A : Rep k G<VAR>x : CoeSort.coe A<GOAL>(A.leftRegularHom x).hom (Finsupp.single 1 1) = x
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>inst✝ : Monoid G<VAR>X Y : Action (Type u) (MonCat.of G)<VAR>f : X ⟶ Y<VAR>A : Rep k G<VAR>x : CoeSort.coe A<GOAL>0 • (A.ρ 1) x = 0
<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 μ<GOAL>0 < μ {x | f x ≤ ⨍⁻ (a : α), f a ∂μ}
<VAR>f : Ordinal.{u} → Ordinal.{u}<VAR>a b : Ordinal.{u}<GOAL>a < nfp f b ↔ ∃ n, a < f^[n] b
<VAR>f : Ordinal.{u} → Ordinal.{u}<VAR>a b : Ordinal.{u}<GOAL>a < (fun a => sup fun n => f^[n] a) b ↔ ∃ n, a < f^[n] b
<VAR>F : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝⁹ : CommSemiring R<VAR>inst✝⁸ : StarRing R<VAR>inst✝⁷ : Semiring A<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : StarRing A<VAR>inst✝⁴ : StarModule R A<VAR>inst✝³ : Semiring B<VAR>inst✝² : Algebra R B<VAR>inst✝¹ : StarRing B<VAR>inst✝ : StarModule R B<VAR>ι : Sort u_5<VAR>S : ι → StarSubalgebra R A<VAR>x : A<GOAL>x ∈ ⨅ i, S i ↔ ∀ (i : ι), x ∈ S i
<VAR>a : ℕ<GOAL>IsUpperSet (range ⇑castOrderEmbedding)
<VAR>n d : ℤ<VAR>d_ne_zero : d ≠ 0<GOAL>↑n / ↑d = n /. d
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹⁵ : RCLike 𝕜<VAR>inst✝¹⁴ : NormedAddCommGroup F<VAR>inst✝¹³ : NormedSpace 𝕜 F<VAR>inst✝¹² : NormedAddCommGroup F'<VAR>inst✝¹¹ : NormedSpace 𝕜 F'<VAR>inst✝¹⁰ : NormedSpace ℝ F'<VAR>inst✝⁹ : CompleteSpace F'<VAR>inst✝⁸ : NormedAddCommGroup G<VAR>inst✝⁷ : NormedAddCommGroup G'<VAR>inst✝⁶ : NormedSpace ℝ G'<VAR>inst✝⁵ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>inst✝⁴ : NormedSpace ℝ G<VAR>hm : m ≤ m0<VAR>inst✝³ : SigmaFinite (μ.trim hm)<VAR>E : Type u_8<VAR>inst✝² : NormedLatticeAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : OrderedSMul ℝ E<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>x : E<VAR>hx : 0 ≤ x<GOAL>0 ≤ (condexpInd E hm μ s) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹⁵ : RCLike 𝕜<VAR>inst✝¹⁴ : NormedAddCommGroup F<VAR>inst✝¹³ : NormedSpace 𝕜 F<VAR>inst✝¹² : NormedAddCommGroup F'<VAR>inst✝¹¹ : NormedSpace 𝕜 F'<VAR>inst✝¹⁰ : NormedSpace ℝ F'<VAR>inst✝⁹ : CompleteSpace F'<VAR>inst✝⁸ : NormedAddCommGroup G<VAR>inst✝⁷ : NormedAddCommGroup G'<VAR>inst✝⁶ : NormedSpace ℝ G'<VAR>inst✝⁵ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>inst✝⁴ : NormedSpace ℝ G<VAR>hm : m ≤ m0<VAR>inst✝³ : SigmaFinite (μ.trim hm)<VAR>E : Type u_8<VAR>inst✝² : NormedLatticeAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : OrderedSMul ℝ E<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>x : E<VAR>hx : 0 ≤ x<GOAL>↑↑0 ≤ᶠ[ae μ] ↑↑((condexpInd E hm μ s) x)