ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>F F' F'' : Cᵒᵖ ⥤ Type w<VAR>G G' : Subpresheaf F<VAR>hF : Presieve.IsSheaf J F<VAR>U : C<VAR>S : Sieve U<VAR>hS : S ∈ J.sieves U<VAR>x : Presieve.FamilyOfElements (sheafify J G).toPresheaf S.arrows<VAR>hx : x.Compatible<VAR>S' : Sieve U := Sieve.bind S.arrows fun Y f hf => G.sieveOfSection ↑(x f hf)<VAR>W : (V : C) → (i : V ⟶ U) → S'.arrows i → C<VAR>i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi<VAR>i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U<VAR>hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)<VAR>h₁ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), (fun Y f h => ((fun Y f hf => G.sieveOfSection ↑(x f hf)) Y f h).arrows) (W V i hi) (i₂ V i hi) ⋯ (i₁ V i hi)<VAR>h₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), i₁ V i hi ≫ i₂ V i hi = i<GOAL>∃! t, x.IsAmalgamation t
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>F F' F'' : Cᵒᵖ ⥤ Type w<VAR>G G' : Subpresheaf F<VAR>hF : Presieve.IsSheaf J F<VAR>U : C<VAR>S : Sieve U<VAR>hS : S ∈ J.sieves U<VAR>x : Presieve.FamilyOfElements (sheafify J G).toPresheaf S.arrows<VAR>hx : x.Compatible<VAR>S' : Sieve U := Sieve.bind S.arrows fun Y f hf => G.sieveOfSection ↑(x f hf)<VAR>W : (V : C) → (i : V ⟶ U) → S'.arrows i → C<VAR>i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi<VAR>i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U<VAR>hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)<VAR>h₁ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), F.map (i₁ V i hi).op ↑(x (i₂ V i hi) ⋯) ∈ G.obj (op V)<VAR>h₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), i₁ V i hi ≫ i₂ V i hi = i<GOAL>∃! t, x.IsAmalgamation t
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>F F' F'' : Cᵒᵖ ⥤ Type w<VAR>G G' : Subpresheaf F<VAR>hF : Presieve.IsSheaf J F<VAR>U : C<VAR>S : Sieve U<VAR>hS : S ∈ J.sieves U<VAR>x : Presieve.FamilyOfElements (sheafify J G).toPresheaf S.arrows<VAR>hx : x.Compatible<VAR>S' : Sieve U := Sieve.bind S.arrows fun Y f hf => G.sieveOfSection ↑(x f hf)<VAR>W : (V : C) → (i : V ⟶ U) → S'.arrows i → C<VAR>i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi<VAR>i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U<VAR>hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)<VAR>h₁ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), F.map (i₁ V i hi).op ↑(x (i₂ V i hi) ⋯) ∈ G.obj (op V)<VAR>h₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), i₁ V i hi ≫ i₂ V i hi = i<VAR>x'' : Presieve.FamilyOfElements F S'.arrows := fun V i hi => F.map (i₁ V i hi).op ↑(x (i₂ V i hi) ⋯)<VAR>H : ∀ (s : (sheafify J G).toPresheaf.obj (op U)), x.IsAmalgamation s ↔ x''.IsAmalgamation ↑s<GOAL>∃! t, x.IsAmalgamation t
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>F F' F'' : Cᵒᵖ ⥤ Type w<VAR>G G' : Subpresheaf F<VAR>hF : Presieve.IsSheaf J F<VAR>U : C<VAR>S : Sieve U<VAR>hS : S ∈ J.sieves U<VAR>x : Presieve.FamilyOfElements (sheafify J G).toPresheaf S.arrows<VAR>hx : x.Compatible<VAR>S' : Sieve U := Sieve.bind S.arrows fun Y f hf => G.sieveOfSection ↑(x f hf)<VAR>W : (V : C) → (i : V ⟶ U) → S'.arrows i → C<VAR>i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi<VAR>i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U<VAR>hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)<VAR>h₁ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), F.map (i₁ V i hi).op ↑(x (i₂ V i hi) ⋯) ∈ G.obj (op V)<VAR>h₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), i₁ V i hi ≫ i₂ V i hi = i<VAR>x'' : Presieve.FamilyOfElements F S'.arrows := fun V i hi => F.map (i₁ V i hi).op ↑(x (i₂ V i hi) ⋯)<VAR>H : ∀ (s : (sheafify J G).toPresheaf.obj (op U)), x.IsAmalgamation s ↔ x''.IsAmalgamation ↑s<VAR>this : x''.Compatible<GOAL>∃! t, x.IsAmalgamation t
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>F F' F'' : Cᵒᵖ ⥤ Type w<VAR>G G' : Subpresheaf F<VAR>hF : Presieve.IsSheaf J F<VAR>U : C<VAR>S : Sieve U<VAR>hS : S ∈ J.sieves U<VAR>x : Presieve.FamilyOfElements (sheafify J G).toPresheaf S.arrows<VAR>hx : x.Compatible<VAR>S' : Sieve U := Sieve.bind S.arrows fun Y f hf => G.sieveOfSection ↑(x f hf)<VAR>W : (V : C) → (i : V ⟶ U) → S'.arrows i → C<VAR>i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi<VAR>i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U<VAR>hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)<VAR>h₁ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), F.map (i₁ V i hi).op ↑(x (i₂ V i hi) ⋯) ∈ G.obj (op V)<VAR>h₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), i₁ V i hi ≫ i₂ V i hi = i<VAR>x'' : Presieve.FamilyOfElements F S'.arrows := fun V i hi => F.map (i₁ V i hi).op ↑(x (i₂ V i hi) ⋯)<VAR>H : ∀ (s : (sheafify J G).toPresheaf.obj (op U)), x.IsAmalgamation s ↔ x''.IsAmalgamation ↑s<VAR>this : x''.Compatible<VAR>t : F.obj (op U)<VAR>ht : x''.IsAmalgamation t<VAR>ht' : ∀ (y : F.obj (op U)), (fun t => x''.IsAmalgamation t) y → y = t<GOAL>∃! t, x.IsAmalgamation t
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>F F' F'' : Cᵒᵖ ⥤ Type w<VAR>G G' : Subpresheaf F<VAR>hF : Presieve.IsSheaf J F<VAR>U : C<VAR>S : Sieve U<VAR>hS : S ∈ J.sieves U<VAR>x : Presieve.FamilyOfElements (sheafify J G).toPresheaf S.arrows<VAR>hx : x.Compatible<VAR>S' : Sieve U := Sieve.bind S.arrows fun Y f hf => G.sieveOfSection ↑(x f hf)<VAR>W : (V : C) → (i : V ⟶ U) → S'.arrows i → C<VAR>i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi<VAR>i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U<VAR>hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)<VAR>h₁ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), F.map (i₁ V i hi).op ↑(x (i₂ V i hi) ⋯) ∈ G.obj (op V)<VAR>h₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), i₁ V i hi ≫ i₂ V i hi = i<VAR>x'' : Presieve.FamilyOfElements F S'.arrows := fun V i hi => F.map (i₁ V i hi).op ↑(x (i₂ V i hi) ⋯)<VAR>H : ∀ (s : (sheafify J G).toPresheaf.obj (op U)), x.IsAmalgamation s ↔ x''.IsAmalgamation ↑s<VAR>this : x''.Compatible<VAR>t : F.obj (op U)<VAR>ht : x''.IsAmalgamation t<VAR>ht' : ∀ (y : F.obj (op U)), (fun t => x''.IsAmalgamation t) y → y = t<GOAL>t ∈ (sheafify J G).obj (op U)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>F F' F'' : Cᵒᵖ ⥤ Type w<VAR>G G' : Subpresheaf F<VAR>hF : Presieve.IsSheaf J F<VAR>U : C<VAR>S : Sieve U<VAR>hS : S ∈ J.sieves U<VAR>x : Presieve.FamilyOfElements (sheafify J G).toPresheaf S.arrows<VAR>hx : x.Compatible<VAR>S' : Sieve U := Sieve.bind S.arrows fun Y f hf => G.sieveOfSection ↑(x f hf)<VAR>W : (V : C) → (i : V ⟶ U) → S'.arrows i → C<VAR>i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi<VAR>i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U<VAR>hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)<VAR>h₁ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), F.map (i₁ V i hi).op ↑(x (i₂ V i hi) ⋯) ∈ G.obj (op V)<VAR>h₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), i₁ V i hi ≫ i₂ V i hi = i<VAR>x'' : Presieve.FamilyOfElements F S'.arrows := fun V i hi => F.map (i₁ V i hi).op ↑(x (i₂ V i hi) ⋯)<VAR>H : ∀ (s : (sheafify J G).toPresheaf.obj (op U)), x.IsAmalgamation s ↔ x''.IsAmalgamation ↑s<VAR>this : x''.Compatible<VAR>t : F.obj (op U)<VAR>ht : x''.IsAmalgamation t<VAR>ht' : ∀ (y : F.obj (op U)), (fun t => x''.IsAmalgamation t) y → y = t<GOAL>(Sieve.bind S.arrows fun V i hi => G.sieveOfSection ↑(x i hi)) ≤ G.sieveOfSection t
<VAR>n : ℕ<GOAL>0 ≤ Λ n
<VAR>n : ℕ<GOAL>0 ≤ if IsPrimePow n then Real.log ↑n.minFac else 0
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>f : Filter β<VAR>u : β → α<VAR>a : α<GOAL>Tendsto u f (𝓝 a) ↔ Tendsto (fun x => (u x, a)) f (𝓤 α)
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>f : Filter β<VAR>u : β → α<VAR>a : α<GOAL>Tendsto ((fun y => (y, a)) ∘ u) f (𝓤 α) ↔ Tendsto (fun x => (u x, a)) f (𝓤 α)
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>E : EllipticCurve R<VAR>A : Type v<VAR>inst✝ : CommRing A<VAR>φ✝ φ : R →+* A<VAR>hφ : Function.Injective ⇑φ<VAR>x✝¹ x✝ : EllipticCurve R<VAR>h : (fun E => E.map φ) x✝¹ = (fun E => E.map φ) x✝<VAR>h1 : x✝¹.map φ = x✝.map φ<VAR>h2 : (Units.map ↑φ) x✝¹.Δ' = (Units.map ↑φ) x✝.Δ'<GOAL>x✝¹ = x✝
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>E : EllipticCurve R<VAR>A : Type v<VAR>inst✝ : CommRing A<VAR>φ✝ φ : R →+* A<VAR>hφ : Function.Injective ⇑φ<VAR>x✝¹ x✝ : EllipticCurve R<VAR>h : (fun E => E.map φ) x✝¹ = (fun E => E.map φ) x✝<VAR>h1 : x✝¹.map φ = x✝.map φ<VAR>h2 : ↑φ ↑x✝¹.Δ' = ↑φ ↑x✝.Δ'<GOAL>x✝¹ = x✝
<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✝⁵ : AddCommGroup E<VAR>inst✝⁴ : AddCommGroup F<VAR>inst✝³ : (i : ι) → AddCommGroup (π i)<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Module 𝕜 F<VAR>inst✝ : (i : ι) → Module 𝕜 (π i)<VAR>A B : Set E<VAR>x✝ : E<VAR>s : (i : ι) → Set (π i)<VAR>x : (i : ι) → π i<GOAL>x ∈ extremePoints 𝕜 (univ.pi s) ↔ x ∈ univ.pi fun i => extremePoints 𝕜 (s i)
<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✝⁵ : AddCommGroup E<VAR>inst✝⁴ : AddCommGroup F<VAR>inst✝³ : (i : ι) → AddCommGroup (π i)<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Module 𝕜 F<VAR>inst✝ : (i : ι) → Module 𝕜 (π i)<VAR>A B : Set E<VAR>x✝ : E<VAR>s : (i : ι) → Set (π i)<VAR>x : (i : ι) → π i<GOAL>((∀ (i : ι), x i ∈ s i) ∧ ∀ (x₁ : (i : ι) → π i), (∀ (i : ι), x₁ i ∈ s i) → ∀ (x₂ : (i : ι) → π i), (∀ (i : ι), x₂ i ∈ s i) → x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x ∧ x₂ = x) ↔ (∀ (i : ι), x i ∈ s i) ∧ ∀ (x_1 : ι), ∀ x₁ ∈ s x_1, ∀ x₂ ∈ s x_1, x x_1 ∈ openSegment 𝕜 x₁ x₂ → x₁ = x x_1 ∧ x₂ = x x_1
<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✝⁵ : AddCommGroup E<VAR>inst✝⁴ : AddCommGroup F<VAR>inst✝³ : (i : ι) → AddCommGroup (π i)<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Module 𝕜 F<VAR>inst✝ : (i : ι) → Module 𝕜 (π i)<VAR>A B : Set E<VAR>x✝ : E<VAR>s : (i : ι) → Set (π i)<VAR>x : (i : ι) → π i<VAR>hx : ∀ (i : ι), x i ∈ s i<VAR>h : ∀ (x₁ : (i : ι) → π i), (∀ (i : ι), x₁ i ∈ s i) → ∀ (x₂ : (i : ι) → π i), (∀ (i : ι), x₂ i ∈ s i) → x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x ∧ x₂ = x<VAR>i : ι<GOAL>∀ x₁ ∈ s i, ∀ x₂ ∈ s i, x i ∈ openSegment 𝕜 x₁ x₂ → x₁ = x i ∧ x₂ = x i
<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✝⁵ : AddCommGroup E<VAR>inst✝⁴ : AddCommGroup F<VAR>inst✝³ : (i : ι) → AddCommGroup (π i)<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Module 𝕜 F<VAR>inst✝ : (i : ι) → Module 𝕜 (π i)<VAR>A B : Set E<VAR>x✝ : E<VAR>s : (i : ι) → Set (π i)<VAR>x : (i : ι) → π i<VAR>hx : ∀ (i : ι), x i ∈ s i<VAR>h : ∀ (x_1 : ι), ∀ x₁ ∈ s x_1, ∀ x₂ ∈ s x_1, x x_1 ∈ openSegment 𝕜 x₁ x₂ → x₁ = x x_1 ∧ x₂ = x x_1<GOAL>∀ (x₁ : (i : ι) → π i), (∀ (i : ι), x₁ i ∈ s i) → ∀ (x₂ : (i : ι) → π i), (∀ (i : ι), x₂ i ∈ s i) → x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x ∧ x₂ = x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁵ : NormedDivisionRing 𝕜<VAR>inst✝⁴ : SeminormedAddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : BoundedSMul 𝕜 E<VAR>P : Type u_3<VAR>inst✝¹ : PseudoMetricSpace P<VAR>inst✝ : NormedAddTorsor E P<VAR>c : P<VAR>k : 𝕜<VAR>hk : k ≠ 0<VAR>x y : E<VAR>h : dist x y ≠ 0<GOAL>dist ((smulTorsor c hk) x) ((smulTorsor c hk) y) = ↑‖k‖₊ * dist x y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : PredOrder α<VAR>a b : α<VAR>h : pred a ≤ b<GOAL>Icc (pred a) b = insert (pred a) (Icc a b)
<VAR>ι✝ : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι✝ → M<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>a b : R<VAR>x y : M<VAR>ι : Type u_8<VAR>s : Set ι<VAR>f : ι → M<VAR>hs : LinearIndependent R fun (x : ↑s) => f ↑x<GOAL>LinearIndependent R fun (x : ↑(f '' s)) => ↑x
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>D : Type u_3<VAR>inst✝⁷ : Category.{?u.35500, u_1} C₁<VAR>inst✝⁶ : Category.{?u.35504, u_2} C₂<VAR>inst✝⁵ : Category.{?u.35508, u_3} D<VAR>inst✝⁴ : HasZeroMorphisms C₁<VAR>inst✝³ : HasZeroMorphisms C₂<VAR>inst✝² : HasZeroMorphisms D<VAR>F : C₁ ⥤ C₂ ⥤ D<VAR>I₁ : Type u_4<VAR>I₂ : Type u_5<VAR>J : Type u_6<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>inst✝¹ : F.PreservesZeroMorphisms<VAR>inst✝ : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms<VAR>K₁ K₁' : HomologicalComplex C₁ c₁<VAR>f : K₁ ⟶ K₁'<VAR>K₂ : HomologicalComplex C₂ c₂<VAR>i₁✝ i₁'✝ : I₁<VAR>i₂✝ : I₂<VAR>a✝ : c₁.Rel i₁✝ i₁'✝<GOAL>(F.map (f.f i₁✝)).app (K₂.X i₂✝) ≫ (F.map (K₁'.d i₁✝ i₁'✝)).app (K₂.X i₂✝) = (F.map (K₁.d i₁✝ i₁'✝)).app (K₂.X i₂✝) ≫ (F.map (f.f i₁'✝)).app (K₂.X i₂✝)
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>v : PicardLindelof E<VAR>inst✝ : CompleteSpace E<GOAL>∃ f, f ↑v.t₀ = v.x₀ ∧ ∀ t ∈ Icc v.tMin v.tMax, HasDerivWithinAt f (v.toFun t (f t)) (Icc v.tMin v.tMax) t
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>v : PicardLindelof E<VAR>inst✝ : CompleteSpace E<VAR>f : v.FunSpace<VAR>hf : f.next = f<GOAL>∃ f, f ↑v.t₀ = v.x₀ ∧ ∀ t ∈ Icc v.tMin v.tMax, HasDerivWithinAt f (v.toFun t (f t)) (Icc v.tMin v.tMax) t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : Preorder α<VAR>inst✝⁴ : Preorder β<VAR>inst✝³ : OrderTop α<VAR>inst✝² : OrderBot β<VAR>inst✝¹ : LocallyFiniteOrder α<VAR>inst✝ : LocallyFiniteOrder β<VAR>a a₁ a₂ : α<VAR>b b₁ b₂ : β<GOAL>Icc (inrₗ b₁) (inrₗ b₂) = map (Embedding.inr.trans toLex.toEmbedding) (Icc b₁ b₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : Preorder α<VAR>inst✝⁴ : Preorder β<VAR>inst✝³ : OrderTop α<VAR>inst✝² : OrderBot β<VAR>inst✝¹ : LocallyFiniteOrder α<VAR>inst✝ : LocallyFiniteOrder β<VAR>a a₁ a₂ : α<VAR>b b₁ b₂ : β<GOAL>Icc (inrₗ b₁) (inrₗ b₂) = map toLex.toEmbedding (map Embedding.inr (Icc b₁ b₂))
<VAR>K R : Type u<VAR>V✝ V₁ V₂ V₃ : Type v<VAR>V' V'₁ : Type v'<VAR>V'' : Type v''<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝² : DivisionRing K<VAR>V : Type v<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>h : ℵ₀ ≤ Module.rank K V<GOAL>lift.{u, v} (Module.rank K V) < Module.rank Kᵐᵒᵖ (V →ₗ[K] K)
<VAR>K R : Type u<VAR>V✝ V₁ V₂ V₃ : Type v<VAR>V' V'₁ : Type v'<VAR>V'' : Type v''<VAR>ι✝ : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝² : DivisionRing K<VAR>V : Type v<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>h : ℵ₀ ≤ Module.rank K V<VAR>ι : Type v<VAR>b : Basis ι K V<GOAL>lift.{u, v} (Module.rank K V) < Module.rank Kᵐᵒᵖ (V →ₗ[K] K)
<VAR>K R : Type u<VAR>V✝ V₁ V₂ V₃ : Type v<VAR>V' V'₁ : Type v'<VAR>V'' : Type v''<VAR>ι✝ : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝² : DivisionRing K<VAR>V : Type v<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>h : ℵ₀ ≤ Module.rank K V<VAR>ι : Type v<VAR>b : Basis ι K V<GOAL>lift.{u, v} #ι < lift.{v, u} #K ^ lift.{u, v} #ι
<VAR>K R : Type u<VAR>V✝ V₁ V₂ V₃ : Type v<VAR>V' V'₁ : Type v'<VAR>V'' : Type v''<VAR>ι✝ : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝² : DivisionRing K<VAR>V : Type v<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>h : ℵ₀ ≤ Module.rank K V<VAR>ι : Type v<VAR>b : Basis ι K V<GOAL>1 < lift.{v, u} #K
<VAR>K R : Type u<VAR>V✝ V₁ V₂ V₃ : Type v<VAR>V' V'₁ : Type v'<VAR>V'' : Type v''<VAR>ι✝ : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝² : DivisionRing K<VAR>V : Type v<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>h : ℵ₀ ≤ Module.rank K V<VAR>ι : Type v<VAR>b : Basis ι K V<GOAL>Nontrivial K
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>x y z : X<VAR>ι : Type u_3<VAR>γ✝ : Path x y<VAR>a b : X<VAR>γ : Path a b<VAR>t : ℝ<GOAL>γ.extend (min t t) = γ.extend t
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>x✝ y z : X<VAR>ι : Type u_3<VAR>γ✝ : Path x✝ y<VAR>a b : X<VAR>γ : Path a b<VAR>t : ℝ<VAR>x : ↑I<GOAL>(γ.truncate t t) x = ((refl (γ.extend t)).cast ⋯ ⋯) x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>x✝ y z : X<VAR>ι : Type u_3<VAR>γ✝ : Path x✝ y<VAR>a b : X<VAR>γ : Path a b<VAR>t : ℝ<VAR>x : ↑I<GOAL>(γ.truncate t t) x = (refl (γ.extend t)) x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>x✝ y z : X<VAR>ι : Type u_3<VAR>γ✝ : Path x✝ y<VAR>a b : X<VAR>γ : Path a b<VAR>t : ℝ<VAR>x : ↑I<GOAL>γ.extend (if (if ↑x ≤ t then t else ↑x) ≤ t then if ↑x ≤ t then t else ↑x else t) = γ.extend t
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x✝ y✝ x y : V<GOAL>angle x y = π / 2 ↔ ⟪x, y⟫_ℝ = 0
<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 (⋃ i ∈ s, f i)
<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.sup f)
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : ConcreteCategory C<VAR>inst✝² : HasLimits C<VAR>inst✝¹ : ConcreteCategory.forget.ReflectsIsomorphisms<VAR>inst✝ : PreservesLimits ConcreteCategory.forget<VAR>X : TopCat<VAR>F : Sheaf C X<VAR>ι : Type v<VAR>U : ι → Opens ↑X<VAR>V : Opens ↑X<VAR>iUV : (i : ι) → U i ⟶ V<VAR>hcover : V ≤ iSup U<VAR>s t : (CategoryTheory.forget C).obj (F.val.obj (op V))<VAR>h : ∀ (i : ι), (F.val.map (iUV i).op) s = (F.val.map (iUV i).op) t<GOAL>s = t
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : ConcreteCategory C<VAR>inst✝² : HasLimits C<VAR>inst✝¹ : ConcreteCategory.forget.ReflectsIsomorphisms<VAR>inst✝ : PreservesLimits ConcreteCategory.forget<VAR>X : TopCat<VAR>F : Sheaf C X<VAR>ι : Type v<VAR>U : ι → Opens ↑X<VAR>V : Opens ↑X<VAR>iUV : (i : ι) → U i ⟶ V<VAR>hcover : V ≤ iSup U<VAR>s t : (CategoryTheory.forget C).obj (F.val.obj (op V))<VAR>h : ∀ (i : ι), (F.val.map (iUV i).op) s = (F.val.map (iUV i).op) t<VAR>V_eq_supr_U : V = iSup U<GOAL>s = t
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : ConcreteCategory C<VAR>inst✝² : HasLimits C<VAR>inst✝¹ : ConcreteCategory.forget.ReflectsIsomorphisms<VAR>inst✝ : PreservesLimits ConcreteCategory.forget<VAR>X : TopCat<VAR>F : Sheaf C X<VAR>ι : Type v<VAR>U : ι → Opens ↑X<VAR>V : Opens ↑X<VAR>iUV : (i : ι) → U i ⟶ V<VAR>hcover : V ≤ iSup U<VAR>s t : (CategoryTheory.forget C).obj (F.val.obj (op V))<VAR>h : ∀ (i : ι), (F.val.map (iUV i).op) s = (F.val.map (iUV i).op) t<VAR>V_eq_supr_U : V = iSup U<GOAL>(F.val.map (eqToHom ⋯).op) s = (F.val.map (eqToHom ⋯).op) t
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : ConcreteCategory C<VAR>inst✝² : HasLimits C<VAR>inst✝¹ : ConcreteCategory.forget.ReflectsIsomorphisms<VAR>inst✝ : PreservesLimits ConcreteCategory.forget<VAR>X : TopCat<VAR>F : Sheaf C X<VAR>ι : Type v<VAR>U : ι → Opens ↑X<VAR>V : Opens ↑X<VAR>iUV : (i : ι) → U i ⟶ V<VAR>hcover : V ≤ iSup U<VAR>s t : (CategoryTheory.forget C).obj (F.val.obj (op V))<VAR>h : ∀ (i : ι), (F.val.map (iUV i).op) s = (F.val.map (iUV i).op) t<VAR>V_eq_supr_U : V = iSup U<GOAL>∀ (i : ι), (F.val.map (leSupr U i).op) ((F.val.map (eqToHom ⋯).op) s) = (F.val.map (leSupr U i).op) ((F.val.map (eqToHom ⋯).op) t)
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : ConcreteCategory C<VAR>inst✝² : HasLimits C<VAR>inst✝¹ : ConcreteCategory.forget.ReflectsIsomorphisms<VAR>inst✝ : PreservesLimits ConcreteCategory.forget<VAR>X : TopCat<VAR>F : Sheaf C X<VAR>ι : Type v<VAR>U : ι → Opens ↑X<VAR>V : Opens ↑X<VAR>iUV : (i : ι) → U i ⟶ V<VAR>hcover : V ≤ iSup U<VAR>s t : (CategoryTheory.forget C).obj (F.val.obj (op V))<VAR>h : ∀ (i : ι), (F.val.map (iUV i).op) s = (F.val.map (iUV i).op) t<VAR>V_eq_supr_U : V = iSup U<VAR>i : ι<GOAL>(F.val.map (leSupr U i).op) ((F.val.map (eqToHom ⋯).op) s) = (F.val.map (leSupr U i).op) ((F.val.map (eqToHom ⋯).op) t)
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : ConcreteCategory C<VAR>inst✝² : HasLimits C<VAR>inst✝¹ : ConcreteCategory.forget.ReflectsIsomorphisms<VAR>inst✝ : PreservesLimits ConcreteCategory.forget<VAR>X : TopCat<VAR>F : Sheaf C X<VAR>ι : Type v<VAR>U : ι → Opens ↑X<VAR>V : Opens ↑X<VAR>iUV : (i : ι) → U i ⟶ V<VAR>hcover : V ≤ iSup U<VAR>s t : (CategoryTheory.forget C).obj (F.val.obj (op V))<VAR>h : ∀ (i : ι), (F.val.map (iUV i).op) s = (F.val.map (iUV i).op) t<VAR>V_eq_supr_U : V = iSup U<VAR>i : ι<GOAL>(F.val.map ((eqToHom ⋯).op ≫ (leSupr U i).op)) s = (F.val.map ((eqToHom ⋯).op ≫ (leSupr U i).op)) t
<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>H : ∀ N' ≤ N, N'.FG → M.LinearDisjoint N'<VAR>x y : ↥M ⊗[R] ↥N<VAR>hxy : (M.mulMap N) x = (M.mulMap N) y<GOAL>x = y
<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>H : ∀ N' ≤ N, N'.FG → M.LinearDisjoint N'<VAR>x y : ↥M ⊗[R] ↥N<VAR>hxy : (M.mulMap N) x = (M.mulMap N) y<VAR>N' : Submodule R S<VAR>hN : N' ≤ N<VAR>hFG : Module.Finite R ↥N'<VAR>h : {x, y} ⊆ ↑(LinearMap.range (LinearMap.lTensor (↥M) (inclusion hN)))<GOAL>x = y
<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>H : ∀ N' ≤ N, N'.FG → M.LinearDisjoint N'<VAR>x y : ↥M ⊗[R] ↥N<VAR>hxy : (M.mulMap N) x = (M.mulMap N) y<VAR>N' : Submodule R S<VAR>hN : N' ≤ N<VAR>hFG : N'.FG<VAR>h : {x, y} ⊆ ↑(LinearMap.range (LinearMap.lTensor (↥M) (inclusion hN)))<GOAL>x = y
<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>H : ∀ N' ≤ N, N'.FG → M.LinearDisjoint N'<VAR>x y : ↥M ⊗[R] ↥N<VAR>hxy : (M.mulMap N) x = (M.mulMap N) y<VAR>N' : Submodule R S<VAR>hN : N' ≤ N<VAR>hFG : N'.FG<VAR>h : {x, y} ⊆ ↑(LinearMap.range (LinearMap.lTensor (↥M) (inclusion hN)))<VAR>x' : ↥M ⊗[R] ↥N'<VAR>hx' : (LinearMap.lTensor (↥M) (inclusion hN)) x' = x<VAR>y' : ↥M ⊗[R] ↥N'<VAR>hy' : (LinearMap.lTensor (↥M) (inclusion hN)) y' = y<GOAL>x' = y'
<VAR>l m r : List Char<VAR>x✝ : Substring<VAR>h : ValidFor l m r x✝<GOAL>x✝.isEmpty = true ↔ m = []
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X✝ : Ω → ℝ<VAR>μ✝ : Measure Ω<VAR>A : Type u_2<VAR>inst✝¹ : CommSemiring A<VAR>inst✝ : Algebra A ℝ<VAR>c : A<VAR>X : Ω → ℝ<VAR>μ : Measure Ω<GOAL>variance (c • X) μ = c ^ 2 • variance X μ
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X✝ : Ω → ℝ<VAR>μ✝ : Measure Ω<VAR>A : Type u_2<VAR>inst✝¹ : CommSemiring A<VAR>inst✝ : Algebra A ℝ<VAR>c : A<VAR>X : Ω → ℝ<VAR>μ : Measure Ω<GOAL>variance (c • X) μ = variance ((algebraMap A ℝ) c • X) μ
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X✝ : Ω → ℝ<VAR>μ✝ : Measure Ω<VAR>A : Type u_2<VAR>inst✝¹ : CommSemiring A<VAR>inst✝ : Algebra A ℝ<VAR>c : A<VAR>X : Ω → ℝ<VAR>μ : Measure Ω<GOAL>c ^ 2 • variance X μ = (algebraMap A ℝ) c ^ 2 * variance X μ
<VAR>n✝ p q m n : ℕ<VAR>hp : Prime p<VAR>hq : Prime q<VAR>h : p ^ (m + 1) = q ^ (n + 1)<GOAL>p = q ∧ m = n
<VAR>n✝ p q m n : ℕ<VAR>hp : Prime p<VAR>hq : Prime q<VAR>h : p ^ (m + 1) = q ^ (n + 1)<VAR>H : p = q<GOAL>p = q ∧ m = n
<VAR>F : Type u_1<VAR>α✝ : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝⁴ : LinearOrder α✝<VAR>inst✝³ : OrderBot α✝<VAR>s✝ : Finset ι<VAR>f✝ : ι → α✝<VAR>a : α✝<VAR>α : Type u_7<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : BoundedOrder α<VAR>inst✝ : Nontrivial α<VAR>s : Finset ι<VAR>f : ι → α<GOAL>s.sup f = ⊤ ↔ ∃ b ∈ s, f b = ⊤