ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ≥0∞<VAR>h : ⨆ φ, ⨆ (_ : ∀ (x : α), ↑(↑φ x) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>φ : α →ₛ ℝ≥0<VAR>hle : ∀ (x : α), ↑(↑φ x) ≤ f x<VAR>b : ℝ≥0∞<VAR>hbφ : b < (SimpleFunc.map ofNNReal φ).lintegral μ + ε<VAR>hb : ∀ (i : α →ₛ ℝ≥0), (∀ (x : α), ↑(↑i x) ≤ f x) → (SimpleFunc.map ofNNReal i).lintegral μ ≤ b<VAR>ψ : α →ₛ ℝ≥0<VAR>hψ : ∀ (x : α), ↑(↑ψ x) ≤ f x<GOAL>(SimpleFunc.map ofNNReal (ψ - φ)).lintegral μ < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ≥0∞<VAR>h : ⨆ φ, ⨆ (_ : ∀ (x : α), ↑(↑φ x) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>φ : α →ₛ ℝ≥0<VAR>hle : ∀ (x : α), ↑(↑φ x) ≤ f x<VAR>b : ℝ≥0∞<VAR>hbφ : b < (SimpleFunc.map ofNNReal φ).lintegral μ + ε<VAR>hb : ∀ (i : α →ₛ ℝ≥0), (∀ (x : α), ↑(↑i x) ≤ f x) → (SimpleFunc.map ofNNReal i).lintegral μ ≤ b<VAR>ψ : α →ₛ ℝ≥0<VAR>hψ : ∀ (x : α), ↑(↑ψ x) ≤ f x<VAR>this : (SimpleFunc.map ofNNReal φ).lintegral μ ≠ ⊤<GOAL>(SimpleFunc.map ofNNReal (ψ - φ)).lintegral μ < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ≥0∞<VAR>h : ⨆ φ, ⨆ (_ : ∀ (x : α), ↑(↑φ x) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>φ : α →ₛ ℝ≥0<VAR>hle : ∀ (x : α), ↑(↑φ x) ≤ f x<VAR>b : ℝ≥0∞<VAR>hbφ : b < (SimpleFunc.map ofNNReal φ).lintegral μ + ε<VAR>hb : ∀ (i : α →ₛ ℝ≥0), (∀ (x : α), ↑(↑i x) ≤ f x) → (SimpleFunc.map ofNNReal i).lintegral μ ≤ b<VAR>ψ : α →ₛ ℝ≥0<VAR>hψ : ∀ (x : α), ↑(↑ψ x) ≤ f x<VAR>this : (SimpleFunc.map ofNNReal φ).lintegral μ ≠ ⊤<GOAL>(SimpleFunc.map ofNNReal (φ + (ψ - φ))).lintegral μ < (SimpleFunc.map ofNNReal φ).lintegral μ + ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ≥0∞<VAR>h : ⨆ φ, ⨆ (_ : ∀ (x : α), ↑(↑φ x) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>φ : α →ₛ ℝ≥0<VAR>hle : ∀ (x : α), ↑(↑φ x) ≤ f x<VAR>b : ℝ≥0∞<VAR>hbφ : b < (SimpleFunc.map ofNNReal φ).lintegral μ + ε<VAR>hb : ∀ (i : α →ₛ ℝ≥0), (∀ (x : α), ↑(↑i x) ≤ f x) → (SimpleFunc.map ofNNReal i).lintegral μ ≤ b<VAR>ψ : α →ₛ ℝ≥0<VAR>hψ : ∀ (x : α), ↑(↑ψ x) ≤ f x<VAR>this : (SimpleFunc.map ofNNReal φ).lintegral μ ≠ ⊤<VAR>x : α<GOAL>↑(↑(φ + (ψ - φ)) x) ≤ max ↑(↑φ x) ↑(↑ψ x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ≥0∞<VAR>h : ⨆ φ, ⨆ (_ : ∀ (x : α), ↑(↑φ x) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>φ : α →ₛ ℝ≥0<VAR>hle : ∀ (x : α), ↑(↑φ x) ≤ f x<VAR>b : ℝ≥0∞<VAR>hbφ : b < (SimpleFunc.map ofNNReal φ).lintegral μ + ε<VAR>hb : ∀ (i : α →ₛ ℝ≥0), (∀ (x : α), ↑(↑i x) ≤ f x) → (SimpleFunc.map ofNNReal i).lintegral μ ≤ b<VAR>ψ : α →ₛ ℝ≥0<VAR>hψ : ∀ (x : α), ↑(↑ψ x) ≤ f x<VAR>this : (SimpleFunc.map ofNNReal φ).lintegral μ ≠ ⊤<VAR>x : α<GOAL>↑(φ + (ψ - φ)) x ≤ max (↑φ x) (↑ψ x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ≥0∞<VAR>h : ⨆ φ, ⨆ (_ : ∀ (x : α), ↑(↑φ x) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>φ : α →ₛ ℝ≥0<VAR>hle : ∀ (x : α), ↑(↑φ x) ≤ f x<VAR>b : ℝ≥0∞<VAR>hbφ : b < (SimpleFunc.map ofNNReal φ).lintegral μ + ε<VAR>hb : ∀ (i : α →ₛ ℝ≥0), (∀ (x : α), ↑(↑i x) ≤ f x) → (SimpleFunc.map ofNNReal i).lintegral μ ≤ b<VAR>ψ : α →ₛ ℝ≥0<VAR>hψ : ∀ (x : α), ↑(↑ψ x) ≤ f x<VAR>this : (SimpleFunc.map ofNNReal φ).lintegral μ ≠ ⊤<VAR>x : α<GOAL>max (↑φ x) (↑ψ x) ≤ max (↑φ x) (↑ψ x)
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>k : ℕ+<VAR>hc : (↑k).Coprime ↑(torsionOrder K)<VAR>ζ : (𝓞 K)ˣ<GOAL>ζ ∈ rootsOfUnity k (𝓞 K) ↔ ζ = 1
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>k : ℕ+<VAR>hc : (↑k).Coprime ↑(torsionOrder K)<VAR>ζ : (𝓞 K)ˣ<GOAL>ζ ^ ↑k = 1 ↔ ζ = 1
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>k : ℕ+<VAR>hc : (↑k).Coprime ↑(torsionOrder K)<VAR>ζ : (𝓞 K)ˣ<VAR>h : ζ ^ ↑k = 1<GOAL>ζ = 1
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>k : ℕ+<VAR>hc : (↑k).Coprime ↑(torsionOrder K)<VAR>ζ : (𝓞 K)ˣ<VAR>h : ζ ^ ↑k = 1<GOAL>orderOf ζ ∣ ↑k
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>k : ℕ+<VAR>hc : (↑k).Coprime ↑(torsionOrder K)<VAR>ζ : (𝓞 K)ˣ<VAR>h : ζ ^ ↑k = 1<GOAL>orderOf ζ ∣ ↑(torsionOrder K)
<VAR>z : ℂ<VAR>E : Type u_1<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>ι : Type u_2<VAR>a b : ℝ<VAR>f : ι → ℂ<VAR>s : Finset ι<VAR>ha₀ : 0 ≤ a<VAR>ha : ↑a = ∑ i ∈ s, f i<VAR>hb : b = ∑ i ∈ s, ‖f i‖<GOAL>a ≤ b
<VAR>z : ℂ<VAR>E : Type u_1<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>ι : Type u_2<VAR>a b : ℝ<VAR>f : ι → ℂ<VAR>s : Finset ι<VAR>ha₀ : 0 ≤ a<VAR>ha : ↑a = ∑ i ∈ s, f i<VAR>hb : b = ∑ i ∈ s, ‖f i‖<GOAL>abs (∑ i ∈ s, f i) ≤ ∑ i ∈ s, ‖f i‖
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℝ → E<VAR>T : ℝ<VAR>hf : Periodic f T<VAR>n : ℤ<VAR>t : ℝ<VAR>h_int : ∀ (t₁ t₂ : ℝ), IntervalIntegrable f volume t₁ t₂<GOAL>∫ (x : ℝ) in t..t + n • T, f x = n • ∫ (x : ℝ) in t..t + T, f x
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℝ → E<VAR>T : ℝ<VAR>hf : Periodic f T<VAR>n : ℤ<VAR>t : ℝ<VAR>h_int : ∀ (t₁ t₂ : ℝ), IntervalIntegrable f volume t₁ t₂<GOAL>∫ (x : ℝ) in 0 ..n • T, f x = n • ∫ (x : ℝ) in 0 ..T, f x
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜 ℬ : Finset (Finset α)<VAR>s : Finset α<VAR>a : α<GOAL>nonMemberSubfamily a (image (insert a) 𝒜) = ∅
<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>f g : E → F<VAR>p pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r r'✝ : ℝ≥0∞<VAR>r' : ℝ≥0<VAR>hf : HasFPowerSeriesOnBall f p x r<VAR>h : ↑r' < r<GOAL>TendstoUniformlyOn (fun n y => p.partialSum n (y - x)) f atTop (Metric.ball x ↑r')
<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>f g : E → F<VAR>p pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r r'✝ : ℝ≥0∞<VAR>r' : ℝ≥0<VAR>hf : HasFPowerSeriesOnBall f p x r<VAR>h : ↑r' < r<GOAL>f = (fun y => f (x + y)) ∘ fun y => y - 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>f g : E → F<VAR>p pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r r'✝ : ℝ≥0∞<VAR>r' : ℝ≥0<VAR>hf : HasFPowerSeriesOnBall f p x r<VAR>h : ↑r' < r<GOAL>Metric.ball x ↑r' = (fun y => y - x) ⁻¹' Metric.ball 0 ↑r'
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝³ : Fintype ι<VAR>inst✝² : (i : ι) → SeminormedGroup (π i)<VAR>inst✝¹ : SeminormedGroup E<VAR>f x : (i : ι) → π i<VAR>r : ℝ<VAR>inst✝ : Nonempty ι<VAR>a : E<GOAL>‖fun _i => a‖ = ‖a‖
<VAR>R : Type u<VAR>a b : R<VAR>m n✝ : ℕ<VAR>inst✝ : Semiring R<VAR>p q : R[X]<VAR>n : ℕ<VAR>r : R<GOAL>X * (monomial n) r = (monomial (n + 1)) r
<VAR>K : Type u_1<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>v : K<VAR>n : ℕ<GOAL>∃ q, (of v).nums n = ↑q
<VAR>K : Type u_1<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>v : K<VAR>n : ℕ<VAR>a b✝ : ℚ<VAR>nth_cont_eq : (of v).conts n = Pair.map Rat.cast { a := a, b := b✝ }<GOAL>∃ q, (of v).nums n = ↑q
<VAR>K : Type u_1<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>v : K<VAR>n : ℕ<VAR>a b✝ : ℚ<VAR>nth_cont_eq : (of v).conts n = Pair.map Rat.cast { a := a, b := b✝ }<GOAL>(of v).nums n = ↑a
<VAR>G : Type u<VAR>inst✝³ : Groupoid G<VAR>inst✝² : IsFreeGroupoid G<VAR>T : WideSubquiver (Symmetrify (Generators G))<VAR>inst✝¹ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)<VAR>X : Type ?u.22662<VAR>inst✝ : Monoid X<VAR>f : End (IsFreeGroupoid.SpanningTree.root' T) →* X<VAR>a : G<GOAL>f (treeHom T a ≫ 𝟙 a ≫ inv (treeHom T a)) = 𝟙 ()
<VAR>G : Type u<VAR>inst✝³ : Groupoid G<VAR>inst✝² : IsFreeGroupoid G<VAR>T : WideSubquiver (Symmetrify (Generators G))<VAR>inst✝¹ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)<VAR>X : Type ?u.22662<VAR>inst✝ : Monoid X<VAR>f : End (IsFreeGroupoid.SpanningTree.root' T) →* X<VAR>X✝ Y✝ Z✝ : G<VAR>f✝ : X✝ ⟶ Y✝<VAR>g✝ : Y✝ ⟶ Z✝<GOAL>{ obj := fun x => (), map := fun {X_1 Y} p => f (loopOfHom T p) }.map (f✝ ≫ g✝) = { obj := fun x => (), map := fun {X_1 Y} p => f (loopOfHom T p) }.map f✝ ≫ { obj := fun x => (), map := fun {X_1 Y} p => f (loopOfHom T p) }.map g✝
<VAR>G : Type u<VAR>inst✝³ : Groupoid G<VAR>inst✝² : IsFreeGroupoid G<VAR>T : WideSubquiver (Symmetrify (Generators G))<VAR>inst✝¹ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)<VAR>X : Type ?u.22662<VAR>inst✝ : Monoid X<VAR>f : End (IsFreeGroupoid.SpanningTree.root' T) →* X<VAR>X✝ Y✝ Z✝ : G<VAR>f✝ : X✝ ⟶ Y✝<VAR>g✝ : Y✝ ⟶ Z✝<GOAL>{ obj := fun x => (), map := fun {X_1 Y} p => f (loopOfHom T p) }.map (f✝ ≫ g✝) = f (loopOfHom T g✝ * loopOfHom T f✝)
<VAR>n : ℕ<GOAL>n.fastFib = fib n
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<VAR>c : F<GOAL>fderivWithin 𝕜 (fun y => c - f y) s x = -fderivWithin 𝕜 f s x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Fintype α<VAR>inst✝² : Fintype β<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>G : SimpleGraph α<VAR>a✝ b✝ : α<VAR>p : G.Walk a✝ b✝<VAR>hG : G.IsHamiltonian<VAR>a b : α<GOAL>G.Reachable a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Fintype α<VAR>inst✝² : Fintype β<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>G : SimpleGraph α<VAR>a✝ b : α<VAR>p : G.Walk a✝ b<VAR>hG : G.IsHamiltonian<VAR>a : α<GOAL>G.Reachable a a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Fintype α<VAR>inst✝² : Fintype β<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>G : SimpleGraph α<VAR>a✝ b✝ : α<VAR>p : G.Walk a✝ b✝<VAR>hG : G.IsHamiltonian<VAR>a b : α<VAR>hab : a ≠ b<GOAL>G.Reachable a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Fintype α<VAR>inst✝² : Fintype β<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>G : SimpleGraph α<VAR>a✝ b✝ : α<VAR>p : G.Walk a✝ b✝<VAR>hG : G.IsHamiltonian<VAR>a b : α<VAR>hab : a ≠ b<VAR>this : Nontrivial α<GOAL>G.Reachable a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Fintype α<VAR>inst✝² : Fintype β<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>G : SimpleGraph α<VAR>a✝ b✝ : α<VAR>p✝ : G.Walk a✝ b✝<VAR>hG : G.IsHamiltonian<VAR>a b : α<VAR>hab : a ≠ b<VAR>this : Nontrivial α<VAR>w✝ : α<VAR>p : G.Walk w✝ w✝<VAR>hp : p.IsHamiltonianCycle<GOAL>G.Reachable a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Fintype α<VAR>inst✝² : Fintype β<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>G : SimpleGraph α<VAR>a✝ b✝ : α<VAR>p✝ : G.Walk a✝ b✝<VAR>hG : G.IsHamiltonian<VAR>a b : α<VAR>hab : a ≠ b<VAR>this : Nontrivial α<VAR>w✝ : α<VAR>p : G.Walk w✝ w✝<VAR>hp : p.IsHamiltonianCycle<VAR>a_mem : a ∈ p.support<GOAL>G.Reachable a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Fintype α<VAR>inst✝² : Fintype β<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>G : SimpleGraph α<VAR>a✝ b✝ : α<VAR>p✝ : G.Walk a✝ b✝<VAR>hG : G.IsHamiltonian<VAR>a b : α<VAR>hab : a ≠ b<VAR>this : Nontrivial α<VAR>w✝ : α<VAR>p : G.Walk w✝ w✝<VAR>hp : p.IsHamiltonianCycle<VAR>a_mem : a ∈ p.support<VAR>b_mem : b ∈ p.support<GOAL>G.Reachable a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Fintype α<VAR>inst✝² : Fintype β<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>G : SimpleGraph α<VAR>a b : α<VAR>p : G.Walk a b<VAR>hG : G.IsHamiltonian<VAR>x✝ : IsEmpty α<GOAL>False
<VAR>𝕜 : Type u_1<VAR>𝕝 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>β : Type u_5<VAR>inst✝⁷ : OrderedSemiring 𝕜<VAR>inst✝⁶ : TopologicalSpace E<VAR>inst✝⁵ : TopologicalSpace F<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Module 𝕜 F<VAR>inst✝ : ContinuousAdd E<VAR>s t : Set E<VAR>hs : StrictConvex 𝕜 s<VAR>z : E<GOAL>StrictConvex 𝕜 ((fun x => z + x) '' s)
<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>x : ⨂[𝕜] (i : ι), E i<VAR>x✝ : ContinuousMultilinearMap 𝕜 E F<GOAL>‖((↑lift).flip x ∘ₗ ContinuousMultilinearMap.toMultilinearMapLinear) x✝‖ ≤ projectiveSeminorm x * ‖x✝‖
<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>x : ⨂[𝕜] (i : ι), E i<VAR>x✝ : ContinuousMultilinearMap 𝕜 E F<GOAL>‖(lift x✝.toMultilinearMap) x‖ ≤ projectiveSeminorm x * ‖x✝‖
<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>x y : ⨂[𝕜] (i : ι), E i<VAR>x✝ : ContinuousMultilinearMap 𝕜 E F<GOAL>((fun x => ((↑lift).flip x ∘ₗ ContinuousMultilinearMap.toMultilinearMapLinear).mkContinuous (projectiveSeminorm x) ⋯) (x + y)) x✝ = ((fun x => ((↑lift).flip x ∘ₗ ContinuousMultilinearMap.toMultilinearMapLinear).mkContinuous (projectiveSeminorm x) ⋯) x + (fun x => ((↑lift).flip x ∘ₗ ContinuousMultilinearMap.toMultilinearMapLinear).mkContinuous (projectiveSeminorm x) ⋯) y) x✝
<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>a : 𝕜<VAR>x : ⨂[𝕜] (i : ι), E i<VAR>x✝ : ContinuousMultilinearMap 𝕜 E F<GOAL>({ toFun := fun x => ((↑lift).flip x ∘ₗ ContinuousMultilinearMap.toMultilinearMapLinear).mkContinuous (projectiveSeminorm x) ⋯, map_add' := ⋯ }.toFun (a • x)) x✝ = ((RingHom.id 𝕜) a • { toFun := fun x => ((↑lift).flip x ∘ₗ ContinuousMultilinearMap.toMultilinearMapLinear).mkContinuous (projectiveSeminorm x) ⋯, map_add' := ⋯ }.toFun x) x✝
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝³ : Monoid M<VAR>inst✝² : AddMonoid N<VAR>G : Type u_3<VAR>H : Type u_4<VAR>inst✝¹ : Group G<VAR>inst✝ : AddGroup H<VAR>s : Finset G<GOAL>Group.rank ↥(closure ↑s) ≤ s.card
<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>s✝ : Finset α<VAR>H : s✝.Nonempty<VAR>x : α<VAR>s : Finset α<GOAL>WithBot.map (⇑toDual) s.max = (image (⇑toDual) s).min
<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>s✝ : Finset α<VAR>H : s✝.Nonempty<VAR>x : α<VAR>s : Finset α<GOAL>WithBot.map (⇑toDual) s.max = s.inf (WithTop.some ∘ ⇑toDual)
<VAR>S : SSet<VAR>filler : ∀ ⦃n : ℕ⦄ ⦃i : Fin (n + 3)⦄ (σ₀ : Λ[n + 2, i] ⟶ S), 0 < i → i < Fin.last (n + 2) → ∃ σ, ∀ (j : Fin (n + 3)) (h : j ≠ i), SimplicialObject.δ S j σ = σ₀.app (Opposite.op [n + 1]) (horn.face i j h)<VAR>n : ℕ<VAR>i : Fin (n + 3)<VAR>σ₀ : Λ[n + 2, i] ⟶ S<VAR>h₀ : 0 < i<VAR>hₙ : i < Fin.last (n + 2)<VAR>σ : S _[n + 2]<VAR>h : ∀ (j : Fin (n + 3)) (h : j ≠ i), SimplicialObject.δ S j σ = σ₀.app (Opposite.op [n + 1]) (horn.face i j h)<GOAL>σ₀ = hornInclusion (n + 2) i ≫ (S.yonedaEquiv [n + 2]).symm σ
<VAR>S : SSet<VAR>filler : ∀ ⦃n : ℕ⦄ ⦃i : Fin (n + 3)⦄ (σ₀ : Λ[n + 2, i] ⟶ S), 0 < i → i < Fin.last (n + 2) → ∃ σ, ∀ (j : Fin (n + 3)) (h : j ≠ i), SimplicialObject.δ S j σ = σ₀.app (Opposite.op [n + 1]) (horn.face i j h)<VAR>n : ℕ<VAR>i : Fin (n + 3)<VAR>σ₀ : Λ[n + 2, i] ⟶ S<VAR>h₀ : 0 < i<VAR>hₙ : i < Fin.last (n + 2)<VAR>σ : S _[n + 2]<VAR>h : ∀ (j : Fin (n + 3)) (h : j ≠ i), SimplicialObject.δ S j σ = σ₀.app (Opposite.op [n + 1]) (horn.face i j h)<GOAL>∀ (j : Fin (n + 1 + 2)) (h : j ≠ i), σ₀.app (Opposite.op [n + 1]) (horn.face i j h) = (hornInclusion (n + 2) i ≫ (S.yonedaEquiv [n + 2]).symm σ).app (Opposite.op [n + 1]) (horn.face i j h)
<VAR>S : SSet<VAR>filler : ∀ ⦃n : ℕ⦄ ⦃i : Fin (n + 3)⦄ (σ₀ : Λ[n + 2, i] ⟶ S), 0 < i → i < Fin.last (n + 2) → ∃ σ, ∀ (j : Fin (n + 3)) (h : j ≠ i), SimplicialObject.δ S j σ = σ₀.app (Opposite.op [n + 1]) (horn.face i j h)<VAR>n : ℕ<VAR>i : Fin (n + 3)<VAR>σ₀ : Λ[n + 2, i] ⟶ S<VAR>h₀ : 0 < i<VAR>hₙ : i < Fin.last (n + 2)<VAR>σ : S _[n + 2]<VAR>h : ∀ (j : Fin (n + 3)) (h : j ≠ i), SimplicialObject.δ S j σ = σ₀.app (Opposite.op [n + 1]) (horn.face i j h)<VAR>j : Fin (n + 1 + 2)<VAR>hj : j ≠ i<GOAL>σ₀.app (Opposite.op [n + 1]) (horn.face i j hj) = (hornInclusion (n + 2) i ≫ (S.yonedaEquiv [n + 2]).symm σ).app (Opposite.op [n + 1]) (horn.face i j hj)
<VAR>S : SSet<VAR>filler : ∀ ⦃n : ℕ⦄ ⦃i : Fin (n + 3)⦄ (σ₀ : Λ[n + 2, i] ⟶ S), 0 < i → i < Fin.last (n + 2) → ∃ σ, ∀ (j : Fin (n + 3)) (h : j ≠ i), SimplicialObject.δ S j σ = σ₀.app (Opposite.op [n + 1]) (horn.face i j h)<VAR>n : ℕ<VAR>i : Fin (n + 3)<VAR>σ₀ : Λ[n + 2, i] ⟶ S<VAR>h₀ : 0 < i<VAR>hₙ : i < Fin.last (n + 2)<VAR>σ : S _[n + 2]<VAR>h : ∀ (j : Fin (n + 3)) (h : j ≠ i), SimplicialObject.δ S j σ = σ₀.app (Opposite.op [n + 1]) (horn.face i j h)<VAR>j : Fin (n + 1 + 2)<VAR>hj : j ≠ i<GOAL>SimplicialObject.δ S j σ = ((hornInclusion (n + 2) i).app (Opposite.op [n + 1]) ≫ ((S.yonedaEquiv [n + 2]).symm σ).app (Opposite.op [n + 1])) (horn.face i j hj)
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>C : Type u₁<VAR>D : Type v₁<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : Semiring A<VAR>inst✝⁶ : Semiring B<VAR>inst✝⁵ : Semiring C<VAR>inst✝⁴ : Semiring D<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra R B<VAR>inst✝¹ : Algebra R C<VAR>inst✝ : Algebra R D<VAR>φ : A →ₐ[R] B<VAR>f : A →ₗ[R] B<VAR>map_one : f 1 = 1<VAR>map_mul : ∀ (x y : A), f (x * y) = f x * f y<VAR>c : R<GOAL>(↑↑{ toFun := ⇑f, map_one' := map_one, map_mul' := map_mul, map_zero' := ⋯, map_add' := ⋯ }).toFun ((algebraMap R A) c) = (algebraMap R B) c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>f : α ≃o β<VAR>s : Set β<VAR>x : β<GOAL>IsLUB (⇑f ⁻¹' s) (f.symm x) ↔ IsLUB s x
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>n : Type u_3<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>f : R →+* S<GOAL>Polynomial.map (MvPolynomial.map f) (univ R n) = univ S n
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>n : Type u_3<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>f : R →+* S<GOAL>(of (Function.curry MvPolynomial.X)).charpoly = univ S n
<VAR>E : Type u_1<VAR>inst✝³ : SeminormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>P : Type u_2<VAR>inst✝¹ : PseudoMetricSpace P<VAR>inst✝ : NormedAddTorsor E P<VAR>c : P<VAR>r : ℝ<GOAL>Continuous ↑(univBall c r)
<VAR>x : ℝ<VAR>hx₁ : -π < x<VAR>hx₂ : x < π<VAR>h : sin x = 0<GOAL>x = 0
<VAR>x : ℝ<VAR>hx₁ : -π < x<VAR>hx₂ : x < π<VAR>h : x ≠ 0<GOAL>sin x ≠ 0
<VAR>l : List Char<GOAL>utf8Len l = 0 ↔ l = []
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : Invertible 2<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>x✝ y✝ z x y : P<GOAL>y = midpoint R x y ↔ x = y
<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>G : Type u_1<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>𝕜' : Type u_2<VAR>inst✝¹ : NontriviallyNormedField 𝕜'<VAR>inst✝ : NormedAlgebra 𝕜 𝕜'<VAR>c d✝ : 𝕜 → 𝕜'<VAR>c' d' : 𝕜'<VAR>hc : HasDerivAt c c' x<VAR>d : 𝕜'<GOAL>HasDerivAt (fun x => c x / d) (c' / d) x
<VAR>R✝ : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M✝ : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝¹⁰ : Semiring R✝<VAR>inst✝⁹ : AddCommMonoid M✝<VAR>inst✝⁸ : Module R✝ M✝<VAR>x✝ : M✝<VAR>p✝ p'✝ : Submodule R✝ M✝<VAR>inst✝⁷ : Semiring R₂<VAR>σ₁₂ : R✝ →+* R₂<VAR>inst✝⁶ : AddCommMonoid M₂<VAR>inst✝⁵ : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝⁴ : FunLike F M✝ M₂<VAR>inst✝³ : SemilinearMapClass F σ₁₂ M✝ M₂<VAR>s t : Set M✝<VAR>R : Type u_9<VAR>M : Type u_10<VAR>inst✝² : Ring R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>p p' : Submodule R M<VAR>x : M<GOAL>x ∈ (p ⊔ p').toAddSubgroup ↔ x ∈ p.toAddSubgroup ⊔ p'.toAddSubgroup
<VAR>R✝ : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M✝ : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝¹⁰ : Semiring R✝<VAR>inst✝⁹ : AddCommMonoid M✝<VAR>inst✝⁸ : Module R✝ M✝<VAR>x✝ : M✝<VAR>p✝ p'✝ : Submodule R✝ M✝<VAR>inst✝⁷ : Semiring R₂<VAR>σ₁₂ : R✝ →+* R₂<VAR>inst✝⁶ : AddCommMonoid M₂<VAR>inst✝⁵ : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝⁴ : FunLike F M✝ M₂<VAR>inst✝³ : SemilinearMapClass F σ₁₂ M✝ M₂<VAR>s t : Set M✝<VAR>R : Type u_9<VAR>M : Type u_10<VAR>inst✝² : Ring R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>p p' : Submodule R M<VAR>x : M<GOAL>(∃ y ∈ p, ∃ z ∈ p', y + z = x) ↔ ∃ y ∈ p.toAddSubgroup, ∃ z ∈ p'.toAddSubgroup, y + z = x
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>W : Type v<VAR>G : SimpleGraph V<VAR>G₁ G₂ : G.Subgraph<VAR>a b : V<VAR>x y : G.Subgraph<VAR>h✝ : x ≤ y<VAR>v w : ↑x.verts<VAR>h : (inclusion h✝) v = (inclusion h✝) w<GOAL>v = w
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>W : Type v<VAR>G : SimpleGraph V<VAR>G₁ G₂ : G.Subgraph<VAR>a b : V<VAR>x y : G.Subgraph<VAR>h✝ : x ≤ y<VAR>v w : ↑x.verts<VAR>h : ↑(RelHom.instFunLike.1 { toFun := fun v => ⟨↑v, ⋯⟩, map_rel' := ⋯ } v) = ↑(RelHom.instFunLike.1 { toFun := fun v => ⟨↑v, ⋯⟩, map_rel' := ⋯ } w)<GOAL>v = w
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : PredOrder α<VAR>a : α<GOAL>pred a = ⨆ b, ⨆ (_ : b < a), b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : PredOrder α<VAR>a : α<GOAL>pred a ≤ ⨆ b, ⨆ (_ : b < a), b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : PredOrder α<GOAL>pred ⊥ ≤ ⨆ b, ⨆ (_ : b < ⊥), b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : PredOrder α<VAR>a : α<VAR>ha : a ≠ ⊥<GOAL>pred a ≤ ⨆ b, ⨆ (_ : b < a), b
<VAR>𝕜 : Type u_1<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f g : 𝕜 → E<VAR>x : 𝕜<VAR>m : ℕ<VAR>hf : AnalyticAt 𝕜 (fun z => (z - x) ^ m • f z) x<VAR>n : ℕ<VAR>hg : AnalyticAt 𝕜 (fun z => (z - x) ^ n • g z) x<GOAL>AnalyticAt 𝕜 (fun z => (z - x) ^ max m n • (f + g) z) x