ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>inst✝¹¹ : CompleteSpace 𝕜<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : MeasurableSpace E<VAR>inst✝⁸ : BorelSpace E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : MeasurableSpace F<VAR>inst✝⁴ : BorelSpace F<VAR>inst✝³ : NormedSpace 𝕜 F<VAR>L : E →ₗ[𝕜] F<VAR>μ : Measure E<VAR>ν : Measure F<VAR>inst✝² : μ.IsAddHaarMeasure<VAR>inst✝¹ : ν.IsAddHaarMeasure<VAR>inst✝ : LocallyCompactSpace E<VAR>h : Function.Surjective ⇑L<VAR>this✝¹ : ProperSpace E<VAR>this✝ : FiniteDimensional 𝕜 E<VAR>this : ProperSpace F<VAR>S : Submodule 𝕜 E := ker L<VAR>T : Submodule 𝕜 E<VAR>hT : IsCompl S T<VAR>M : (↥S × ↥T) ≃ₗ[𝕜] E := S.prodEquivOfIsCompl T hT<VAR>M_cont : Continuous ⇑M.symm<VAR>P : ↥S × ↥T →ₗ[𝕜] ↥T := snd 𝕜 ↥S ↥T<VAR>P_cont : Continuous ⇑P<VAR>I✝ : Function.Bijective ⇑(L.domRestrict T)<VAR>L' : ↥T ≃ₗ[𝕜] F := LinearEquiv.ofBijective (L.domRestrict T) I✝<VAR>L'_cont : Continuous ⇑L'<VAR>A : L = ↑L' ∘ₗ P ∘ₗ ↑M.symm<VAR>I : map (⇑L) μ = map (⇑L') (map (⇑P) (map (⇑M.symm) μ))<VAR>μS : Measure ↥S := addHaar<VAR>μT : Measure ↥T := addHaar<VAR>c₀ : ℝ≥0∞<VAR>c₀_pos : c₀ ≠ 0<VAR>c₀_fin : c₀ ≠ ⊤<VAR>h₀ : map (⇑M.symm) μ = c₀ • μS.prod μT<VAR>J : map (⇑P) (μS.prod μT) = μS univ • μT<VAR>c₁ : ℝ≥0∞<VAR>c₁_pos : c₁ ≠ 0<VAR>c₁_fin : c₁ ≠ ⊤<VAR>h₁ : map (⇑L') μT = c₁ • ν<GOAL>map (⇑L) μ = (c₀ * c₁ * addHaar univ) • ν
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>inst✝¹¹ : CompleteSpace 𝕜<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : MeasurableSpace E<VAR>inst✝⁸ : BorelSpace E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : MeasurableSpace F<VAR>inst✝⁴ : BorelSpace F<VAR>inst✝³ : NormedSpace 𝕜 F<VAR>L : E →ₗ[𝕜] F<VAR>μ : Measure E<VAR>ν : Measure F<VAR>inst✝² : μ.IsAddHaarMeasure<VAR>inst✝¹ : ν.IsAddHaarMeasure<VAR>inst✝ : LocallyCompactSpace E<VAR>h : Function.Surjective ⇑L<VAR>this✝¹ : ProperSpace E<VAR>this✝ : FiniteDimensional 𝕜 E<VAR>this : ProperSpace F<VAR>S : Submodule 𝕜 E := ker L<VAR>T : Submodule 𝕜 E<VAR>hT : IsCompl S T<VAR>M : (↥S × ↥T) ≃ₗ[𝕜] E := S.prodEquivOfIsCompl T hT<VAR>M_cont : Continuous ⇑M.symm<VAR>P : ↥S × ↥T →ₗ[𝕜] ↥T := snd 𝕜 ↥S ↥T<VAR>P_cont : Continuous ⇑P<VAR>I✝ : Function.Bijective ⇑(L.domRestrict T)<VAR>L' : ↥T ≃ₗ[𝕜] F := LinearEquiv.ofBijective (L.domRestrict T) I✝<VAR>L'_cont : Continuous ⇑L'<VAR>A : L = ↑L' ∘ₗ P ∘ₗ ↑M.symm<VAR>I : map (⇑L) μ = map (⇑L') (map (⇑P) (map (⇑M.symm) μ))<VAR>μS : Measure ↥S := addHaar<VAR>μT : Measure ↥T := addHaar<VAR>c₀ : ℝ≥0∞<VAR>c₀_pos : c₀ ≠ 0<VAR>c₀_fin : c₀ ≠ ⊤<VAR>h₀ : map (⇑M.symm) μ = c₀ • μS.prod μT<VAR>J : map (⇑P) (μS.prod μT) = μS univ • μT<VAR>c₁ : ℝ≥0∞<VAR>c₁_pos : c₁ ≠ 0<VAR>c₁_fin : c₁ ≠ ⊤<VAR>h₁ : map (⇑L') μT = c₁ • ν<GOAL>(c₀ * μS univ * c₁) • ν = (c₀ * c₁ * addHaar univ) • ν
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>E : Type u_3<VAR>E' : Type u_4<VAR>F : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁴ : SeminormedRing 𝕜<VAR>inst✝³ : AddZeroClass E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : ContinuousAdd E<VAR>inst✝ : DistribSMul 𝕜 E<VAR>s t : Set E<VAR>hs : IsVonNBounded 𝕜 s<VAR>ht : IsVonNBounded 𝕜 t<VAR>U : Set E<VAR>hU : U ∈ 𝓝 0<GOAL>Absorbs 𝕜 U (s + t)
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>E : Type u_3<VAR>E' : Type u_4<VAR>F : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁴ : SeminormedRing 𝕜<VAR>inst✝³ : AddZeroClass E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : ContinuousAdd E<VAR>inst✝ : DistribSMul 𝕜 E<VAR>s t : Set E<VAR>hs : IsVonNBounded 𝕜 s<VAR>ht : IsVonNBounded 𝕜 t<VAR>U : Set E<VAR>hU : U ∈ 𝓝 0<VAR>V : Set E<VAR>hVo : IsOpen V<VAR>hV : 0 ∈ V<VAR>hVU : V + V ⊆ U<GOAL>Absorbs 𝕜 U (s + t)
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝² : Category.{v', u'} D<VAR>inst✝¹ : HasZeroObject C<VAR>inst✝ : HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>i : Y ≅ 0<GOAL>f = 0
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝² : Category.{v', u'} D<VAR>inst✝¹ : HasZeroObject C<VAR>inst✝ : HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>i : Y ≅ 0<VAR>h : f = f ≫ i.hom ≫ 𝟙 0 ≫ i.inv<GOAL>f = 0
<VAR>u v m n : ℤ<GOAL>¬Even 1
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<GOAL>IsFiltered C ↔ ∀ {J : Type v} [inst : SmallCategory J] [inst_1 : FinCategory J] (F : J ⥤ C), ∃ X, Nonempty (limit (F.op ⋙ yoneda.obj X))
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<GOAL>(∀ {J : Type v} [inst : SmallCategory J] [inst_1 : FinCategory J] (F : J ⥤ C), Nonempty (Cocone F)) ↔ ∀ {J : Type v} [inst : SmallCategory J] [inst_1 : FinCategory J] (F : J ⥤ C), ∃ X, Nonempty (limit (F.op ⋙ yoneda.obj 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>s : Set X<VAR>hs : s ⊆ e.source<GOAL>IsOpen (↑e '' s) ↔ IsOpen s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>p✝ : FormalMultilinearSeries 𝕜 E F<VAR>r : ℝ≥0<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>hx : x ∈ EMetric.ball 0 p.radius<GOAL>Summable fun n => ‖(p n) fun x_1 => x‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>p✝ : FormalMultilinearSeries 𝕜 E F<VAR>r : ℝ≥0<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>hx : ↑‖x‖₊ < p.radius<GOAL>Summable fun n => ‖(p n) fun x_1 => x‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>p✝ : FormalMultilinearSeries 𝕜 E F<VAR>r : ℝ≥0<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>hx : ↑‖x‖₊ < p.radius<VAR>n : ℕ<GOAL>‖p n‖ * ∏ i : Fin n, ‖x‖ = ‖p n‖ * ↑‖x‖₊ ^ n
<VAR>Γ : Type u_1<VAR>inst✝ : Inhabited Γ<VAR>T : Tape Γ<VAR>n : ℕ<GOAL>T.right₀.nth n = T.nth ↑n
<VAR>E : ℕ → Type u_1<VAR>inst✝¹ : (n : ℕ) → TopologicalSpace (E n)<VAR>inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)<VAR>s : Set ((n : ℕ) → E n)<VAR>hs : IsClosed s<VAR>hne : s.Nonempty<GOAL>∃ f, (∀ (x : ↑s), f ↑x = x) ∧ Surjective f ∧ Continuous f
<VAR>E : ℕ → Type u_1<VAR>inst✝¹ : (n : ℕ) → TopologicalSpace (E n)<VAR>inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)<VAR>f : ((n : ℕ) → E n) → (n : ℕ) → E n<VAR>f_cont : Continuous f<VAR>hs : IsClosed (range f)<VAR>hne : (range f).Nonempty<VAR>fs : ∀ x ∈ range f, f x = x<GOAL>∃ f_1, (∀ (x : ↑(range f)), f_1 ↑x = x) ∧ Surjective f_1 ∧ Continuous f_1
<VAR>E : ℕ → Type u_1<VAR>inst✝¹ : (n : ℕ) → TopologicalSpace (E n)<VAR>inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)<VAR>f : ((n : ℕ) → E n) → (n : ℕ) → E n<VAR>f_cont : Continuous f<VAR>hs : IsClosed (range f)<VAR>hne : (range f).Nonempty<VAR>fs : ∀ x ∈ range f, f x = x<VAR>A : ∀ (x : ↑(range f)), rangeFactorization f ↑x = x<GOAL>∃ f_1, (∀ (x : ↑(range f)), f_1 ↑x = x) ∧ Surjective f_1 ∧ Continuous f_1
<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 : a ∈ upperClosure ↑s<VAR>ht : a ∉ upperClosure ↑t<GOAL>(s ∪ t).truncatedInf 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 : a ∈ upperClosure ↑s<VAR>ht : ∀ x ∈ t, ¬x ≤ a<GOAL>(s ∪ t).truncatedInf a = s.truncatedInf a
<VAR>𝕜 : Type u<VAR>A : Type v<VAR>inst✝³ : Field 𝕜<VAR>inst✝² : Ring A<VAR>inst✝¹ : Algebra 𝕜 A<VAR>inst✝ : IsAlgClosed 𝕜<VAR>a : A<VAR>n : ℕ<VAR>hn : 0 < n<GOAL>σ (a ^ n) = (fun x => x ^ n) '' σ a
<VAR>E : Type u_1<VAR>inst✝ : SeminormedCommGroup E<VAR>ε δ : ℝ<VAR>s t : Set E<VAR>x y : E<GOAL>{x} * ball y δ = ball (x * y) δ
<VAR>α : Type u<VAR>β : Type v<VAR>e : α ≃ β<GOAL>toPartENat #α = toPartENat #β
<VAR>A : Type u_1<VAR>inst✝¹ : NonUnitalNonAssocCommRing A<VAR>inst✝ : IsCommJordan A<VAR>a b c : A<GOAL>⁅L a + L b + L c, L (a * a) + L (b * b) + L (c * c) + 2 • L (a * b) + 2 • L (c * a) + 2 • L (b * c)⁆ = ⁅L a, L (a * a)⁆ + ⁅L a, L (b * b)⁆ + ⁅L a, L (c * c)⁆ + ⁅L a, 2 • L (a * b)⁆ + ⁅L a, 2 • L (c * a)⁆ + ⁅L a, 2 • L (b * c)⁆ + (⁅L b, L (a * a)⁆ + ⁅L b, L (b * b)⁆ + ⁅L b, L (c * c)⁆ + ⁅L b, 2 • L (a * b)⁆ + ⁅L b, 2 • L (c * a)⁆ + ⁅L b, 2 • L (b * c)⁆) + (⁅L c, L (a * a)⁆ + ⁅L c, L (b * b)⁆ + ⁅L c, L (c * c)⁆ + ⁅L c, 2 • L (a * b)⁆ + ⁅L c, 2 • L (c * a)⁆ + ⁅L c, 2 • L (b * c)⁆)
<VAR>A : Type u_1<VAR>inst✝¹ : NonUnitalNonAssocCommRing A<VAR>inst✝ : IsCommJordan A<VAR>a b c : A<GOAL>⁅L a, L (a * a) + L (b * b) + L (c * c) + 2 • L (a * b) + 2 • L (c * a) + 2 • L (b * c)⁆ + ⁅L b, L (a * a) + L (b * b) + L (c * c) + 2 • L (a * b) + 2 • L (c * a) + 2 • L (b * c)⁆ + ⁅L c, L (a * a) + L (b * b) + L (c * c) + 2 • L (a * b) + 2 • L (c * a) + 2 • L (b * c)⁆ = ⁅L a, L (a * a)⁆ + ⁅L a, L (b * b)⁆ + ⁅L a, L (c * c)⁆ + ⁅L a, 2 • L (a * b)⁆ + ⁅L a, 2 • L (c * a)⁆ + ⁅L a, 2 • L (b * c)⁆ + (⁅L b, L (a * a)⁆ + ⁅L b, L (b * b)⁆ + ⁅L b, L (c * c)⁆ + ⁅L b, 2 • L (a * b)⁆ + ⁅L b, 2 • L (c * a)⁆ + ⁅L b, 2 • L (b * c)⁆) + (⁅L c, L (a * a)⁆ + ⁅L c, L (b * b)⁆ + ⁅L c, L (c * c)⁆ + ⁅L c, 2 • L (a * b)⁆ + ⁅L c, 2 • L (c * a)⁆ + ⁅L c, 2 • L (b * c)⁆)
<VAR>n : ℕ<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f✝ g : (Fin n → ℂ) → E<VAR>c✝ : Fin n → ℂ<VAR>R✝ : Fin n → ℝ<VAR>f : (Fin 0 → ℂ) → E<VAR>c : Fin 0 → ℂ<VAR>R : Fin 0 → ℝ<GOAL>(∯ (x : Fin 0 → ℂ) in T(c, R), f x) = f c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝ : CompleteLattice α<VAR>f : Filter β<VAR>p q : β → Prop<VAR>u : β → α<VAR>h : ∀ᶠ (x : β) in f, u x ≠ ⊥ → (p x ↔ q x)<GOAL>blimsup u f p = blimsup u f q
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝ : CompleteLattice α<VAR>f : Filter β<VAR>p q : β → Prop<VAR>u : β → α<VAR>h : ∀ᶠ (x : β) in f, u x ≠ ⊥ → (p x ↔ q x)<GOAL>sInf {a | ∀ᶠ (x : β) in f, p x → u x ≤ a} = sInf {a | ∀ᶠ (x : β) in f, q x → u x ≤ a}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝ : CompleteLattice α<VAR>f : Filter β<VAR>p q : β → Prop<VAR>u : β → α<VAR>h : ∀ᶠ (x : β) in f, u x ≠ ⊥ → (p x ↔ q x)<VAR>a : α<GOAL>a ∈ {a | ∀ᶠ (x : β) in f, p x → u x ≤ a} ↔ a ∈ {a | ∀ᶠ (x : β) in f, q x → u x ≤ a}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝ : CompleteLattice α<VAR>f : Filter β<VAR>p q : β → Prop<VAR>u : β → α<VAR>h : ∀ᶠ (x : β) in f, u x ≠ ⊥ → (p x ↔ q x)<VAR>a : α<VAR>b : β<VAR>hb : u b ≠ ⊥ → (p b ↔ q b)<GOAL>p b → u b ≤ a ↔ q b → u b ≤ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝ : CompleteLattice α<VAR>f : Filter β<VAR>p q : β → Prop<VAR>u : β → α<VAR>h : ∀ᶠ (x : β) in f, u x ≠ ⊥ → (p x ↔ q x)<VAR>a : α<VAR>b : β<VAR>hb : u b ≠ ⊥ → (p b ↔ q b)<VAR>hu : u b = ⊥<GOAL>p b → u b ≤ a ↔ q b → u b ≤ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝ : CompleteLattice α<VAR>f : Filter β<VAR>p q : β → Prop<VAR>u : β → α<VAR>h : ∀ᶠ (x : β) in f, u x ≠ ⊥ → (p x ↔ q x)<VAR>a : α<VAR>b : β<VAR>hb : u b ≠ ⊥ → (p b ↔ q b)<VAR>hu : u b ≠ ⊥<GOAL>p b → u b ≤ a ↔ q b → u b ≤ a
<VAR>σ : Type u<VAR>R : Type v<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Nonempty σ<VAR>inst✝ : Nontrivial R<GOAL>max (lift.{v, u} #(σ →₀ ℕ)) (lift.{u, v} #R) = max (max (lift.{u, v} #R) (lift.{v, u} #σ)) ℵ₀
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<GOAL>a / b ≠ 0 ↔ a ≠ 0 ∧ b ≠ ⊤
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>inst✝²¹ : Semiring R₁<VAR>inst✝²⁰ : Semiring R₂<VAR>inst✝¹⁹ : Semiring R₃<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R₁ →+* R₃<VAR>M₁ : Type u_4<VAR>inst✝¹⁸ : TopologicalSpace M₁<VAR>inst✝¹⁷ : AddCommMonoid M₁<VAR>M'₁ : Type u_5<VAR>inst✝¹⁶ : TopologicalSpace M'₁<VAR>inst✝¹⁵ : AddCommMonoid M'₁<VAR>M₂ : Type u_6<VAR>inst✝¹⁴ : TopologicalSpace M₂<VAR>inst✝¹³ : AddCommMonoid M₂<VAR>M₃ : Type u_7<VAR>inst✝¹² : TopologicalSpace M₃<VAR>inst✝¹¹ : AddCommMonoid M₃<VAR>M₄ : Type u_8<VAR>inst✝¹⁰ : TopologicalSpace M₄<VAR>inst✝⁹ : AddCommMonoid M₄<VAR>inst✝⁸ : Module R₁ M₁<VAR>inst✝⁷ : Module R₁ M'₁<VAR>inst✝⁶ : Module R₂ M₂<VAR>inst✝⁵ : Module R₃ M₃<VAR>inst✝⁴ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>F : Type u_9<VAR>inst✝³ : Module R₁ M₂<VAR>inst✝² : TopologicalSpace R₁<VAR>inst✝¹ : ContinuousSMul R₁ M₂<VAR>inst✝ : ContinuousMul R₁<VAR>x : M₂<VAR>c : R₁<GOAL>((smulRight 1 x).comp (smulRight 1 c)) 1 = (smulRight 1 (c • x)) 1
<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✝⁶ : OrderedRing R<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 : P<VAR>f : P →ᵃ[R] P'<VAR>hf : Injective ⇑f<GOAL>Wbtw R (f x) (f y) (f z) ↔ Wbtw R x y z
<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✝⁶ : OrderedRing R<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 : P<VAR>f : P →ᵃ[R] P'<VAR>hf : Injective ⇑f<VAR>h : Wbtw R (f x) (f y) (f z)<GOAL>Wbtw R x y z
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>S : Type u_2<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>I J : Ideal S<VAR>r : S<VAR>hr : r ∈ I<VAR>p : R[X]<VAR>hp : eval₂ f r p ∈ I<GOAL>p.coeff 0 ∈ comap f I
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>S : Type u_2<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>I J : Ideal S<VAR>r : S<VAR>hr : r ∈ I<VAR>p : R[X]<VAR>hp : eval₂ f r p.divX * r + f (p.coeff 0) ∈ I<GOAL>p.coeff 0 ∈ comap f I
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>S : Type u_2<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>I J : Ideal S<VAR>r : S<VAR>hr : r ∈ I<VAR>p : R[X]<VAR>hp : eval₂ f r p.divX * r + f (p.coeff 0) ∈ I<GOAL>eval₂ f r p.divX * r ∈ I
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>s t✝ : Set α<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : Infinite α<VAR>t : Set β<VAR>f : α → β<VAR>hf : ∀ (a : α), f a ∈ t<VAR>ht : t.Finite<GOAL>∃ a b, a < b ∧ f a = f b
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>s t✝ : Set α<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : Infinite α<VAR>t : Set β<VAR>f : α → β<VAR>hf : MapsTo f univ t<VAR>ht : t.Finite<GOAL>∃ a b, a < b ∧ f a = f b
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>s t✝ : Set α<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : Infinite α<VAR>t : Set β<VAR>f : α → β<VAR>hf : MapsTo f univ t<VAR>ht : t.Finite<VAR>a b : α<VAR>h : a < b ∧ f a = f b<GOAL>∃ a b, a < b ∧ f a = f b
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{?u.30268, u_1} C<VAR>inst✝⁴ : Preadditive C<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : HasShift C ℤ<VAR>inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝ : Pretriangulated C<VAR>X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C<VAR>u₁₂ : X₁ ⟶ X₂<VAR>u₂₃ : X₂ ⟶ X₃<VAR>u₁₃ : X₁ ⟶ X₃<VAR>comm : u₁₂ ≫ u₂₃ = u₁₃<VAR>v₁₂ : X₂ ⟶ Z₁₂<VAR>w₁₂ : Z₁₂ ⟶ (shiftFunctor C 1).obj X₁<VAR>h₁₂ : Triangle.mk u₁₂ v₁₂ w₁₂ ∈ distinguishedTriangles<VAR>v₂₃ : X₃ ⟶ Z₂₃<VAR>w₂₃ : Z₂₃ ⟶ (shiftFunctor C 1).obj X₂<VAR>h₂₃ : Triangle.mk u₂₃ v₂₃ w₂₃ ∈ distinguishedTriangles<VAR>v₁₃ : X₃ ⟶ Z₁₃<VAR>w₁₃ : Z₁₃ ⟶ (shiftFunctor C 1).obj X₁<VAR>h₁₃ : Triangle.mk u₁₃ v₁₃ w₁₃ ∈ distinguishedTriangles<VAR>h : Octahedron comm h₁₂ h₂₃ h₁₃<GOAL>u₁₃ ≫ 𝟙 X₃ = u₁₂ ≫ u₂₃
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{?u.30268, u_1} C<VAR>inst✝⁴ : Preadditive C<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : HasShift C ℤ<VAR>inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝ : Pretriangulated C<VAR>X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C<VAR>u₁₂ : X₁ ⟶ X₂<VAR>u₂₃ : X₂ ⟶ X₃<VAR>u₁₃ : X₁ ⟶ X₃<VAR>comm : u₁₂ ≫ u₂₃ = u₁₃<VAR>v₁₂ : X₂ ⟶ Z₁₂<VAR>w₁₂ : Z₁₂ ⟶ (shiftFunctor C 1).obj X₁<VAR>h₁₂ : Triangle.mk u₁₂ v₁₂ w₁₂ ∈ distinguishedTriangles<VAR>v₂₃ : X₃ ⟶ Z₂₃<VAR>w₂₃ : Z₂₃ ⟶ (shiftFunctor C 1).obj X₂<VAR>h₂₃ : Triangle.mk u₂₃ v₂₃ w₂₃ ∈ distinguishedTriangles<VAR>v₁₃ : X₃ ⟶ Z₁₃<VAR>w₁₃ : Z₁₃ ⟶ (shiftFunctor C 1).obj X₁<VAR>h₁₃ : Triangle.mk u₁₃ v₁₃ w₁₃ ∈ distinguishedTriangles<VAR>h : Octahedron comm h₁₂ h₂₃ h₁₃<GOAL>v₁₃ ≫ h.m₃ = 𝟙 X₃ ≫ v₂₃
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>x : K<GOAL>(mixedEmbedding K) x ∈ Submodule.span ℚ (Set.range ⇑(latticeBasis K))
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>x : K<GOAL>∑ x_1 : ChooseBasisIndex ℤ (𝓞 K), (mixedEmbedding K) (((integralBasis K).repr x) x_1 • (integralBasis K) x_1) ∈ Submodule.span ℚ (Set.range ⇑(latticeBasis K))
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>x : K<GOAL>∑ x_1 : ChooseBasisIndex ℤ (𝓞 K), ((integralBasis K).repr x) x_1 • (mixedEmbedding K) ((integralBasis K) x_1) ∈ Submodule.span ℚ (Set.range ⇑(latticeBasis K))
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>x : K<VAR>i : ChooseBasisIndex ℤ (𝓞 K)<VAR>x✝ : i ∈ univ<GOAL>(mixedEmbedding K) ((integralBasis K) i) ∈ Set.range ⇑(latticeBasis K)
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>x : K<VAR>i : ChooseBasisIndex ℤ (𝓞 K)<VAR>x✝ : i ∈ univ<GOAL>(latticeBasis K) i ∈ Set.range ⇑(latticeBasis K)
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>J : Type u₂<VAR>inst✝ : Category.{v₂, u₂} J<VAR>F : Jᵒᵖ ⥤ C<VAR>c : Cocone F<VAR>hc : IsColimit c<VAR>s : Cone F.rightOp<VAR>m : s.pt ⟶ (coneRightOpOfCocone c).pt<VAR>w : ∀ (j : J), m ≫ (coneRightOpOfCocone c).π.app j = s.π.app j<GOAL>m = (fun s => (hc.desc (coconeOfConeRightOp s)).op) s
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>J : Type u₂<VAR>inst✝ : Category.{v₂, u₂} J<VAR>F : Jᵒᵖ ⥤ C<VAR>c : Cocone F<VAR>hc : IsColimit c<VAR>s : Cone F.rightOp<VAR>m : s.pt ⟶ (coneRightOpOfCocone c).pt<VAR>w : ∀ (j : J), m ≫ (coneRightOpOfCocone c).π.app j = s.π.app j<VAR>j : Jᵒᵖ<GOAL>(c.ι.app j ≫ m.unop).op = (c.ι.app j ≫ ((fun s => (hc.desc (coconeOfConeRightOp s)).op) s).unop).op
<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>F : Set X<VAR>n : ℕ<VAR>s : Set X<VAR>h : IsPathConnected s<VAR>p : Fin (n + 1) → X<VAR>hp : ∀ (i : Fin (n + 1)), p i ∈ s<GOAL>∃ γ t, (∀ (t : ↑I), γ t ∈ s) ∧ ∀ (i : Fin (n + 1)), γ (t i) = p i
<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>F : Set X<VAR>n : ℕ<VAR>s : Set X<VAR>h : IsPathConnected s<VAR>p : Fin (n + 1) → X<VAR>hp : ∀ (i : Fin (n + 1)), p i ∈ s<VAR>γ : Path (p 0) (p ↑n)<VAR>hγ : range ⇑γ ⊆ s ∧ ∀ (i : Fin (n + 1)), p i ∈ range ⇑γ<GOAL>∃ γ t, (∀ (t : ↑I), γ t ∈ s) ∧ ∀ (i : Fin (n + 1)), γ (t i) = p i
<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>F : Set X<VAR>n : ℕ<VAR>s : Set X<VAR>h : IsPathConnected s<VAR>p : Fin (n + 1) → X<VAR>hp : ∀ (i : Fin (n + 1)), p i ∈ s<VAR>γ : Path (p 0) (p ↑n)<VAR>h₁ : range ⇑γ ⊆ s<VAR>h₂ : ∀ (i : Fin (n + 1)), p i ∈ range ⇑γ<GOAL>∃ γ t, (∀ (t : ↑I), γ t ∈ s) ∧ ∀ (i : Fin (n + 1)), γ (t i) = p i
<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>F : Set X<VAR>n : ℕ<VAR>s : Set X<VAR>h : IsPathConnected s<VAR>p : Fin (n + 1) → X<VAR>hp : ∀ (i : Fin (n + 1)), p i ∈ s<VAR>γ : Path (p 0) (p ↑n)<VAR>h₁ : range ⇑γ ⊆ s<VAR>h₂ : ∀ (i : Fin (n + 1)), ∃ y, γ y = p i<GOAL>∃ γ t, (∀ (t : ↑I), γ t ∈ s) ∧ ∀ (i : Fin (n + 1)), γ (t i) = p i
<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>F : Set X<VAR>n : ℕ<VAR>s : Set X<VAR>h : IsPathConnected s<VAR>p : Fin (n + 1) → X<VAR>hp : ∀ (i : Fin (n + 1)), p i ∈ s<VAR>γ : Path (p 0) (p ↑n)<VAR>h₁ : ∀ (y : ↑I), γ y ∈ s<VAR>h₂ : ∀ (i : Fin (n + 1)), ∃ y, γ y = p i<GOAL>∃ γ t, (∀ (t : ↑I), γ t ∈ s) ∧ ∀ (i : Fin (n + 1)), γ (t i) = p i
<VAR>α β : Type u<VAR>c : Cardinal.{?u.233813}<GOAL>#α = 2 ↔ ∃ x y, x ≠ y ∧ {x, y} = univ
<VAR>α β : Type u<VAR>c : Cardinal.{?u.233813}<GOAL>(∃ t, ↑t = univ ∧ ∃ x y, x ≠ y ∧ t = {x, y}) ↔ ∃ x y, x ≠ y ∧ {x, y} = univ
<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>T : Type u_3<VAR>inst✝³ : CommRing T<VAR>inst✝² : Algebra R T<VAR>inst✝¹ : Algebra S T<VAR>inst✝ : IsScalarTower R S T<VAR>g : S →+* T<VAR>f : R →+* S<VAR>hg : (g.comp f).SurjectiveOnStalks<VAR>I : Ideal T<VAR>hI : I.IsPrime<VAR>this : Function.Surjective ⇑(Localization.localRingHom (Ideal.comap (g.comp f) I) I (g.comp f) ⋯)<GOAL>Function.Surjective ⇑(Localization.localRingHom (Ideal.comap g I) I g ⋯)
<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>T : Type u_3<VAR>inst✝³ : CommRing T<VAR>inst✝² : Algebra R T<VAR>inst✝¹ : Algebra S T<VAR>inst✝ : IsScalarTower R S T<VAR>g : S →+* T<VAR>f : R →+* S<VAR>hg : (g.comp f).SurjectiveOnStalks<VAR>I : Ideal T<VAR>hI : I.IsPrime<VAR>this : Function.Surjective (⇑(Localization.localRingHom (Ideal.comap g I) I g ⋯) ∘ ⇑(Localization.localRingHom (Ideal.comap (g.comp f) I) (Ideal.comap g I) f ⋯))<GOAL>Function.Surjective ⇑(Localization.localRingHom (Ideal.comap g I) I g ⋯)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a a₁ a₂ : α<VAR>b b₁ b₂ : β<VAR>inst✝³ : OrderedRing α<VAR>inst✝² : OrderedAddCommGroup β<VAR>inst✝¹ : Module α β<VAR>inst✝ : PosSMulStrictMono α β<VAR>hb : b₁ < b₂<VAR>ha : a < 0<GOAL>a • b₂ < a • b₁
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a a₁ a₂ : α<VAR>b b₁ b₂ : β<VAR>inst✝³ : OrderedRing α<VAR>inst✝² : OrderedAddCommGroup β<VAR>inst✝¹ : Module α β<VAR>inst✝ : PosSMulStrictMono α β<VAR>hb : b₁ < b₂<VAR>ha : a < 0<GOAL>-a • b₁ < -a • b₂
<VAR>a b c d n k : ℕ<VAR>p q : ℕ → Prop<GOAL>0 ≤ n.succ → pred 0 ≤ n
<VAR>a b c d n k : ℕ<VAR>p q : ℕ → Prop<VAR>n✝ : ℕ<GOAL>n✝ + 1 ≤ n.succ → (n✝ + 1).pred ≤ n
<VAR>ds₁ ds₂ ds₃ is : List ℕ<VAR>h : Forall₂ (fun x x_1 => x < x_1) is (ds₁ ++ ds₂ ++ ds₃)<GOAL>↑(assocRight ⟨is, h⟩).take = ↑(take ⟨is, h⟩).take
<VAR>𝕜 : Type u_1<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>R : Type u_3<VAR>inst✝³ : Semiring R<VAR>inst✝² : Module R F<VAR>inst✝¹ : SMulCommClass 𝕜 R F<VAR>inst✝ : ContinuousConstSMul R F<VAR>n : ℕ<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>hx : x ∈ s<VAR>h : UniqueDiffOn 𝕜 s<VAR>f g : 𝕜 → F<VAR>c : R<VAR>hf : ContDiffOn 𝕜 (↑n) f s<GOAL>((iteratedFDerivWithin 𝕜 n (c • f) s x) fun x => 1) = c • (iteratedFDerivWithin 𝕜 n f s x) fun x => 1
<VAR>𝕜 : Type u_1<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>R : Type u_3<VAR>inst✝³ : Semiring R<VAR>inst✝² : Module R F<VAR>inst✝¹ : SMulCommClass 𝕜 R F<VAR>inst✝ : ContinuousConstSMul R F<VAR>n : ℕ<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>hx : x ∈ s<VAR>h : UniqueDiffOn 𝕜 s<VAR>f g : 𝕜 → F<VAR>c : R<VAR>hf : ContDiffOn 𝕜 (↑n) f s<GOAL>((c • iteratedFDerivWithin 𝕜 n f s x) fun x => 1) = c • (iteratedFDerivWithin 𝕜 n f s x) fun x => 1
<VAR>α : Type u_1<VAR>inst✝⁴ : LinearOrder α<VAR>inst✝³ : Semigroup α<VAR>inst✝² : IsCancelMul α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>s t : Finset α<VAR>hs : s.Nonempty<VAR>ht : t.Nonempty<GOAL>s.card + t.card - 1 ≤ (s * t).card