ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>h : Differentiable 𝕜 fun y => -f y<GOAL>Differentiable 𝕜 f
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F✝ : Type u_3<VAR>inst✝¹ : SeminormedAddCommGroup F✝<VAR>inst✝ : NormedSpace ℝ F✝<VAR>F : Subspace 𝕜 E<VAR>hFc : IsClosed ↑F<VAR>hF : ∃ x, x ∉ F<VAR>r : ℝ<VAR>hr : r < 1<GOAL>∃ x₀ ∉ F, ∀ y ∈ F, r * ‖x₀‖ ≤ ‖x₀ - y‖
<VAR>α : Type u_1<VAR>inst✝ : Monoid α<VAR>s : Set α<GOAL>∀ (x : α), x ∈ 1 • s ↔ x ∈ s
<VAR>M : Type u_1<VAR>inst✝ : CommMonoid M<VAR>S : Submonoid M<VAR>hS : S ≤ IsUnit.submonoid M<VAR>x : ↥S<GOAL>↥S.leftInv
<VAR>M : Type u_1<VAR>inst✝ : CommMonoid M<VAR>S : Submonoid M<VAR>hS : S ≤ IsUnit.submonoid M<VAR>x : ↥S<VAR>x' : Mˣ<VAR>hx : ↑x' = ↑x<GOAL>↥S.leftInv
<VAR>M : Type u_1<VAR>inst✝ : CommMonoid M<VAR>S : Submonoid M<VAR>hS : S ≤ IsUnit.submonoid M<VAR>x : ↥S.leftInv<VAR>h : ∃ u, ↑u = ↑((↑S.fromCommLeftInv).toFun x)<GOAL>(Classical.choose h).inv = ↑x
<VAR>M : Type u_1<VAR>inst✝ : CommMonoid M<VAR>S : Submonoid M<VAR>hS : S ≤ IsUnit.submonoid M<VAR>x : ↥S.leftInv<VAR>h : ∃ u, ↑u = ↑((↑S.fromCommLeftInv).toFun x)<GOAL>(Classical.choose h).inv * ↑h.choose = ↑x * ↑h.choose
<VAR>M : Type u_1<VAR>inst✝ : CommMonoid M<VAR>S : Submonoid M<VAR>hS : S ≤ IsUnit.submonoid M<VAR>x : ↥S.leftInv<VAR>h : ∃ u, ↑u = ↑((↑S.fromCommLeftInv).toFun x)<GOAL>(Classical.choose h).inv * ↑h.choose = ↑x * ↑((↑S.fromCommLeftInv).toFun x)
<VAR>M : Type u_1<VAR>inst✝ : CommMonoid M<VAR>S : Submonoid M<VAR>hS : S ≤ IsUnit.submonoid M<VAR>x : ↥S<GOAL>↑(S.fromLeftInv ⟨(Classical.choose ⋯).inv, ⋯⟩) = ↑x
<VAR>M : Type u_1<VAR>inst✝ : CommMonoid M<VAR>S : Submonoid M<VAR>hS : S ≤ IsUnit.submonoid M<VAR>x : ↥S<GOAL>↑⟨(Classical.choose ⋯).inv, ⋯⟩ * ↑x = 1
<VAR>M : Type u_1<VAR>inst✝ : CommMonoid M<VAR>S : Submonoid M<VAR>hS : S ≤ IsUnit.submonoid M<VAR>x : ↥S<GOAL>↑x = ↑(Exists.choose ⋯)
<VAR>R : Type u_1<VAR>inst✝⁴ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝³ : CommSemiring S<VAR>inst✝² : Algebra R S<VAR>P : Type u_3<VAR>inst✝¹ : CommSemiring P<VAR>inst✝ : IsLocalization M S<VAR>x y : R<VAR>m : ↥M<GOAL>x • mk' S y m = mk' S (x * y) m
<VAR>R : Type u_1<VAR>inst✝⁴ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝³ : CommSemiring S<VAR>inst✝² : Algebra R S<VAR>P : Type u_3<VAR>inst✝¹ : CommSemiring P<VAR>inst✝ : IsLocalization M S<VAR>x y : R<VAR>m : ↥M<GOAL>x • mk' S y m = mk' S (x * y) (1 * m)
<VAR>α✝ : Type u_1<VAR>r : α✝ → α✝ → Prop<VAR>β α : Type u<VAR>f : β → α<VAR>θ : Cardinal.{u}<VAR>hθ : θ ≤ #β<VAR>h₁ : ℵ₀ ≤ θ<VAR>h₂ : #α < θ.ord.cof<GOAL>∃ a, θ ≤ #↑(f ⁻¹' {a})
<VAR>α✝ : Type u_1<VAR>r : α✝ → α✝ → Prop<VAR>β α : Type u<VAR>f : β → α<VAR>s : Set β<VAR>hθ : #↑s ≤ #β<VAR>h₁ : ℵ₀ ≤ #↑s<VAR>h₂ : #α < (#↑s).ord.cof<GOAL>∃ a, #↑s ≤ #↑(f ⁻¹' {a})
<VAR>α✝ : Type u_1<VAR>r : α✝ → α✝ → Prop<VAR>β α : Type u<VAR>f : β → α<VAR>s : Set β<VAR>hθ : #↑s ≤ #β<VAR>h₁ : ℵ₀ ≤ #↑s<VAR>h₂ : #α < (#↑s).ord.cof<VAR>a : α<VAR>ha : #↑(f ∘ Subtype.val ⁻¹' {a}) = #↑s<GOAL>∃ a, #↑s ≤ #↑(f ⁻¹' {a})
<VAR>α✝ : Type u_1<VAR>r : α✝ → α✝ → Prop<VAR>β α : Type u<VAR>f : β → α<VAR>s : Set β<VAR>hθ : #↑s ≤ #β<VAR>h₁ : ℵ₀ ≤ #↑s<VAR>h₂ : #α < (#↑s).ord.cof<VAR>a : α<VAR>ha : #↑(f ∘ Subtype.val ⁻¹' {a}) = #↑s<GOAL>#↑s ≤ #↑(f ⁻¹' {a})
<VAR>α✝ : Type u_1<VAR>r : α✝ → α✝ → Prop<VAR>β α : Type u<VAR>f : β → α<VAR>s : Set β<VAR>hθ : #↑s ≤ #β<VAR>h₁ : ℵ₀ ≤ #↑s<VAR>h₂ : #α < (#↑s).ord.cof<VAR>a : α<VAR>ha : #↑(f ∘ Subtype.val ⁻¹' {a}) = #↑s<GOAL>#↑(Subtype.val ⁻¹' (f ⁻¹' {a})) ≤ #↑(f ⁻¹' {a})
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : FirstCountableTopology X<VAR>inst✝ : R1Space X<VAR>x y : X<VAR>K L : Set X<VAR>hK : IsCompact K<VAR>hL : IsCompact L<VAR>h'L : IsClosed L<VAR>hd : Disjoint K L<GOAL>SeparatedNhds K L
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : FirstCountableTopology X<VAR>inst✝ : R1Space X<VAR>x y : X<VAR>K L : Set X<VAR>hK : IsCompact K<VAR>hL : IsCompact L<VAR>h'L : IsClosed L<VAR>hd : Disjoint K L<GOAL>∀ x ∈ K, ∀ x_1 ∈ L, ¬Inseparable x x_1
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : FirstCountableTopology X<VAR>inst✝ : R1Space X<VAR>x✝ y✝ : X<VAR>K L : Set X<VAR>hK : IsCompact K<VAR>hL : IsCompact L<VAR>h'L : IsClosed L<VAR>hd : Disjoint K L<VAR>x : X<VAR>hx : x ∈ K<VAR>y : X<VAR>hy : y ∈ L<VAR>h : Inseparable x y<GOAL>False
<VAR>R : Type u_1<VAR>inst✝³ : NonAssocRing R<VAR>inst✝² : Pow R ℕ<VAR>inst✝¹ : BinomialRing R<VAR>inst✝ : NatPowAssoc R<VAR>r : R<VAR>n k : ℕ<GOAL>(n + k).choose k • choose (r + ↑k) (n + k) = choose (r + ↑k) k * choose r n
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n : ℕ<VAR>b : ℤ√↑(Pell.d a1)<VAR>h1 : 1 ≤ b<VAR>hp : IsPell b<VAR>h : b ≤ pellZd a1 (n + 1)<VAR>a1p : 0 ≤ { re := ↑a, im := 1 }<GOAL>Pell.d a1 ≤ a * a
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n : ℕ<VAR>b : ℤ√↑(Pell.d a1)<VAR>h1 : 1 ≤ b<VAR>hp : IsPell b<VAR>h : b ≤ pellZd a1 (n + 1)<VAR>a1p : 0 ≤ { re := ↑a, im := 1 }<VAR>am1p : 0 ≤ { re := ↑a, im := -1 }<VAR>a1m : { re := ↑a, im := 1 } * { re := ↑a, im := -1 } = 1<VAR>ha : { re := ↑a, im := 1 } ≤ b<GOAL>{ re := ↑a, im := 1 } * { re := ↑a, im := -1 } ≤ b * { re := ↑a, im := -1 }
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n : ℕ<VAR>b : ℤ√↑(Pell.d a1)<VAR>h1 : 1 ≤ b<VAR>hp : IsPell b<VAR>h : b ≤ pellZd a1 (n + 1)<VAR>a1p : 0 ≤ { re := ↑a, im := 1 }<VAR>am1p : 0 ≤ { re := ↑a, im := -1 }<VAR>a1m : { re := ↑a, im := 1 } * { re := ↑a, im := -1 } = 1<VAR>ha : { re := ↑a, im := 1 } ≤ b<GOAL>b * { re := ↑a, im := -1 } ≤ pellZd a1 n
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n : ℕ<VAR>b : ℤ√↑(Pell.d a1)<VAR>h1 : 1 ≤ b<VAR>hp : IsPell b<VAR>h : b ≤ pellZd a1 (n + 1)<VAR>a1p : 0 ≤ { re := ↑a, im := 1 }<VAR>am1p : 0 ≤ { re := ↑a, im := -1 }<VAR>a1m : { re := ↑a, im := 1 } * { re := ↑a, im := -1 } = 1<VAR>ha : { re := ↑a, im := 1 } ≤ b<VAR>t : b * { re := ↑a, im := -1 } ≤ pellZd a1 (n + 1) * { re := ↑a, im := -1 }<GOAL>b * { re := ↑a, im := -1 } ≤ pellZd a1 n
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n : ℕ<VAR>b : ℤ√↑(Pell.d a1)<VAR>h1 : 1 ≤ b<VAR>hp : IsPell b<VAR>h : b ≤ pellZd a1 (n + 1)<VAR>a1p : 0 ≤ { re := ↑a, im := 1 }<VAR>am1p : 0 ≤ { re := ↑a, im := -1 }<VAR>a1m : { re := ↑a, im := 1 } * { re := ↑a, im := -1 } = 1<VAR>ha : { re := ↑a, im := 1 } ≤ b<VAR>m : ℕ<VAR>e : b * { re := ↑a, im := -1 } = pellZd a1 m<GOAL>b = pellZd a1 (m + 1)
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n : ℕ<VAR>a1p : 0 ≤ { re := ↑a, im := 1 }<VAR>am1p : 0 ≤ { re := ↑a, im := -1 }<VAR>a1m : { re := ↑a, im := 1 } * { re := ↑a, im := -1 } = 1<VAR>x y : ℤ<VAR>h1 : 1 ≤ { re := x, im := y }<VAR>hp : IsPell { re := x, im := y }<VAR>h : { re := x, im := y } ≤ pellZd a1 (n + 1)<VAR>ha : ¬{ re := ↑a, im := 1 } ≤ { re := x, im := y }<VAR>h1l : 1 < { re := x, im := y }<GOAL>False
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁶ : _root_.RCLike 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : InnerProductSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : InnerProductSpace ℝ F<VAR>V : Type u_4<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℂ V<VAR>T : V →ₗ[ℂ] V<VAR>x y : V<GOAL>⟪T x, y⟫_ℂ = (⟪T (x + y), x + y⟫_ℂ - ⟪T (x - y), x - y⟫_ℂ - Complex.I * ⟪T (x + Complex.I • y), x + Complex.I • y⟫_ℂ + Complex.I * ⟪T (x - Complex.I • y), x - Complex.I • y⟫_ℂ) / 4
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁶ : _root_.RCLike 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : InnerProductSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : InnerProductSpace ℝ F<VAR>V : Type u_4<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℂ V<VAR>T : V →ₗ[ℂ] V<VAR>x y : V<GOAL>⟪T x, y⟫_ℂ = (⟪T x, x⟫_ℂ + ⟪T y, x⟫_ℂ + (⟪T x, y⟫_ℂ + ⟪T y, y⟫_ℂ) - (⟪T x, x⟫_ℂ - (⟪T y, x⟫_ℂ + (⟪T x, y⟫_ℂ - ⟪T y, y⟫_ℂ)) + (Complex.I * ⟪T x, x⟫_ℂ + ⟪T y, x⟫_ℂ + (-⟪T x, y⟫_ℂ + Complex.I * ⟪T y, y⟫_ℂ))) + (Complex.I * ⟪T x, x⟫_ℂ - (⟪T y, x⟫_ℂ + (-⟪T x, y⟫_ℂ - Complex.I * ⟪T y, y⟫_ℂ)))) / 4
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x✝ : X<VAR>s s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<VAR>x : X<VAR>F : Filter X<GOAL>AccPt x F ↔ ClusterPt x (𝓟 {x}ᶜ ⊓ F)
<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>X : Type u_5<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : MeasurableSpace X<VAR>inst✝ : OpensMeasurableSpace X<VAR>f : X → E<VAR>hf : Continuous f<VAR>h'f : HasCompactSupport f<VAR>μ : Measure X<VAR>this✝¹ : MeasurableSpace E := borel E<VAR>this✝ : BorelSpace E<GOAL>Memℒp f ⊤ μ
<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>X : Type u_5<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : MeasurableSpace X<VAR>inst✝ : OpensMeasurableSpace X<VAR>f : X → E<VAR>hf : Continuous f<VAR>h'f : HasCompactSupport f<VAR>μ : Measure X<VAR>this✝¹ : MeasurableSpace E := borel E<VAR>this✝ : BorelSpace E<VAR>C : ℝ<VAR>hC : ∀ (x : X), ‖f x‖ ≤ C<GOAL>Memℒp f ⊤ μ
<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>X : Type u_5<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : MeasurableSpace X<VAR>inst✝ : OpensMeasurableSpace X<VAR>f : X → E<VAR>hf : Continuous f<VAR>h'f : HasCompactSupport f<VAR>μ : Measure X<VAR>this✝¹ : MeasurableSpace E := borel E<VAR>this✝ : BorelSpace E<VAR>C : ℝ<VAR>hC : ∀ (x : X), ‖f x‖ ≤ C<GOAL>AEStronglyMeasurable f μ
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f✝ : α → β<VAR>f : Set α → Set β<VAR>hf : Injective f<VAR>h2 : f ∅ = ∅<VAR>s : Set α<GOAL>(f s).Nonempty ↔ s.Nonempty
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : CommRing T<VAR>α : Type u_4<VAR>β : Type u_5<VAR>x y : 𝕎 R<GOAL>WittVector.ghostFun (x - y) = WittVector.ghostFun x - WittVector.ghostFun y
<VAR>J : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝² : Category.{v₂, u₂} K<VAR>C : Type u₂<VAR>inst✝¹ : Category.{u₁, u₂} C<VAR>inst✝ : IsPreconnected J<VAR>X Y : C<VAR>α : (Functor.const J).obj X ⟶ (Functor.const J).obj Y<VAR>x✝¹ x✝ : J<VAR>f : x✝¹ ⟶ x✝<GOAL>(fun j => α.app j) x✝¹ = (fun j => α.app j) x✝
<VAR>J : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝² : Category.{v₂, u₂} K<VAR>C : Type u₂<VAR>inst✝¹ : Category.{u₁, u₂} C<VAR>inst✝ : IsPreconnected J<VAR>X Y : C<VAR>α : (Functor.const J).obj X ⟶ (Functor.const J).obj Y<VAR>x✝¹ x✝ : J<VAR>f : x✝¹ ⟶ x✝<VAR>this : ((Functor.const J).obj X).map f ≫ α.app x✝ = α.app x✝¹ ≫ ((Functor.const J).obj Y).map f<GOAL>(fun j => α.app j) x✝¹ = (fun j => α.app j) x✝
<VAR>J : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝² : Category.{v₂, u₂} K<VAR>C : Type u₂<VAR>inst✝¹ : Category.{u₁, u₂} C<VAR>inst✝ : IsPreconnected J<VAR>X Y : C<VAR>α : (Functor.const J).obj X ⟶ (Functor.const J).obj Y<VAR>x✝¹ x✝ : J<VAR>f : x✝¹ ⟶ x✝<VAR>this : α.app x✝ = α.app x✝¹<GOAL>(fun j => α.app j) x✝¹ = (fun j => α.app j) x✝
<VAR>n : ℕ<VAR>A : Type u_1<VAR>R : Type u_2<VAR>inst✝⁵ : AddGroup A<VAR>inst✝⁴ : Ring R<VAR>α✝ : Type u_3<VAR>β✝ : Type u_4<VAR>inst✝³ : Group α✝<VAR>a✝ : α✝<VAR>inst✝² : MulAction α✝ β✝<VAR>b✝ : β✝<VAR>α : Type u_5<VAR>β : Type u_6<VAR>inst✝¹ : AddGroup α<VAR>a : α<VAR>inst✝ : AddAction α β<VAR>b : β<VAR>k : ℤ<GOAL>(orbitZMultiplesEquiv a b).symm ↑k = k • ⟨a, ⋯⟩ +ᵥ ⟨b, ⋯⟩
<VAR>n : ℕ<VAR>A : Type u_1<VAR>R : Type u_2<VAR>inst✝⁵ : AddGroup A<VAR>inst✝⁴ : Ring R<VAR>α✝ : Type u_3<VAR>β✝ : Type u_4<VAR>inst✝³ : Group α✝<VAR>a✝ : α✝<VAR>inst✝² : MulAction α✝ β✝<VAR>b✝ : β✝<VAR>α : Type u_5<VAR>β : Type u_6<VAR>inst✝¹ : AddGroup α<VAR>a : α<VAR>inst✝ : AddAction α β<VAR>b : β<VAR>k : ℤ<GOAL>(k % ↑(minimalPeriod (fun x => a +ᵥ x) b)) • ⟨a, ⋯⟩ +ᵥ ⟨b, ⋯⟩ = k • ⟨a, ⋯⟩ +ᵥ ⟨b, ⋯⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : Fintype α<VAR>s✝ t : Finset α<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>s : Finset α<GOAL>s ∩ univ = s
<VAR>f g : CircleDeg1Lift<VAR>n : ℤ<GOAL>f ↑n = f 0 + ↑n
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>X : Type u_2<VAR>inst✝ : MulAction G X<VAR>B : Set X<VAR>H : Subgroup G<VAR>hB : IsBlock (↥H) B<VAR>g : G<GOAL>IsBlock (↥(Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) H)) (g • B)
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>X : Type u_2<VAR>inst✝ : MulAction G X<VAR>B : Set X<VAR>H : Subgroup G<VAR>hB : IsBlock (↥H) B<VAR>g : G<GOAL>∀ (g_1 : ↥(Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) H)), g_1 • g • B = g • B ∨ Disjoint (g_1 • g • B) (g • B)
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>X : Type u_2<VAR>inst✝ : MulAction G X<VAR>B : Set X<VAR>H : Subgroup G<VAR>hB : IsBlock (↥H) B<VAR>g : G<VAR>h' : ↥(Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) H)<GOAL>h' • g • B = g • B ∨ Disjoint (h' • g • B) (g • B)
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>X : Type u_2<VAR>inst✝ : MulAction G X<VAR>B : Set X<VAR>H : Subgroup G<VAR>hB : IsBlock (↥H) B<VAR>g : G<VAR>h' : ↥(Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) H)<VAR>h : G<VAR>hH : h ∈ H<VAR>hh : (MulEquiv.toMonoidHom (MulAut.conj g)) h = ↑h'<GOAL>h' • g • B = g • B ∨ Disjoint (h' • g • B) (g • B)
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>X : Type u_2<VAR>inst✝ : MulAction G X<VAR>B : Set X<VAR>H : Subgroup G<VAR>hB : IsBlock (↥H) B<VAR>g : G<VAR>h' : ↥(Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) H)<VAR>h : G<VAR>hH : h ∈ H<VAR>hh : g * h * g⁻¹ = ↑h'<GOAL>h' • g • B = g • B ∨ Disjoint (h' • g • B) (g • B)
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>X : Type u_2<VAR>inst✝ : MulAction G X<VAR>B : Set X<VAR>H : Subgroup G<VAR>hB : IsBlock (↥H) B<VAR>g : G<VAR>h' : ↥(Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) H)<VAR>h : G<VAR>hH : h ∈ H<VAR>hh : g * h * g⁻¹ = ↑h'<GOAL>↑h' • g • B = g • h • B
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>s t u v : Set α<VAR>h : AEDisjoint μ s t<GOAL>AEDisjoint μ t s
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n✝ m : ℕ<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Nontrivial R<VAR>p q : R[X]<VAR>n : ℕ<GOAL>(X ^ n).degree = ↑n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝ : NontriviallyNormedField 𝕜<VAR>m : ℤ<VAR>x : 𝕜<GOAL>ContinuousAt (fun x => x ^ m) x ↔ x ≠ 0 ∨ 0 ≤ m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝ : NontriviallyNormedField 𝕜<VAR>m : ℤ<VAR>x : 𝕜<GOAL>ContinuousAt (fun x => x ^ m) x → x ≠ 0 ∨ 0 ≤ m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝ : NontriviallyNormedField 𝕜<VAR>m : ℤ<VAR>x : 𝕜<GOAL>x = 0 ∧ m < 0 → ¬ContinuousAt (fun x => x ^ m) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝ : NontriviallyNormedField 𝕜<VAR>m : ℤ<VAR>hm : m < 0<VAR>hc : ContinuousAt (fun x => x ^ m) 0<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : Multiset α<GOAL>card m.sym2 = (card m + 1).choose 2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : Multiset α<VAR>xs : List α<GOAL>card (Multiset.sym2 ⟦xs⟧) = (card ⟦xs⟧ + 1).choose 2
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>inst✝ : DecidableEq α<VAR>a d₁ : α<VAR>t₁ : List α<VAR>ih : ¬a ∈ t₁ → indexOf a (t₁ ++ l₂) = t₁.length + indexOf a l₂<VAR>h : ¬a ∈ d₁ :: t₁<GOAL>indexOf a (d₁ :: t₁ ++ l₂) = (d₁ :: t₁).length + indexOf a l₂
<VAR>V : Type u<VAR>V' : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>u v : V<VAR>p : G.Walk u v<GOAL>p.toSubgraph.Connected
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z✝ : Type u_3<VAR>Z : Type u_4<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>e : X ≃ Y<VAR>he : ∀ (s : Set Y), IsOpen (⇑e ⁻¹' s) ↔ IsOpen s<VAR>s : Set X<GOAL>IsOpen s → IsOpen (e.invFun ⁻¹' s)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z✝ : Type u_3<VAR>Z : Type u_4<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>e : X ≃ Y<VAR>he : ∀ (s : Set Y), IsOpen (⇑e ⁻¹' s) ↔ IsOpen s<VAR>s : Set X<GOAL>s = ⇑e ⁻¹' (e.invFun ⁻¹' s)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : OrderedCancelCommMonoid α<VAR>s : Multiset ι<VAR>f g : ι → α<VAR>l : List ι<VAR>hle : ∀ i ∈ Quot.mk Setoid.r l, f i ≤ g i<VAR>hlt : ∃ i ∈ Quot.mk Setoid.r l, f i < g i<GOAL>(map f (Quot.mk Setoid.r l)).prod < (map g (Quot.mk Setoid.r l)).prod
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : OrderedCancelCommMonoid α<VAR>s : Multiset ι<VAR>f g : ι → α<VAR>l : List ι<VAR>hle : ∀ i ∈ Quot.mk Setoid.r l, f i ≤ g i<VAR>hlt : ∃ i ∈ Quot.mk Setoid.r l, f i < g i<GOAL>(List.map f l).prod < (List.map g l).prod
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝² : PseudoEMetricSpace α<VAR>inst✝¹ : PseudoEMetricSpace β<VAR>inst✝ : PseudoEMetricSpace γ<VAR>K✝ : ℝ≥0<VAR>f✝ : α → β<VAR>x y : α<VAR>r : ℝ≥0∞<VAR>f : Function.End α<VAR>K : ℝ≥0<VAR>h : LipschitzWith K f<GOAL>LipschitzWith (K ^ 0) (f ^ 0)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝² : PseudoEMetricSpace α<VAR>inst✝¹ : PseudoEMetricSpace β<VAR>inst✝ : PseudoEMetricSpace γ<VAR>K✝ : ℝ≥0<VAR>f✝ : α → β<VAR>x y : α<VAR>r : ℝ≥0∞<VAR>f : Function.End α<VAR>K : ℝ≥0<VAR>h : LipschitzWith K f<VAR>n : ℕ<GOAL>LipschitzWith (K ^ (n + 1)) (f ^ (n + 1))
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝² : PseudoEMetricSpace α<VAR>inst✝¹ : PseudoEMetricSpace β<VAR>inst✝ : PseudoEMetricSpace γ<VAR>K✝ : ℝ≥0<VAR>f✝ : α → β<VAR>x y : α<VAR>r : ℝ≥0∞<VAR>f : Function.End α<VAR>K : ℝ≥0<VAR>h : LipschitzWith K f<VAR>n : ℕ<GOAL>LipschitzWith (K ^ n * K) (f ^ n * f)
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>inst✝¹ : Mul G<VAR>inst✝ : Mul H<VAR>A✝ B✝ : Finset G<VAR>a0✝ b0✝ : G<VAR>f : G →ₙ* H<VAR>hf : Function.Injective ⇑f<VAR>a0 b0 : G<VAR>A B : Finset H<VAR>u : UniqueMul A B (f a0) (f b0)<VAR>a b : G<VAR>ha : a ∈ A.preimage ⇑f ⋯<VAR>hb : b ∈ B.preimage ⇑f ⋯<VAR>ab : a * b = a0 * b0<GOAL>a = a0 ∧ b = b0
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>inst✝¹ : Mul G<VAR>inst✝ : Mul H<VAR>A✝ B✝ : Finset G<VAR>a0✝ b0✝ : G<VAR>f : G →ₙ* H<VAR>hf : Function.Injective ⇑f<VAR>a0 b0 : G<VAR>A B : Finset H<VAR>u : UniqueMul A B (f a0) (f b0)<VAR>a b : G<VAR>ha : a ∈ A.preimage ⇑f ⋯<VAR>hb : b ∈ B.preimage ⇑f ⋯<VAR>ab : f a * f b = f a0 * f b0<GOAL>f a = f a0 ∧ f b = f b0
<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 → F<VAR>hPz : P z ≠ 0<VAR>hy : P y = W.negY P<GOAL>W.Nonsingular P ↔ W.Equation P ∧ (eval P) W.polynomialX ≠ 0
<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 → F<VAR>hPz : P z ≠ 0<VAR>hy : P y = W.negY P<VAR>this : (eval P) W.polynomialY = P y - W.negY P<GOAL>W.Nonsingular P ↔ W.Equation P ∧ (eval P) W.polynomialX ≠ 0
<VAR>x : ℝ<GOAL>‖↑x‖ = |x - ↑(round x)|
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>G : Cᵒᵖ ⥤ Grp<VAR>X : C<VAR>I : Type w'<VAR>U : I → C<VAR>γ₁ γ₂ : OneCochain G U<VAR>α : ZeroCochain G U<VAR>h : OneCohomologyRelation γ₁ γ₂ α<VAR>i j : I<VAR>T : C<VAR>a : T ⟶ U i<VAR>b : T ⟶ U j<GOAL>(G.map a.op) (α⁻¹ i) * γ₂.ev i j a b = γ₁.ev i j a b * (G.map b.op) (α⁻¹ j)
<VAR>C : Type uC<VAR>inst✝³ : Category.{vC, uC} C<VAR>D : Type uD<VAR>inst✝² : Category.{vD, uD} D<VAR>G✝ : C ⥤ D<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>A : Type u_1<VAR>inst✝¹ : Category.{?u.7470, u_1} A<VAR>G : C ⥤ D<VAR>inst✝ : G.IsLocallyFull K<VAR>ℱ : SheafOfTypes K<VAR>X Y : C<VAR>i : G.obj X ⟶ G.obj Y<VAR>s t : ℱ.val.obj (op (G.obj X))<VAR>h : ∀ ⦃Z : C⦄ (j : Z ⟶ X) (f : Z ⟶ Y), G.map f = G.map j ≫ i → ℱ.val.map (G.map j).op s = ℱ.val.map (G.map j).op t<GOAL>s = t
<VAR>C : Type uC<VAR>inst✝³ : Category.{vC, uC} C<VAR>D : Type uD<VAR>inst✝² : Category.{vD, uD} D<VAR>G✝ : C ⥤ D<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>A : Type u_1<VAR>inst✝¹ : Category.{?u.7470, u_1} A<VAR>G : C ⥤ D<VAR>inst✝ : G.IsLocallyFull K<VAR>ℱ : SheafOfTypes K<VAR>X Y : C<VAR>i : G.obj X ⟶ G.obj Y<VAR>s t : ℱ.val.obj (op (G.obj X))<VAR>h : ∀ ⦃Z : C⦄ (j : Z ⟶ X) (f : Z ⟶ Y), G.map f = G.map j ≫ i → ℱ.val.map (G.map j).op s = ℱ.val.map (G.map j).op t<GOAL>∀ ⦃Y_1 : D⦄ ⦃f : Y_1 ⟶ G.obj X⦄, (Sieve.functorPushforward G (G.imageSieve i)).arrows f → ℱ.val.map f.op s = ℱ.val.map f.op t
<VAR>α : Type u_1<VAR>n : PosNum<GOAL>0 < n.natSize
<VAR>α✝ : Type u_1<VAR>α' : Type u_2<VAR>β✝ : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁵ : MeasurableSpace α✝<VAR>inst✝⁴ : MeasurableSpace α'<VAR>inst✝³ : MeasurableSpace β✝<VAR>inst✝² : MeasurableSpace β'<VAR>inst✝¹ : MeasurableSpace γ<VAR>μ μ' : Measure α✝<VAR>ν ν' : Measure β✝<VAR>τ : Measure γ<VAR>inst✝ : NormedAddCommGroup E<VAR>α : Type u_7<VAR>β : Type u_8<VAR>C : Set (Set α)<VAR>D : Set (Set β)<VAR>hC : IsCountablySpanning C<VAR>hD : IsCountablySpanning D<GOAL>Prod.instMeasurableSpace = generateFrom (image2 (fun x x_1 => x ×ˢ x_1) C D)
<VAR>α✝ : Type u_1<VAR>α' : Type u_2<VAR>β✝ : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁵ : MeasurableSpace α✝<VAR>inst✝⁴ : MeasurableSpace α'<VAR>inst✝³ : MeasurableSpace β✝<VAR>inst✝² : MeasurableSpace β'<VAR>inst✝¹ : MeasurableSpace γ<VAR>μ μ' : Measure α✝<VAR>ν ν' : Measure β✝<VAR>τ : Measure γ<VAR>inst✝ : NormedAddCommGroup E<VAR>α : Type u_7<VAR>β : Type u_8<VAR>C : Set (Set α)<VAR>D : Set (Set β)<VAR>hC : IsCountablySpanning C<VAR>hD : IsCountablySpanning D<GOAL>Prod.instMeasurableSpace ≤ generateFrom (image2 (fun x x_1 => x ×ˢ x_1) C D)
<VAR>α✝ : Type u_1<VAR>α' : Type u_2<VAR>β✝ : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁵ : MeasurableSpace α✝<VAR>inst✝⁴ : MeasurableSpace α'<VAR>inst✝³ : MeasurableSpace β✝<VAR>inst✝² : MeasurableSpace β'<VAR>inst✝¹ : MeasurableSpace γ<VAR>μ μ' : Measure α✝<VAR>ν ν' : Measure β✝<VAR>τ : Measure γ<VAR>inst✝ : NormedAddCommGroup E<VAR>α : Type u_7<VAR>β : Type u_8<VAR>C : Set (Set α)<VAR>D : Set (Set β)<VAR>hC : IsCountablySpanning C<VAR>hD : IsCountablySpanning D<GOAL>generateFrom (image2 (fun x x_1 => x ×ˢ x_1) C D) ≤ Prod.instMeasurableSpace
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : ClosedIciTopology α<VAR>inst✝ : TopologicalSpace β<VAR>a b c : α<VAR>f : α → β<VAR>h : a < b<GOAL>ContinuousWithinAt f (Icc a b) a ↔ ContinuousWithinAt f (Ici a) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>n : ℕ<VAR>i : Fin (n + 1)<VAR>l : List α<VAR>hl : l.length = n + 1<GOAL>ContinuousAt (Vector.eraseIdx i) ⟨l, hl⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>n : ℕ<VAR>i : Fin (n + 1)<VAR>l : List α<VAR>hl : l.length = n + 1<GOAL>Tendsto (fun x => ↑(Vector.eraseIdx i x)) (𝓝 ⟨l, hl⟩) (𝓝 ↑(match ⟨l, hl⟩ with | ⟨l, p⟩ => ⟨l.eraseIdx ↑i, ⋯⟩))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>n : ℕ<VAR>i : Fin (n + 1)<VAR>l : List α<VAR>hl : l.length = n + 1<GOAL>Tendsto (fun x => (↑x).eraseIdx ↑i) (𝓝 ⟨l, hl⟩) (𝓝 (l.eraseIdx ↑i))
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N✝ : Type u_3<VAR>P : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup N✝<VAR>inst✝⁵ : AddCommGroup P<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R N✝<VAR>inst✝² : Module R P<VAR>f : M →ₗ[R] N✝<VAR>g : N✝ →ₗ[R] P<VAR>Q : Type u_5<VAR>inst✝¹ : AddCommGroup Q<VAR>inst✝ : Module R Q<VAR>hfg : Exact ⇑f ⇑g<VAR>hg : Surjective ⇑g<VAR>N : Submodule R M<GOAL>ker (lTensor Q N.mkQ) = range (lTensor Q N.subtype)