ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>f g : Ordinal.{u} → Ordinal.{u}<VAR>hf : IsNormal f<VAR>hg : IsNormal g<VAR>x✝ : f 0 = g 0 ∧ ∀ (a : Ordinal.{u}), f a = g a → f (succ a) = g (succ a)<VAR>h₁ : f 0 = g 0<VAR>h₂ : ∀ (a : Ordinal.{u}), f a = g a → f (succ a) = g (succ a)<GOAL>f 0 = g 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>f g : Ordinal.{u} → Ordinal.{u}<VAR>hf : IsNormal f<VAR>hg : IsNormal g<VAR>x✝ : f 0 = g 0 ∧ ∀ (a : Ordinal.{u}), f a = g a → f (succ a) = g (succ a)<VAR>h₁ : f 0 = g 0<VAR>h₂ : ∀ (a : Ordinal.{u}), f a = g a → f (succ a) = g (succ a)<VAR>o✝ : Ordinal.{u}<VAR>a✝ : f o✝ = g o✝<GOAL>f (succ o✝) = g (succ o✝)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>f g : Ordinal.{u} → Ordinal.{u}<VAR>hf : IsNormal f<VAR>hg : IsNormal g<VAR>x✝ : f 0 = g 0 ∧ ∀ (a : Ordinal.{u}), f a = g a → f (succ a) = g (succ a)<VAR>h₁ : f 0 = g 0<VAR>h₂ : ∀ (a : Ordinal.{u}), f a = g a → f (succ a) = g (succ a)<VAR>o✝ : Ordinal.{u}<VAR>ho : o✝.IsLimit<VAR>H : ∀ o' < o✝, f o' = g o'<GOAL>f o✝ = g o✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>f g : Ordinal.{u} → Ordinal.{u}<VAR>hf : IsNormal f<VAR>hg : IsNormal g<VAR>x✝ : f 0 = g 0 ∧ ∀ (a : Ordinal.{u}), f a = g a → f (succ a) = g (succ a)<VAR>h₁ : f 0 = g 0<VAR>h₂ : ∀ (a : Ordinal.{u}), f a = g a → f (succ a) = g (succ a)<VAR>o✝ : Ordinal.{u}<VAR>ho : o✝.IsLimit<VAR>H : ∀ o' < o✝, f o' = g o'<GOAL>(o✝.bsup fun x x_1 => f x) = o✝.bsup fun x x_1 => g x
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>H : Type u_4<VAR>A : Type u_5<VAR>B : Type u_6<VAR>α : Type u_7<VAR>β : Type u_8<VAR>γ : Type u_9<VAR>δ : Type u_10<VAR>inst✝⁴ : SMul M α<VAR>inst✝³ : SMul N α<VAR>inst✝² : SMul M β<VAR>inst✝¹ : SMul N β<VAR>inst✝ : SMulCommClass M N α<VAR>f : α → β<VAR>hf : Surjective f<VAR>h₁ : ∀ (c : M) (x : α), f (c • x) = c • f x<VAR>h₂ : ∀ (c : N) (x : α), f (c • x) = c • f x<VAR>c₁ : M<VAR>c₂ : N<VAR>x : α<GOAL>c₁ • c₂ • f x = c₂ • c₁ • f x
<VAR>R : Type u<VAR>R' : Type u'<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>inst✝⁹ : Ring R<VAR>inst✝⁸ : Ring R'<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup M'<VAR>inst✝⁵ : AddCommGroup M₁<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module R M₁<VAR>inst✝¹ : Module R' M'<VAR>inst✝ : Module R' M₁<VAR>f : M →ₗ[R] M'<VAR>h : Surjective ⇑f<GOAL>lift.{v, v'} (Module.rank R M') ≤ lift.{v', v} (Module.rank R M)
<VAR>R : Type u<VAR>R' : Type u'<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>inst✝⁹ : Ring R<VAR>inst✝⁸ : Ring R'<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup M'<VAR>inst✝⁵ : AddCommGroup M₁<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module R M₁<VAR>inst✝¹ : Module R' M'<VAR>inst✝ : Module R' M₁<VAR>f : M →ₗ[R] M'<VAR>h : Surjective ⇑f<GOAL>lift.{v, v'} (Module.rank R ↥(range f)) ≤ lift.{v', v} (Module.rank R M)
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>u v : UniformSpace α<GOAL>u ≤ v ↔ UniformContinuous id
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝¹¹ : NormedAddCommGroup V<VAR>inst✝¹⁰ : NormedSpace ℝ V<VAR>inst✝⁹ : StrictConvexSpace ℝ V<VAR>E : Type u_3<VAR>F : Type u_4<VAR>PE : Type u_5<VAR>PF : Type u_6<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : StrictConvexSpace ℝ E<VAR>inst✝³ : MetricSpace PE<VAR>inst✝² : MetricSpace PF<VAR>inst✝¹ : NormedAddTorsor E PE<VAR>inst✝ : NormedAddTorsor F PF<VAR>r : ℝ<VAR>f : PF → PE<VAR>x y z : PE<VAR>hx : dist x y = dist x z / 2<VAR>hy : dist y z = dist x z / 2<GOAL>y = midpoint ℝ x z
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝¹¹ : NormedAddCommGroup V<VAR>inst✝¹⁰ : NormedSpace ℝ V<VAR>inst✝⁹ : StrictConvexSpace ℝ V<VAR>E : Type u_3<VAR>F : Type u_4<VAR>PE : Type u_5<VAR>PF : Type u_6<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : StrictConvexSpace ℝ E<VAR>inst✝³ : MetricSpace PE<VAR>inst✝² : MetricSpace PF<VAR>inst✝¹ : NormedAddTorsor E PE<VAR>inst✝ : NormedAddTorsor F PF<VAR>r : ℝ<VAR>f : PF → PE<VAR>x y z : PE<VAR>hx : dist x y = dist x z / 2<VAR>hy : dist y z = dist x z / 2<GOAL>dist x y = ⅟2 * dist x z
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝¹¹ : NormedAddCommGroup V<VAR>inst✝¹⁰ : NormedSpace ℝ V<VAR>inst✝⁹ : StrictConvexSpace ℝ V<VAR>E : Type u_3<VAR>F : Type u_4<VAR>PE : Type u_5<VAR>PF : Type u_6<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : StrictConvexSpace ℝ E<VAR>inst✝³ : MetricSpace PE<VAR>inst✝² : MetricSpace PF<VAR>inst✝¹ : NormedAddTorsor E PE<VAR>inst✝ : NormedAddTorsor F PF<VAR>r : ℝ<VAR>f : PF → PE<VAR>x y z : PE<VAR>hx : dist x y = dist x z / 2<VAR>hy : dist y z = dist x z / 2<GOAL>dist y z = (1 - ⅟2) * dist x z
<VAR>α : Type u_1<VAR>β : Type u_2<GOAL>¬Nontrivial α ↔ Subsingleton α
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : UniformSpace α<VAR>inst✝² : Group α<VAR>inst✝¹ : UniformGroup α<VAR>inst✝ : (𝓝 1).IsCountablyGenerated<GOAL>(𝓤 α).IsCountablyGenerated
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : UniformSpace α<VAR>inst✝² : Group α<VAR>inst✝¹ : UniformGroup α<VAR>inst✝ : (𝓝 1).IsCountablyGenerated<GOAL>(comap (fun x => x.2 / x.1) (𝓝 1)).IsCountablyGenerated
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x y : α<GOAL>dist x y = (edist x y).toReal
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>H : Type u_4<VAR>A : Type u_5<VAR>B : Type u_6<VAR>α : Type u_7<VAR>β : Type u_8<VAR>γ : Type u_9<VAR>δ : Type u_10<VAR>inst✝³ : Monoid M<VAR>inst✝² : MulAction M α<VAR>inst✝¹ : Group G<VAR>inst✝ : MulAction G α<VAR>g : G<VAR>a b : α<VAR>h : g⁻¹ • a = b<GOAL>a = g • b
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>H : Type u_4<VAR>A : Type u_5<VAR>B : Type u_6<VAR>α : Type u_7<VAR>β : Type u_8<VAR>γ : Type u_9<VAR>δ : Type u_10<VAR>inst✝³ : Monoid M<VAR>inst✝² : MulAction M α<VAR>inst✝¹ : Group G<VAR>inst✝ : MulAction G α<VAR>g : G<VAR>a b : α<VAR>h : a = g • b<GOAL>g⁻¹ • a = b
<VAR>M₀ : Type u_1<VAR>G₀ : Type u_2<VAR>inst✝ : MulZeroClass M₀<VAR>s : Set M₀<VAR>x✝ : M₀<GOAL>0 * x✝ = x✝ * 0
<VAR>M₀ : Type u_1<VAR>G₀ : Type u_2<VAR>inst✝ : MulZeroClass M₀<VAR>s : Set M₀<VAR>x✝¹ x✝ : M₀<GOAL>0 * (x✝¹ * x✝) = 0 * x✝¹ * x✝
<VAR>M₀ : Type u_1<VAR>G₀ : Type u_2<VAR>inst✝ : MulZeroClass M₀<VAR>s : Set M₀<VAR>x✝¹ x✝ : M₀<GOAL>x✝¹ * 0 * x✝ = x✝¹ * (0 * x✝)
<VAR>M₀ : Type u_1<VAR>G₀ : Type u_2<VAR>inst✝ : MulZeroClass M₀<VAR>s : Set M₀<VAR>x✝¹ x✝ : M₀<GOAL>x✝¹ * x✝ * 0 = x✝¹ * (x✝ * 0)
<VAR>R : Type u_1<VAR>inst✝⁸ : CommSemiring R<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>Q : Type u_5<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : AddCommMonoid N<VAR>inst✝⁵ : AddCommMonoid P<VAR>inst✝⁴ : AddCommMonoid Q<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R N<VAR>inst✝¹ : Module R P<VAR>inst✝ : Module R Q<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>hg : Function.Surjective ⇑g<VAR>z : Q ⊗[R] P<GOAL>∃ a, (lTensor Q g) a = z
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X✝ Y✝ Z✝ X Y Z : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>inst✝ : Mono (f ≫ g)<GOAL>Mono f
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : Preorder α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a a₁ a₂ b b₁ b₂ c x : α<VAR>ha : a₂ ≤ a₁<VAR>hb : b₁ ≤ b₂<GOAL>Ioo a₁ b₁ ⊆ Ioo a₂ b₂
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>inst✝⁸ : RCLike 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : InnerProductSpace 𝕜 E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : InnerProductSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : InnerProductSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup E'<VAR>inst✝ : InnerProductSpace ℝ E'<VAR>T : E →L[𝕜] E<VAR>hT : (↑T).IsSymmetric<VAR>x : E<GOAL>∃ r, ⟪T x, x⟫_𝕜 = ↑r
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>inst✝⁸ : RCLike 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : InnerProductSpace 𝕜 E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : InnerProductSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : InnerProductSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup E'<VAR>inst✝ : InnerProductSpace ℝ E'<VAR>T : E →L[𝕜] E<VAR>hT : (↑T).IsSymmetric<VAR>x : E<GOAL>(starRingEnd 𝕜) ⟪T x, x⟫_𝕜 = ⟪T x, x⟫_𝕜
<VAR>y : ℝ<VAR>hy : 1 ≤ y<GOAL>↑(harmonic ⌊y⌋₊) ≤ 1 + Real.log y
<VAR>y : ℝ<VAR>hy : 1 ≤ y<GOAL>1 + Real.log ↑⌊y⌋₊ ≤ 1 + Real.log y
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>fst✝⁴ : C<VAR>snd✝⁴ : C ⥤ D<VAR>fst✝³ : C<VAR>snd✝³ : C ⥤ D<VAR>fst✝² : (fst✝³, snd✝³).1 ⟶ (fst✝⁴, snd✝⁴).1<VAR>snd✝² : (fst✝³, snd✝³).2 ⟶ (fst✝⁴, snd✝⁴).2<VAR>fst✝¹ : C<VAR>snd✝¹ : C ⥤ D<VAR>fst✝ : (fst✝¹, snd✝¹).1 ⟶ (fst✝³, snd✝³).1<VAR>snd✝ : (fst✝¹, snd✝¹).2 ⟶ (fst✝³, snd✝³).2<GOAL>{ obj := fun p => p.2.obj p.1, map := fun {x y} f => x.2.map f.1 ≫ f.2.app y.1 }.map ((fst✝, snd✝) ≫ (fst✝², snd✝²)) = { obj := fun p => p.2.obj p.1, map := fun {x y} f => x.2.map f.1 ≫ f.2.app y.1 }.map (fst✝, snd✝) ≫ { obj := fun p => p.2.obj p.1, map := fun {x y} f => x.2.map f.1 ≫ f.2.app y.1 }.map (fst✝², snd✝²)
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>fst✝⁴ : C<VAR>snd✝⁴ : C ⥤ D<VAR>fst✝³ : C<VAR>snd✝³ : C ⥤ D<VAR>fst✝² : (fst✝³, snd✝³).1 ⟶ (fst✝⁴, snd✝⁴).1<VAR>snd✝² : (fst✝³, snd✝³).2 ⟶ (fst✝⁴, snd✝⁴).2<VAR>fst✝¹ : C<VAR>snd✝¹ : C ⥤ D<VAR>fst✝ : (fst✝¹, snd✝¹).1 ⟶ (fst✝³, snd✝³).1<VAR>snd✝ : (fst✝¹, snd✝¹).2 ⟶ (fst✝³, snd✝³).2<GOAL>snd✝¹.map fst✝ ≫ snd✝¹.map fst✝² ≫ snd✝.app fst✝⁴ ≫ snd✝².app fst✝⁴ = snd✝¹.map fst✝ ≫ snd✝.app fst✝³ ≫ snd✝³.map fst✝² ≫ snd✝².app fst✝⁴
<VAR>m✝ n✝ a✝ b✝ c d a b m n : ℕ<VAR>hmn : m.Coprime n<VAR>h : a ≡ b [MOD m] ∧ a ≡ b [MOD n]<GOAL>a ≡ b [MOD m * n]
<VAR>m✝ n✝ a✝ b✝ c d a b m n : ℕ<VAR>hmn : m.Coprime n<VAR>h : m ∣ (↑b - ↑a).natAbs ∧ n ∣ (↑b - ↑a).natAbs<GOAL>a ≡ b [MOD m * n]
<VAR>m✝ n✝ a✝ b✝ c d a b m n : ℕ<VAR>hmn : m.Coprime n<VAR>h : m ∣ (↑b - ↑a).natAbs ∧ n ∣ (↑b - ↑a).natAbs<GOAL>m * n ∣ (↑b - ↑a).natAbs
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedSemifield α<VAR>a b c d e : α<VAR>m✝ n✝ : ℤ<VAR>a1 : 1 ≤ a<VAR>m n : ℕ<VAR>mn : m ≤ n<GOAL>(a ^ n)⁻¹ ≤ (a ^ m)⁻¹
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>β : Type u<VAR>u : F (α ::: β) → β<VAR>x y : (P F).W α<GOAL>WEquiv x y → recF u x = recF u y
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>β : Type u<VAR>u : F (α ::: β) → β<VAR>x y : (P F).W α<GOAL>∀ (a : (P F).A) (f' : (P F).drop.B a ⟹ α) (f : (P F).last.B a → (P F).W α), WEquiv ((P F).wMk a f' f) y → recF u ((P F).wMk a f' f) = recF u y
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>β : Type u<VAR>u : F (α ::: β) → β<VAR>x y : (P F).W α<VAR>a₀ : (P F).A<VAR>f'₀ : (P F).drop.B a₀ ⟹ α<VAR>f₀ : (P F).last.B a₀ → (P F).W α<GOAL>WEquiv ((P F).wMk a₀ f'₀ f₀) y → recF u ((P F).wMk a₀ f'₀ f₀) = recF u y
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>β : Type u<VAR>u : F (α ::: β) → β<VAR>x y : (P F).W α<VAR>a₀ : (P F).A<VAR>f'₀ : (P F).drop.B a₀ ⟹ α<VAR>f₀ : (P F).last.B a₀ → (P F).W α<GOAL>∀ (a : (P F).A) (f' : (P F).drop.B a ⟹ α) (f : (P F).last.B a → (P F).W α), WEquiv ((P F).wMk a₀ f'₀ f₀) ((P F).wMk a f' f) → recF u ((P F).wMk a₀ f'₀ f₀) = recF u ((P F).wMk a f' f)
<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>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>h : s ∈ 𝓝 x<GOAL>derivWithin f s x = deriv f x
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>A : Type u'<VAR>inst✝ : Category.{v', u'} A<VAR>I : Type u_1<VAR>Y : I → C<VAR>hY : J.CoversTop Y<VAR>F : Sheaf J A<VAR>c : Cone F.val<VAR>hc : IsLimit c<VAR>X : A<VAR>f g : X ⟶ c.pt<VAR>h : ∀ (i : I), f ≫ c.π.app (Opposite.op (Y i)) = g ≫ c.π.app (Opposite.op (Y i))<GOAL>f = g
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>A : Type u'<VAR>inst✝ : Category.{v', u'} A<VAR>I : Type u_1<VAR>Y : I → C<VAR>hY : J.CoversTop Y<VAR>F : Sheaf J A<VAR>c : Cone F.val<VAR>hc : IsLimit c<VAR>X : A<VAR>f g : X ⟶ c.pt<VAR>h : ∀ (i : I), f ≫ c.π.app (Opposite.op (Y i)) = g ≫ c.π.app (Opposite.op (Y i))<VAR>Z : Cᵒᵖ<GOAL>∀ (I_1 : (hY.cover (Opposite.unop Z)).Arrow), (f ≫ c.π.app Z) ≫ F.val.map I_1.f.op = (g ≫ c.π.app Z) ≫ F.val.map I_1.f.op
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>A : Type u'<VAR>inst✝ : Category.{v', u'} A<VAR>I : Type u_1<VAR>Y : I → C<VAR>hY : J.CoversTop Y<VAR>F : Sheaf J A<VAR>c : Cone F.val<VAR>hc : IsLimit c<VAR>X : A<VAR>f g : X ⟶ c.pt<VAR>h : ∀ (i : I), f ≫ c.π.app (Opposite.op (Y i)) = g ≫ c.π.app (Opposite.op (Y i))<VAR>Z : Cᵒᵖ<VAR>W : C<VAR>a : W ⟶ Opposite.unop Z<VAR>i : I<VAR>b : W ⟶ Y i<GOAL>(f ≫ c.π.app Z) ≫ F.val.map { Y := W, f := a, hf := ⋯ }.f.op = (g ≫ c.π.app Z) ≫ F.val.map { Y := W, f := a, hf := ⋯ }.f.op
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>f g : End R M<VAR>hf : f.IsSemisimple<VAR>μ : R<GOAL>f.maxGenEigenspace μ = f.eigenspace μ
<VAR>ι : Type uι<VAR>E : Type uE<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : FiniteDimensional ℝ E<VAR>F : Type uF<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>H : Type uH<VAR>inst✝⁵ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝⁴ : TopologicalSpace M<VAR>inst✝³ : ChartedSpace H M<VAR>inst✝² : SmoothManifoldWithCorners I M<VAR>inst✝¹ : T2Space M<VAR>inst✝ : SigmaCompactSpace M<VAR>s : Set M<VAR>hs : IsClosed s<GOAL>∃ f, f.IsSubordinate fun x => (chartAt H ↑x).source
<VAR>ι : Type uι<VAR>E : Type uE<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : FiniteDimensional ℝ E<VAR>F : Type uF<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>H : Type uH<VAR>inst✝⁵ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝⁴ : TopologicalSpace M<VAR>inst✝³ : ChartedSpace H M<VAR>inst✝² : SmoothManifoldWithCorners I M<VAR>inst✝¹ : T2Space M<VAR>inst✝ : SigmaCompactSpace M<VAR>s : Set M<VAR>hs : IsClosed s<VAR>x : M<VAR>hx : x ∈ s<GOAL>x ∈ ⋃ i, (chartAt H ↑i).source
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝ : CompleteDistribLattice α<VAR>f : Filter β<VAR>p q : β → Prop<VAR>u : β → α<VAR>g : Filter β<GOAL>limsup u (f ⊔ g) = limsup u f ⊔ limsup u g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝ : CompleteDistribLattice α<VAR>f : Filter β<VAR>p q : β → Prop<VAR>u : β → α<VAR>g : Filter β<GOAL>limsup u (f ⊔ g) ≤ limsup u f ⊔ limsup u g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝ : CompleteDistribLattice α<VAR>f : Filter β<VAR>p q : β → Prop<VAR>u : β → α<VAR>g : Filter β<GOAL>∀ (i : α), (∀ᶠ (n : β) in f, u n ≤ i) → ∀ (i_1 : α), (∀ᶠ (n : β) in g, u n ≤ i_1) → sInf {a | ∀ᶠ (n : β) in f ⊔ g, u n ≤ a} ≤ i ⊔ i_1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝ : CompleteDistribLattice α<VAR>f : Filter β<VAR>p q : β → Prop<VAR>u : β → α<VAR>g : Filter β<VAR>a : α<VAR>ha : ∀ᶠ (n : β) in f, u n ≤ a<VAR>b : α<VAR>hb : ∀ᶠ (n : β) in g, u n ≤ b<GOAL>sInf {a | ∀ᶠ (n : β) in f ⊔ g, u n ≤ a} ≤ a ⊔ b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝ : LE α<VAR>S : Set (LowerSet α)<VAR>s t : LowerSet α<VAR>a : α<GOAL>Disjoint ↑s ↑t ↔ Disjoint s t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Preorder α<VAR>inst✝ : SuccOrder α<VAR>a b : α<VAR>hb : ¬IsMax b<GOAL>Ico a (succ b) = Icc a b
<VAR>R : Type u<VAR>S : Type v<VAR>ι : Type w<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝¹ : Semiring R<VAR>p✝ q r : R[X]<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>p : R[X]<GOAL>(map f p).degree = p.degree ↔ f p.leadingCoeff ≠ 0 ∨ p = 0
<VAR>R : Type u<VAR>S : Type v<VAR>ι : Type w<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝¹ : Semiring R<VAR>p✝ q r : R[X]<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>p : R[X]<VAR>h : p = 0<GOAL>(map f p).degree = p.degree ↔ f p.leadingCoeff ≠ 0 ∨ p = 0
<VAR>R : Type u<VAR>S : Type v<VAR>ι : Type w<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝¹ : Semiring R<VAR>p✝ q r : R[X]<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>p : R[X]<VAR>h : p ≠ 0<GOAL>(map f p).degree = p.degree ↔ f p.leadingCoeff ≠ 0 ∨ p = 0
<VAR>R : Type u<VAR>S : Type v<VAR>ι : Type w<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝¹ : Semiring R<VAR>p✝ q r : R[X]<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>p : R[X]<VAR>h : p ≠ 0<GOAL>(map f p).degree = p.degree ↔ f p.leadingCoeff ≠ 0
<VAR>R : Type u<VAR>S : Type v<VAR>ι : Type w<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝¹ : Semiring R<VAR>p✝ q r : R[X]<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>p : R[X]<VAR>h : p ≠ 0<VAR>h2 : (map f p).degree = p.degree<GOAL>f p.leadingCoeff ≠ 0
<VAR>R : Type u<VAR>S : Type v<VAR>ι : Type w<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝¹ : Semiring R<VAR>p✝ q r : R[X]<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>p : R[X]<VAR>h : p ≠ 0<VAR>h2 : (map f p).degree = p.degree<VAR>h3 : (map f p).natDegree = p.natDegree<GOAL>f p.leadingCoeff ≠ 0
<VAR>R : Type u<VAR>S : Type v<VAR>ι : Type w<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝¹ : Semiring R<VAR>p✝ q r : R[X]<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>p : R[X]<VAR>h : p ≠ 0<VAR>h2 : (map f p).degree = p.degree<VAR>h3 : (map f p).natDegree = p.natDegree<VAR>h4 : map f p ≠ 0<GOAL>f p.leadingCoeff ≠ 0
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝⁵ : LinearOrderedAddCommMonoid α<VAR>inst✝⁴ : OrderedAddCommMonoid β<VAR>inst✝³ : SMulZeroClass α β<VAR>inst✝² : PosSMulReflectLE α β<VAR>inst✝¹ : FloorDiv α β<VAR>inst✝ : CeilDiv α β<VAR>a : α<VAR>b c : β<GOAL>b ⌊/⌋ a ≤ b ⌈/⌉ a
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝⁵ : LinearOrderedAddCommMonoid α<VAR>inst✝⁴ : OrderedAddCommMonoid β<VAR>inst✝³ : SMulZeroClass α β<VAR>inst✝² : PosSMulReflectLE α β<VAR>inst✝¹ : FloorDiv α β<VAR>inst✝ : CeilDiv α β<VAR>a : α<VAR>b c : β<VAR>ha : a ≤ 0<GOAL>b ⌊/⌋ a ≤ b ⌈/⌉ a
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝⁵ : LinearOrderedAddCommMonoid α<VAR>inst✝⁴ : OrderedAddCommMonoid β<VAR>inst✝³ : SMulZeroClass α β<VAR>inst✝² : PosSMulReflectLE α β<VAR>inst✝¹ : FloorDiv α β<VAR>inst✝ : CeilDiv α β<VAR>a : α<VAR>b c : β<VAR>ha : 0 < a<GOAL>b ⌊/⌋ a ≤ b ⌈/⌉ a
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>F : Type u_3<VAR>inst✝³ : FunLike F (Set α) ℝ≥0∞<VAR>inst✝² : OuterMeasureClass F α<VAR>μ : F<VAR>s✝ t : Set α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : SecondCountableTopology α<VAR>s : Set α<VAR>hs : μ s ≠ 0<GOAL>∃ x ∈ s, ∀ t ∈ 𝓝[s] x, 0 < μ t
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>F : Type u_3<VAR>inst✝³ : FunLike F (Set α) ℝ≥0∞<VAR>inst✝² : OuterMeasureClass F α<VAR>μ : F<VAR>s✝ t : Set α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : SecondCountableTopology α<VAR>s : Set α<VAR>hs : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, μ t ≤ 0<GOAL>μ s = 0
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>F : Type u_3<VAR>inst✝³ : FunLike F (Set α) ℝ≥0∞<VAR>inst✝² : OuterMeasureClass F α<VAR>μ : F<VAR>s✝ t : Set α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : SecondCountableTopology α<VAR>s : Set α<VAR>hs : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, μ t = 0<GOAL>μ s = 0
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s : Set α<VAR>m₁ m₂ : MeasurableSpace α<VAR>hm₁₂ : m₁ ≤ m₂<VAR>hm₂ : m₂ ≤ m0<GOAL>(μ.trim hm₂).trim hm₁₂ = μ.trim ⋯
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s : Set α<VAR>m₁ m₂ : MeasurableSpace α<VAR>hm₁₂ : m₁ ≤ m₂<VAR>hm₂ : m₂ ≤ m0<VAR>t : Set α<VAR>ht : MeasurableSet t<GOAL>((μ.trim hm₂).trim hm₁₂) t = (μ.trim ⋯) t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>l l' : Filter α<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>t : Set α<VAR>i : ι<VAR>p' : ι' → Prop<VAR>s' : ι' → Set α<VAR>i' : ι'<VAR>hl : l.HasBasis p s<GOAL>(∀ {i : ι}, p i → (s i).Nonempty) ↔ ¬∃ i, p i ∧ s i = ∅
<VAR>ι : Type uι<VAR>inst✝¹⁰ : Fintype ι<VAR>𝕜 : Type u𝕜<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>inst✝⁸ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝⁷ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>F : Type uF<VAR>inst✝⁶ : SeminormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>E' : ι → Type u_1<VAR>E'' : ι → Type u_2<VAR>inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E' i)<VAR>inst✝³ : (i : ι) → NormedSpace 𝕜 (E' i)<VAR>inst✝² : (i : ι) → SeminormedAddCommGroup (E'' i)<VAR>inst✝¹ : (i : ι) → NormedSpace 𝕜 (E'' i)<VAR>g : (i : ι) → E' i →L[𝕜] E'' i<VAR>f : (i : ι) → E i →L[𝕜] E' i<VAR>inst✝ : DecidableEq ι<VAR>i : ι<VAR>u v : E i →L[𝕜] E' i<VAR>x : ⨂[𝕜] (i : ι), E i<GOAL>(mapL (update f i (u + v))) x = (mapL (update f i u) + mapL (update f i v)) x
<VAR>α : Type u_1<VAR>l₁ l₂ l₃ : List α<VAR>h₁ : l₁ <+ l₂<VAR>h₂ : l₂ <+ l₃<GOAL>l₁ <+ l₃
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁶ : SemilatticeInf α<VAR>inst✝⁵ : BoundedOrder α<VAR>inst✝⁴ : DecidableRel fun x x_1 => x ≤ x_1<VAR>inst✝³ : SemilatticeInf β<VAR>inst✝² : BoundedOrder β<VAR>inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1<VAR>s t : Finset α<VAR>a : α<VAR>inst✝ : DecidableEq α<VAR>hs : IsAntichain (fun x x_1 => x ≤ x_1) ↑s<VAR>ha : a ∈ s<GOAL>s.truncatedInf a = a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁶ : SemilatticeInf α<VAR>inst✝⁵ : BoundedOrder α<VAR>inst✝⁴ : DecidableRel fun x x_1 => x ≤ x_1<VAR>inst✝³ : SemilatticeInf β<VAR>inst✝² : BoundedOrder β<VAR>inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1<VAR>s t : Finset α<VAR>a : α<VAR>inst✝ : DecidableEq α<VAR>hs : IsAntichain (fun x x_1 => x ≤ x_1) ↑s<VAR>ha : a ∈ s<GOAL>a ≤ s.truncatedInf a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁶ : SemilatticeInf α<VAR>inst✝⁵ : BoundedOrder α<VAR>inst✝⁴ : DecidableRel fun x x_1 => x ≤ x_1<VAR>inst✝³ : SemilatticeInf β<VAR>inst✝² : BoundedOrder β<VAR>inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1<VAR>s t : Finset α<VAR>a : α<VAR>inst✝ : DecidableEq α<VAR>hs : IsAntichain (fun x x_1 => x ≤ x_1) ↑s<VAR>ha : a ∈ s<GOAL>∀ (b : α), b ∈ s ∧ b ≤ a → a ≤ id b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁶ : SemilatticeInf α<VAR>inst✝⁵ : BoundedOrder α<VAR>inst✝⁴ : DecidableRel fun x x_1 => x ≤ x_1<VAR>inst✝³ : SemilatticeInf β<VAR>inst✝² : BoundedOrder β<VAR>inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1<VAR>s t : Finset α<VAR>a : α<VAR>inst✝ : DecidableEq α<VAR>hs : IsAntichain (fun x x_1 => x ≤ x_1) ↑s<VAR>ha : a ∈ s<VAR>b : α<VAR>hb : b ∈ s<VAR>hba : b ≤ a<GOAL>a ≤ id b
<VAR>z τ : ℂ<GOAL>jacobiTheta₂ z (τ + 2) = jacobiTheta₂ z τ
<VAR>z τ : ℂ<VAR>n : ℤ<GOAL>jacobiTheta₂_term n z (τ + 2) = jacobiTheta₂_term n z τ
<VAR>z τ : ℂ<VAR>n : ℤ<GOAL>cexp (2 * ↑π * I * ↑n * z) * cexp (↑π * I * ↑n ^ 2 * (τ + 2)) = cexp (2 * ↑π * I * ↑n * z) * cexp (↑π * I * ↑n ^ 2 * τ)
<VAR>z τ : ℂ<VAR>n : ℤ<GOAL>cexp (↑π * I * ↑n ^ 2 * 2) = 1
<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✝ : RankCondition R<VAR>J : Set M<VAR>v : Basis ι R M<VAR>hJ : span R J = ⊤<GOAL>#↑(range ⇑v) ≤ #↑J
<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✝ : RankCondition R<VAR>J : Set M<VAR>v : Basis ι R M<VAR>hJ : span R J = ⊤<VAR>this : Nontrivial R<GOAL>#↑(range ⇑v) ≤ #↑J
<VAR>α : Type u_1<VAR>β : ?m.16439<VAR>inst✝² : Preorder α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : IsUpper α<VAR>s : Set α<GOAL>IsOpen s ↔ GenerateOpen {t | ∃ a, (Iic a)ᶜ = t} s