ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>M : Type w<VAR>A : Set M<VAR>L : Language<VAR>inst✝ : L.Structure M<VAR>α : Type u₁<VAR>β : Type u_1<VAR>B : Set M<VAR>s✝ s t : Set (α → M)<VAR>hs : A.Definable L s<VAR>ht : A.Definable L t<GOAL>A.Definable L (s ⇨ t)
<VAR>M : Type w<VAR>A : Set M<VAR>L : Language<VAR>inst✝ : L.Structure M<VAR>α : Type u₁<VAR>β : Type u_1<VAR>B : Set M<VAR>s✝ s t : Set (α → M)<VAR>hs : A.Definable L s<VAR>ht : A.Definable L t<GOAL>A.Definable L (t ⊔ sᶜ)
<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>S : Type u_4<VAR>inst✝³ : CommRing S<VAR>inst✝² : IsDomain S<VAR>inst✝¹ : Algebra R S<VAR>inst✝ : Finite ι<VAR>b : Basis ι R S<VAR>I : Ideal S<VAR>hI : I ≠ ⊥<VAR>i : ι<VAR>hi : smithCoeffs b I hI i = 0<GOAL>False
<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>S : Type u_4<VAR>inst✝³ : CommRing S<VAR>inst✝² : IsDomain S<VAR>inst✝¹ : Algebra R S<VAR>inst✝ : Finite ι<VAR>b : Basis ι R S<VAR>I : Ideal S<VAR>hI : I ≠ ⊥<VAR>i : ι<VAR>hi : smithCoeffs b I hI i = 0<GOAL>(selfBasis b I hI) i = 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>S : Type u_4<VAR>inst✝³ : CommRing S<VAR>inst✝² : IsDomain S<VAR>inst✝¹ : Algebra R S<VAR>inst✝ : Finite ι<VAR>b : Basis ι R S<VAR>I : Ideal S<VAR>hI : I ≠ ⊥<VAR>i : ι<VAR>hi : smithCoeffs b I hI i = 0<GOAL>(fun a => ↑a) ((selfBasis b I hI) i) = (fun a => ↑a) 0
<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✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>a b c d : ℝ<VAR>f g : ℝ → E<VAR>μ : Measure ℝ<VAR>a₁ a₂ a₃ : ℝ<VAR>h : a₂ ∈ Icc a₁ a₃<GOAL>∫ (x : ℝ) in a₁..a₃, {x | x ≤ a₂}.indicator f x ∂μ = ∫ (x : ℝ) in a₁..a₂, f x ∂μ
<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✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>a b c d : ℝ<VAR>f g : ℝ → E<VAR>μ : Measure ℝ<VAR>a₁ a₂ a₃ : ℝ<VAR>h : a₂ ∈ Icc a₁ a₃<VAR>this : {x | x ≤ a₂} ∩ Ioc a₁ a₃ = Ioc a₁ a₂<GOAL>∫ (x : ℝ) in a₁..a₃, {x | x ≤ a₂}.indicator f x ∂μ = ∫ (x : ℝ) in a₁..a₂, f x ∂μ
<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✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>a b c d : ℝ<VAR>f g : ℝ → E<VAR>μ : Measure ℝ<VAR>a₁ a₂ a₃ : ℝ<VAR>h : a₂ ∈ Icc a₁ a₃<VAR>this : {x | x ≤ a₂} ∩ Ioc a₁ a₃ = Ioc a₁ a₂<GOAL>MeasurableSet {x | x ≤ a₂}
<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>inst✝⁴ : CommRing T<VAR>p : T[X]<VAR>S : Type u_1<VAR>inst✝³ : CommRing S<VAR>inst✝² : IsDomain S<VAR>inst✝¹ : Algebra T S<VAR>inst✝ : NoZeroSMulDivisors T S<VAR>a : S<GOAL>a ∈ p.rootSet S ↔ p ≠ 0 ∧ (aeval a) p = 0
<VAR>J : Type w<VAR>C✝ : Type u<VAR>inst✝² : Category.{v, u} C✝<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>B : C<VAR>objs : J → C<VAR>arrows : (j : J) → objs j ⟶ B<VAR>inst✝ : HasWidePullback B objs arrows<VAR>X : C<VAR>f : X ⟶ B<VAR>fs : (j : J) → X ⟶ objs j<VAR>w : ∀ (j : J), fs j ≫ arrows j = f<GOAL>lift f fs w ≫ base arrows = f
<VAR>a b : ℝ<VAR>n : ℕ<VAR>r : ℝ<VAR>h : -1 < r ∨ r ≠ -1 ∧ 0 ∉ [[a, b]]<VAR>h' : -1 < (↑r).re ∨ ↑r ≠ -1 ∧ 0 ∉ [[a, b]]<GOAL>∫ (x : ℝ) in a..b, x ^ r = (b ^ (r + 1) - a ^ (r + 1)) / (r + 1)
<VAR>a b : ℝ<VAR>n : ℕ<VAR>r : ℝ<VAR>h : -1 < r ∨ r ≠ -1 ∧ 0 ∉ [[a, b]]<VAR>h' : -1 < (↑r).re ∨ ↑r ≠ -1 ∧ 0 ∉ [[a, b]]<VAR>this : ∫ (x : ℝ) in a..b, ↑x ^ ↑r = (↑b ^ (↑r + 1) - ↑a ^ (↑r + 1)) / (↑r + 1)<GOAL>∫ (x : ℝ) in a..b, x ^ r = (b ^ (r + 1) - a ^ (r + 1)) / (r + 1)
<VAR>a b r : ℤ<VAR>hr : 0 < r<GOAL>↑(filter (fun x => r ∣ x) (Ioc a b)).card = max (⌊↑b / ↑r⌋ - ⌊↑a / ↑r⌋) 0
<VAR>C : Type u<VAR>inst✝ : Groupoid C<VAR>S : Subgroupoid C<VAR>c : C<GOAL>univ.Nonempty
<VAR>R : Type u_1<VAR>k : Type u_2<VAR>V1 : Type u_3<VAR>P1 : Type u_4<VAR>V2 : Type u_5<VAR>P2 : Type u_6<VAR>V3 : Type u_7<VAR>P3 : Type u_8<VAR>inst✝⁵ : CommRing k<VAR>inst✝⁴ : AddCommGroup V1<VAR>inst✝³ : AffineSpace V1 P1<VAR>inst✝² : AddCommGroup V2<VAR>inst✝¹ : Module k V1<VAR>inst✝ : Module k V2<VAR>c p : P1<GOAL>(homothety c 0) p = (const k P1 c) p
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrderedAddCommGroup α<VAR>a b c d : α<VAR>h : a ≤ b<VAR>δ : α<VAR>inst✝ : Archimedean α<VAR>hδ : 0 < δ<GOAL>∃ m, ∀ n ≥ m, ↑(addNSMul h δ n) = b
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrderedAddCommGroup α<VAR>a b c d : α<VAR>h : a ≤ b<VAR>δ : α<VAR>inst✝ : Archimedean α<VAR>hδ : 0 < δ<VAR>m : ℕ<VAR>hm : b - a ≤ m • δ<GOAL>∃ m, ∀ n ≥ m, ↑(addNSMul h δ n) = b
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrderedAddCommGroup α<VAR>a b c d : α<VAR>h : a ≤ b<VAR>δ : α<VAR>inst✝ : Archimedean α<VAR>hδ : 0 < δ<VAR>m : ℕ<VAR>hm : b - a ≤ m • δ<VAR>n : ℕ<VAR>hn : n ≥ m<GOAL>↑(addNSMul h δ n) = b
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrderedAddCommGroup α<VAR>a b c d : α<VAR>h : a ≤ b<VAR>δ : α<VAR>inst✝ : Archimedean α<VAR>hδ : 0 < δ<VAR>m : ℕ<VAR>hm : b - a ≤ m • δ<VAR>n : ℕ<VAR>hn : n ≥ m<GOAL>b ≤ n • δ + a
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁵ : Ring K<VAR>inst✝⁴ : StrongRankCondition K<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module K V<VAR>inst✝¹ : Module.Free K V<VAR>inst✝ : Module.Finite K V<GOAL>lift.{u, v} #V = lift.{v, u} #K ^ lift.{u, v} (Module.rank K V)
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁵ : Ring K<VAR>inst✝⁴ : StrongRankCondition K<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module K V<VAR>inst✝¹ : Module.Free K V<VAR>inst✝ : Module.Finite K V<VAR>this : Nontrivial K<GOAL>lift.{u, v} #V = lift.{v, u} #K ^ lift.{u, v} (Module.rank K V)
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁵ : Ring K<VAR>inst✝⁴ : StrongRankCondition K<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module K V<VAR>inst✝¹ : Module.Free K V<VAR>inst✝ : Module.Finite K V<VAR>this : Nontrivial K<VAR>s : Type v<VAR>hs : Basis s K V<GOAL>lift.{u, v} #V = lift.{v, u} #K ^ lift.{u, v} (Module.rank K V)
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁵ : Ring K<VAR>inst✝⁴ : StrongRankCondition K<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module K V<VAR>inst✝¹ : Module.Free K V<VAR>inst✝ : Module.Finite K V<VAR>this✝ : Nontrivial K<VAR>s : Type v<VAR>hs : Basis s K V<VAR>this : Finite s<GOAL>lift.{u, v} #V = lift.{v, u} #K ^ lift.{u, v} (Module.rank K V)
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁵ : Ring K<VAR>inst✝⁴ : StrongRankCondition K<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module K V<VAR>inst✝¹ : Module.Free K V<VAR>inst✝ : Module.Finite K V<VAR>this✝¹ : Nontrivial K<VAR>s : Type v<VAR>hs : Basis s K V<VAR>this✝ : Finite s<VAR>this : lift.{max u v, v} #V = lift.{v, max u v} #(s →₀ K)<GOAL>lift.{u, v} #V = lift.{v, u} #K ^ lift.{u, v} (Module.rank K V)
<VAR>α : Type u<VAR>β : Type v<VAR>f✝ : α → α<VAR>m✝ n✝ : ℕ<VAR>a : α<VAR>f : α → α<VAR>m n : ℕ<GOAL>f^[n * m] = f^[m * n]
<VAR>m : ℕ<VAR>h : 0 < m<GOAL>range' (m - 1) (m - (m - 1)) = [m - 1]
<VAR>m : ℕ<VAR>h : 0 < m<GOAL>range' (m - 1) (succ 0) = [m - 1]
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝¹ : SemilatticeSup α<VAR>inst✝ : OrderBot α<VAR>s✝ s₁ s₂ : Finset β<VAR>f g : β → α<VAR>a : α<VAR>s : Finset β<GOAL>(s.sup fun x => ⊥) = ⊥
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝¹ : SemilatticeSup α<VAR>inst✝ : OrderBot α<VAR>s s₁ s₂ : Finset β<VAR>f g : β → α<VAR>a : α<GOAL>(∅.sup fun x => ⊥) = ⊥
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝¹ : SemilatticeSup α<VAR>inst✝ : OrderBot α<VAR>s✝ s₁ s₂ : Finset β<VAR>f g : β → α<VAR>a : α<VAR>s : Finset β<VAR>hs : s.Nonempty<GOAL>(s.sup fun x => ⊥) = ⊥
<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>S : Type u_2<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R S<VAR>I : Ideal S<VAR>T : Type u_3<VAR>inst✝ : CommRing T<VAR>f : R →+* T<GOAL>map f (spanNorm R I) = span (⇑f ∘ ⇑(Algebra.norm R) '' ↑I)
<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>S : Type u_2<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R S<VAR>I : Ideal S<VAR>T : Type u_3<VAR>inst✝ : CommRing T<VAR>f : R →+* T<GOAL>span ((fun x => f ((Algebra.norm R) x)) '' ↑I) = span (⇑f ∘ ⇑(Algebra.norm R) '' ↑I)
<VAR>R : Type u_1<VAR>inst✝ : NonUnitalNonAssocRing R<VAR>I : TwoSidedIdeal R<VAR>x : R<VAR>hx : x ∈ I<GOAL>-x ∈ I
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>E : Type u_5<VAR>inst✝³ : Countable G<VAR>inst✝² : Group G<VAR>inst✝¹ : MulAction G α<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>s : Set α<VAR>hs : IsFundamentalDomain G s μ<GOAL>μ (fundamentalFrontier G s) = 0
<VAR>C : Type u₁<VAR>inst✝ : Category.{v, u₁} C<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>U : Y.Opens<GOAL>((pullbackRestrictIsoRestrict f U).inv ≫ pullback.snd f U.ι) ≫ U.ι = (f ⁻¹ᵁ U).ι ≫ f
<VAR>x y : ℝ<GOAL>cos x ^ 2 + sin x ^ 2 = 1
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : Affine R<VAR>x y : R<GOAL>evalEval x y W.negPolynomial = W.negY x y
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : Affine R<VAR>x y : R<GOAL>evalEval x y (-Y - C (C W.a₁ * X + C W.a₃)) = -y - (W.a₁ * x + W.a₃)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_4<VAR>inst✝³ : Primcodable α<VAR>inst✝² : Primcodable β<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Primcodable σ<VAR>f : α →. σ<VAR>h : Partrec fun a => Part.map Option.some (f a)<VAR>n : ℕ<GOAL>(do let n ← (↑(decode n)).bind fun a => Part.map encode ((fun a => Part.map Option.some (f a)) a) ↑n.ppred) = (↑(decode n)).bind fun a => Part.map encode (f a)
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CompatibleRing R<VAR>p : FreeCommRing α<VAR>v : α → R<VAR>x✝ : CompatibleRing (FreeCommRing α) := compatibleRingOfRing (FreeCommRing α)<GOAL>Term.realize v (Classical.choose ⋯) = (FreeCommRing.lift v) p
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CompatibleRing R<VAR>p : FreeCommRing α<VAR>v : α → R<VAR>x✝ : CompatibleRing (FreeCommRing α) := compatibleRingOfRing (FreeCommRing α)<GOAL>Term.realize v (Classical.choose ⋯) = (FreeCommRing.lift v) (Term.realize FreeCommRing.of (Classical.choose ⋯))
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g : ι → α<VAR>hF : UniformCauchySeqOn F p s<GOAL>UniformCauchySeqOnFilter F p (𝓟 s)
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>f : α → Option β → γ<VAR>as✝ : List α<VAR>a : α<VAR>as : List α<VAR>b : β<VAR>bs : List β<VAR>h : (a :: as).length ≤ (b :: bs).length<GOAL>map₂Left f (a :: as) (b :: bs) = zipWith (fun a b => f a (some b)) (a :: as) (b :: bs)
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>f : α → Option β → γ<VAR>as✝ : List α<VAR>a : α<VAR>as : List α<VAR>b : β<VAR>bs : List β<VAR>h : as.length ≤ bs.length<GOAL>map₂Left f (a :: as) (b :: bs) = zipWith (fun a b => f a (some b)) (a :: as) (b :: bs)
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>H : Subgroup G<VAR>inst✝ : H.Normal<VAR>h : Group.IsNilpotent G<GOAL>NormalizerCondition G
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>H : Subgroup G<VAR>inst✝ : H.Normal<VAR>h : Group.IsNilpotent G<GOAL>∀ (H : Subgroup G), H.normalizer = H → H = ⊤
<GOAL>∀ (G : Type u_1) [inst : Group G] [inst_1 : Subsingleton G] (H : Subgroup G), H.normalizer = H → H = ⊤
<GOAL>∀ (G : Type u_1) [inst : Group G] [inst_1 : Group.IsNilpotent G], (∀ (H : Subgroup (G ⧸ center G)), H.normalizer = H → H = ⊤) → ∀ (H : Subgroup G), H.normalizer = H → H = ⊤
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>J : Type<VAR>inst✝¹ : Fintype J<VAR>f : J → C<VAR>inst✝ : HasBiproduct f<VAR>T : C<VAR>g : (j : J) → T ⟶ f j<VAR>j : J<GOAL>lift g ≫ π f j = (∑ j : J, g j ≫ ι f j) ≫ π f j
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x y z : α<VAR>δ ε ε₁ ε₂ : ℝ<VAR>s : Set α<VAR>F : ι → β → α<VAR>f : β → α<VAR>p : Filter ι<GOAL>TendstoUniformly F f p ↔ ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ (x : β), dist (f x) (F n x) < ε
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x y z : α<VAR>δ ε ε₁ ε₂ : ℝ<VAR>s : Set α<VAR>F : ι → β → α<VAR>f : β → α<VAR>p : Filter ι<GOAL>(∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ univ, dist (f x) (F n x) < ε) ↔ ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ (x : β), dist (f x) (F n x) < ε
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : Order.Frame α<VAR>a : α<VAR>ha : IsAtom a<VAR>f : ι → α<GOAL>a ≤ iSup f ↔ ∃ i, a ≤ f i
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : Order.Frame α<VAR>a : α<VAR>ha : IsAtom a<VAR>f : ι → α<GOAL>a ≤ iSup f → ∃ i, a ≤ f i
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : Order.Frame α<VAR>a : α<VAR>ha : IsAtom a<VAR>f : ι → α<GOAL>a ≤ ⨆ i, f i → ∃ i, a ≤ f i
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : Order.Frame α<VAR>a : α<VAR>ha : IsAtom a<VAR>f : ι → α<VAR>h : a ≤ ⨆ i, f i<VAR>ha' : ¬∃ i, a ≤ f i<GOAL>False
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : Order.Frame α<VAR>a : α<VAR>ha : IsAtom a<VAR>f : ι → α<VAR>h : a ≤ ⨆ i, f i<VAR>ha' : ∀ (i : ι), ¬a ≤ f i<GOAL>False
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : Order.Frame α<VAR>a : α<VAR>ha : IsAtom a<VAR>f : ι → α<VAR>h : a ≤ ⨆ i, f i<VAR>ha' : ∀ (i : ι), ¬a ≤ f i<VAR>ha'' : Disjoint a (⨆ i, f i)<GOAL>False
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : Order.Frame α<VAR>f : ι → α<VAR>ha : IsAtom ⊥<VAR>h : ⊥ ≤ ⨆ i, f i<VAR>ha' : ∀ (i : ι), ¬⊥ ≤ f i<VAR>ha'' : Disjoint ⊥ (⨆ i, f i)<GOAL>False
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g : ι → α<GOAL>(∀ u ∈ 𝓤 β, ∀ᶠ (m : ι × ι) in p ×ˢ p, ∀ x ∈ s, (F m.1 x, F m.2 x) ∈ u) ↔ ∀ u ∈ 𝓤 β, ∀ᶠ (m : (ι × ι) × α) in (p ×ˢ p) ×ˢ 𝓟 s, (F m.1.1 m.2, F m.1.2 m.2) ∈ u
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g : ι → α<VAR>u : Set (β × β)<VAR>hu : u ∈ 𝓤 β<GOAL>(∀ᶠ (m : ι × ι) in p ×ˢ p, ∀ x ∈ s, (F m.1 x, F m.2 x) ∈ u) ↔ ∀ᶠ (m : (ι × ι) × α) in (p ×ˢ p) ×ˢ 𝓟 s, (F m.1.1 m.2, F m.1.2 m.2) ∈ u
<VAR>x y z : ℝ<VAR>n : ℕ<VAR>b : ℝ<VAR>hb₀ : 0 < b<VAR>hb₁ : b < 1<GOAL>StrictAnti fun x => b ^ x
<VAR>x y z : ℝ<VAR>n : ℕ<VAR>b : ℝ<VAR>hb₀ : 0 < b<VAR>hb₁ : b < 1<GOAL>StrictAnti fun x => rexp (log b * x)
<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>α : Type u_2<VAR>f : M × ↥S → M × ↥S → α<VAR>wd : ∀ (p q p' q' : M × ↥S), p ≈ p' → q ≈ q' → f p q = f p' q'<VAR>m m' : M<VAR>s s' : ↥S<GOAL>(mk m s).liftOn₂ (mk m' s') f wd = f (m, s) (m', s')
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y : V<VAR>h : ‖x‖ = ‖y‖<GOAL>angle x (x - y) = angle y (y - x)
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y : V<VAR>h : ‖x‖ = ‖y‖<GOAL>Real.cos (angle x (x - y)) = Real.cos (angle y (y - x))
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝³ : LinearOrderedField α<VAR>inst✝² : ConditionallyCompleteLinearOrderedField β<VAR>inst✝¹ : ConditionallyCompleteLinearOrderedField γ<VAR>inst✝ : Archimedean α<VAR>a : α<VAR>b✝ : β<VAR>q : ℚ<VAR>ha : 0 < a<VAR>b : β<VAR>hba : b < inducedMap α β a * inducedMap α β a<GOAL>∃ c ∈ cutMap β (a * a), b < c
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝³ : LinearOrderedField α<VAR>inst✝² : ConditionallyCompleteLinearOrderedField β<VAR>inst✝¹ : ConditionallyCompleteLinearOrderedField γ<VAR>inst✝ : Archimedean α<VAR>a : α<VAR>b✝ : β<VAR>q : ℚ<VAR>ha : 0 < a<VAR>b : β<VAR>hba : b < inducedMap α β a * inducedMap α β a<VAR>hb : b < 0<GOAL>∃ c ∈ cutMap β (a * a), b < c
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝³ : LinearOrderedField α<VAR>inst✝² : ConditionallyCompleteLinearOrderedField β<VAR>inst✝¹ : ConditionallyCompleteLinearOrderedField γ<VAR>inst✝ : Archimedean α<VAR>a : α<VAR>b✝ : β<VAR>q : ℚ<VAR>ha : 0 < a<VAR>b : β<VAR>hba : b < inducedMap α β a * inducedMap α β a<VAR>hb : 0 ≤ b<GOAL>∃ c ∈ cutMap β (a * a), b < c
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝³ : LinearOrderedField α<VAR>inst✝² : ConditionallyCompleteLinearOrderedField β<VAR>inst✝¹ : ConditionallyCompleteLinearOrderedField γ<VAR>inst✝ : Archimedean α<VAR>a : α<VAR>b✝ : β<VAR>q✝ : ℚ<VAR>ha : 0 < a<VAR>b : β<VAR>hba : b < inducedMap α β a * inducedMap α β a<VAR>hb : 0 ≤ b<VAR>q : ℚ<VAR>hq : 0 < q<VAR>hbq : b < ↑q ^ 2<VAR>hqa : ↑q ^ 2 < inducedMap α β a * inducedMap α β a<GOAL>∃ c ∈ cutMap β (a * a), b < c
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝³ : LinearOrderedField α<VAR>inst✝² : ConditionallyCompleteLinearOrderedField β<VAR>inst✝¹ : ConditionallyCompleteLinearOrderedField γ<VAR>inst✝ : Archimedean α<VAR>a : α<VAR>b✝ : β<VAR>q✝ : ℚ<VAR>ha : 0 < a<VAR>b : β<VAR>hba : b < inducedMap α β a * inducedMap α β a<VAR>hb : 0 ≤ b<VAR>q : ℚ<VAR>hq : 0 < q<VAR>hbq : b < ↑(q ^ 2)<VAR>hqa : ↑q ^ 2 < inducedMap α β a * inducedMap α β a<GOAL>∃ c ∈ cutMap β (a * a), b < c
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝³ : LinearOrderedField α<VAR>inst✝² : ConditionallyCompleteLinearOrderedField β<VAR>inst✝¹ : ConditionallyCompleteLinearOrderedField γ<VAR>inst✝ : Archimedean α<VAR>a : α<VAR>b✝ : β<VAR>q✝ : ℚ<VAR>ha : 0 < a<VAR>b : β<VAR>hba : b < inducedMap α β a * inducedMap α β a<VAR>hb : 0 ≤ b<VAR>q : ℚ<VAR>hq : 0 < q<VAR>hbq : b < ↑(q ^ 2)<VAR>hqa : ↑q ^ 2 < inducedMap α β a * inducedMap α β a<GOAL>↑(q ^ 2) < a * a
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝³ : LinearOrderedField α<VAR>inst✝² : ConditionallyCompleteLinearOrderedField β<VAR>inst✝¹ : ConditionallyCompleteLinearOrderedField γ<VAR>inst✝ : Archimedean α<VAR>a : α<VAR>b✝ : β<VAR>q✝ : ℚ<VAR>ha : 0 < a<VAR>b : β<VAR>hba : b < inducedMap α β a * inducedMap α β a<VAR>hb : 0 ≤ b<VAR>q : ℚ<VAR>hq : 0 < q<VAR>hbq : b < ↑(q ^ 2)<VAR>hqa : ↑q * ↑q < inducedMap α β a * inducedMap α β a<GOAL>↑(q * q) < a * a
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝³ : LinearOrderedField α<VAR>inst✝² : ConditionallyCompleteLinearOrderedField β<VAR>inst✝¹ : ConditionallyCompleteLinearOrderedField γ<VAR>inst✝ : Archimedean α<VAR>a : α<VAR>b✝ : β<VAR>q✝ : ℚ<VAR>ha : 0 < a<VAR>b : β<VAR>hba : b < inducedMap α β a * inducedMap α β a<VAR>hb : 0 ≤ b<VAR>q : ℚ<VAR>hq : 0 < q<VAR>hbq : b < ↑(q ^ 2)<VAR>hqa : ↑q * ↑q < inducedMap α β a * inducedMap α β a<GOAL>↑q * ↑q < a * a
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝³ : LinearOrderedField α<VAR>inst✝² : ConditionallyCompleteLinearOrderedField β<VAR>inst✝¹ : ConditionallyCompleteLinearOrderedField γ<VAR>inst✝ : Archimedean α<VAR>a : α<VAR>b✝ : β<VAR>q✝ : ℚ<VAR>ha : 0 < a<VAR>b : β<VAR>hba : b < inducedMap α β a * inducedMap α β a<VAR>hb : 0 ≤ b<VAR>q : ℚ<VAR>hq : 0 < q<VAR>hbq : b < ↑(q ^ 2)<VAR>hqa : ↑q * ↑q < inducedMap α β a * inducedMap α β a<VAR>q' : ℚ<VAR>hq' : ↑q < ↑q'<VAR>hqa' : ↑q' < a<GOAL>↑q * ↑q < a * a
<VAR>α : Type u_1<VAR>a : α<VAR>l : List α<VAR>p : α → Bool<VAR>h : p a = true<GOAL>eraseP p (a :: l) = l
<VAR>α β : Type u<VAR>n : ℕ<VAR>c : Cardinal.{u_1}<GOAL>↑n + 1 ≤ c ↔ ↑n < c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : PartialOrder α<VAR>a b c : α<VAR>h : a ⩿ b<GOAL>Ico a b ⊆ {a}
<VAR>Γ : Type u_1<VAR>Γ' : Type u_2<VAR>R : Type u_3<VAR>V : Type u_4<VAR>inst✝¹ : OrderedCancelAddCommMonoid Γ<VAR>inst✝ : NonAssocSemiring R<VAR>r s : R<VAR>rs : C r = C s<GOAL>r = s
<VAR>Γ : Type u_1<VAR>Γ' : Type u_2<VAR>R : Type u_3<VAR>V : Type u_4<VAR>inst✝¹ : OrderedCancelAddCommMonoid Γ<VAR>inst✝ : NonAssocSemiring R<VAR>r s : R<VAR>rs : ∀ (a : Γ), (C r).coeff a = (C s).coeff a<GOAL>r = s
<VAR>Γ : Type u_1<VAR>Γ' : Type u_2<VAR>R : Type u_3<VAR>V : Type u_4<VAR>inst✝¹ : OrderedCancelAddCommMonoid Γ<VAR>inst✝ : NonAssocSemiring R<VAR>r s : R<VAR>rs : ∀ (a : Γ), (C r).coeff a = (C s).coeff a<VAR>h : (C r).coeff 0 = (C s).coeff 0<GOAL>r = s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>f : α → E<VAR>p : ℝ≥0∞<VAR>μ : Measure α<VAR>P : (α → E) → Prop<VAR>h_ind : ∀ (c : E) ⦃s : Set α⦄, MeasurableSet s → μ s < ⊤ → P (s.indicator fun x => c)<VAR>h_add : ∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → Integrable f μ → Integrable g μ → P f → P g → P (f + g)<VAR>h_closed : IsClosed {f | P ↑↑f}<VAR>h_ae : ∀ ⦃f g : α → E⦄, f =ᶠ[ae μ] g → Integrable f μ → P f → P g<GOAL>∀ ⦃f : α → E⦄, Integrable f μ → P f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>f : α → E<VAR>p : ℝ≥0∞<VAR>μ : Measure α<VAR>P : (α → E) → Prop<VAR>h_ind : ∀ (c : E) ⦃s : Set α⦄, MeasurableSet s → μ s < ⊤ → P (s.indicator fun x => c)<VAR>h_closed : IsClosed {f | P ↑↑f}<VAR>h_add : ∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → Memℒp f 1 μ → Memℒp g 1 μ → P f → P g → P (f + g)<VAR>h_ae : ∀ ⦃f g : α → E⦄, f =ᶠ[ae μ] g → Memℒp f 1 μ → P f → P g<GOAL>∀ ⦃f : α → E⦄, Memℒp f 1 μ → P f
<VAR>n a b n' a' b' : ℕ<VAR>H : IsFibAux n a b<VAR>hn : 2 * n + 1 = n'<VAR>h1 : a * a + b * b = a'<VAR>h2 : b * (2 * a + b) = b'<GOAL>fib n' = a'
<VAR>n a b n' a' b' : ℕ<VAR>H : IsFibAux n a b<VAR>hn : 2 * n + 1 = n'<VAR>h1 : a * a + b * b = a'<VAR>h2 : b * (2 * a + b) = b'<GOAL>fib (n' + 1) = b'
<VAR>a : UnitAddCircle<VAR>s : ℂ<VAR>hs : ∀ (n : ℕ), s ≠ 1 - ↑n<GOAL>cosZeta a (1 - s) = s.Gammaℂ * Complex.cos (↑π * s / 2) * hurwitzZetaEven a s
<VAR>a : UnitAddCircle<VAR>s : ℂ<VAR>hs : ∀ (n : ℕ), s ≠ 1 - ↑n<VAR>this : cosZeta a (1 - s) = completedCosZeta a (1 - s) * (1 - s).Gammaℝ⁻¹<GOAL>cosZeta a (1 - s) = s.Gammaℂ * Complex.cos (↑π * s / 2) * hurwitzZetaEven a s
<VAR>a : UnitAddCircle<VAR>s : ℂ<VAR>hs : ∀ (n : ℕ), s ≠ 1 - ↑n<VAR>this : cosZeta a (1 - s) = completedCosZeta a (1 - s) * (1 - s).Gammaℝ⁻¹<GOAL>completedHurwitzZetaEven a s * (s.Gammaℂ * Complex.cos (↑π * s / 2) * s.Gammaℝ⁻¹) = s.Gammaℂ * Complex.cos (↑π * s / 2) * (completedHurwitzZetaEven a s / s.Gammaℝ)
<VAR>R✝ : Type u<VAR>F : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>inst✝⁷ : NonUnitalSemiring R<VAR>inst✝⁶ : PartialOrder R<VAR>inst✝⁵ : StarRing R<VAR>inst✝⁴ : StarOrderedRing R<VAR>inst✝³ : NonUnitalSemiring S<VAR>inst✝² : PartialOrder S<VAR>inst✝¹ : StarRing S<VAR>inst✝ : StarOrderedRing S<VAR>f : R →⋆ₙ+* S<VAR>x y : R<VAR>hxy : x ≤ y<GOAL>f x ≤ f y
<VAR>R✝ : Type u<VAR>F : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>inst✝⁷ : NonUnitalSemiring R<VAR>inst✝⁶ : PartialOrder R<VAR>inst✝⁵ : StarRing R<VAR>inst✝⁴ : StarOrderedRing R<VAR>inst✝³ : NonUnitalSemiring S<VAR>inst✝² : PartialOrder S<VAR>inst✝¹ : StarRing S<VAR>inst✝ : StarOrderedRing S<VAR>f : R →⋆ₙ+* S<VAR>x y : R<VAR>hxy : ∃ p ∈ AddSubmonoid.closure (range fun s => star s * s), y = x + p<GOAL>∃ p ∈ AddSubmonoid.closure (range fun s => star s * s), f y = f x + p
<VAR>R✝ : Type u<VAR>F : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>inst✝⁷ : NonUnitalSemiring R<VAR>inst✝⁶ : PartialOrder R<VAR>inst✝⁵ : StarRing R<VAR>inst✝⁴ : StarOrderedRing R<VAR>inst✝³ : NonUnitalSemiring S<VAR>inst✝² : PartialOrder S<VAR>inst✝¹ : StarRing S<VAR>inst✝ : StarOrderedRing S<VAR>f : R →⋆ₙ+* S<VAR>x p : R<VAR>hp : p ∈ AddSubmonoid.closure (range fun s => star s * s)<GOAL>∃ p_1 ∈ AddSubmonoid.closure (range fun s => star s * s), f (x + p) = f x + p_1