ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝²⁰ : CommRing R<VAR>inst✝¹⁹ : CommRing S<VAR>inst✝¹⁸ : CommRing T<VAR>inst✝¹⁷ : Algebra R S<VAR>inst✝¹⁶ : Algebra R T<VAR>K : Type u_4<VAR>L : Type u_5<VAR>inst✝¹⁵ : Field K<VAR>inst✝¹⁴ : Field L<VAR>inst✝¹³ : Algebra K L<VAR>ι κ : Type w<VAR>inst✝¹² : Fintype ι<VAR>F : Type u_6<VAR>inst✝¹¹ : Field F<VAR>inst✝¹⁰ : Algebra R L<VAR>inst✝⁹ : Algebra L F<VAR>inst✝⁸ : Algebra R F<VAR>inst✝⁷ : IsScalarTower R L F<VAR>inst✝⁶ : Algebra K F<VAR>inst✝⁵ : IsScalarTower K L F<VAR>E : Type u_7<VAR>inst✝⁴ : Field E<VAR>inst✝³ : Algebra K E<VAR>inst✝² : IsAlgClosed E<VAR>x : L<VAR>inst✝¹ : FiniteDimensional K L<VAR>inst✝ : IsGalois K L<GOAL>(L →ₐ[K] AlgebraicClosure L) → AlgebraicClosure L
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝²⁰ : CommRing R<VAR>inst✝¹⁹ : CommRing S<VAR>inst✝¹⁸ : CommRing T<VAR>inst✝¹⁷ : Algebra R S<VAR>inst✝¹⁶ : Algebra R T<VAR>K : Type u_4<VAR>L : Type u_5<VAR>inst✝¹⁵ : Field K<VAR>inst✝¹⁴ : Field L<VAR>inst✝¹³ : Algebra K L<VAR>ι κ : Type w<VAR>inst✝¹² : Fintype ι<VAR>F : Type u_6<VAR>inst✝¹¹ : Field F<VAR>inst✝¹⁰ : Algebra R L<VAR>inst✝⁹ : Algebra L F<VAR>inst✝⁸ : Algebra R F<VAR>inst✝⁷ : IsScalarTower R L F<VAR>inst✝⁶ : Algebra K F<VAR>inst✝⁵ : IsScalarTower K L F<VAR>E : Type u_7<VAR>inst✝⁴ : Field E<VAR>inst✝³ : Algebra K E<VAR>inst✝² : IsAlgClosed E<VAR>x : L<VAR>inst✝¹ : FiniteDimensional K L<VAR>inst✝ : IsGalois K L<GOAL>∀ (x_1 : L →ₐ[K] AlgebraicClosure L), ?a.f✝ x_1 = (algebraMap L (AlgebraicClosure L)) (((Normal.algHomEquivAut K (AlgebraicClosure L) L) x_1) x)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : Ring R<VAR>inst✝ : Ring S<VAR>f : R →+* S<VAR>h : ∀ x ∈ RingHom.ker f, IsNilpotent x<VAR>e₂ : R<VAR>he₂ : IsIdempotentElem e₂<VAR>e₁ : R<VAR>he₁ : IsIdempotentElem (f e₁)<VAR>he₁e₂ : f e₁ * f e₂ = 0<GOAL>∃ e', IsIdempotentElem e' ∧ f e' = f e₁ ∧ e' * e₂ = 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : Ring R<VAR>inst✝ : Ring S<VAR>f : R →+* S<VAR>h : ∀ x ∈ RingHom.ker f, IsNilpotent x<VAR>e₂ : R<VAR>he₂ : IsIdempotentElem e₂<VAR>e₁ : R<VAR>he₁ : IsIdempotentElem (f e₁)<VAR>he₁e₂ : f e₁ * f e₂ = 0<VAR>h✝ : Subsingleton R<GOAL>∃ e', IsIdempotentElem e' ∧ f e' = f e₁ ∧ e' * e₂ = 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : Ring R<VAR>inst✝ : Ring S<VAR>f : R →+* S<VAR>h : ∀ x ∈ RingHom.ker f, IsNilpotent x<VAR>e₂ : R<VAR>he₂ : IsIdempotentElem e₂<VAR>e₁ : R<VAR>he₁ : IsIdempotentElem (f e₁)<VAR>he₁e₂ : f e₁ * f e₂ = 0<VAR>h✝ : Nontrivial R<GOAL>∃ e', IsIdempotentElem e' ∧ f e' = f e₁ ∧ e' * e₂ = 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : Ring R<VAR>inst✝ : Ring S<VAR>f : R →+* S<VAR>h : ∀ x ∈ RingHom.ker f, IsNilpotent x<VAR>e₂ : R<VAR>he₂ : IsIdempotentElem e₂<VAR>e₁ : R<VAR>he₁ : IsIdempotentElem (f e₁)<VAR>he₁e₂ : f e₁ * f e₂ = 0<VAR>h✝ : Nontrivial R<VAR>a : R := e₁ - e₁ * e₂<GOAL>∃ e', IsIdempotentElem e' ∧ f e' = f e₁ ∧ e' * e₂ = 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : Ring R<VAR>inst✝ : Ring S<VAR>f : R →+* S<VAR>h : ∀ x ∈ RingHom.ker f, IsNilpotent x<VAR>e₂ : R<VAR>he₂ : IsIdempotentElem e₂<VAR>e₁ : R<VAR>he₁ : IsIdempotentElem (f e₁)<VAR>he₁e₂ : f e₁ * f e₂ = 0<VAR>h✝ : Nontrivial R<VAR>a : R := e₁ - e₁ * e₂<VAR>ha : f a = f e₁<GOAL>∃ e', IsIdempotentElem e' ∧ f e' = f e₁ ∧ e' * e₂ = 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : Ring R<VAR>inst✝ : Ring S<VAR>f : R →+* S<VAR>h : ∀ x ∈ RingHom.ker f, IsNilpotent x<VAR>e₂ : R<VAR>he₂ : IsIdempotentElem e₂<VAR>e₁ : R<VAR>he₁ : IsIdempotentElem (f e₁)<VAR>he₁e₂ : f e₁ * f e₂ = 0<VAR>h✝ : Nontrivial R<VAR>a : R := e₁ - e₁ * e₂<VAR>ha : f a = f e₁<VAR>ha' : a * e₂ = 0<GOAL>∃ e', IsIdempotentElem e' ∧ f e' = f e₁ ∧ e' * e₂ = 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : Ring R<VAR>inst✝ : Ring S<VAR>f : R →+* S<VAR>h : ∀ x ∈ RingHom.ker f, IsNilpotent x<VAR>e₂ : R<VAR>he₂ : IsIdempotentElem e₂<VAR>e₁ : R<VAR>he₁ : IsIdempotentElem (f e₁)<VAR>he₁e₂ : f e₁ * f e₂ = 0<VAR>h✝ : Nontrivial R<VAR>a : R := e₁ - e₁ * e₂<VAR>ha : f a = f e₁<VAR>ha' : a * e₂ = 0<VAR>hx' : a - a ^ 2 ∈ RingHom.ker f<GOAL>∃ e', IsIdempotentElem e' ∧ f e' = f e₁ ∧ e' * e₂ = 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : Ring R<VAR>inst✝ : Ring S<VAR>f : R →+* S<VAR>h : ∀ x ∈ RingHom.ker f, IsNilpotent x<VAR>e₂ : R<VAR>he₂ : IsIdempotentElem e₂<VAR>e₁ : R<VAR>he₁ : IsIdempotentElem (f e₁)<VAR>he₁e₂ : f e₁ * f e₂ = 0<VAR>h✝ : Nontrivial R<VAR>a : R := e₁ - e₁ * e₂<VAR>ha : f a = f e₁<VAR>ha' : a * e₂ = 0<VAR>hx' : a - a ^ 2 ∈ RingHom.ker f<VAR>n : ℕ<VAR>hn : (a - a ^ 2) ^ n = 0<GOAL>∃ e', IsIdempotentElem e' ∧ f e' = f e₁ ∧ e' * e₂ = 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : Ring R<VAR>inst✝ : Ring S<VAR>f : R →+* S<VAR>h : ∀ x ∈ RingHom.ker f, IsNilpotent x<VAR>e₂ : R<VAR>he₂ : IsIdempotentElem e₂<VAR>e₁ : R<VAR>he₁ : IsIdempotentElem (f e₁)<VAR>he₁e₂ : f e₁ * f e₂ = 0<VAR>h✝ : Nontrivial R<VAR>a : R := e₁ - e₁ * e₂<VAR>ha : f a = f e₁<VAR>ha' : a * e₂ = 0<VAR>hx' : a - a ^ 2 ∈ RingHom.ker f<VAR>n : ℕ<VAR>hn : (a - a ^ 2) ^ n = 0<GOAL>f (1 - (1 - a ^ n) ^ n) = f e₁
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : Ring R<VAR>inst✝ : Ring S<VAR>f : R →+* S<VAR>h : ∀ x ∈ RingHom.ker f, IsNilpotent x<VAR>e₂ : R<VAR>he₂ : IsIdempotentElem e₂<VAR>e₁ : R<VAR>he₁ : IsIdempotentElem (f e₁)<VAR>he₁e₂ : f e₁ * f e₂ = 0<VAR>h✝ : Nontrivial R<VAR>a : R := e₁ - e₁ * e₂<VAR>ha : f a = f e₁<VAR>ha' : a * e₂ = 0<VAR>hx' : a - a ^ 2 ∈ RingHom.ker f<VAR>n : ℕ<VAR>hn : (a - a ^ 2) ^ n = 0<GOAL>(1 - (1 - a ^ n) ^ n) * e₂ = 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>inst✝¹ : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>f : α → β<VAR>inst✝ : Zero β<VAR>hs : MeasurableSet s<VAR>hf : f =ᶠ[ae (μ.restrict s)] 0<GOAL>s.indicator f =ᶠ[ae μ] 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>inst✝¹ : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>f : α → β<VAR>inst✝ : Zero β<VAR>hs : MeasurableSet s<VAR>hf : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = 0 x<GOAL>s.indicator f =ᶠ[ae μ] 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>inst✝¹ : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>f : α → β<VAR>inst✝ : Zero β<VAR>hs : MeasurableSet s<VAR>hf : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = 0 x<VAR>x : α<VAR>hx : x ∈ s → f x = 0 x<GOAL>s.indicator f x = 0 x
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>S : Type v<VAR>inst✝¹ : CommRing S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>P : Ideal S<VAR>hfp : NeZero e<VAR>inst✝ : IsDedekindDomain S<VAR>hP0 : P ≠ ⊥<VAR>hP : P.IsPrime<VAR>i : ℕ<VAR>hi : i < e<VAR>a : S<VAR>a_mem : a ∈ P ^ i<VAR>a_not_mem : a ∉ P ^ (i + 1)<VAR>b✝ : ↥(map (Quotient.mk (P ^ e)) (P ^ i)) ⧸ LinearMap.range (powQuotSuccInclusion f p P i)<VAR>val✝ : S ⧸ P ^ e<VAR>x : S<VAR>hx : Quot.mk Setoid.r x ∈ map (Quotient.mk (P ^ e)) (P ^ i)<GOAL>∃ a_1, (quotientToQuotientRangePowQuotSucc f p P a_mem) a_1 = Quot.mk Setoid.r ⟨Quot.mk Setoid.r x, hx⟩
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>S : Type v<VAR>inst✝¹ : CommRing S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>P : Ideal S<VAR>hfp : NeZero e<VAR>inst✝ : IsDedekindDomain S<VAR>hP0 : P ≠ ⊥<VAR>hP : P.IsPrime<VAR>i : ℕ<VAR>hi : i < e<VAR>a : S<VAR>a_mem : a ∈ P ^ i<VAR>a_not_mem : a ∉ P ^ (i + 1)<VAR>b✝ : ↥(map (Quotient.mk (P ^ e)) (P ^ i)) ⧸ LinearMap.range (powQuotSuccInclusion f p P i)<VAR>val✝ : S ⧸ P ^ e<VAR>x : S<VAR>hx : Quot.mk Setoid.r x ∈ map (Quotient.mk (P ^ e)) (P ^ i)<VAR>Pe_le_Pi : P ^ e ≤ P ^ i<GOAL>∃ a_1, (quotientToQuotientRangePowQuotSucc f p P a_mem) a_1 = Quot.mk Setoid.r ⟨Quot.mk Setoid.r x, hx⟩
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>S : Type v<VAR>inst✝¹ : CommRing S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>P : Ideal S<VAR>hfp : NeZero e<VAR>inst✝ : IsDedekindDomain S<VAR>hP0 : P ≠ ⊥<VAR>hP : P.IsPrime<VAR>i : ℕ<VAR>hi : i < e<VAR>a : S<VAR>a_mem : a ∈ P ^ i<VAR>a_not_mem : a ∉ P ^ (i + 1)<VAR>b✝ : ↥(map (Quotient.mk (P ^ e)) (P ^ i)) ⧸ LinearMap.range (powQuotSuccInclusion f p P i)<VAR>val✝ : S ⧸ P ^ e<VAR>x : S<VAR>hx✝ : Quot.mk Setoid.r x ∈ map (Quotient.mk (P ^ e)) (P ^ i)<VAR>hx : x ∈ P ^ i<VAR>Pe_le_Pi : P ^ e ≤ P ^ i<GOAL>∃ a_1, (quotientToQuotientRangePowQuotSucc f p P a_mem) a_1 = Quot.mk Setoid.r ⟨Quot.mk Setoid.r x, hx✝⟩
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>S : Type v<VAR>inst✝¹ : CommRing S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>P : Ideal S<VAR>hfp : NeZero e<VAR>inst✝ : IsDedekindDomain S<VAR>hP0 : P ≠ ⊥<VAR>hP : P.IsPrime<VAR>i : ℕ<VAR>hi : i < e<VAR>a : S<VAR>a_mem : a ∈ P ^ i<VAR>a_not_mem : a ∉ P ^ (i + 1)<VAR>b✝ : ↥(map (Quotient.mk (P ^ e)) (P ^ i)) ⧸ LinearMap.range (powQuotSuccInclusion f p P i)<VAR>val✝ : S ⧸ P ^ e<VAR>x : S<VAR>hx✝ : Quot.mk Setoid.r x ∈ map (Quotient.mk (P ^ e)) (P ^ i)<VAR>hx : x ∈ P ^ i<VAR>Pe_le_Pi : P ^ e ≤ P ^ i<GOAL>x ∈ span {a} ⊔ P ^ (i + 1)
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>S : Type v<VAR>inst✝¹ : CommRing S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>P : Ideal S<VAR>hfp : NeZero e<VAR>inst✝ : IsDedekindDomain S<VAR>hP0 : P ≠ ⊥<VAR>hP : P.IsPrime<VAR>i : ℕ<VAR>hi : i < e<VAR>a : S<VAR>a_mem : a ∈ P ^ i<VAR>a_not_mem : a ∉ P ^ (i + 1)<VAR>b✝ : ↥(map (Quotient.mk (P ^ e)) (P ^ i)) ⧸ LinearMap.range (powQuotSuccInclusion f p P i)<VAR>val✝ : S ⧸ P ^ e<VAR>x : S<VAR>hx✝ : Quot.mk Setoid.r x ∈ map (Quotient.mk (P ^ e)) (P ^ i)<VAR>hx : x ∈ P ^ i<VAR>Pe_le_Pi : P ^ e ≤ P ^ i<VAR>this : DecidableEq (Ideal S) := Classical.decEq (Ideal S)<GOAL>x ∈ span {a} ⊔ P ^ (i + 1)
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>S : Type v<VAR>inst✝¹ : CommRing S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>P : Ideal S<VAR>hfp : NeZero e<VAR>inst✝ : IsDedekindDomain S<VAR>hP0 : P ≠ ⊥<VAR>hP : P.IsPrime<VAR>i : ℕ<VAR>hi : i < e<VAR>a : S<VAR>a_mem : a ∈ P ^ i<VAR>a_not_mem : a ∉ P ^ (i + 1)<VAR>b✝ : ↥(map (Quotient.mk (P ^ e)) (P ^ i)) ⧸ LinearMap.range (powQuotSuccInclusion f p P i)<VAR>val✝ : S ⧸ P ^ e<VAR>x : S<VAR>hx✝ : Quot.mk Setoid.r x ∈ map (Quotient.mk (P ^ e)) (P ^ i)<VAR>hx : x ∈ P ^ i<VAR>Pe_le_Pi : P ^ e ≤ P ^ i<VAR>this : DecidableEq (Ideal S) := Classical.decEq (Ideal S)<GOAL>x ∈ P ^ min (Multiset.count P (normalizedFactors (span {a}))) (i + 1)
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>S : Type v<VAR>inst✝¹ : CommRing S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>P : Ideal S<VAR>hfp : NeZero e<VAR>inst✝ : IsDedekindDomain S<VAR>hP0 : P ≠ ⊥<VAR>hP : P.IsPrime<VAR>i : ℕ<VAR>hi : i < e<VAR>a : S<VAR>a_mem : a ∈ P ^ i<VAR>a_not_mem : a ∉ P ^ (i + 1)<VAR>b✝ : ↥(map (Quotient.mk (P ^ e)) (P ^ i)) ⧸ LinearMap.range (powQuotSuccInclusion f p P i)<VAR>val✝ : S ⧸ P ^ e<VAR>x : S<VAR>hx✝ : Quot.mk Setoid.r x ∈ map (Quotient.mk (P ^ e)) (P ^ i)<VAR>hx : x ∈ P ^ i<VAR>Pe_le_Pi : P ^ e ≤ P ^ i<VAR>this : DecidableEq (Ideal S) := Classical.decEq (Ideal S)<GOAL>span {a} ≠ ⊥
<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>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L : Filter 𝕜<GOAL>deriv (fun y => -f y) x = -deriv f x
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s✝ s : Multiset α<VAR>x : { x // x ∈ s }<GOAL>map val (s.attach.erase x) = s.erase ↑x
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>hdomain : IsDomain R<VAR>r s : R<VAR>p q : R[X]<VAR>f : RatFunc R<GOAL>(laurentAux r) ((algebraMap R[X] (RatFunc R)) p) = (algebraMap R[X] (RatFunc R)) ((taylor r) p)
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Preadditive C<VAR>X Y : C<VAR>t : BinaryBicone X Y<VAR>ht : IsLimit t.toCone<GOAL>t.inr = ht.lift (BinaryFan.mk 0 (𝟙 Y))
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Preadditive C<VAR>X Y : C<VAR>t : BinaryBicone X Y<VAR>ht : IsLimit t.toCone<GOAL>∀ (j : Discrete WalkingPair), t.inr ≫ t.toCone.π.app j = (BinaryFan.mk 0 (𝟙 Y)).π.app j
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : α → β<VAR>g : β → γ<VAR>s : Stream' (Option α)<VAR>al : s.IsSeq<GOAL>map (g ∘ f) ⟨s, al⟩ = map g (map f ⟨s, al⟩)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : α → β<VAR>g : β → γ<VAR>s : Stream' (Option α)<VAR>al : s.IsSeq<GOAL>↑(map (g ∘ f) ⟨s, al⟩) = ↑(map g (map f ⟨s, al⟩))
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : α → β<VAR>g : β → γ<VAR>s : Stream' (Option α)<VAR>al : s.IsSeq<GOAL>Option.map (g ∘ f) = Option.map g ∘ Option.map f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>S : Set (Set α)<GOAL>⋃₀ S = (⋂₀ (compl '' S))ᶜ
<VAR>R : Type u<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : Semiring R<VAR>p q : R[X]<GOAL>(↑m).coeff n = ↑(if n = 0 then m else 0)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : ConditionallyCompleteLinearOrder α<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : DenselyOrdered α<VAR>f : Filter β<VAR>u : β → α<VAR>s : Set α<VAR>hs : Dense s<VAR>H : ∀ a ∈ s, ∀ b ∈ s, a < b → ¬((∃ᶠ (n : β) in f, u n < a) ∧ ∃ᶠ (n : β) in f, b < u n)<VAR>h : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝<VAR>h' : autoParam (IsBoundedUnder (fun x x_1 => x ≥ x_1) f u) _auto✝<GOAL>∃ c, Tendsto u f (𝓝 c)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : ConditionallyCompleteLinearOrder α<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : DenselyOrdered α<VAR>u : β → α<VAR>s : Set α<VAR>hs : Dense s<VAR>H : ∀ a ∈ s, ∀ b ∈ s, a < b → ¬((∃ᶠ (n : β) in ⊥, u n < a) ∧ ∃ᶠ (n : β) in ⊥, b < u n)<VAR>h : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) ⊥ u) _auto✝<VAR>h' : autoParam (IsBoundedUnder (fun x x_1 => x ≥ x_1) ⊥ u) _auto✝<GOAL>∃ c, Tendsto u ⊥ (𝓝 c)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : ConditionallyCompleteLinearOrder α<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : DenselyOrdered α<VAR>f : Filter β<VAR>u : β → α<VAR>s : Set α<VAR>hs : Dense s<VAR>H : ∀ a ∈ s, ∀ b ∈ s, a < b → ¬((∃ᶠ (n : β) in f, u n < a) ∧ ∃ᶠ (n : β) in f, b < u n)<VAR>h : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝<VAR>h' : autoParam (IsBoundedUnder (fun x x_1 => x ≥ x_1) f u) _auto✝<VAR>hbot : f.NeBot<GOAL>∃ c, Tendsto u f (𝓝 c)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : ConditionallyCompleteLinearOrder α<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : DenselyOrdered α<VAR>f : Filter β<VAR>u : β → α<VAR>s : Set α<VAR>hs : Dense s<VAR>H : ∀ a ∈ s, ∀ b ∈ s, a < b → ¬((∃ᶠ (n : β) in f, u n < a) ∧ ∃ᶠ (n : β) in f, b < u n)<VAR>h : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝<VAR>h' : autoParam (IsBoundedUnder (fun x x_1 => x ≥ x_1) f u) _auto✝<VAR>hbot : f.NeBot<GOAL>Tendsto u f (𝓝 (limsup u f))
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : ConditionallyCompleteLinearOrder α<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : DenselyOrdered α<VAR>f : Filter β<VAR>u : β → α<VAR>s : Set α<VAR>hs : Dense s<VAR>H : ∀ a ∈ s, ∀ b ∈ s, a < b → ¬((∃ᶠ (n : β) in f, u n < a) ∧ ∃ᶠ (n : β) in f, b < u n)<VAR>h : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝<VAR>h' : autoParam (IsBoundedUnder (fun x x_1 => x ≥ x_1) f u) _auto✝<VAR>hbot : f.NeBot<GOAL>limsup u f ≤ liminf u f
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : ConditionallyCompleteLinearOrder α<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : DenselyOrdered α<VAR>f : Filter β<VAR>u : β → α<VAR>s : Set α<VAR>hs : Dense s<VAR>H : ∀ a ∈ s, ∀ b ∈ s, a < b → ¬((∃ᶠ (n : β) in f, u n < a) ∧ ∃ᶠ (n : β) in f, b < u n)<VAR>h : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝<VAR>h' : autoParam (IsBoundedUnder (fun x x_1 => x ≥ x_1) f u) _auto✝<VAR>hbot : f.NeBot<VAR>hlt : liminf u f < limsup u f<GOAL>False
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : ConditionallyCompleteLinearOrder α<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : DenselyOrdered α<VAR>f : Filter β<VAR>u : β → α<VAR>s : Set α<VAR>hs : Dense s<VAR>H : ∀ a ∈ s, ∀ b ∈ s, a < b → ¬((∃ᶠ (n : β) in f, u n < a) ∧ ∃ᶠ (n : β) in f, b < u n)<VAR>h : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝<VAR>h' : autoParam (IsBoundedUnder (fun x x_1 => x ≥ x_1) f u) _auto✝<VAR>hbot : f.NeBot<VAR>hlt : liminf u f < limsup u f<VAR>a : α<VAR>as : a ∈ s<VAR>la : liminf u f < a<VAR>au : a < limsup u f<GOAL>False
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : ConditionallyCompleteLinearOrder α<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : DenselyOrdered α<VAR>f : Filter β<VAR>u : β → α<VAR>s : Set α<VAR>hs : Dense s<VAR>H : ∀ a ∈ s, ∀ b ∈ s, a < b → ¬((∃ᶠ (n : β) in f, u n < a) ∧ ∃ᶠ (n : β) in f, b < u n)<VAR>h : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝<VAR>h' : autoParam (IsBoundedUnder (fun x x_1 => x ≥ x_1) f u) _auto✝<VAR>hbot : f.NeBot<VAR>hlt : liminf u f < limsup u f<VAR>a : α<VAR>as : a ∈ s<VAR>la : liminf u f < a<VAR>au : a < limsup u f<VAR>b : α<VAR>bs : b ∈ s<VAR>ab : a < b<VAR>bu : b < limsup u f<GOAL>False
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : ConditionallyCompleteLinearOrder α<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : DenselyOrdered α<VAR>f : Filter β<VAR>u : β → α<VAR>s : Set α<VAR>hs : Dense s<VAR>H : ∀ a ∈ s, ∀ b ∈ s, a < b → ¬((∃ᶠ (n : β) in f, u n < a) ∧ ∃ᶠ (n : β) in f, b < u n)<VAR>h : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝<VAR>h' : autoParam (IsBoundedUnder (fun x x_1 => x ≥ x_1) f u) _auto✝<VAR>hbot : f.NeBot<VAR>hlt : liminf u f < limsup u f<VAR>a : α<VAR>as : a ∈ s<VAR>la : liminf u f < a<VAR>au : a < limsup u f<VAR>b : α<VAR>bs : b ∈ s<VAR>ab : a < b<VAR>bu : b < limsup u f<VAR>A : ∃ᶠ (n : β) in f, u n < a<GOAL>False
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : ConditionallyCompleteLinearOrder α<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : DenselyOrdered α<VAR>f : Filter β<VAR>u : β → α<VAR>s : Set α<VAR>hs : Dense s<VAR>H : ∀ a ∈ s, ∀ b ∈ s, a < b → ¬((∃ᶠ (n : β) in f, u n < a) ∧ ∃ᶠ (n : β) in f, b < u n)<VAR>h : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝<VAR>h' : autoParam (IsBoundedUnder (fun x x_1 => x ≥ x_1) f u) _auto✝<VAR>hbot : f.NeBot<VAR>hlt : liminf u f < limsup u f<VAR>a : α<VAR>as : a ∈ s<VAR>la : liminf u f < a<VAR>au : a < limsup u f<VAR>b : α<VAR>bs : b ∈ s<VAR>ab : a < b<VAR>bu : b < limsup u f<VAR>A : ∃ᶠ (n : β) in f, u n < a<VAR>B : ∃ᶠ (n : β) in f, b < u n<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : CommSemigroup α<VAR>inst✝ : CommSemigroup β<VAR>f : α → β<VAR>a b : α<GOAL>f (min a b) * f (max a b) = f a * f b
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : OrderedSemiring 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : AddCommMonoid F<VAR>inst✝¹ : SMul 𝕜 E<VAR>inst✝ : SMul 𝕜 F<VAR>x : E<VAR>s✝ t : Set E<VAR>ι : Sort u_4<VAR>s : ι → Set E<VAR>hs : ∀ (i : ι), StarConvex 𝕜 x (s i)<VAR>y : E<VAR>hy : y ∈ ⋃ i, s i<VAR>a b : 𝕜<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>hab : a + b = 1<GOAL>a • x + b • y ∈ ⋃ i, s i
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : OrderedSemiring 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : AddCommMonoid F<VAR>inst✝¹ : SMul 𝕜 E<VAR>inst✝ : SMul 𝕜 F<VAR>x : E<VAR>s✝ t : Set E<VAR>ι : Sort u_4<VAR>s : ι → Set E<VAR>hs : ∀ (i : ι), StarConvex 𝕜 x (s i)<VAR>y : E<VAR>hy : ∃ i, y ∈ s i<VAR>a b : 𝕜<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>hab : a + b = 1<GOAL>∃ i, a • x + b • y ∈ s i
<VAR>G✝ : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝⁵ : TopologicalSpace G✝<VAR>inst✝⁴ : Group G✝<VAR>inst✝³ : TopologicalGroup G✝<VAR>inst✝² : TopologicalSpace α<VAR>f : α → G✝<VAR>s : Set α<VAR>x : α<VAR>G : Type u<VAR>inst✝¹ : CommGroup G<VAR>inst✝ : TopologicalSpace G<VAR>hmul : Tendsto (uncurry fun x x_1 => x * x_1) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)<VAR>hinv : Tendsto (fun x => x⁻¹) (𝓝 1) (𝓝 1)<VAR>hleft : ∀ (x₀ : G), 𝓝 x₀ = map (fun x => x₀ * x) (𝓝 1)<GOAL>∀ (x₀ : G), Tendsto (fun x => x₀ * x * x₀⁻¹) (𝓝 1) (𝓝 1)
<VAR>X : Type u_1<VAR>inst✝ : TopologicalSpace X<VAR>s : Set (OnePoint X)<VAR>t : Set X<VAR>α : Type u_2<VAR>f : OnePoint X → α<VAR>l : Filter α<GOAL>Tendsto f (pure ∞) l ∧ Tendsto (f ∘ some) (coclosedCompact X) l ↔ ∀ s ∈ l, f ∞ ∈ s ∧ ∃ t, IsClosed t ∧ IsCompact t ∧ MapsTo (f ∘ some) tᶜ s
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝² : SeminormedRing 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : SMul 𝕜 E<VAR>p✝ : Seminorm 𝕜 E<VAR>x y✝ : E<VAR>r✝ : ℝ<VAR>p : Seminorm 𝕜 E<VAR>x₁ x₂ y : E<VAR>r : ℝ<GOAL>x₁ - x₂ ∈ p.ball y r ↔ x₁ ∈ p.ball (x₂ + y) r
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ p₄ p₅ p₆ : P<VAR>h : 2 • ∡ p₁ p₂ p₃ = 2 • ∡ p₄ p₅ p₆<GOAL>Collinear ℝ {p₁, p₂, p₃} ↔ Collinear ℝ {p₄, p₅, p₆}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p q : α → Prop<VAR>inst✝² : DecidablePred p<VAR>inst✝¹ : DecidablePred q<VAR>s✝ t : Finset α<VAR>inst✝ : DecidableEq α<VAR>s : Finset α<VAR>a : α<GOAL>a ∈ filter (fun a => ¬p a) s ↔ a ∈ s \ filter p s
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : Ring A<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : Ring B<VAR>inst✝⁴ : Algebra R B<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>f g : M →ₗ[R] N<VAR>x✝ : M<GOAL>((AlgebraTensorModule.curry (baseChange A (-f))) 1) x✝ = ((AlgebraTensorModule.curry (-baseChange A f)) 1) x✝
<VAR>G : Type u_1<VAR>inst✝⁵ : Group G<VAR>H : Subgroup G<VAR>inst✝⁴ : H.Normal<VAR>G₁ : Type u_2<VAR>G₂ : Type u_3<VAR>inst✝³ : Group G₁<VAR>inst✝² : Group G₂<VAR>inst✝¹ : Group.IsNilpotent G₁<VAR>inst✝ : Group.IsNilpotent G₂<GOAL>Group.nilpotencyClass (G₁ × G₂) = max (Group.nilpotencyClass G₁) (Group.nilpotencyClass G₂)
<VAR>G : Type u_1<VAR>inst✝⁵ : Group G<VAR>H : Subgroup G<VAR>inst✝⁴ : H.Normal<VAR>G₁ : Type u_2<VAR>G₂ : Type u_3<VAR>inst✝³ : Group G₁<VAR>inst✝² : Group G₂<VAR>inst✝¹ : Group.IsNilpotent G₁<VAR>inst✝ : Group.IsNilpotent G₂<VAR>k : ℕ<GOAL>Group.nilpotencyClass (G₁ × G₂) ≤ k ↔ max (Group.nilpotencyClass G₁) (Group.nilpotencyClass G₂) ≤ k
<VAR>n : ℕ<GOAL>2 * powHalf (n + 1) = powHalf n
<VAR>n : ℕ<GOAL>powHalf (n + 1) + powHalf (n + 1) = powHalf n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>R : Type u_12<VAR>R' : Type u_13<VAR>𝕜 : Type u_14<VAR>𝕜' : Type u_15<VAR>inst✝¹² : Norm E<VAR>inst✝¹¹ : Norm F<VAR>inst✝¹⁰ : Norm G<VAR>inst✝⁹ : SeminormedAddCommGroup E'<VAR>inst✝⁸ : SeminormedAddCommGroup F'<VAR>inst✝⁷ : SeminormedAddCommGroup G'<VAR>inst✝⁶ : NormedAddCommGroup E''<VAR>inst✝⁵ : NormedAddCommGroup F''<VAR>inst✝⁴ : NormedAddCommGroup G''<VAR>inst✝³ : SeminormedRing R<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedField 𝕜<VAR>inst✝ : NormedField 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g✝ : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>l l' : Filter α<VAR>g : α → ℝ<VAR>h : (fun x => ‖f' x‖) =ᶠ[l] g<VAR>x : α<VAR>hx : (fun x => ‖f' x‖) x = g x<GOAL>(fun x => ‖f' x‖) x = (fun x => ‖g x‖) x