ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f : α → F<VAR>hq_pos : 0 < q<VAR>h0 : ¬p = 0<VAR>hp_top : ¬p = ⊤<GOAL>eLpNorm' (fun x => ‖f x‖ ^ q) p.toReal μ = eLpNorm' f (p * ENNReal.ofReal q).toReal μ ^ q
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f : α → F<VAR>hq_pos : 0 < q<VAR>h0 : ¬p = 0<VAR>hp_top : ¬p = ⊤<GOAL>p * ENNReal.ofReal q ≠ 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f : α → F<VAR>hq_pos : 0 < q<VAR>h0 : ¬p = 0<VAR>hp_top : ¬p = ⊤<GOAL>p * ENNReal.ofReal q ≠ ⊤
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f : α → F<VAR>hq_pos : 0 < q<VAR>h0 : ¬p = 0<VAR>hp_top : ¬p = ⊤<GOAL>eLpNorm' (fun x => ‖f x‖ ^ q) p.toReal μ = eLpNorm' f (p.toReal * q) μ ^ q
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : SuccOrder α<VAR>a b : α<VAR>h : a < succ b<GOAL>Ioc a (succ b) = insert (succ b) (Ioc a b)
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ✝ : Measure Ω<VAR>ℱ✝ : Filtration ℕ m0<VAR>f : ℕ → Ω → ℝ<VAR>ω : Ω<VAR>r : ℝ<VAR>R : ℝ≥0<VAR>s✝ : ℕ → Set Ω<VAR>ℱ : Filtration ℕ m0<VAR>μ : Measure Ω<VAR>s : ℕ → Set Ω<VAR>n : ℕ<GOAL>predictablePart (process s) ℱ μ n = ∑ k ∈ Finset.range n, μ[(s (k + 1)).indicator 1|↑ℱ k]
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ✝ : Measure Ω<VAR>ℱ✝ : Filtration ℕ m0<VAR>f : ℕ → Ω → ℝ<VAR>ω : Ω<VAR>r : ℝ<VAR>R : ℝ≥0<VAR>s✝ : ℕ → Set Ω<VAR>ℱ : Filtration ℕ m0<VAR>μ : Measure Ω<VAR>s : ℕ → Set Ω<VAR>n : ℕ<VAR>this : martingalePart (process s) ℱ μ n = ∑ k ∈ Finset.range n, ((s (k + 1)).indicator 1 - μ[(s (k + 1)).indicator 1|↑ℱ k])<GOAL>predictablePart (process s) ℱ μ n = ∑ k ∈ Finset.range n, μ[(s (k + 1)).indicator 1|↑ℱ k]
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ✝ : Measure Ω<VAR>ℱ✝ : Filtration ℕ m0<VAR>f : ℕ → Ω → ℝ<VAR>ω : Ω<VAR>r : ℝ<VAR>R : ℝ≥0<VAR>s✝ : ℕ → Set Ω<VAR>ℱ : Filtration ℕ m0<VAR>μ : Measure Ω<VAR>s : ℕ → Set Ω<VAR>n : ℕ<VAR>this : ∑ k ∈ Finset.range n, (s (k + 1)).indicator 1 - predictablePart (process s) ℱ μ n = ∑ k ∈ Finset.range n, (s (k + 1)).indicator 1 - ∑ x ∈ Finset.range n, μ[(s (x + 1)).indicator 1|↑ℱ x]<GOAL>predictablePart (process s) ℱ μ n = ∑ k ∈ Finset.range n, μ[(s (k + 1)).indicator 1|↑ℱ k]
<VAR>R : Type u<VAR>S : Type u_1<VAR>A : Type v<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : CommRing S<VAR>inst✝⁶ : Ring A<VAR>inst✝⁵ : Algebra R A<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : Algebra S A<VAR>inst✝² : IsScalarTower R S A<VAR>K : Type u_2<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra R K<VAR>x : K<VAR>hx : ¬x = 0<VAR>this : Invertible x := invertibleOfNonzero hx<GOAL>IsAlgebraic R x⁻¹ ↔ IsAlgebraic R x
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>X : Type u_5<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : Monoid M<VAR>inst✝ : ContinuousMul M<VAR>s t : Set M<VAR>hs : IsCompact s<VAR>ht : IsCompact t<GOAL>IsCompact (s * t)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>X : Type u_5<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : Monoid M<VAR>inst✝ : ContinuousMul M<VAR>s t : Set M<VAR>hs : IsCompact s<VAR>ht : IsCompact t<GOAL>IsCompact ((fun x => x.1 * x.2) '' s ×ˢ t)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : Seq α<VAR>n : ℕ<GOAL>(↑s).drop (n + 1) = ↑(s.drop (n + 1))
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : Seq α<VAR>n : ℕ<GOAL>((↑s).drop n).tail = ↑(s.drop n).tail
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>G : D ⥤ C<VAR>adj : CoreHomEquiv F G<VAR>X' X : C<VAR>Y Y' : D<VAR>f : X' ⟶ X<VAR>g : F.obj X ⟶ Y<GOAL>(adj.homEquiv X' Y) (F.map f ≫ g) = f ≫ (adj.homEquiv X Y) g
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>G : D ⥤ C<VAR>adj : CoreHomEquiv F G<VAR>X' X : C<VAR>Y Y' : D<VAR>f : X' ⟶ X<VAR>g : F.obj X ⟶ Y<GOAL>F.map f ≫ g = (adj.homEquiv X' Y).symm (f ≫ (adj.homEquiv X Y) g)
<VAR>R : Type u_1<VAR>inst✝¹ : CommMonoid R<VAR>R' : Type u_2<VAR>inst✝ : CommMonoidWithZero R'<VAR>a : R<VAR>ha : ¬IsUnit a<GOAL>(↑{ toFun := fun x => if IsUnit x then 1 else 0, map_one' := ⋯, map_mul' := ⋯ }).toFun a = 0
<VAR>R : Type u_1<VAR>inst✝¹ : CommMonoid R<VAR>R' : Type u_2<VAR>inst✝ : CommMonoidWithZero R'<GOAL>(if IsUnit 1 then 1 else 0) = 1
<VAR>R : Type u_1<VAR>inst✝¹ : CommMonoid R<VAR>R' : Type u_2<VAR>inst✝ : CommMonoidWithZero R'<VAR>x y : R<GOAL>{ toFun := fun x => if IsUnit x then 1 else 0, map_one' := ⋯ }.toFun (x * y) = { toFun := fun x => if IsUnit x then 1 else 0, map_one' := ⋯ }.toFun x * { toFun := fun x => if IsUnit x then 1 else 0, map_one' := ⋯ }.toFun y
<VAR>α : Type u_1<VAR>x : α<VAR>xs : List α<VAR>i : Nat<VAR>h : i + 1 < (x :: xs).length<GOAL>((x :: xs).eraseIdx (i + 1)).length = (x :: xs).length - 1
<VAR>α : Type u_1<VAR>x : α<VAR>xs : List α<VAR>i : Nat<VAR>h : i + 1 < (x :: xs).length<VAR>this : i < xs.length<GOAL>((x :: xs).eraseIdx (i + 1)).length = (x :: xs).length - 1
<VAR>α : Type u_1<VAR>x : α<VAR>xs : List α<VAR>i : Nat<VAR>h : i + 1 < (x :: xs).length<VAR>this : i < xs.length<GOAL>(xs.eraseIdx i).length + 1 = xs.length
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>inst✝³ : Group G<VAR>inst✝² : Group G'<VAR>H K L : Subgroup G<VAR>inst✝¹ : Finite ↑(commutatorSet G)<VAR>inst✝ : Group.FG G<GOAL>(center G).index ≤ Nat.card ↑(commutatorSet G) ^ Group.rank G
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>inst✝³ : Group G<VAR>inst✝² : Group G'<VAR>H K L : Subgroup G<VAR>inst✝¹ : Finite ↑(commutatorSet G)<VAR>inst✝ : Group.FG G<VAR>S : Finset G<VAR>hS1 : S.card = Group.rank G<VAR>hS2 : closure ↑S = ⊤<GOAL>(center G).index ≤ Nat.card ↑(commutatorSet G) ^ Group.rank G
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>inst✝³ : Group G<VAR>inst✝² : Group G'<VAR>H K L : Subgroup G<VAR>inst✝¹ : Finite ↑(commutatorSet G)<VAR>inst✝ : Group.FG G<VAR>S : Finset G<VAR>hS1 : S.card = Group.rank G<VAR>hS2 : closure ↑S = ⊤<GOAL>(center G).index ≤ Nat.card (↑↑S → ↑(commutatorSet G))
<VAR>α✝ : Type u<VAR>β✝ : Type u_1<VAR>γ : Type u_2<VAR>r✝ : α✝ → α✝ → Prop<VAR>s✝ : β✝ → β✝ → Prop<VAR>t : γ → γ → Prop<VAR>α β : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>inst✝¹ : IsWellOrder α r<VAR>inst✝ : IsWellOrder β s<VAR>f : r ≺i s<VAR>x✝ : ↑{b | s b f.top}<VAR>a : β<VAR>h : a ∈ {b | s b f.top}<GOAL>∃ a_1, (RelEmbedding.codRestrict {b | s b f.top} { toRelEmbedding := f.toRelEmbedding, init' := ⋯ }.toRelEmbedding ⋯) a_1 = ⟨a, h⟩
<VAR>α✝ : Type u<VAR>β✝ : Type u_1<VAR>γ : Type u_2<VAR>r✝ : α✝ → α✝ → Prop<VAR>s✝ : β✝ → β✝ → Prop<VAR>t : γ → γ → Prop<VAR>α β : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>inst✝¹ : IsWellOrder α r<VAR>inst✝ : IsWellOrder β s<VAR>f : r ≺i s<VAR>x✝ : ↑{b | s b f.top}<VAR>b : α<VAR>h : f.toRelEmbedding b ∈ {b | s b f.top}<GOAL>∃ a, (RelEmbedding.codRestrict {b | s b f.top} { toRelEmbedding := f.toRelEmbedding, init' := ⋯ }.toRelEmbedding ⋯) a = ⟨f.toRelEmbedding b, h⟩
<VAR>R : Type u_1<VAR>C : Type u_2<VAR>inst✝³ : Semiring R<VAR>inst✝² : Category.{u_3, u_2} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : Linear R C<VAR>S₁ S₂ : ShortComplex C<VAR>φ φ' : S₁ ⟶ S₂<VAR>h₁ : S₁.RightHomologyData<VAR>h₂ : S₂.RightHomologyData<VAR>a : R<VAR>γ : RightHomologyMapData φ h₁ h₂<GOAL>opcyclesMap' (a • φ) h₁ h₂ = a • opcyclesMap' φ h₁ h₂
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f : α → β → β<VAR>op : α → α → α<VAR>inst✝¹ : Monoid α<VAR>inst✝ : Monoid β<VAR>s : Multiset α<VAR>a : α<VAR>comm : {x | x ∈ a ::ₘ s}.Pairwise Commute<GOAL>(a ::ₘ s).noncommProd comm = a * s.noncommProd ⋯
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f : α → β → β<VAR>op : α → α → α<VAR>inst✝¹ : Monoid α<VAR>inst✝ : Monoid β<VAR>a : α<VAR>a✝ : List α<VAR>comm : {x | x ∈ a ::ₘ ⟦a✝⟧}.Pairwise Commute<GOAL>(a ::ₘ ⟦a✝⟧).noncommProd comm = a * noncommProd ⟦a✝⟧ ⋯
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>t u v w : V<VAR>p : G.Walk u v<VAR>p' : G.Walk v w<GOAL>t ∈ (p.append p').support ↔ t ∈ p.support ∨ t ∈ p'.support
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>t u v w : V<VAR>p : G.Walk u v<VAR>p' : G.Walk v w<GOAL>t = u ∨ t ∈ p.support.tail ∨ t ∈ p'.support.tail ↔ (t = u ∨ t ∈ p.support.tail) ∨ t = v ∨ t ∈ p'.support.tail
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>p : β → Prop<VAR>s : β → Set (α × α)<VAR>h : (𝓤 α).HasBasis p s<VAR>t : Set (α × α)<GOAL>(∃ i, p i ∧ s i ⊆ t) ↔ ∃ i, p i ∧ ∀ (a b : α), (a, b) ∈ s i → (a, b) ∈ t
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>n : ℕ<VAR>inst✝ : Group G<VAR>A : Rep k G<VAR>f : (Fin n → G) → CoeSort.coe A<VAR>g : Fin (n + 1) → G<VAR>a : Fin (n + 1)<GOAL>((diagonalHomEquiv n A).symm f).hom (Finsupp.single (Fin.partialProd g ∘ a.succ.succAbove) 1) = f (a.contractNth (fun x x_1 => x * x_1) g)
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>n : ℕ<VAR>inst✝ : Group G<VAR>A : Rep k G<VAR>f : (Fin n → G) → CoeSort.coe A<VAR>g : Fin (n + 1) → G<VAR>a : Fin (n + 1)<GOAL>(f fun i => (Fin.partialProd g (a.succ.succAbove i.castSucc))⁻¹ * (Fin.partialProd g (a.succAbove i).castSucc * g (a.succAbove i))) = f (a.contractNth (fun x x_1 => x * x_1) g)
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>n : ℕ<VAR>inst✝ : Group G<VAR>A : Rep k G<VAR>f : (Fin n → G) → CoeSort.coe A<VAR>g : Fin (n + 1) → G<VAR>a : Fin (n + 1)<VAR>x✝ : Fin n<GOAL>(Fin.partialProd g (a.succ.succAbove x✝.castSucc))⁻¹ * (Fin.partialProd g (a.succAbove x✝).castSucc * g (a.succAbove x✝)) = a.contractNth (fun x x_1 => x * x_1) g x✝
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>a b : R<VAR>s : S<VAR>inst✝⁵ : SMul R M<VAR>inst✝⁴ : SMul R S<VAR>inst✝³ : SMul S M<VAR>inst✝² : IsScalarTower R S M<VAR>inst✝¹ : Mul R<VAR>inst✝ : IsScalarTower R R M<VAR>ab : IsSMulRegular M (a * b)<GOAL>IsSMulRegular M b
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>a b : R<VAR>s : S<VAR>inst✝⁵ : SMul R M<VAR>inst✝⁴ : SMul R S<VAR>inst✝³ : SMul S M<VAR>inst✝² : IsScalarTower R S M<VAR>inst✝¹ : Mul R<VAR>inst✝ : IsScalarTower R R M<VAR>ab : IsSMulRegular M (a • b)<GOAL>IsSMulRegular M b
<VAR>n : Int<VAR>d : Nat<GOAL>-mkRat n d = mkRat (-n) d
<VAR>E : Type u_1<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : TopologicalSpace E<VAR>inst✝⁴ : TopologicalAddGroup E<VAR>inst✝³ : T2Space E<VAR>inst✝² : Module ℝ E<VAR>inst✝¹ : ContinuousSMul ℝ E<VAR>inst✝ : FiniteDimensional ℝ E<VAR>R : ℝ<VAR>s : Set E<VAR>x : E<VAR>hR : 0 < R<VAR>hs : IsClosed s<VAR>h : s ⊆ ball x R<GOAL>∃ r ∈ Ioo 0 R, s ⊆ ball x r
<VAR>E : Type u_1<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : TopologicalSpace E<VAR>inst✝⁴ : TopologicalAddGroup E<VAR>inst✝³ : T2Space E<VAR>inst✝² : Module ℝ E<VAR>inst✝¹ : ContinuousSMul ℝ E<VAR>inst✝ : FiniteDimensional ℝ E<VAR>R : ℝ<VAR>s : Set E<VAR>x : E<VAR>hR : 0 < R<VAR>hs : IsClosed s<VAR>h : ⇑toEuclidean '' s ⊆ Metric.ball (toEuclidean x) R<GOAL>∃ r ∈ Ioo 0 R, s ⊆ ball x r
<VAR>E : Type u_1<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : TopologicalSpace E<VAR>inst✝⁴ : TopologicalAddGroup E<VAR>inst✝³ : T2Space E<VAR>inst✝² : Module ℝ E<VAR>inst✝¹ : ContinuousSMul ℝ E<VAR>inst✝ : FiniteDimensional ℝ E<VAR>R : ℝ<VAR>s : Set E<VAR>x : E<VAR>hR : 0 < R<VAR>hs : IsClosed s<VAR>h : ⇑toEuclidean '' s ⊆ Metric.ball (toEuclidean x) R<VAR>r : ℝ<VAR>hr : r ∈ Ioo 0 R<VAR>hsr : ⇑toEuclidean '' s ⊆ Metric.ball (toEuclidean x) r<GOAL>∃ r ∈ Ioo 0 R, s ⊆ ball x r
<VAR>n m : ℕ<VAR>p i : Fin (n + 1)<VAR>h : i ≤ p<VAR>hp : p ≠ last n<VAR>hi : optParam (i ≠ last n) ⋯<GOAL>(p.castPred hp).predAbove i = i.castPred hi
<VAR>N : Type u_1<VAR>X : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>x : X<VAR>inst✝ : DecidableEq N<VAR>i : N<VAR>p : Ω (↑(Ω^ { j // j ≠ i } X x)) const<VAR>y : N → ↑I<VAR>j : N<VAR>Hj : y j = 0 ∨ y j = 1<GOAL>(({ toFun := Subtype.val, continuous_toFun := ⋯ }.comp p.toContinuousMap).uncurry.comp (Cube.splitAt i).toContinuousMap) y = x
<VAR>N : Type u_1<VAR>X : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>x : X<VAR>inst✝ : DecidableEq N<VAR>i : N<VAR>p : Ω (↑(Ω^ { j // j ≠ i } X x)) const<VAR>y : N → ↑I<VAR>j : N<VAR>Hj : y j = 0 ∨ y j = 1<GOAL>(↑(p.toContinuousMap (y i)) fun j => y ↑j) = x
<VAR>N : Type u_1<VAR>X : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>x : X<VAR>inst✝ : DecidableEq N<VAR>y : N → ↑I<VAR>j : N<VAR>Hj : y j = 0 ∨ y j = 1<VAR>p : Ω (↑(Ω^ { j_1 // j_1 ≠ j } X x)) const<GOAL>(↑(p.toContinuousMap (y j)) fun j_1 => y ↑j_1) = x
<VAR>N : Type u_1<VAR>X : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>x : X<VAR>inst✝ : DecidableEq N<VAR>i : N<VAR>p : Ω (↑(Ω^ { j // j ≠ i } X x)) const<VAR>y : N → ↑I<VAR>j : N<VAR>Hj : y j = 0 ∨ y j = 1<VAR>Hne : j ≠ i<GOAL>(↑(p.toContinuousMap (y i)) fun j => y ↑j) = x
<VAR>ι : Sort u_1<VAR>κ : ι → Sort u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : TopologicalSpace β<VAR>s t : Set α<VAR>a x y : α<VAR>inst✝¹ : AlexandrovDiscrete α<VAR>inst✝ : AlexandrovDiscrete β<GOAL>IsOpen s ↔ ∀ (x y : α), x ⤳ y → y ∈ s → x ∈ s
<VAR>ι : Sort u_1<VAR>κ : ι → Sort u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : TopologicalSpace β<VAR>s t : Set α<VAR>a x y : α<VAR>inst✝¹ : AlexandrovDiscrete α<VAR>inst✝ : AlexandrovDiscrete β<VAR>hs : ∀ (x y : α), x ⤳ y → y ∈ s → x ∈ s<GOAL>IsOpen s
<VAR>ι : Sort u_1<VAR>κ : ι → Sort u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : TopologicalSpace β<VAR>s t : Set α<VAR>a x y : α<VAR>inst✝¹ : AlexandrovDiscrete α<VAR>inst✝ : AlexandrovDiscrete β<VAR>hs : ∀ (x y : α), exterior {x} ⊆ exterior {y} → y ∈ s → x ∈ s<GOAL>IsOpen s
<VAR>ι : Sort u_1<VAR>κ : ι → Sort u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : TopologicalSpace β<VAR>s t : Set α<VAR>a x y : α<VAR>inst✝¹ : AlexandrovDiscrete α<VAR>inst✝ : AlexandrovDiscrete β<VAR>hs : ∀ (x y : α), exterior {x} ⊆ exterior {y} → y ∈ s → x ∈ s<GOAL>∀ x ∈ s, ∃ t ⊆ s, IsOpen t ∧ x ∈ t
<VAR>ι : Sort u_1<VAR>κ : ι → Sort u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : TopologicalSpace β<VAR>s t : Set α<VAR>a✝ x y : α<VAR>inst✝¹ : AlexandrovDiscrete α<VAR>inst✝ : AlexandrovDiscrete β<VAR>hs : ∀ (x y : α), exterior {x} ⊆ exterior {y} → y ∈ s → x ∈ s<VAR>a : α<VAR>ha : a ∈ s<GOAL>∃ t ⊆ s, IsOpen t ∧ a ∈ t
<VAR>ι : Sort u_1<VAR>κ : ι → Sort u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : TopologicalSpace β<VAR>s t : Set α<VAR>a✝ x y : α<VAR>inst✝¹ : AlexandrovDiscrete α<VAR>inst✝ : AlexandrovDiscrete β<VAR>hs : ∀ (x y : α), exterior {x} ⊆ exterior {y} → y ∈ s → x ∈ s<VAR>a : α<VAR>ha : a ∈ s<VAR>b : α<VAR>hb : b ∈ exterior {a}<GOAL>exterior {b} ⊆ exterior {a}
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type uX<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>m n✝ : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<VAR>hs : UniqueDiffOn 𝕜 s<VAR>hx : x ∈ s<GOAL>‖iteratedFDerivWithin 𝕜 n (fderivWithin 𝕜 f s) s x‖ = ‖iteratedFDerivWithin 𝕜 (n + 1) f s x‖
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s s' t : Set α<VAR>p : α → Prop<VAR>hp : NullMeasurableSet {x | p x} (μ.restrict s)<GOAL>(∀ᵐ (x : α) ∂μ.restrict s, p x) ↔ ∀ᵐ (x : α) ∂μ, x ∈ s → p x
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s s' t : Set α<VAR>p : α → Prop<VAR>hp : NullMeasurableSet {x | p x} (μ.restrict s)<GOAL>μ ({x | p x}ᶜ ∩ s) = 0 ↔ μ {x | x ∈ s → p x}ᶜ = 0
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s s' t : Set α<VAR>p : α → Prop<VAR>hp : NullMeasurableSet {x | p x} (μ.restrict s)<GOAL>(μ ({x | p x}ᶜ ∩ s) = 0) = (μ {x | x ∈ s → p x}ᶜ = 0)
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s s' t : Set α<VAR>p : α → Prop<VAR>hp : NullMeasurableSet {x | p x} (μ.restrict s)<VAR>x : α<GOAL>x ∈ {x | p x}ᶜ ∩ s ↔ x ∈ {x | x ∈ s → p x}ᶜ
<VAR>A : Type u_1<VAR>inst✝³ : AddCommGroup A<VAR>inst✝² : Module ℂ A<VAR>inst✝¹ : StarAddMonoid A<VAR>inst✝ : StarModule ℂ A<VAR>r : ℝ<GOAL>↑(ℑ ↑r) = ↑0
<VAR>R S : Type u<VAR>M : Type v<VAR>M' : Type v'<VAR>M₁ : Type v<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : CommRing S<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₁<GOAL>finrank R (ULift.{u_2, v} M) = finrank R M
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>D : Set ℝ<VAR>hD : Convex ℝ D<VAR>f f' : ℝ → ℝ<VAR>hf : ContinuousOn f D<VAR>hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x<VAR>hf'₀ : ∀ x ∈ interior D, 0 < f' x<VAR>x : ℝ<VAR>hx : x ∈ interior D<GOAL>0 < deriv f x
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>D : Set ℝ<VAR>hD : Convex ℝ D<VAR>f f' : ℝ → ℝ<VAR>hf : ContinuousOn f D<VAR>hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x<VAR>hf'₀ : ∀ x ∈ interior D, 0 < f' x<VAR>x : ℝ<VAR>hx : x ∈ interior D<GOAL>0 < f' x
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : StrictOrderedRing α<VAR>inst✝ : Archimedean α<VAR>x : α<VAR>this : (a : Prop) → Decidable a<GOAL>∃ fl, ∀ (z : ℤ), z ≤ fl ↔ ↑z ≤ x
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : StrictOrderedRing α<VAR>inst✝ : Archimedean α<VAR>x : α<VAR>this✝ : (a : Prop) → Decidable a<VAR>this : ∃ ub, ↑ub ≤ x ∧ ∀ (z : ℤ), ↑z ≤ x → z ≤ ub<GOAL>∃ fl, ∀ (z : ℤ), z ≤ fl ↔ ↑z ≤ x
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : StrictOrderedRing α<VAR>inst✝ : Archimedean α<VAR>x : α<VAR>this✝ : (a : Prop) → Decidable a<VAR>this : ∃ ub, ↑ub ≤ x ∧ ∀ (z : ℤ), ↑z ≤ x → z ≤ ub<VAR>fl : ℤ<VAR>h : ↑fl ≤ x ∧ ∀ (z : ℤ), ↑z ≤ x → z ≤ fl<VAR>z : ℤ<GOAL>z ≤ fl ↔ ↑z ≤ x
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : StrictOrderedRing α<VAR>inst✝ : Archimedean α<VAR>x : α<VAR>this✝ : (a : Prop) → Decidable a<VAR>this : ∃ ub, ↑ub ≤ x ∧ ∀ (z : ℤ), ↑z ≤ x → z ≤ ub<VAR>fl z : ℤ<VAR>h₁ : ↑fl ≤ x<VAR>h₂ : ∀ (z : ℤ), ↑z ≤ x → z ≤ fl<GOAL>z ≤ fl ↔ ↑z ≤ x
<VAR>C : Type u₁<VAR>inst✝³ : Category.{u₂, u₁} C<VAR>I : Type v₁<VAR>inst✝² : Category.{v₂, v₁} I<VAR>F : Iᵒᵖ ⥤ C<VAR>inst✝¹ : HasColimit F<VAR>inst✝ : HasLimitsOfShape I (Type u₂)<VAR>A : C<VAR>i : I<GOAL>(colimitHomIsoLimitYoneda' F A).hom ≫ limit.π (F.rightOp ⋙ yoneda.obj A) i = (coyoneda.map (colimit.ι F (op i)).op).app A
<VAR>C : Type u₁<VAR>inst✝³ : Category.{u₂, u₁} C<VAR>I : Type v₁<VAR>inst✝² : Category.{v₂, v₁} I<VAR>F : Iᵒᵖ ⥤ C<VAR>inst✝¹ : HasColimit F<VAR>inst✝ : HasLimitsOfShape I (Type u₂)<VAR>A : C<VAR>i : I<GOAL>(coyonedaOpColimitIsoLimitCoyoneda' F).hom.app A ≫ (limitObjIsoLimitCompEvaluation (F.rightOp ⋙ coyoneda) A).hom ≫ limit.π (F.rightOp ⋙ yoneda.obj A) i = (coyoneda.map (colimit.ι F (op i)).op).app A
<VAR>C : Type u₁<VAR>inst✝³ : Category.{u₂, u₁} C<VAR>I : Type v₁<VAR>inst✝² : Category.{v₂, v₁} I<VAR>F : Iᵒᵖ ⥤ C<VAR>inst✝¹ : HasColimit F<VAR>inst✝ : HasLimitsOfShape I (Type u₂)<VAR>A : C<VAR>i : I<GOAL>(coyonedaOpColimitIsoLimitCoyoneda' F).hom.app A ≫ (limit.π (F.rightOp ⋙ coyoneda) i).app A = (coyoneda.map (colimit.ι F (op i)).op).app A
<VAR>C : Type u₁<VAR>inst✝³ : Category.{u₂, u₁} C<VAR>I : Type v₁<VAR>inst✝² : Category.{v₂, v₁} I<VAR>F : Iᵒᵖ ⥤ C<VAR>inst✝¹ : HasColimit F<VAR>inst✝ : HasLimitsOfShape I (Type u₂)<VAR>A : C<VAR>i : I<GOAL>((coyonedaOpColimitIsoLimitCoyoneda' F).hom ≫ limit.π (F.rightOp ⋙ coyoneda) i).app A = (coyoneda.map (colimit.ι F (op i)).op).app A
<VAR>S : Type u_1<VAR>inst✝¹ : CommRing S<VAR>inst✝ : IsDomain S<VAR>P : Ideal S<VAR>i : ℕ<VAR>a d d' e e' : S<VAR>a_mem : a ∈ P ^ i<VAR>e_mem : e ∈ P ^ (i + 1)<VAR>e'_mem : e' ∈ P ^ (i + 1)<VAR>h : d - d' ∈ P<GOAL>a * d + e - (a * d' + e') ∈ P ^ (i + 1)
<VAR>S : Type u_1<VAR>inst✝¹ : CommRing S<VAR>inst✝ : IsDomain S<VAR>P : Ideal S<VAR>i : ℕ<VAR>a d d' e e' : S<VAR>a_mem : a ∈ P ^ i<VAR>e_mem : e ∈ P ^ (i + 1)<VAR>e'_mem : e' ∈ P ^ (i + 1)<VAR>h : d - d' ∈ P<VAR>this : a * d - a * d' ∈ P ^ (i + 1)<GOAL>a * d + e - (a * d' + e') ∈ P ^ (i + 1)
<VAR>S : Type u_1<VAR>inst✝¹ : CommRing S<VAR>inst✝ : IsDomain S<VAR>P : Ideal S<VAR>i : ℕ<VAR>a d d' e e' : S<VAR>a_mem : a ∈ P ^ i<VAR>e_mem : e ∈ P ^ (i + 1)<VAR>e'_mem : e' ∈ P ^ (i + 1)<VAR>h : d - d' ∈ P<VAR>this : a * d - a * d' ∈ P ^ (i + 1)<GOAL>a * d + e - (a * d' + e') = a * d - a * d' + (e - e')
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>a b c u v w : V<VAR>e : Sym2 V<VAR>G₁ G₂ : SimpleGraph V<GOAL>G.Adj a b ↔ ∃ e, ↑e = s(a, b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : EDist α<VAR>x y : α<VAR>s t : Set α<GOAL>s.einfsep = 0 ↔ ∀ C > 0, ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ edist x y < C
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace ℝ E<VAR>inst✝ : Fact (finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>a x : E<VAR>ha : ¬a = 0<GOAL>⟪a, x⟫_ℝ • o.areaForm a - (o.areaForm a) x • (innerₛₗ ℝ) a = ‖a‖ ^ 2 • o.areaForm x
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace ℝ E<VAR>inst✝ : Fact (finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>a x : E<VAR>ha : ¬a = 0<GOAL>∀ (i : Fin 2), (⟪a, x⟫_ℝ • o.areaForm a - (o.areaForm a) x • (innerₛₗ ℝ) a) ((o.basisRightAngleRotation a ha) i) = (‖a‖ ^ 2 • o.areaForm x) ((o.basisRightAngleRotation a ha) i)
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P : Fin 3 → R<GOAL>W'.dblU P = W'.a₁ * P y * P z - (3 * P x ^ 2 + 2 * W'.a₂ * P x * P z ^ 2 + W'.a₄ * P z ^ 4)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>s : Set α<VAR>inst✝ : MeasurableSingletonClass α<VAR>hsc : count s = 0<GOAL>s = ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>s : Set α<VAR>inst✝ : MeasurableSingletonClass α<VAR>hsc : count s = 0<VAR>hs : s.Finite<GOAL>s = ∅
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : ℝ × ℝ → E<VAR>B : ℝ × ℝ → ℝ × ℝ →L[ℝ] ℝ × ℝ := fun p => LinearMap.toContinuousLinearMap ((Matrix.toLin (Basis.finTwoProd ℝ) (Basis.finTwoProd ℝ)) !![cos p.2, -p.1 * sin p.2; sin p.2, p.1 * cos p.2])<GOAL>∫ (p : ℝ × ℝ) in polarCoord.target, p.1 • f (↑polarCoord.symm p) = ∫ (p : ℝ × ℝ), f p