ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝ : LinearOrder ι<VAR>f : Filtration ι m<VAR>τ : Ω → ι<VAR>hτ : IsStoppingTime f τ<VAR>i : ι<GOAL>MeasurableSet {ω | i < τ ω}
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝ : LinearOrder ι<VAR>f : Filtration ι m<VAR>τ : Ω → ι<VAR>hτ : IsStoppingTime f τ<VAR>i : ι<VAR>this : {ω | i < τ ω} = {ω | τ ω ≤ i}ᶜ<GOAL>MeasurableSet {ω | i < τ ω}
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝ : LinearOrder ι<VAR>f : Filtration ι m<VAR>τ : Ω → ι<VAR>hτ : IsStoppingTime f τ<VAR>i : ι<VAR>this : {ω | i < τ ω} = {ω | τ ω ≤ i}ᶜ<GOAL>MeasurableSet {ω | τ ω ≤ i}ᶜ
<VAR>w x✝ y✝ z y : ℝ<VAR>hy : y ≠ 0<VAR>x : ℝ≥0<GOAL>(x ^ y) ^ y⁻¹ = x
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : Field K<VAR>inst✝⁹ : Field L<VAR>inst✝⁸ : DecidableEq L<VAR>inst✝⁷ : Algebra R K<VAR>inst✝⁶ : IsFractionRing R K<VAR>inst✝⁵ : Algebra K L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>inst✝³ : Algebra R L<VAR>inst✝² : IsScalarTower R K L<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : IsDedekindDomain R<VAR>I : ↥(Ideal R)⁰<GOAL>(equiv K) (mk0 I) = (QuotientGroup.mk' (toPrincipalIdeal R K).range) ((FractionalIdeal.mk0 K) I)
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : Field K<VAR>inst✝⁹ : Field L<VAR>inst✝⁸ : DecidableEq L<VAR>inst✝⁷ : Algebra R K<VAR>inst✝⁶ : IsFractionRing R K<VAR>inst✝⁵ : Algebra K L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>inst✝³ : Algebra R L<VAR>inst✝² : IsScalarTower R K L<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : IsDedekindDomain R<VAR>I : ↥(Ideal R)⁰<GOAL>(QuotientGroup.mk' (toPrincipalIdeal R K).range) ((Units.mapEquiv ↑(canonicalEquiv R⁰ (FractionRing R) K)) ((FractionalIdeal.mk0 (FractionRing R)) I)) = (QuotientGroup.mk' (toPrincipalIdeal R K).range) ((FractionalIdeal.mk0 K) I)
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : Field K<VAR>inst✝⁹ : Field L<VAR>inst✝⁸ : DecidableEq L<VAR>inst✝⁷ : Algebra R K<VAR>inst✝⁶ : IsFractionRing R K<VAR>inst✝⁵ : Algebra K L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>inst✝³ : Algebra R L<VAR>inst✝² : IsScalarTower R K L<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : IsDedekindDomain R<VAR>I : ↥(Ideal R)⁰<GOAL>(Units.mapEquiv ↑(canonicalEquiv R⁰ (FractionRing R) K)) ((FractionalIdeal.mk0 (FractionRing R)) I) = (FractionalIdeal.mk0 K) I
<VAR>Δ Δ'' : SimplexCategory<VAR>φ : Δ ⟶ Δ''<VAR>e : Δ ⟶ image φ<VAR>inst✝¹ : Epi e<VAR>i : image φ ⟶ Δ''<VAR>inst✝ : Mono i<VAR>fac : e ≫ i = φ<GOAL>image.ι φ = i
<VAR>Δ Δ'' : SimplexCategory<VAR>φ : Δ ⟶ Δ''<VAR>e : Δ ⟶ image φ<VAR>inst✝¹ : Epi e<VAR>i : image φ ⟶ Δ''<VAR>inst✝ : Mono i<VAR>fac : e ≫ i = φ<VAR>this : StrongEpi e<GOAL>image.ι φ = i
<VAR>S : Set Ordinal.{u}<GOAL>enumOrd Set.univ = id
<VAR>S : Set Ordinal.{u}<GOAL>enumOrd (range id) = id
<VAR>ι : Sort u<VAR>α : Type v<VAR>β : Type w<VAR>inst✝ : LinearOrder α<VAR>a₁ a₂ b₁ b₂ : α<GOAL>Disjoint (Ico a₁ a₂) (Ico b₁ b₂) ↔ min a₂ b₂ ≤ max a₁ b₁
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>a : α<VAR>n k : ℕ<VAR>h : k ≤ n<GOAL>replicate k a <+ replicate n a
<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>inst✝⁷ : DecidableEq α'<VAR>inst✝⁶ : DecidableEq β'<VAR>inst✝⁵ : DecidableEq γ<VAR>inst✝⁴ : DecidableEq γ'<VAR>inst✝³ : DecidableEq δ<VAR>inst✝² : DecidableEq δ'<VAR>inst✝¹ : DecidableEq ε<VAR>inst✝ : DecidableEq ε'<VAR>f f' : α → β → γ<VAR>g g' : α → β → γ → δ<VAR>s s' : Finset α<VAR>t t' : Finset β<VAR>u u' : Finset γ<VAR>a a' : α<VAR>b b' : β<VAR>c : γ<VAR>hf : Injective2 f<GOAL>f a b ∈ image₂ f s t ↔ a ∈ s ∧ b ∈ t
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<GOAL>a ≤ 1 * a
<VAR>S : Type u_1<VAR>inst✝ : Semiring S<VAR>a b : ℕ<GOAL>↑a ! = Polynomial.eval 1 (ascPochhammer S a)
<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<GOAL>eLpNorm (fun x => 0) p μ = 0
<VAR>m n k : ℕ+<GOAL>k.Coprime m → m.gcd (n * k) = m.gcd n
<VAR>m n k : ℕ+<GOAL>k.Coprime m → m.gcd (k * n) = m.gcd n
<VAR>u : ZFSet<GOAL>u = ∅ ∨ u.Nonempty
<VAR>u : ZFSet<GOAL>(¬∃ x, x ∈ u) ∨ u.Nonempty
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>w : W<VAR>i : B<GOAL>cs.IsRightInversion w (cs.simple i) ↔ cs.IsRightDescent w i
<VAR>z : ℂ<GOAL>↑(normSq z) = (starRingEnd ℂ) z * z
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : Ring R<VAR>p q : R[X]<VAR>inst✝ : Ring S<VAR>f : R →+* S<VAR>hf : Function.Injective ⇑f<VAR>x y : R[X]<VAR>hx : x.Monic<GOAL>map f x ∣ map f y ↔ x ∣ y
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : Ring R<VAR>p q : R[X]<VAR>inst✝ : Ring S<VAR>f : R →+* S<VAR>hf : Function.Injective ⇑f<VAR>x y : R[X]<VAR>hx : x.Monic<GOAL>map f (y %ₘ x) = 0 ↔ y %ₘ x = 0
<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>pb : PowerBasis K L<VAR>inst✝ : Algebra.IsSeparable K L<GOAL>(traceMatrix K ⇑pb.basis).det ≠ 0
<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>pb : PowerBasis K L<VAR>inst✝ : Algebra.IsSeparable K L<GOAL>(algebraMap K (AlgebraicClosure L)) (traceMatrix K ⇑pb.basis).det ≠ 0
<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>pb : PowerBasis K L<VAR>inst✝ : Algebra.IsSeparable K L<VAR>this : FiniteDimensional K L<GOAL>(algebraMap K (AlgebraicClosure L)) (traceMatrix K ⇑pb.basis).det ≠ 0
<VAR>n b : ℕ<VAR>L : List ℕ<GOAL>ofDigits b L = (List.mapIdx (fun i a => a * b ^ i) L).sum
<VAR>n b : ℕ<VAR>L : List ℕ<GOAL>List.foldr (fun x y => ↑x + b * y) 0 L = (List.zipWith (fun i a => a * b ^ i) (List.range L.length) L).sum
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : CoheytingAlgebra α<VAR>a✝ a b : α<VAR>h : IsCompl a b<GOAL>a ∆ b = ⊤
<VAR>c : ℂ<GOAL>CliffordAlgebraComplex.equiv (ofComplex ((starRingEnd ℂ) c)) = CliffordAlgebraComplex.equiv (involute (ofComplex c))
<VAR>b d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>x y : ℕ<GOAL>b * x / b * (d * y / d) = b * x * (d * y) / (b * d)
<VAR>d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>x y : ℕ<GOAL>0 * x / 0 * (d * y / d) = 0 * x * (d * y) / (0 * d)
<VAR>b d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>x y : ℕ<VAR>hb : b > 0<GOAL>b * x / b * (d * y / d) = b * x * (d * y) / (b * d)
<VAR>b m n k : ℕ<VAR>p q : ℕ → Prop<VAR>x y : ℕ<VAR>hb : b > 0<GOAL>b * x / b * (0 * y / 0) = b * x * (0 * y) / (b * 0)
<VAR>b d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>x y : ℕ<VAR>hb : b > 0<VAR>hd : d > 0<GOAL>b * x / b * (d * y / d) = b * x * (d * y) / (b * d)
<VAR>θ : Angle<VAR>ψ : ℝ<GOAL>θ.cos = Real.cos ψ ↔ θ = ↑ψ ∨ θ = -↑ψ
<VAR>ψ x✝ : ℝ<GOAL>(↑x✝).cos = Real.cos ψ ↔ ↑x✝ = ↑ψ ∨ ↑x✝ = -↑ψ
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : LocallyFiniteOrderTop α<VAR>a : α<GOAL>Ici a = cons a (Ioi a) ⋯
<VAR>C : Type u_1<VAR>inst✝⁷ : Category.{u_5, u_1} C<VAR>D : Type u_2<VAR>inst✝⁶ : Category.{?u.45870, u_2} D<VAR>E : Type u_3<VAR>inst✝⁵ : Category.{?u.45877, u_3} E<VAR>M : Type u_4<VAR>inst✝⁴ : AddMonoid M<VAR>inst✝³ : HasShift C M<VAR>inst✝² : HasShift D M<VAR>inst✝¹ : HasShift E M<VAR>X Y Z T : C<VAR>inst✝ : Preadditive C<VAR>a b c : M<VAR>α : ShiftedHom X Y a<VAR>β : ShiftedHom Y Z b<VAR>h : b + a = c<GOAL>(-α).comp β h = -α.comp β h
<VAR>M : Type u_1<VAR>M₂ : Type u_2<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module ℚ M<VAR>inst✝¹ : AddCommGroup M₂<VAR>inst✝ : Module ℚ M₂<VAR>f g : M →+ M₂<VAR>h : f.toRatLinearMap = g.toRatLinearMap<VAR>x : M<GOAL>f x = g x
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l : List α<GOAL>map pure l <+ l.sublists
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<GOAL>[] <+ [].sublists
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l : List α<VAR>a : α<VAR>ih : map pure l <+ l.sublists<GOAL>map pure l ++ [pure a] <+ l.sublists ++ map (fun x => x ++ [a]) l.sublists
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>f g : Filter α<VAR>s✝ t s : Set α<GOAL>s ∈ ⊤ ↔ s = univ
<VAR>P : Type u_1<VAR>inst✝ : BooleanAlgebra P<VAR>x : P<VAR>I : Ideal P<VAR>hI : I.IsProper<VAR>hxc : xᶜ ∈ I<VAR>hx : x ∈ I<GOAL>False
<VAR>P : Type u_1<VAR>inst✝ : BooleanAlgebra P<VAR>x : P<VAR>I : Ideal P<VAR>hI : I.IsProper<VAR>hxc : xᶜ ∈ I<VAR>hx : x ∈ I<GOAL>⊤ ∈ I
<VAR>P : Type u_1<VAR>inst✝ : BooleanAlgebra P<VAR>x : P<VAR>I : Ideal P<VAR>hI : I.IsProper<VAR>hxc : xᶜ ∈ I<VAR>hx : x ∈ I<VAR>ht : x ⊔ xᶜ ∈ I<GOAL>⊤ ∈ I
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommSemiring S₁<VAR>p✝ q : MvPolynomial σ R<VAR>inst✝ : IsEmpty σ<VAR>p : MvPolynomial σ R<GOAL>p = C (coeff 0 p)
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommSemiring S₁<VAR>p q : MvPolynomial σ R<VAR>inst✝ : IsEmpty σ<VAR>x : R<GOAL>C x = C (coeff 0 (C x))
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>D : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>V : Type u_7<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : SMulCommClass ℝ 𝕜 F<VAR>f : 𝓢(E, F)<VAR>n : ℕ<VAR>IH : ∀ (m : Fin (n + 1) → E), (iteratedPDeriv 𝕜 m) f = (iteratedPDeriv 𝕜 (Fin.init m)) ((pderivCLM 𝕜 (m (Fin.last n))) f)<VAR>m : Fin (n + 1 + 1) → E<GOAL>(iteratedPDeriv 𝕜 m) f = (iteratedPDeriv 𝕜 (Fin.init m)) ((pderivCLM 𝕜 (m (Fin.last (n + 1)))) f)
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>D : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>V : Type u_7<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : SMulCommClass ℝ 𝕜 F<VAR>f : 𝓢(E, F)<VAR>n : ℕ<VAR>IH : ∀ (m : Fin (n + 1) → E), (iteratedPDeriv 𝕜 m) f = (iteratedPDeriv 𝕜 (Fin.init m)) ((pderivCLM 𝕜 (m (Fin.last n))) f)<VAR>m : Fin (n + 1 + 1) → E<VAR>hmzero : Fin.init m 0 = m 0<GOAL>(iteratedPDeriv 𝕜 m) f = (iteratedPDeriv 𝕜 (Fin.init m)) ((pderivCLM 𝕜 (m (Fin.last (n + 1)))) f)
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>D : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>V : Type u_7<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : SMulCommClass ℝ 𝕜 F<VAR>f : 𝓢(E, F)<VAR>n : ℕ<VAR>IH : ∀ (m : Fin (n + 1) → E), (iteratedPDeriv 𝕜 m) f = (iteratedPDeriv 𝕜 (Fin.init m)) ((pderivCLM 𝕜 (m (Fin.last n))) f)<VAR>m : Fin (n + 1 + 1) → E<VAR>hmzero : Fin.init m 0 = m 0<VAR>hmtail : Fin.tail m (Fin.last n) = m (Fin.last n.succ)<GOAL>(iteratedPDeriv 𝕜 m) f = (iteratedPDeriv 𝕜 (Fin.init m)) ((pderivCLM 𝕜 (m (Fin.last (n + 1)))) f)
<VAR>s : Set ℕ<GOAL>sInf s = 0 ↔ 0 ∈ s ∨ s = ∅
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : NoZeroSMulDivisors ℕ R<VAR>f g : R⟦X⟧<VAR>hD : (d⁄dX R) f = (d⁄dX R) g<VAR>hc : (constantCoeff R) f = (constantCoeff R) g<VAR>n : ℕ<GOAL>(coeff R n) f = (coeff R n) g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>s s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>a : α<VAR>b : β<VAR>x : α<VAR>y : β<GOAL>(x, y) ∈ s ×ˢ insert b t ↔ (x, y) ∈ (fun a => (a, b)) '' s ∪ s ×ˢ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>s s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>a : α<VAR>b : β<VAR>x : α<VAR>y : β<GOAL>x ∈ s ∧ (y = b ∨ y ∈ t) ↔ (∃ a ∈ s, a = x ∧ b = y) ∨ x ∈ s ∧ y ∈ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : SemilatticeInf α<VAR>inst✝⁴ : BoundedOrder α<VAR>inst✝³ : DecidableRel fun x x_1 => x ≤ x_1<VAR>inst✝² : SemilatticeInf β<VAR>inst✝¹ : BoundedOrder β<VAR>inst✝ : DecidableRel fun x x_1 => x ≤ x_1<VAR>s✝ t : Finset α<VAR>a✝ : α<VAR>e : α ≃o β<VAR>s : Finset α<VAR>a : α<VAR>this : e a ∈ upperClosure ↑(map e.toEmbedding s) ↔ a ∈ upperClosure ↑s<GOAL>e (s.truncatedInf a) = (map e.toEmbedding s).truncatedInf (e a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : SemilatticeInf α<VAR>inst✝⁴ : BoundedOrder α<VAR>inst✝³ : DecidableRel fun x x_1 => x ≤ x_1<VAR>inst✝² : SemilatticeInf β<VAR>inst✝¹ : BoundedOrder β<VAR>inst✝ : DecidableRel fun x x_1 => x ≤ x_1<VAR>s✝ t : Finset α<VAR>a✝ : α<VAR>e : α ≃o β<VAR>s : Finset α<VAR>a : α<VAR>this : e a ∈ upperClosure ↑(map e.toEmbedding s) ↔ a ∈ upperClosure ↑s<GOAL>(if h : a ∈ upperClosure ↑s then (filter (fun x => x ≤ a) s).inf' ⋯ (⇑e ∘ id) else ⊥) = if h : a ∈ upperClosure ↑s then (filter (fun x => x ≤ e a) (map e.toEmbedding s)).inf' ⋯ id else ⊥
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : SemilatticeInf α<VAR>inst✝⁴ : BoundedOrder α<VAR>inst✝³ : DecidableRel fun x x_1 => x ≤ x_1<VAR>inst✝² : SemilatticeInf β<VAR>inst✝¹ : BoundedOrder β<VAR>inst✝ : DecidableRel fun x x_1 => x ≤ x_1<VAR>s✝ t : Finset α<VAR>a✝ : α<VAR>e : α ≃o β<VAR>s : Finset α<VAR>a : α<VAR>this : e a ∈ upperClosure ↑(map e.toEmbedding s) ↔ a ∈ upperClosure ↑s<VAR>h : a ∈ upperClosure ↑s<GOAL>(filter (fun x => x ≤ a) s).inf' ⋯ (⇑e ∘ id) = (filter (fun x => x ≤ e a) (map e.toEmbedding s)).inf' ⋯ id
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>S S' S'' : D<VAR>Y Y' Y'' : C<VAR>T T' : C ⥤ D<VAR>f : S ⟶ S'<VAR>f' : S' ⟶ S''<VAR>h : StructuredArrow S'' T<GOAL>(map (f ≫ f')).obj h = (map f).obj ((map f').obj h)
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>S S' S'' : D<VAR>Y Y' Y'' : C<VAR>T T' : C ⥤ D<VAR>f : S ⟶ S'<VAR>f' : S' ⟶ S''<VAR>h : StructuredArrow S'' T<GOAL>(map (f ≫ f')).obj (mk h.hom) = (map f).obj ((map f').obj (mk h.hom))
<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>c : F<VAR>h : DifferentiableOn 𝕜 (fun y => f y + c) s<GOAL>DifferentiableOn 𝕜 f s
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>inst✝ : MonoidalCategory D<VAR>X✝ Y✝ : C ⥤ Comon_ D<VAR>α : X✝ ⟶ Y✝<VAR>x : C<GOAL>(α.app x).hom ≫ (Y✝.obj x).counit = (X✝.obj x).counit
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>inst✝ : MonoidalCategory D<VAR>X✝ Y✝ : C ⥤ Comon_ D<VAR>α : X✝ ⟶ Y✝<VAR>x : C<GOAL>(α.app x).hom ≫ (Y✝.obj x).comul = (X✝.obj x).comul ≫ ((α.app x).hom ⊗ (α.app x).hom)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>s : Set α<VAR>p : α → Prop<VAR>a : α<VAR>hs : IsUpperSet s<VAR>f : α ≃o β<GOAL>IsUpperSet (⇑↑f '' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>s : Set α<VAR>p : α → Prop<VAR>a : α<VAR>hs : IsUpperSet s<VAR>f : α ≃o β<GOAL>IsUpperSet (⇑(↑f).symm ⁻¹' s)
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>H : Type u_6<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace 𝕜 F<VAR>inst✝⁷ : NormedAddCommGroup G<VAR>inst✝⁶ : NormedSpace 𝕜 G<VAR>inst✝⁵ : NormedAddCommGroup H<VAR>inst✝⁴ : NormedSpace 𝕜 H<VAR>𝕝 : Type u_7<VAR>inst✝³ : NontriviallyNormedField 𝕝<VAR>inst✝² : NormedAlgebra 𝕜 𝕝<VAR>A : Type u_8<VAR>inst✝¹ : NormedRing A<VAR>inst✝ : NormedAlgebra 𝕜 A<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>q : FormalMultilinearSeries 𝕜 E G<GOAL>(p.prod q).radius = min p.radius q.radius
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>H : Type u_6<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace 𝕜 F<VAR>inst✝⁷ : NormedAddCommGroup G<VAR>inst✝⁶ : NormedSpace 𝕜 G<VAR>inst✝⁵ : NormedAddCommGroup H<VAR>inst✝⁴ : NormedSpace 𝕜 H<VAR>𝕝 : Type u_7<VAR>inst✝³ : NontriviallyNormedField 𝕝<VAR>inst✝² : NormedAlgebra 𝕜 𝕝<VAR>A : Type u_8<VAR>inst✝¹ : NormedRing A<VAR>inst✝ : NormedAlgebra 𝕜 A<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>q : FormalMultilinearSeries 𝕜 E G<GOAL>(p.prod q).radius ≤ min p.radius q.radius
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>H : Type u_6<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace 𝕜 F<VAR>inst✝⁷ : NormedAddCommGroup G<VAR>inst✝⁶ : NormedSpace 𝕜 G<VAR>inst✝⁵ : NormedAddCommGroup H<VAR>inst✝⁴ : NormedSpace 𝕜 H<VAR>𝕝 : Type u_7<VAR>inst✝³ : NontriviallyNormedField 𝕝<VAR>inst✝² : NormedAlgebra 𝕜 𝕝<VAR>A : Type u_8<VAR>inst✝¹ : NormedRing A<VAR>inst✝ : NormedAlgebra 𝕜 A<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>q : FormalMultilinearSeries 𝕜 E G<GOAL>min p.radius q.radius ≤ (p.prod q).radius
<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>inst✝ : Finite α<VAR>f : α → σ<VAR>l : List α<VAR>left✝ : l.Nodup<VAR>m : ∀ (x : α), x ∈ l<VAR>this : DecidableEq α<GOAL>Primrec fun a => some (f a)
<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>inst✝ : Finite α<VAR>f : α → σ<VAR>l : List α<VAR>left✝ : l.Nodup<VAR>m : ∀ (x : α), x ∈ l<VAR>this : DecidableEq α<VAR>a : α<GOAL>(List.map f l).get? (List.indexOf a l) = some (f a)
<VAR>α : Type u_1<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : DecidableEq α<VAR>A✝ B✝ C✝ A B C : Finset α<GOAL>(A / C).card * B.card ≤ (A * B).card * (B * C).card
<VAR>α : Type u_1<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : DecidableEq α<VAR>A✝ B✝ C✝ A B C : Finset α<GOAL>(A / C).card * B⁻¹.card ≤ (A / B⁻¹).card * (B⁻¹ / C).card
<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>inst✝ : IsFiniteMeasure μ<VAR>c : E<GOAL>∫ (x : ℝ) in a..b, c ∂μ = ((μ (Iic b)).toReal - (μ (Iic a)).toReal) • c
<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>inst✝ : IsFiniteMeasure μ<VAR>c : E<GOAL>∫ (x : ℝ) in a..b, c ∂μ = ∫ (x : ℝ) in Iic b, c ∂μ - ∫ (x : ℝ) in Iic a, c ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : Group G<VAR>a b c d : G<VAR>n : ℤ<GOAL>b / a = c / a ↔ b = c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : Group G<VAR>a b c d : G<VAR>n : ℤ<GOAL>b * a⁻¹ = c * a⁻¹ ↔ b = c
<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✝³ : NonAssocSemiring α<VAR>inst✝² : Fintype m<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq m<VAR>v : m → α<VAR>x✝ : m<GOAL>(v ᵥ* 1) x✝ = v x✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>K : Type u_3<VAR>inst✝¹ : DivisionMonoid K<VAR>inst✝ : HasDistribNeg K<VAR>a✝ b✝ a b : K<GOAL>b / -a = b * (1 / -a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>K : Type u_3<VAR>inst✝¹ : DivisionMonoid K<VAR>inst✝ : HasDistribNeg K<VAR>a✝ b✝ a b : K<GOAL>b * (1 / -a) = b * -(1 / a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>K : Type u_3<VAR>inst✝¹ : DivisionMonoid K<VAR>inst✝ : HasDistribNeg K<VAR>a✝ b✝ a b : K<GOAL>b * -(1 / a) = -(b * (1 / a))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>K : Type u_3<VAR>inst✝¹ : DivisionMonoid K<VAR>inst✝ : HasDistribNeg K<VAR>a✝ b✝ a b : K<GOAL>-(b * (1 / a)) = -(b / a)
<VAR>E : Type u_1<VAR>X : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : TopologicalSpace X<VAR>a b b₀ b₁ b₂ : ℝ<VAR>μ : Measure ℝ<VAR>f : ℝ → E<VAR>inst✝ : NoAtoms μ<VAR>h_int : IntegrableOn f [[a, b]] μ<GOAL>ContinuousOn (fun x => ∫ (t : ℝ) in x..b, f t ∂μ) [[a, b]]
<VAR>E : Type u_1<VAR>X : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : TopologicalSpace X<VAR>a b b₀ b₁ b₂ : ℝ<VAR>μ : Measure ℝ<VAR>f : ℝ → E<VAR>inst✝ : NoAtoms μ<VAR>h_int : IntegrableOn f [[b, a]] μ<GOAL>ContinuousOn (fun x => ∫ (t : ℝ) in x..b, f t ∂μ) [[b, a]]
<VAR>E : Type u_1<VAR>X : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : TopologicalSpace X<VAR>a b b₀ b₁ b₂ : ℝ<VAR>μ : Measure ℝ<VAR>f : ℝ → E<VAR>inst✝ : NoAtoms μ<VAR>h_int : IntegrableOn f [[b, a]] μ<GOAL>ContinuousOn (fun x => -∫ (t : ℝ) in b..x, f t ∂μ) [[b, a]]
<VAR>s : ℂ<VAR>hs : 0 < s.re<GOAL>s.Gammaℝ ≠ 0
<VAR>s : ℂ<VAR>hs : 0 < s.re<GOAL>↑π ^ (-s / 2) ≠ 0
<VAR>s : ℂ<VAR>hs : 0 < s.re<GOAL>Gamma (s / 2) ≠ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s✝ s' : Finset α<VAR>t✝ t' : Finset β<VAR>a : α<VAR>b : β<VAR>inst✝ : DecidableEq γ<VAR>s : Finset α<VAR>t : Finset β<VAR>f : α × β → Finset γ<GOAL>(s ×ˢ t).biUnion f = s.biUnion fun a => t.biUnion fun b => f (a, b)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>hn : 0 < n<GOAL>(aeval (Function.uncurry fun i => (![] i).coeff)) (wittOne p n) = 0
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝² : TopologicalSpace α<VAR>s t u v : Set α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : TotallyDisconnectedSpace β<VAR>f : α → β<VAR>h : Continuous f<GOAL>∀ (a b : α), Setoid.r a b → f a = f b
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>ι : Type u_3<VAR>inst✝³ : CommRing R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>e : ι → M<VAR>ε : ι → Dual R M<VAR>inst✝ : DecidableEq ι<VAR>h : DualBases e ε<VAR>m : M<GOAL>lc e (h.coeffs m) = m
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>ι : Type u_3<VAR>inst✝³ : CommRing R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>e : ι → M<VAR>ε : ι → Dual R M<VAR>inst✝ : DecidableEq ι<VAR>h : DualBases e ε<VAR>m : M<VAR>i : ι<GOAL>(ε i) (lc e (h.coeffs m) - m) = 0