ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>X : Type u<VAR>inst✝ : MetricSpace X<VAR>p q : NonemptyCompacts X<VAR>ha : Isometry Subtype.val<VAR>hb : Isometry Subtype.val<VAR>A : dist p q = hausdorffDist ↑p ↑q<VAR>I : ↑p = range Subtype.val<VAR>J : ↑q = range Subtype.val<GOAL>dist p.toGHSpace q.toGHSpace ≤ hausdorffDist (range Subtype.val) (range Subtype.val)
<VAR>x y z : ℝ<VAR>p : ℝ × ℝ<VAR>hp : 0 < p.1<GOAL>HasStrictFDerivAt (fun x => x.1 ^ x.2) ((p.2 * p.1 ^ (p.2 - 1)) • ContinuousLinearMap.fst ℝ ℝ ℝ + (p.1 ^ p.2 * log p.1) • ContinuousLinearMap.snd ℝ ℝ ℝ) p
<VAR>x y z : ℝ<VAR>p : ℝ × ℝ<VAR>hp : 0 < p.1<VAR>this : (fun x => x.1 ^ x.2) =ᶠ[𝓝 p] fun x => rexp (log x.1 * x.2)<GOAL>HasStrictFDerivAt (fun x => x.1 ^ x.2) ((p.2 * p.1 ^ (p.2 - 1)) • ContinuousLinearMap.fst ℝ ℝ ℝ + (p.1 ^ p.2 * log p.1) • ContinuousLinearMap.snd ℝ ℝ ℝ) p
<VAR>x y z : ℝ<VAR>p : ℝ × ℝ<VAR>hp : 0 < p.1<VAR>this : (fun x => x.1 ^ x.2) =ᶠ[𝓝 p] fun x => rexp (log x.1 * x.2)<GOAL>HasStrictFDerivAt (fun x => rexp (log x.1 * x.2)) ((p.2 * p.1 ^ (p.2 - 1)) • ContinuousLinearMap.fst ℝ ℝ ℝ + (p.1 ^ p.2 * log p.1) • ContinuousLinearMap.snd ℝ ℝ ℝ) p
<VAR>x y z : ℝ<VAR>p : ℝ × ℝ<VAR>hp : 0 < p.1<VAR>this : (fun x => x.1 ^ x.2) =ᶠ[𝓝 p] fun x => rexp (log x.1 * x.2)<GOAL>(p.2 * p.1 ^ (p.2 - 1)) • ContinuousLinearMap.fst ℝ ℝ ℝ + (p.1 ^ p.2 * log p.1) • ContinuousLinearMap.snd ℝ ℝ ℝ = rexp (log p.1 * p.2) • (log p.1 • ContinuousLinearMap.snd ℝ ℝ ℝ + p.2 • p.1⁻¹ • ContinuousLinearMap.fst ℝ ℝ ℝ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : CountablySeparated α<GOAL>MeasurableSingletonClass α
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : CountablySeparated α<VAR>f : α → ℕ → Bool<VAR>fmeas : Measurable f<VAR>finj : Injective f<GOAL>MeasurableSingletonClass α
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : CountablySeparated α<VAR>f : α → ℕ → Bool<VAR>fmeas : Measurable f<VAR>finj : Injective f<VAR>x : α<GOAL>MeasurableSet {x}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : CountablySeparated α<VAR>f : α → ℕ → Bool<VAR>fmeas : Measurable f<VAR>finj : Injective f<VAR>x : α<GOAL>MeasurableSet (f ⁻¹' {f x})
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>β : ι → Type u_3<VAR>s✝ s₁ s₂ : Set ι<VAR>t t₁ t₂ : (i : ι) → Set (α i)<VAR>i✝ : ι<VAR>inst✝ : DecidableEq ι<VAR>x : (i : ι) → β i<VAR>i : ι<VAR>s : Set (β i)<VAR>y : (a : ι) → β a<GOAL>y ∈ update x i '' s ↔ y ∈ univ.pi (update (fun j => {x j}) i s)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>p q : R[X]<VAR>m : Multiset R[X]<VAR>L : List R[X]<GOAL>0 ∉ Quot.mk Setoid.r L → (prod (Quot.mk Setoid.r L)).roots = Multiset.bind (Quot.mk Setoid.r L) roots
<VAR>α✝ : Type u_1<VAR>α : Type u_2<VAR>s : Set (Set α)<VAR>h₁ : s.PairwiseDisjoint id<VAR>h₂ : ∀ (a : α), ∃ x ∈ s, a ∈ x<VAR>h₃ : ∅ ∉ s<GOAL>IsPartition s
<VAR>α✝ : Type u_1<VAR>α : Type u_2<VAR>s : Set (Set α)<VAR>h₁ : s.PairwiseDisjoint id<VAR>h₂ : ∀ (a : α), ∃ x ∈ s, a ∈ x<VAR>h₃ : ∅ ∉ s<VAR>a : α<GOAL>∀ (y₁ y₂ : Set α), y₁ ∈ s ∧ a ∈ y₁ → y₂ ∈ s ∧ a ∈ y₂ → y₁ = y₂
<VAR>α✝ : Type u_1<VAR>α : Type u_2<VAR>s : Set (Set α)<VAR>h₁ : s.PairwiseDisjoint id<VAR>h₂ : ∀ (a : α), ∃ x ∈ s, a ∈ x<VAR>h₃ : ∅ ∉ s<VAR>a : α<VAR>b₁ b₂ : Set α<VAR>hb₁ : b₁ ∈ s ∧ a ∈ b₁<VAR>hb₂ : b₂ ∈ s ∧ a ∈ b₂<GOAL>b₁ = b₂
<VAR>α✝ : Type u_1<VAR>α : Type u_2<VAR>s : Set (Set α)<VAR>h₁ : s.PairwiseDisjoint id<VAR>h₂ : ∀ (a : α), ∃ x ∈ s, a ∈ x<VAR>h₃ : ∅ ∉ s<VAR>a : α<VAR>b₁ b₂ : Set α<VAR>hb₁ : b₁ ∈ s ∧ a ∈ b₁<VAR>hb₂ : b₂ ∈ s ∧ a ∈ b₂<GOAL>¬Disjoint (id b₁) (id b₂)
<VAR>α✝ : Type u_1<VAR>α : Type u_2<VAR>s : Set (Set α)<VAR>h₁ : s.PairwiseDisjoint id<VAR>h₂ : ∀ (a : α), ∃ x ∈ s, a ∈ x<VAR>h₃ : ∅ ∉ s<VAR>a : α<VAR>b₁ b₂ : Set α<VAR>hb₁ : b₁ ∈ s ∧ a ∈ b₁<VAR>hb₂ : b₂ ∈ s ∧ a ∈ b₂<GOAL>∃ x ∈ id b₁, x ∈ id b₂
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>α : Type u_7<VAR>inst✝⁸ : LinearOrderedField R<VAR>inst✝⁷ : LinearOrderedField R'<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : AddCommGroup F<VAR>inst✝⁴ : LinearOrderedAddCommGroup α<VAR>inst✝³ : Module R E<VAR>inst✝² : Module R F<VAR>inst✝¹ : Module R α<VAR>inst✝ : OrderedSMul R α<VAR>s : Set E<VAR>i j : ι<VAR>c : R<VAR>t : Finset ι<VAR>w : ι → R<VAR>z : ι → E<VAR>ha : i ∉ t<VAR>hw : ∑ j ∈ t, w j ≠ 0<GOAL>(insert i t).centerMass w z = (w i / (w i + ∑ j ∈ t, w j)) • z i + ((∑ j ∈ t, w j) / (w i + ∑ j ∈ t, w j)) • t.centerMass w z
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>α : Type u_7<VAR>inst✝⁸ : LinearOrderedField R<VAR>inst✝⁷ : LinearOrderedField R'<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : AddCommGroup F<VAR>inst✝⁴ : LinearOrderedAddCommGroup α<VAR>inst✝³ : Module R E<VAR>inst✝² : Module R F<VAR>inst✝¹ : Module R α<VAR>inst✝ : OrderedSMul R α<VAR>s : Set E<VAR>i j : ι<VAR>c : R<VAR>t : Finset ι<VAR>w : ι → R<VAR>z : ι → E<VAR>ha : i ∉ t<VAR>hw : ∑ j ∈ t, w j ≠ 0<GOAL>(w i / (w i + ∑ i ∈ t, w i)) • z i + (w i + ∑ i ∈ t, w i)⁻¹ • ∑ i ∈ t, w i • z i = (w i / (w i + ∑ i ∈ t, w i)) • z i + ((∑ i ∈ t, w i) / (w i + ∑ i ∈ t, w i) * (∑ i ∈ t, w i)⁻¹) • ∑ i ∈ t, w i • z i
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>α : Type u_7<VAR>inst✝⁸ : LinearOrderedField R<VAR>inst✝⁷ : LinearOrderedField R'<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : AddCommGroup F<VAR>inst✝⁴ : LinearOrderedAddCommGroup α<VAR>inst✝³ : Module R E<VAR>inst✝² : Module R F<VAR>inst✝¹ : Module R α<VAR>inst✝ : OrderedSMul R α<VAR>s : Set E<VAR>i j : ι<VAR>c : R<VAR>t : Finset ι<VAR>w : ι → R<VAR>z : ι → E<VAR>ha : i ∉ t<VAR>hw : ∑ j ∈ t, w j ≠ 0<GOAL>(w i + ∑ i ∈ t, w i)⁻¹ = (∑ i ∈ t, w i) / (w i + ∑ i ∈ t, w i) * (∑ i ∈ t, w i)⁻¹
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s t u v : Finset α<VAR>a b : α<VAR>ha : a ∉ t<GOAL>_root_.Disjoint (s.erase a) (insert a t) ↔ _root_.Disjoint s t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a a₁ a₂ b b₁ b₂ c d : α<VAR>h : min c d ≤ b<GOAL>Iio b ∪ Ico c d = Iio (max b d)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a a₁ a₂ b b₁ b₂ c d : α<VAR>hcd : c ≤ d<VAR>h : c ≤ b<GOAL>Iio b ∪ Ico c d = Iio (max b d)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a a₁ a₂ b b₁ b₂ c d : α<VAR>hcd : d ≤ c<VAR>h : d ≤ b<GOAL>Iio b ∪ Ico c d = Iio (max b d)
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>β✝ : Type u_4<VAR>β' : Type u_5<VAR>γ : Type u_6<VAR>γ' : Type u_7<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μ : Measure α<VAR>f✝ : Ω → β✝<VAR>g : Ω → β'<VAR>β : ι → Type u_8<VAR>m : (i : ι) → MeasurableSpace (β i)<VAR>f : (i : ι) → Ω → β i<VAR>h : iIndepFun m f κ μ<GOAL>∀ᵐ (a : α) ∂μ, IsProbabilityMeasure (κ a)
<VAR>d : ℕ<VAR>a : ℤ√↑d<VAR>ha✝ : a.Nonneg<VAR>x y : ℕ<VAR>ha : { re := ↑x, im := -↑y }.Nonneg<GOAL>(sqrtd * { re := ↑x, im := -↑y }).Nonneg
<VAR>d : ℕ<VAR>a : ℤ√↑d<VAR>ha✝ : a.Nonneg<VAR>x y : ℕ<VAR>ha : { re := ↑x, im := -↑y }.Nonneg<GOAL>{ re := -(↑d * ↑y), im := ↑x }.Nonneg
<VAR>d : ℕ<VAR>a : ℤ√↑d<VAR>ha✝ : a.Nonneg<VAR>x y : ℕ<VAR>ha : { re := ↑x, im := -↑y }.Nonneg<GOAL>SqLe (d * y) 1 x d
<VAR>d : ℕ<VAR>a : ℤ√↑d<VAR>ha✝ : a.Nonneg<VAR>x y : ℕ<VAR>ha : { re := -↑x, im := ↑y }.Nonneg<GOAL>(sqrtd * { re := -↑x, im := ↑y }).Nonneg
<VAR>d : ℕ<VAR>a : ℤ√↑d<VAR>ha✝ : a.Nonneg<VAR>x y : ℕ<VAR>ha : { re := -↑x, im := ↑y }.Nonneg<GOAL>{ re := ↑d * ↑y, im := -↑x }.Nonneg
<VAR>d : ℕ<VAR>a : ℤ√↑d<VAR>ha✝ : a.Nonneg<VAR>x y : ℕ<VAR>ha : { re := -↑x, im := ↑y }.Nonneg<GOAL>SqLe x d (d * y) 1
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>inst✝² : MulOneClass M<VAR>inst✝¹ : MulOneClass N<VAR>inst✝ : Monoid P<VAR>f✝ : M →* P<VAR>g : N →* P<VAR>comm : ∀ (m : M) (n : N), Commute (f✝ m) (g n)<VAR>f : M × N →* P<VAR>x : M × N<GOAL>((f.comp (inl M N)).noncommCoprod (f.comp (inr M N)) ⋯) x = f x
<VAR>X✝ : Type u_1<VAR>Y✝ : Type u_2<VAR>inst✝⁴ : TopologicalSpace X✝<VAR>inst✝³ : FirstCountableTopology X✝<VAR>X : Type u_3<VAR>Y : Type u_4<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : T2Space Y<VAR>f : X → Y<VAR>hf : Continuous f<GOAL>t2Setoid X ≤ Setoid.ker f
<VAR>S : Type u_1<VAR>inst✝ : UnitalShelf S<VAR>x y z : S<GOAL>(x ◃ y) ◃ z = x ◃ y ◃ z
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : Fintype α<VAR>s t : Finset α<VAR>a b : α<GOAL>s.dens = 0 ↔ s = ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrderedField α<VAR>x y : α<GOAL>(const y - const x).Pos ↔ x < y
<VAR>C : Type u_1<VAR>inst✝ : Category.{u_2, u_1} C<VAR>X Y : SimplicialObject C<VAR>s : Splitting X<VAR>n : ℕ<GOAL>(s.cofan (op [n])).inj (IndexSet.id (op [n])) = s.ι n
<VAR>C : Type u_1<VAR>inst✝ : Category.{u_2, u_1} C<VAR>X Y : SimplicialObject C<VAR>s : Splitting X<VAR>n : ℕ<GOAL>s.ι (unop (IndexSet.id (op [n])).fst).len = s.ι n
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type w<VAR>inst✝¹ : MetricSpace X<VAR>inst✝ : MetricSpace Y<VAR>x : X<VAR>y : Y<GOAL>1 ≤ Sum.dist (Sum.inr y) (Sum.inl x)
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type w<VAR>inst✝¹ : MetricSpace X<VAR>inst✝ : MetricSpace Y<VAR>x : X<VAR>y : Y<GOAL>1 ≤ Sum.dist (Sum.inl x) (Sum.inr y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : Ring β<VAR>abv : β → α<VAR>inst✝ : IsAbsoluteValue abv<VAR>f1 f2 g1 g2 : CauSeq β abv<VAR>hf : f1 ≈ f2<VAR>hg : g1 ≈ g2<GOAL>f1 - g1 ≈ f2 - g2
<VAR>x y z : ℝ<GOAL>sinh x = 0 ↔ x = 0
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : NonPreadditiveAbelian C<VAR>X Y : C<VAR>a : X ⟶ Y<GOAL>- -a = a
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : NonPreadditiveAbelian C<VAR>X Y : C<VAR>a : X ⟶ Y<GOAL>0 - (0 - a) = a
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : NonPreadditiveAbelian C<VAR>X Y : C<VAR>a : X ⟶ Y<GOAL>a - a - (0 - a) = a
<VAR>R : Type u<VAR>inst✝⁵ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type v<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>T : Type u_1<VAR>inst✝² : CommSemiring T<VAR>inst✝¹ : Algebra R T<VAR>inst✝ : IsLocalization S T<VAR>x : T<GOAL>x • 0 = 0
<VAR>G : Type w<VAR>inst✝² : TopologicalSpace G<VAR>μ : Content G<VAR>inst✝¹ : R1Space G<VAR>inst✝ : WeaklyLocallyCompactSpace G<VAR>K : Set G<VAR>hK : IsCompact K<GOAL>μ.outerMeasure K < ⊤
<VAR>G : Type w<VAR>inst✝² : TopologicalSpace G<VAR>μ : Content G<VAR>inst✝¹ : R1Space G<VAR>inst✝ : WeaklyLocallyCompactSpace G<VAR>K : Set G<VAR>hK : IsCompact K<VAR>F : Set G<VAR>h1F : IsCompact F<VAR>h2F : K ⊆ interior F<GOAL>μ.outerMeasure K < ⊤
<VAR>c : ℝ<VAR>f✝ g : ℕ → Bool<VAR>n : ℕ<VAR>f : ℕ → Bool<VAR>h1 : 0 ≤ c<VAR>h2 : c < 1<GOAL>Summable (cantorFunctionAux c f)
<VAR>c : ℝ<VAR>f✝ g : ℕ → Bool<VAR>n : ℕ<VAR>f : ℕ → Bool<VAR>h1 : 0 ≤ c<VAR>h2 : c < 1<GOAL>∀ (b : ℕ), cantorFunctionAux c f b = 0 ∨ cantorFunctionAux c f b = c ^ b
<VAR>α β : Type u<VAR>f g : α ⟶ β<VAR>h : ∀ (a : α), f a = g a<GOAL>f = g
<VAR>α β : Type u<VAR>f g : α ⟶ β<VAR>h : ∀ (a : α), f a = g a<VAR>x : α<GOAL>f x = g x
<VAR>α : Type u_1<VAR>s : Cycle α<VAR>h : s.Subsingleton<GOAL>s.Nodup
<VAR>α : Type u_1<VAR>l : List α<VAR>h : Subsingleton (Quot.mk Setoid.r l)<GOAL>Nodup (Quot.mk Setoid.r l)
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>f✝¹ : ℝ → E<VAR>g'✝ g✝ φ : ℝ → ℝ<VAR>a b : ℝ<VAR>inst✝² : CompleteSpace E<VAR>f✝ f'✝ : ℝ → E<VAR>G : Type u_6<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace ℝ G<VAR>f f' : ℝ → ℝ<VAR>g g' : ℝ → E<VAR>hf : ContinuousOn f [[a, b]]<VAR>hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Ioi x) x<VAR>hf' : ContinuousOn f' [[a, b]]<VAR>hg : ContinuousOn g [[f a, f b]]<VAR>hgg' : ∀ x ∈ Ioo (min (f a) (f b)) (max (f a) (f b)), HasDerivWithinAt g (g' x) (Ioi x) x<VAR>hg' : ContinuousOn g' (f '' [[a, b]])<GOAL>∫ (x : ℝ) in a..b, f' x • (g' ∘ f) x = (g ∘ f) b - (g ∘ f) a
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>f✝¹ : ℝ → E<VAR>g'✝ g✝ φ : ℝ → ℝ<VAR>a b : ℝ<VAR>inst✝² : CompleteSpace E<VAR>f✝ f'✝ : ℝ → E<VAR>G : Type u_6<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace ℝ G<VAR>f f' : ℝ → ℝ<VAR>g g' : ℝ → E<VAR>hf : ContinuousOn f [[a, b]]<VAR>hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Ioi x) x<VAR>hf' : ContinuousOn f' [[a, b]]<VAR>hg : ContinuousOn g [[f a, f b]]<VAR>hgg' : ∀ x ∈ Ioo (min (f a) (f b)) (max (f a) (f b)), HasDerivWithinAt g (g' x) (Ioi x) x<VAR>hg' : ContinuousOn g' (f '' [[a, b]])<GOAL>g (f b) - g (f a) = (g ∘ f) b - (g ∘ f) a
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>f✝¹ : ℝ → E<VAR>g'✝ g✝ φ : ℝ → ℝ<VAR>a b : ℝ<VAR>inst✝² : CompleteSpace E<VAR>f✝ f'✝ : ℝ → E<VAR>G : Type u_6<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace ℝ G<VAR>f f' : ℝ → ℝ<VAR>g g' : ℝ → E<VAR>hf : ContinuousOn f [[a, b]]<VAR>hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Ioi x) x<VAR>hf' : ContinuousOn f' [[a, b]]<VAR>hg : ContinuousOn g [[f a, f b]]<VAR>hgg' : ∀ x ∈ Ioo (min (f a) (f b)) (max (f a) (f b)), HasDerivWithinAt g (g' x) (Ioi x) x<VAR>hg' : ContinuousOn g' (f '' [[a, b]])<GOAL>[[f a, f b]] ⊆ f '' [[a, b]]
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>s t : Set α<VAR>a : α<VAR>hs : s.Finite<VAR>ht : t.Finite<GOAL>hs.toFinset.Nonempty ↔ s.Nonempty
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>a : Ordinal.{u_3}<GOAL>a < 1 ↔ a = 0
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : AddCommGroup β<VAR>f : α → β<VAR>x : α<GOAL>(lift f) (of x) = f x
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : AddCommGroup β<VAR>f : α → β<VAR>x : α<VAR>e_1✝ : β = Multiplicative β<GOAL>f x = (FreeGroup.lift f) (FreeGroup.of x)
<VAR>n : ℕ<VAR>a : ℝ<VAR>h : 2 - ((a - 1 / 4 ^ n) / 2 ^ (n + 1)) ^ 2 ≤ (↑0 / ↑1).sqrtTwoAddSeries n<VAR>h₂ : 1 / 4 ^ n ≤ a<GOAL>π < a
<VAR>n : ℕ<VAR>a : ℝ<VAR>h : 2 - ((a - 1 / 4 ^ n) / 2 ^ (n + 1)) ^ 2 ≤ (↑0 / ↑1).sqrtTwoAddSeries n<VAR>h₂ : 1 / 4 ^ n ≤ a<GOAL>2 ^ (n + 1) * √(2 - sqrtTwoAddSeries 0 n) + 1 / 4 ^ n ≤ a
<VAR>n : ℕ<VAR>a : ℝ<VAR>h : 2 - ((a - 1 / 4 ^ n) / 2 ^ (n + 1)) ^ 2 ≤ (↑0 / ↑1).sqrtTwoAddSeries n<VAR>h₂ : 1 / 4 ^ n ≤ a<GOAL>2 - ((a - 1 / 4 ^ n) / 2 ^ (n + 1)) ^ 2 ≤ sqrtTwoAddSeries 0 n
<VAR>n : ℕ<VAR>a : ℝ<VAR>h : 2 - ((a - 1 / 4 ^ n) / 2 ^ (n + 1)) ^ 2 ≤ (↑0 / ↑1).sqrtTwoAddSeries n<VAR>h₂ : 1 / 4 ^ n ≤ a<GOAL>0 ≤ (a - 1 / 4 ^ n) / 2 ^ (n + 1)
<VAR>n : ℕ<VAR>a : ℝ<VAR>h : 2 - ((a - 1 / 4 ^ n) / 2 ^ (n + 1)) ^ 2 ≤ (↑0 / ↑1).sqrtTwoAddSeries n<VAR>h₂ : 1 / 4 ^ n ≤ a<GOAL>0 < 2 ^ (n + 1)
<VAR>x✝ y z : ℝ<VAR>n : ℕ<VAR>x t : ℝ<VAR>h1 : 0 < x<VAR>h2 : x ≤ 1<VAR>ht : 0 < t<GOAL>|log x * x ^ t| < 1 / t
<VAR>x✝ y z : ℝ<VAR>n : ℕ<VAR>x t : ℝ<VAR>h1 : 0 < x<VAR>h2 : x ≤ 1<VAR>ht : 0 < t<GOAL>|log x * x ^ t| * t < 1
<VAR>x✝ y z : ℝ<VAR>n : ℕ<VAR>x t : ℝ<VAR>h1 : 0 < x<VAR>h2 : x ≤ 1<VAR>ht : 0 < t<VAR>this : |log (x ^ t) * x ^ t| < 1<GOAL>|log x * x ^ t| * t < 1
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>inst✝² : NonAssocSemiring R<VAR>M : Submonoid R<VAR>inst✝¹ : NonAssocSemiring S<VAR>inst✝ : NonAssocSemiring T<VAR>f : R ≃+* S<VAR>K : Subsemiring R<VAR>x : S<GOAL>x ∈ map (↑f) K ↔ f.symm x ∈ K
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝³ : SemilatticeInf α<VAR>inst✝² : SemilatticeInf β<VAR>inst✝¹ : FunLike F α β<VAR>inst✝ : InfHomClass F α β<VAR>s✝ s₁ s₂ t✝ t₁ t₂ u v : Set α<VAR>a b c : α<VAR>s t : Set α<VAR>this : (uncurry fun x x_1 => x ⊓ x_1) '' s ×ˢ t = image2 (fun x x_1 => x ⊓ x_1) s t<GOAL>(uncurry fun x x_1 => x ⊓ x_1) '' s ×ˢ t = s ⊼ t
<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✝¹⁰ : Semiring R<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : AddCommMonoid M'<VAR>inst✝⁷ : AddCommMonoid 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>inst✝³ : Semiring K<VAR>inst✝² : SMulWithZero R K<VAR>inst✝¹ : Module K M<VAR>inst✝ : IsScalarTower R K M<VAR>hinj : Injective fun r => r • 1<VAR>li : LinearIndependent K v<GOAL>LinearIndependent R v
<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✝¹⁰ : Semiring R<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : AddCommMonoid M'<VAR>inst✝⁷ : AddCommMonoid 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>inst✝³ : Semiring K<VAR>inst✝² : SMulWithZero R K<VAR>inst✝¹ : Module K M<VAR>inst✝ : IsScalarTower R K M<VAR>hinj : Injective fun r => r • 1<VAR>li : LinearIndependent K v<VAR>s : Finset ι<VAR>g : ι → R<VAR>hg : ∑ i ∈ s, g i • v i = 0<VAR>i : ι<VAR>hi : i ∈ s<GOAL>(fun r => r • 1) (g i) = (fun r => r • 1) 0
<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✝¹⁰ : Semiring R<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : AddCommMonoid M'<VAR>inst✝⁷ : AddCommMonoid 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>inst✝³ : Semiring K<VAR>inst✝² : SMulWithZero R K<VAR>inst✝¹ : Module K M<VAR>inst✝ : IsScalarTower R K M<VAR>hinj : Injective fun r => r • 1<VAR>li : LinearIndependent K v<VAR>s : Finset ι<VAR>g : ι → R<VAR>hg : ∑ i ∈ s, g i • v i = 0<VAR>i : ι<VAR>hi : i ∈ s<GOAL>g i • 1 = 0 • 1
<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✝¹⁰ : Semiring R<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : AddCommMonoid M'<VAR>inst✝⁷ : AddCommMonoid 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>inst✝³ : Semiring K<VAR>inst✝² : SMulWithZero R K<VAR>inst✝¹ : Module K M<VAR>inst✝ : IsScalarTower R K M<VAR>hinj : Injective fun r => r • 1<VAR>li : LinearIndependent K v<VAR>s : Finset ι<VAR>g : ι → R<VAR>hg : ∑ i ∈ s, g i • v i = 0<VAR>i : ι<VAR>hi : i ∈ s<GOAL>g i • 1 = 0
<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✝¹⁰ : Semiring R<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : AddCommMonoid M'<VAR>inst✝⁷ : AddCommMonoid 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>inst✝³ : Semiring K<VAR>inst✝² : SMulWithZero R K<VAR>inst✝¹ : Module K M<VAR>inst✝ : IsScalarTower R K M<VAR>hinj : Injective fun r => r • 1<VAR>li : LinearIndependent K v<VAR>s : Finset ι<VAR>g : ι → R<VAR>hg : ∑ i ∈ s, g i • v i = 0<VAR>i : ι<VAR>hi : i ∈ s<GOAL>∑ i ∈ s, (fun x => g x • 1) i • v i = 0
<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✝¹⁰ : Semiring R<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : AddCommMonoid M'<VAR>inst✝⁷ : AddCommMonoid 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>inst✝³ : Semiring K<VAR>inst✝² : SMulWithZero R K<VAR>inst✝¹ : Module K M<VAR>inst✝ : IsScalarTower R K M<VAR>hinj : Injective fun r => r • 1<VAR>li : LinearIndependent K v<VAR>s : Finset ι<VAR>g : ι → R<VAR>hg : ∑ i ∈ s, g i • v i = 0<VAR>i : ι<VAR>hi : i ∈ s<GOAL>∑ x ∈ s, g x • v x = 0
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : IsDomain R<VAR>inst✝⁴ : IsPrincipalIdealRing R<VAR>M : Type u_3<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>b : ι → M<VAR>inst✝¹ : _root_.Finite ι<VAR>s : ι → M<VAR>hs : span R (range s) = ⊤<VAR>inst✝ : NoZeroSMulDivisors R M<GOAL>Free R M
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : IsDomain R<VAR>inst✝⁴ : IsPrincipalIdealRing R<VAR>M : Type u_3<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>b : ι → M<VAR>inst✝¹ : _root_.Finite ι<VAR>s : ι → M<VAR>hs : span R (range s) = ⊤<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>val✝ : Fintype ι<GOAL>Free R M
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : IsDomain R<VAR>inst✝⁴ : IsPrincipalIdealRing R<VAR>M : Type u_3<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>b✝ : ι → M<VAR>inst✝¹ : _root_.Finite ι<VAR>s : ι → M<VAR>hs : span R (range s) = ⊤<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>val✝ : Fintype ι<VAR>n : ℕ<VAR>b : Basis (Fin n) R M<GOAL>Free R M
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : DecidableEq γ<VAR>g : β → γ<VAR>f : α →ₛ β<GOAL>↑(map g f).range = ↑(Finset.image g f.range)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝³ : LinearOrderedRing α<VAR>inst✝² : LinearOrderedAddCommGroup β<VAR>inst✝¹ : Module α β<VAR>inst✝ : OrderedSMul α β<VAR>f : ι → α<VAR>g : ι → β<VAR>s : Set ι<VAR>a a₁ a₂ : α<VAR>b b₁ b₂ : β<VAR>i : ι<VAR>x✝¹ : i ∈ s<VAR>j : ι<VAR>x✝ : j ∈ s<GOAL>0 ≤ (f j - f i) • (g j - g i) ↔ f i • g j + f j • g i ≤ f i • g i + f j • g j
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>x : 𝕎 R<VAR>n : ℕ<GOAL>x.frobeniusFun.coeff n = (aeval x.coeff) (frobeniusPoly p n)
<VAR>R✝ : Type u<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Semiring A<VAR>f : R →+* A<VAR>h : Function.Injective ⇑f<VAR>q : ℕ<VAR>hprime : Nat.Prime q<VAR>hchar✝ : CharP R q<GOAL>ExpChar A q
<VAR>R✝ : Type u<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Semiring A<VAR>f : R →+* A<VAR>h : Function.Injective ⇑f<VAR>q : ℕ<VAR>hprime : Nat.Prime q<VAR>hchar✝ : CharP R q<VAR>this : CharP A q<GOAL>ExpChar A q
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν : Measure α<VAR>s✝ t✝ s t : SignedMeasure α<VAR>μ : Measure α<VAR>inst✝¹ : s.HaveLebesgueDecomposition μ<VAR>inst✝ : t.HaveLebesgueDecomposition μ<GOAL>(s + t).singularPart μ = s.singularPart μ + t.singularPart μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν : Measure α<VAR>s✝ t✝ s t : SignedMeasure α<VAR>μ : Measure α<VAR>inst✝¹ : s.HaveLebesgueDecomposition μ<VAR>inst✝ : t.HaveLebesgueDecomposition μ<GOAL>s + t = s.singularPart μ + t.singularPart μ + μ.withDensityᵥ (s.rnDeriv μ + t.rnDeriv μ)
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Linear R C<VAR>K L M : CochainComplex C ℤ<VAR>n : ℤ<VAR>γ : Cocycle K L n<VAR>a n' : ℤ<VAR>hn' : n + a = n'<GOAL>δ n' (n' + 1) ((↑γ).leftShift a n' hn') = 0
<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>x : X<VAR>p : Y → Prop<VAR>hx : x ∈ e.source<GOAL>(∀ᶠ (y : Y) in 𝓝 (↑e x), p y) ↔ ∀ᶠ (b : Y) in map (↑e) (𝓝 x), p b
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>a b : α<GOAL>some ⁻¹' Ioo ↑a ↑b = Ioo a b
<VAR>α : Type u_1<VAR>𝕜✝ : Type u_2<VAR>inst✝¹⁶ : NontriviallyNormedField 𝕜✝<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>H : Type u_6<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>inst✝⁹ : NormedAddCommGroup H<VAR>inst✝⁸ : NormedSpace 𝕜✝ H<VAR>𝕝 : Type u_7<VAR>inst✝⁷ : NontriviallyNormedField 𝕝<VAR>inst✝⁶ : NormedAlgebra 𝕜✝ 𝕝<VAR>A✝ : Type u_8<VAR>inst✝⁵ : NormedRing A✝<VAR>inst✝⁴ : NormedAlgebra 𝕜✝ A✝<VAR>𝕜 : Type u_10<VAR>inst✝³ : NontriviallyNormedField 𝕜<VAR>A : Type u_9<VAR>inst✝² : NormedRing A<VAR>inst✝¹ : NormOneClass A<VAR>inst✝ : NormedAlgebra 𝕜 A<GOAL>(formalMultilinearSeries_geometric 𝕜 A).radius = 1