ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>inst✝ : NonUnitalNonAssocRing R<VAR>I✝ I J : TwoSidedIdeal R<GOAL>↑I ⊆ ↑J ∧ I ≠ J ↔ ↑I ⊆ ↑J ∧ ↑I ≠ ↑J
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>k : Type u_3<VAR>V : Type u_4<VAR>P : Type u_5<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : AffineSpace V P<VAR>inst✝¹ : Ring k<VAR>inst✝ : Module k V<VAR>b : AffineBasis ι k P<VAR>s : Finset ι<VAR>i j : ι<VAR>e : ι ≃ ι'<VAR>hι : IsEmpty ι<GOAL>False
<VAR>R : Type u<VAR>K : Type u'<VAR>M : Type v<VAR>V : Type v'<VAR>M₂ : Type w<VAR>V₂ : Type w'<VAR>M₃ : Type y<VAR>V₃ : Type y'<VAR>M₄ : Type z<VAR>ι : Type x<VAR>M₅ : Type u_1<VAR>M₆ : Type u_2<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : AddCommMonoid M₂<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R M₂<VAR>p : Submodule R M<VAR>q : Submodule R M₂<GOAL>range (fst R M M₂) = ⊤
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>I J : Box ι<VAR>π : TaggedPrepartition I<VAR>inst✝ : Fintype ι<VAR>l : IntegrationParams<VAR>f g : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>y y' : F<VAR>c c₁ c₂ : ℝ≥0<VAR>ε ε₁ ε₂ : ℝ<VAR>π₁ π₂ : TaggedPrepartition I<VAR>h : Integrable I l f vol<VAR>π₀ : Prepartition I<GOAL>Filter.map (integralSum f vol) (l.toFilteriUnion I π₀) ×ˢ Filter.map (integralSum f vol) (l.toFilteriUnion I π₀) ≤ 𝓤 F
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>I J : Box ι<VAR>π : TaggedPrepartition I<VAR>inst✝ : Fintype ι<VAR>l : IntegrationParams<VAR>f g : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>y y' : F<VAR>c c₁ c₂ : ℝ≥0<VAR>ε ε₁ ε₂ : ℝ<VAR>π₁ π₂ : TaggedPrepartition I<VAR>h : Integrable I l f vol<VAR>π₀ : Prepartition I<GOAL>Filter.map (fun p => (integralSum f vol p.1, integralSum f vol p.2)) (l.toFilter I ×ˢ l.toFilter I ⊓ 𝓟 ({π | π.iUnion = π₀.iUnion} ×ˢ {π | π.iUnion = π₀.iUnion})) ≤ 𝓤 F
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β✝<VAR>inst✝¹ : MeasurableSpace γ<VAR>μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s s' t : Set α<VAR>f✝ : α → β✝<VAR>β : Type u_8<VAR>inst✝ : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>f : α → β<VAR>hfi : Injective f<VAR>hf : ∀ (s : Set α), MeasurableSet s → MeasurableSet (f '' s)<VAR>μ : Measure β<VAR>hs : MeasurableSet s<GOAL>((comapₗ f) μ) s = μ (f '' s)
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β✝<VAR>inst✝¹ : MeasurableSpace γ<VAR>μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s s' t : Set α<VAR>f✝ : α → β✝<VAR>β : Type u_8<VAR>inst✝ : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>f : α → β<VAR>hfi : Injective f<VAR>hf : ∀ (s : Set α), MeasurableSet s → MeasurableSet (f '' s)<VAR>μ : Measure β<VAR>hs : MeasurableSet s<GOAL>Injective f ∧ ∀ (s : Set α), MeasurableSet s → MeasurableSet (f '' s)
<VAR>L : Language<VAR>ι : Type v<VAR>inst✝⁵ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝⁴ : (i : ι) → L.Structure (G i)<VAR>f : (i j : ι) → i ≤ j → G i ↪[L] G j<VAR>inst✝³ : Nonempty ι<VAR>inst✝² : IsDirected ι fun x x_1 => x ≤ x_1<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝¹ : L.Structure M<VAR>inst✝ : L.Structure N<VAR>S : ι →o L.Substructure M<VAR>i : ι<VAR>x : ↥(S i)<GOAL>((Equiv_iSup S).symm.toEmbedding.comp (Substructure.inclusion ⋯)) x = (of L ι (fun x => ↥(S x)) (fun x x_1 h => Substructure.inclusion ⋯) i) x
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁶ : Field F<VAR>inst✝⁵ : Field E<VAR>inst✝⁴ : Algebra F E<VAR>K : Type w<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra F K<VAR>L : IntermediateField F E<VAR>inst✝¹ : IsPurelyInseparable F ↥L<VAR>inst✝ : Algebra.IsSeparable F ↥L<VAR>x : E<VAR>hx : x ∈ L<GOAL>x ∈ ⊥
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁶ : Field F<VAR>inst✝⁵ : Field E<VAR>inst✝⁴ : Algebra F E<VAR>K : Type w<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra F K<VAR>L : IntermediateField F E<VAR>inst✝¹ : IsPurelyInseparable F ↥L<VAR>inst✝ : Algebra.IsSeparable F ↥L<VAR>x : E<VAR>hx : x ∈ L<VAR>y : F<VAR>hy : (algebraMap F ↥L) y = ⟨x, hx⟩<GOAL>x ∈ ⊥
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Ring k<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>p : ι → P<VAR>j : ι<VAR>w₁ w₂ : ι → k<VAR>hw : ∀ (i : ι), i ≠ j → w₁ i = w₂ i<GOAL>(s.weightedVSubOfPoint p (p j)) w₁ = (s.weightedVSubOfPoint p (p j)) w₂
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Ring k<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>p : ι → P<VAR>j : ι<VAR>w₁ w₂ : ι → k<VAR>hw : ∀ (i : ι), i ≠ j → w₁ i = w₂ i<GOAL>∑ i ∈ s, w₁ i • (p i -ᵥ p j) = ∑ i ∈ s, w₂ i • (p i -ᵥ p j)
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Ring k<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>p : ι → P<VAR>j : ι<VAR>w₁ w₂ : ι → k<VAR>hw : ∀ (i : ι), i ≠ j → w₁ i = w₂ i<VAR>i : ι<GOAL>w₁ i • (p i -ᵥ p j) = w₂ i • (p i -ᵥ p j)
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Ring k<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>p : ι → P<VAR>j : ι<VAR>w₁ w₂ : ι → k<VAR>hw : ∀ (i : ι), i ≠ j → w₁ i = w₂ i<VAR>i : ι<VAR>h : i = j<GOAL>w₁ i • (p i -ᵥ p j) = w₂ i • (p i -ᵥ p j)
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Ring k<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>p : ι → P<VAR>j : ι<VAR>w₁ w₂ : ι → k<VAR>hw : ∀ (i : ι), i ≠ j → w₁ i = w₂ i<VAR>i : ι<VAR>h : i ≠ j<GOAL>w₁ i • (p i -ᵥ p j) = w₂ i • (p i -ᵥ p j)
<VAR>n : ℕ<GOAL>eval 1 (bernoulli n) = bernoulli' n
<VAR>n : ℕ<GOAL>∑ i ∈ range (n + 1), eval 1 ((monomial (n - i)) (_root_.bernoulli i * ↑(n.choose i))) = bernoulli' n
<VAR>n : ℕ<GOAL>(if n = 1 then 1 else 0) + _root_.bernoulli n = bernoulli' n
<VAR>C : Type u₁<VAR>inst✝⁶ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝⁵ : Category.{v₂, u₂} D<VAR>inst✝⁴ : HasZeroMorphisms C<VAR>inst✝³ : HasZeroMorphisms D<VAR>J : Type w₁<VAR>F : C ⥤ D<VAR>f : J → C<VAR>inst✝² : HasBiproduct f<VAR>inst✝¹ : HasBiproduct (F.obj ∘ f)<VAR>inst✝ : F.PreservesZeroMorphisms<GOAL>F.biproductComparison' f ≫ F.biproductComparison f = 𝟙 (⨁ F.obj ∘ f)
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>hr : r ≠ 0<GOAL>1 ≤ ↑r * ↑r⁻¹
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(-π / 2)<GOAL>⟪y, x⟫_ℝ = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : TopologicalSpace δ<VAR>e : α → β<VAR>de : DenseEmbedding e<VAR>p : α → Prop<VAR>x : β<VAR>hx : x ∈ closure (e '' {x | p x})<GOAL>⟨x, hx⟩ ∈ closure (range (subtypeEmb p e)) ↔ ⟨x, hx⟩ ∈ univ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : TopologicalSpace δ<VAR>e : α → β<VAR>de : DenseEmbedding e<VAR>p : α → Prop<VAR>x : β<VAR>hx✝ : x ∈ closure (e '' {x | p x})<VAR>hx : x ∈ closure (range fun x => e ↑x)<GOAL>⟨x, hx✝⟩ ∈ closure (range (subtypeEmb p e)) ↔ ⟨x, hx✝⟩ ∈ univ
<VAR>α✝ : Type u_1<VAR>G : Type u_2<VAR>α : Type u_3<VAR>inst✝⁵ : Inv G<VAR>inst✝⁴ : MeasurableSpace G<VAR>inst✝³ : MeasurableInv G<VAR>m : MeasurableSpace α<VAR>f✝ : α → G<VAR>μ : Measure α<VAR>G₀ : Type u_4<VAR>inst✝² : GroupWithZero G₀<VAR>inst✝¹ : MeasurableSpace G₀<VAR>inst✝ : MeasurableInv G₀<VAR>f : α → G₀<VAR>h : Measurable fun x => (f x)⁻¹<GOAL>Measurable f
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l : Filter α<VAR>f : α → β<VAR>x : ι → Filter α<VAR>y : Filter β<GOAL>Tendsto f (⨆ i, x i) y ↔ ∀ (i : ι), Tendsto f (x i) y
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>α : ι → Type u_6<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : DecidableEq κ<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : (i : ι) → DecidableEq (α i)<VAR>s : Finset κ<VAR>i : ι<VAR>j : κ<GOAL>(if j ∈ s then ∏ b ∈ univ.erase i, s.card else 0) = if j ∈ s then s.card ^ (card ι - 1) else 0
<VAR>x y z : ℝ<VAR>n : ℕ<VAR>hx0 : 0 < x<VAR>hx1 : x ≤ 1<VAR>hyz : z ≤ y<GOAL>x ^ y ≤ x ^ z
<VAR>x y z : ℝ<VAR>n : ℕ<VAR>hx0 : 0 < x<VAR>hx1 : x ≤ 1<VAR>hyz : z ≤ y<GOAL>rexp (log x * y) ≤ rexp (log x * z)
<VAR>x y z : ℝ<VAR>n : ℕ<VAR>hx0 : 0 < x<VAR>hx1 : x ≤ 1<VAR>hyz : z ≤ y<GOAL>log x * y ≤ log x * z
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝¹ : Zero M<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<VAR>f : α →₀ M<GOAL>filter p f = 0 ↔ ∀ (x : α), p x → f x = 0
<VAR>k : Type u_1<VAR>V1 : Type u_2<VAR>P1 : Type u_3<VAR>V2 : Type u_4<VAR>P2 : Type u_5<VAR>V3 : Type u_6<VAR>P3 : Type u_7<VAR>V4 : Type u_8<VAR>P4 : Type u_9<VAR>inst✝¹² : Ring k<VAR>inst✝¹¹ : AddCommGroup V1<VAR>inst✝¹⁰ : Module k V1<VAR>inst✝⁹ : AffineSpace V1 P1<VAR>inst✝⁸ : AddCommGroup V2<VAR>inst✝⁷ : Module k V2<VAR>inst✝⁶ : AffineSpace V2 P2<VAR>inst✝⁵ : AddCommGroup V3<VAR>inst✝⁴ : Module k V3<VAR>inst✝³ : AffineSpace V3 P3<VAR>inst✝² : AddCommGroup V4<VAR>inst✝¹ : Module k V4<VAR>inst✝ : AffineSpace V4 P4<VAR>p₀ p₁ : P1<GOAL>(lineMap p₀ p₁) 1 = p₁
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>V W : FGModuleCat K<GOAL>FGModuleCatDual K V ◁ FGModuleCatCoevaluation K V ≫ (α_ (FGModuleCatDual K V) V (FGModuleCatDual K V)).inv ≫ FGModuleCatEvaluation K V ▷ FGModuleCatDual K V = (ρ_ (FGModuleCatDual K V)).hom ≫ (λ_ (FGModuleCatDual K V)).inv
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v}<VAR>h : sup f = lsub f<VAR>i : ι<GOAL>f i < lsub f
<VAR>R : Type u<VAR>S✝ : Type v<VAR>a b : R<VAR>m n : ℕ<VAR>ι : Type y<VAR>inst✝² : Semiring R<VAR>p✝ : R[X]<VAR>S : Type u_1<VAR>inst✝¹ : Monoid S<VAR>inst✝ : DistribMulAction S R<VAR>k : S<VAR>p : R[X]<VAR>h : IsSMulRegular R k<GOAL>(k • p).leadingCoeff = k • p.leadingCoeff
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : MeasurableSpace X<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f g : X → E<VAR>s t : Set X<VAR>μ ν : Measure X<VAR>l l' : Filter X<VAR>ht : NullMeasurableSet t μ<VAR>hts : s ⊆ t<VAR>h't : ∀ᵐ (x : X) ∂μ, x ∈ t \ s → f x = 0<VAR>h : IntegrableOn f t μ<GOAL>∫ (x : X) in t, f x ∂μ = ∫ (x : X) in s, f x ∂μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : MeasurableSpace X<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f g : X → E<VAR>s t : Set X<VAR>μ ν : Measure X<VAR>l l' : Filter X<VAR>ht : NullMeasurableSet t μ<VAR>hts : s ⊆ t<VAR>h't : ∀ᵐ (x : X) ∂μ, x ∈ t \ s → f x = 0<VAR>h : IntegrableOn f t μ<VAR>f' : X → E := AEStronglyMeasurable.mk f ⋯<GOAL>∫ (x : X) in t, f x ∂μ = ∫ (x : X) in s, f x ∂μ
<VAR>𝕜 : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>inst✝³ : MeasurableSpace G<VAR>inst✝² : MeasurableSpace H<VAR>inst✝¹ : Mul G<VAR>μ✝ : Measure G<VAR>inst✝ : MeasurableMul G<VAR>μ : Measure G<GOAL>(∀ (g : G), Measure.map (fun x => g * x) μ = μ) ↔ μ.IsMulLeftInvariant
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>inst✝² : NontriviallyNormedField 𝕂<VAR>inst✝¹ : NormedDivisionRing 𝔸<VAR>inst✝ : NormedAlgebra 𝕂 𝔸<VAR>x : 𝔸<VAR>hx : x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius<GOAL>Summable (norm ∘ fun n => x ^ n / ↑n !)
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>inst✝² : NontriviallyNormedField 𝕂<VAR>inst✝¹ : NormedDivisionRing 𝔸<VAR>inst✝ : NormedAlgebra 𝕂 𝔸<VAR>x : 𝔸<VAR>hx : x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius<GOAL>Summable (norm ∘ fun n => (expSeries 𝕂 𝔸 n) fun x_1 => x)
<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>φ n = n.factorization.prod fun p k => p ^ (k - 1) * (p - 1)
<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>(n.factorization.prod fun p k => φ (p ^ k)) = n.factorization.prod fun p k => p ^ (k - 1) * (p - 1)
<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>∀ x ∈ n.factorization.support, φ (x ^ n.factorization x) = x ^ (n.factorization x - 1) * (x - 1)
<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>p : ℕ<VAR>hp : p ∈ n.factorization.support<GOAL>φ (p ^ n.factorization p) = p ^ (n.factorization p - 1) * (p - 1)
<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>p : ℕ<VAR>hp : p ∈ n.factorization.support<VAR>h : 0 < n.factorization p<GOAL>φ (p ^ n.factorization p) = p ^ (n.factorization p - 1) * (p - 1)
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>γ' : Type u_6<VAR>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>ζ : Type u_11<VAR>ζ' : Type u_12<VAR>ν : Type u_13<VAR>f✝ f' : α → β → γ<VAR>g✝ g' : α → β → γ → δ<VAR>s s' : Set α<VAR>t t' : Set β<VAR>u u' : Set γ<VAR>v : Set δ<VAR>a a' : α<VAR>b b' : β<VAR>c c' : γ<VAR>d d' : δ<VAR>f : α → β → γ<VAR>g : γ → δ<GOAL>g '' image2 f s t = image2 (fun a b => g (f a b)) s t
<VAR>α : Type u<VAR>β : Type u_1<VAR>t : TopologicalSpace α<VAR>B : Set (Set α)<VAR>s : Set α<VAR>t₁ t₂ : TopologicalSpace β<VAR>B₁ B₂ : Set (Set β)<VAR>h₁ : IsTopologicalBasis B₁<VAR>h₂ : IsTopologicalBasis B₂<GOAL>IsTopologicalBasis (image2 (fun x x_1 => x ∩ x_1) B₁ B₂)
<VAR>α : Type u<VAR>β : Type u_1<VAR>t : TopologicalSpace α<VAR>B : Set (Set α)<VAR>s : Set α<VAR>t₁ t₂ : TopologicalSpace β<VAR>B₁ B₂ : Set (Set β)<VAR>h₁ : IsTopologicalBasis B₁<VAR>h₂ : IsTopologicalBasis B₂<VAR>a : β<GOAL>(𝓝 a).HasBasis (fun t => t ∈ image2 (fun x x_1 => x ∩ x_1) B₁ B₂ ∧ a ∈ t) id
<VAR>α : Type u<VAR>β : Type u_1<VAR>t : TopologicalSpace α<VAR>B : Set (Set α)<VAR>s : Set α<VAR>t₁ t₂ : TopologicalSpace β<VAR>B₁ B₂ : Set (Set β)<VAR>h₁ : IsTopologicalBasis B₁<VAR>h₂ : IsTopologicalBasis B₂<VAR>a : β<GOAL>(𝓝 a ⊓ 𝓝 a).HasBasis (fun t => t ∈ image2 (fun x x_1 => x ∩ x_1) B₁ B₂ ∧ a ∈ t) id
<VAR>α : Type u<VAR>β : Type u_1<VAR>t : TopologicalSpace α<VAR>B : Set (Set α)<VAR>s : Set α<VAR>t₁ t₂ : TopologicalSpace β<VAR>B₁ B₂ : Set (Set β)<VAR>h₁ : IsTopologicalBasis B₁<VAR>h₂ : IsTopologicalBasis B₂<VAR>a : β<VAR>x✝ : Set β<GOAL>x✝ ∈ image2 (fun x x_1 => x ∩ x_1) B₁ B₂ ∧ a ∈ x✝ ↔ x✝ ∈ (fun i => i.1 ∩ i.2) '' {i | (i.1 ∈ B₁ ∧ a ∈ i.1) ∧ i.2 ∈ B₂ ∧ a ∈ i.2}
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>P : G.Partition<VAR>v w : V<VAR>h : G.Adj v w<VAR>hn : P.partOfVertex v = P.partOfVertex w<GOAL>False
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>P : G.Partition<VAR>v w : V<VAR>h : G.Adj v w<VAR>hn : P.partOfVertex v = P.partOfVertex w<VAR>hw : w ∈ P.partOfVertex w<GOAL>False
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>P : G.Partition<VAR>v w : V<VAR>h : G.Adj v w<VAR>hn : P.partOfVertex v = P.partOfVertex w<VAR>hw : w ∈ P.partOfVertex v<GOAL>False
<VAR>o : Ordinal.{u_1}<GOAL>aleph' (succ o) = succ (aleph' o)
<VAR>o : Ordinal.{u_1}<GOAL>(aleph' (succ o)).alephIdx ≤ (succ (aleph' o)).alephIdx
<VAR>o : Ordinal.{u_1}<GOAL>aleph' o < succ (aleph' o)
<VAR>S : Type u_1<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : IsDomain S<VAR>inst✝³ : Nontrivial S<VAR>inst✝² : IsDedekindDomain S<VAR>inst✝¹ : Module.Free ℤ S<VAR>inst✝ : Module.Finite ℤ S<GOAL>absNorm ⊤ = 1
<VAR>R : Type w₁<VAR>A : Type w₂<VAR>B : Type w₃<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : Algebra R A<VAR>inst✝³ : CommRing B<VAR>inst✝² : Algebra R B<VAR>inst✝¹ : FinitePresentation R A<VAR>ι : Type v<VAR>inst✝ : Finite ι<VAR>hfp : FinitePresentation R A<GOAL>FinitePresentation R (MvPolynomial ι A)
<VAR>R : Type w₁<VAR>A : Type w₂<VAR>B : Type w₃<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : Algebra R A<VAR>inst✝³ : CommRing B<VAR>inst✝² : Algebra R B<VAR>inst✝¹ : FinitePresentation R A<VAR>ι : Type v<VAR>inst✝ : Finite ι<VAR>hfp : ∃ ι x f, Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG<GOAL>∃ ι_1 x f, Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : CanonicallyOrderedAddCommMonoid α<VAR>inst✝ : LocallyFiniteOrder α<VAR>f : ι →₀ α<GOAL>(Iio f).card = ∏ i ∈ f.support, (Iic (f i)).card - 1
<VAR>a b c : ℝ<VAR>hb : 0 ≠ b<GOAL>Tendsto (fun x => x ^ (a / (b * x + c))) atTop (𝓝 1)
<VAR>a b c : ℝ<VAR>hb : 0 ≠ b<GOAL>(rexp ∘ fun x => a * (x / (b * rexp x + c))) ∘ log =ᶠ[atTop] fun x => x ^ (a / (b * x + c))
<VAR>a b c : ℝ<VAR>hb : 0 ≠ b<GOAL>EqOn ((rexp ∘ fun x => a * (x / (b * rexp x + c))) ∘ log) (fun x => x ^ (a / (b * x + c))) (Set.Ioi 0)
<VAR>a b c : ℝ<VAR>hb : 0 ≠ b<VAR>x : ℝ<VAR>hx : x ∈ Set.Ioi 0<GOAL>((rexp ∘ fun x => a * (x / (b * rexp x + c))) ∘ log) x = (fun x => x ^ (a / (b * x + c))) x
<VAR>a b c : ℝ<VAR>hb : 0 ≠ b<VAR>x : ℝ<VAR>hx : 0 < x<GOAL>rexp (a * (log x / (b * rexp (log x) + c))) = x ^ (a / (b * x + c))
<VAR>a b c : ℝ<VAR>hb : 0 ≠ b<VAR>x : ℝ<VAR>hx : 0 < x<GOAL>rexp (a * (log x / (b * x + c))) = rexp (a / (b * x + c) * log x)
<VAR>β : Type u_1<VAR>α : Type u_2<VAR>f : β → α → β<VAR>l₁ l₂ : List α<VAR>p : l₁ ~ l₂<VAR>comm : ∀ (x : α), x ∈ l₁ → ∀ (y : α), y ∈ l₁ → ∀ (z : β), f (f z x) y = f (f z y) x<VAR>init : β<GOAL>foldl f init l₁ = foldl f init l₂
<VAR>R : Type r<VAR>S : Type s<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : WeierstrassCurve R<VAR>n : ℤ<GOAL>W.φ (-n) = W.φ n
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>M : Type u_3<VAR>R : Type u_4<VAR>A : Type u_5<VAR>inst✝² : Monoid M<VAR>inst✝¹ : AddMonoid A<VAR>inst✝ : OrderedCancelCommMonoid α<VAR>s : Set α<VAR>hpos : ∀ x ∈ s, 1 ≤ x<VAR>h : s.IsPWO<GOAL>(↑(Submonoid.closure s)).IsPWO
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>M : Type u_3<VAR>R : Type u_4<VAR>A : Type u_5<VAR>inst✝² : Monoid M<VAR>inst✝¹ : AddMonoid A<VAR>inst✝ : OrderedCancelCommMonoid α<VAR>s : Set α<VAR>hpos : ∀ x ∈ s, 1 ≤ x<VAR>h : s.IsPWO<GOAL>(List.prod '' {l | ∀ x ∈ l, x ∈ s}).IsPWO
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>M : Type u_3<VAR>R : Type u_4<VAR>A : Type u_5<VAR>inst✝² : Monoid M<VAR>inst✝¹ : AddMonoid A<VAR>inst✝ : OrderedCancelCommMonoid α<VAR>s : Set α<VAR>hpos : ∀ x ∈ s, 1 ≤ x<VAR>h : s.IsPWO<GOAL>∀ a₁ ∈ {l | ∀ x ∈ l, x ∈ s}, ∀ a₂ ∈ {l | ∀ x ∈ l, x ∈ s}, List.SublistForall₂ (fun x x_1 => x ≤ x_1) a₁ a₂ → a₁.prod ≤ a₂.prod
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>m' : o → Type u_5<VAR>n' : o → Type u_6<VAR>R : Type u_7<VAR>S : Type u_8<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>inst✝¹ : CommSemiring α<VAR>inst✝ : Fintype n<VAR>A : Matrix m n α<VAR>b : n → α<VAR>a : α<VAR>x✝ : m<GOAL>(A *ᵥ a • b) x✝ = (a • A *ᵥ b) x✝
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>φ : G →* G<VAR>hφ : FixedPointFree ⇑φ<GOAL>Function.Injective (commutatorMap ⇑φ)
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>φ : G →* G<VAR>hφ : FixedPointFree ⇑φ<VAR>x y : G<VAR>h : commutatorMap (⇑φ) x = commutatorMap (⇑φ) y<GOAL>φ (x⁻¹ * y) = x⁻¹ * y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>σ : Type u_5<VAR>inst✝⁴ : Primcodable α<VAR>inst✝³ : Primcodable β<VAR>inst✝² : Primcodable γ<VAR>inst✝¹ : Primcodable δ<VAR>inst✝ : Primcodable σ<VAR>f : α → β<VAR>g : α → ℕ × β → β<VAR>hf : Primrec f<VAR>hg : Primrec₂ g<VAR>n : ℕ<GOAL>Nat.unpaired (fun z n => Nat.casesOn n 0 fun y => Nat.unpaired (fun z n => Nat.rec (encode (Option.map f (decode z))) (fun y IH => encode (Option.map (fun p => g p.1 p.2) (decode (Nat.pair (Nat.unpair (Nat.pair z (Nat.pair y IH))).1 (Nat.pair (Nat.unpair (Nat.unpair (Nat.pair z (Nat.pair y IH))).2).1 (Nat.unpair (Nat.unpair (Nat.pair z (Nat.pair y IH))).2).2.pred))))) n) (Nat.pair (Nat.unpair (Nat.pair z y)).2 (Nat.unpair (Nat.unpair (Nat.pair z y)).1).2)) (Nat.pair (id n) (encode (decode (Nat.unpair n).1))) = Nat.unpaired (fun m n => encode ((decode m).bind fun a => Option.map (fun n => Nat.rec (f a) (fun n IH => g a (n, IH)) n) (decode n))) n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>σ : Type u_5<VAR>inst✝⁴ : Primcodable α<VAR>inst✝³ : Primcodable β<VAR>inst✝² : Primcodable γ<VAR>inst✝¹ : Primcodable δ<VAR>inst✝ : Primcodable σ<VAR>f : α → β<VAR>g : α → ℕ × β → β<VAR>hf : Primrec f<VAR>hg : Primrec₂ g<VAR>n : ℕ<GOAL>Nat.rec 0 (fun n_1 n_ih => Nat.rec (encode (Option.map f (decode n_1))) (fun y IH => encode (Option.map (fun p => g p.1 p.2) ((decode n_1).bind fun a => Option.map (Prod.mk a ∘ Prod.mk y) (decode IH.pred)))) (Nat.unpair n).2) (encode (decode (Nat.unpair n).1)) = encode ((decode (Nat.unpair n).1).bind fun a => some (Nat.rec (f a) (fun n IH => g a (n, IH)) (Nat.unpair n).2))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>σ : Type u_5<VAR>inst✝⁴ : Primcodable α<VAR>inst✝³ : Primcodable β<VAR>inst✝² : Primcodable γ<VAR>inst✝¹ : Primcodable δ<VAR>inst✝ : Primcodable σ<VAR>f : α → β<VAR>g : α → ℕ × β → β<VAR>hf : Primrec f<VAR>hg : Primrec₂ g<VAR>n : ℕ<VAR>a : α<GOAL>Nat.rec 0 (fun n_1 n_ih => Nat.rec (encode (Option.map f (decode n_1))) (fun y IH => encode (Option.map (fun p => g p.1 p.2) ((decode n_1).bind fun a => Option.map (Prod.mk a ∘ Prod.mk y) (decode IH.pred)))) (Nat.unpair n).2) (encode (some a)) = encode ((some a).bind fun a => some (Nat.rec (f a) (fun n IH => g a (n, IH)) (Nat.unpair n).2))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>σ : Type u_5<VAR>inst✝⁴ : Primcodable α<VAR>inst✝³ : Primcodable β<VAR>inst✝² : Primcodable γ<VAR>inst✝¹ : Primcodable δ<VAR>inst✝ : Primcodable σ<VAR>f : α → β<VAR>g : α → ℕ × β → β<VAR>hf : Primrec f<VAR>hg : Primrec₂ g<VAR>n : ℕ<VAR>a : α<GOAL>Nat.rec (encode (f a) + 1) (fun y IH => encode (Option.map ((fun p => g p.1 p.2) ∘ Prod.mk a ∘ Prod.mk y) (decode (IH - 1)))) (Nat.unpair n).2 = encode (Nat.rec (f a) (fun n IH => g a (n, IH)) (Nat.unpair n).2) + 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>σ : Type u_5<VAR>inst✝⁴ : Primcodable α<VAR>inst✝³ : Primcodable β<VAR>inst✝² : Primcodable γ<VAR>inst✝¹ : Primcodable δ<VAR>inst✝ : Primcodable σ<VAR>f : α → β<VAR>g : α → ℕ × β → β<VAR>hf : Primrec f<VAR>hg : Primrec₂ g<VAR>n : ℕ<VAR>a : α<VAR>m : ℕ<VAR>a✝ : Nat.rec (encode (f a) + 1) (fun y IH => encode (Option.map ((fun p => g p.1 p.2) ∘ Prod.mk a ∘ Prod.mk y) (decode (IH - 1)))) m = encode (Nat.rec (f a) (fun n IH => g a (n, IH)) m) + 1<GOAL>encode (Option.map ((fun p => g p.1 p.2) ∘ Prod.mk a ∘ Prod.mk m) (decode (Nat.rec (encode (f a) + 1) (fun y IH => encode (Option.map ((fun p => g p.1 p.2) ∘ Prod.mk a ∘ Prod.mk y) (decode (IH - 1)))) m - 1))) = encode (g a (m, Nat.rec (f a) (fun n IH => g a (n, IH)) m)) + 1
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b✝ c : α<VAR>n : ℤ<VAR>a b : α<GOAL>toIocMod hp (-a) b = p - toIcoMod hp a (-b)
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>hs : IsClopen s<VAR>ht : IsClopen t<GOAL>IsClopen (s ⇨ t)
<VAR>x y z : ℝ<VAR>n : ℕ<VAR>b : ℝ<VAR>hb : 1 < b<GOAL>StrictMono fun x => b ^ x
<VAR>x y z : ℝ<VAR>n : ℕ<VAR>b : ℝ<VAR>hb : 1 < b<GOAL>StrictMono fun x => rexp (log b * x)
<VAR>C : Type u_1<VAR>inst✝ : Category.{?u.8576, u_1} C<VAR>A B X Y : C<VAR>f : A ⟶ X<VAR>i : A ⟶ B<VAR>p : X ⟶ Y<VAR>g : B ⟶ Y<VAR>sq : CommSq f i p g<VAR>l : sq.LiftStruct<GOAL>p.op ≫ l.l.op = g.op
<VAR>C : Type u_1<VAR>inst✝ : Category.{?u.8576, u_1} C<VAR>A B X Y : C<VAR>f : A ⟶ X<VAR>i : A ⟶ B<VAR>p : X ⟶ Y<VAR>g : B ⟶ Y<VAR>sq : CommSq f i p g<VAR>l : sq.LiftStruct<GOAL>l.l.op ≫ i.op = f.op
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x✝ y✝ x y : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>‖x + y‖ = ‖x‖ + ‖y‖ ↔ angle x y = 0
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x✝ y✝ x y : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>h : ‖x + y‖ = ‖x‖ + ‖y‖<GOAL>angle x y = 0