ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>f✝ : α → β<VAR>s t : Set α<VAR>β' : Type u_6<VAR>f : β → γ<VAR>g : α → β<VAR>f' : α → β'<VAR>g' : β' → γ<VAR>h_comm : ∀ (a : α), f (g a) = g' (f' a)<GOAL>f '' (g '' s) = g' '' (f' '' s)
<VAR>l m₂ r m₁ : List Char<VAR>s : Substring<VAR>h : ValidFor l (m₁.reverse ++ m₂) r s<VAR>n : Nat<GOAL>s.prevn n (s.prev { byteIdx := utf8Len m₁ }) = { byteIdx := utf8Len (List.drop (n + 1) m₁) }
<VAR>f : ℕ → ℝ<VAR>hf : Tendsto f atTop atBot<VAR>r : ℝ<VAR>hf' : ∀ (b : ℝ), ∃ i, ∀ (a : ℕ), i ≤ a → f a ≤ b<VAR>i : ℕ<VAR>hi : ∀ (a : ℕ), i ≤ a → f a ≤ r - 1<VAR>hi' : ∀ (a : ℕ), r - 1 < f a → a < i<GOAL>{a | f a < r}ᶜ ⊆ {a | a ≤ i}
<VAR>f : ℕ → ℝ<VAR>hf : Tendsto f atTop atBot<VAR>r : ℝ<VAR>hf' : ∀ (b : ℝ), ∃ i, ∀ (a : ℕ), i ≤ a → f a ≤ b<VAR>i : ℕ<VAR>hi : ∀ (a : ℕ), i ≤ a → f a ≤ r - 1<VAR>hi' : ∀ (a : ℕ), r - 1 < f a → a < i<GOAL>{a | r ≤ f a} ⊆ {a | a ≤ i}
<VAR>K : Type u_1<VAR>inst✝ : Field K<VAR>s : SimpContFract K<VAR>n : ℕ<VAR>hyp : n = 0 ∨ ¬(↑s).TerminatedAt (n - 1)<GOAL>((↑s).contsAux n).a * ((↑s).contsAux (n + 1)).b - ((↑s).contsAux n).b * ((↑s).contsAux (n + 1)).a = (-1) ^ n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>la : Filter α<VAR>pa : ι → Prop<VAR>sa : ι → Set α<VAR>lb : Filter β<VAR>pb : ι' → Prop<VAR>sb : ι' → Set β<VAR>f : α → β<VAR>hl : la.HasBasis pa sa<VAR>i j : ι<VAR>hi : pa i<VAR>hj : pa j<GOAL>∃ k, pa k ∧ sa k ⊆ sa i ∧ sa k ⊆ sa j
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : GeneralizedBooleanAlgebra α<VAR>a b c d : α<GOAL>a ∆ b ⊓ c = (a ⊓ c) ∆ (b ⊓ c)
<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₂ : (i : ι) → Set (α i)<VAR>u : Set ((i : ι) × α i)<VAR>x✝ : (i : ι) × α i<VAR>i j : ι<VAR>a : α i<VAR>h : i ≠ j<VAR>s : Set (α j)<VAR>x : α i<GOAL>x ∈ Sigma.mk i ⁻¹' (Sigma.mk j '' s) ↔ x ∈ ∅
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>inst✝¹ : ReflectsColimit (span f f) F<VAR>inst✝ : Epi (F.map f)<VAR>this : IsColimit (PushoutCocone.mk (𝟙 (F.obj Y)) (𝟙 (F.obj Y)) ⋯)<GOAL>Epi f
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>inst✝¹ : ReflectsColimit (span f f) F<VAR>inst✝ : Epi (F.map f)<VAR>this : IsColimit (PushoutCocone.mk (F.map (𝟙 Y)) (F.map (𝟙 Y)) ⋯)<GOAL>Epi f
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hpi : ¬Irreducible ↑p<GOAL>¬(norm ↑p).natAbs = 1
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hpi : ¬Irreducible ↑p<GOAL>¬((↑p).natAbs = 1 ∧ (↑p).natAbs = 1)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hpi : ¬Irreducible ↑p<VAR>hpu : ¬IsUnit ↑p<GOAL>∃ a b, ↑p = a * b ∧ ¬IsUnit a ∧ ¬IsUnit b
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hpi : ¬Irreducible ↑p<VAR>hpu : ¬IsUnit ↑p<VAR>hab : ∃ a b, ↑p = a * b ∧ ¬IsUnit a ∧ ¬IsUnit b<VAR>a b : ℤ[i]<VAR>hpab : ↑p = a * b<VAR>hau : ¬IsUnit a<VAR>hbu : ¬IsUnit b<GOAL>(norm a).natAbs * (norm b).natAbs = p ^ 2
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hpi : ¬Irreducible ↑p<VAR>hpu : ¬IsUnit ↑p<VAR>hab : ∃ a b, ↑p = a * b ∧ ¬IsUnit a ∧ ¬IsUnit b<VAR>a b : ℤ[i]<VAR>hpab : ↑p = a * b<VAR>hau : ¬IsUnit a<VAR>hbu : ¬IsUnit b<GOAL>↑((norm a).natAbs * (norm b).natAbs) = norm (a * b)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hpi : ¬Irreducible ↑p<VAR>hpu : ¬IsUnit ↑p<VAR>hab : ∃ a b, ↑p = a * b ∧ ¬IsUnit a ∧ ¬IsUnit b<VAR>a b : ℤ[i]<VAR>hpab : ↑p = a * b<VAR>hau : ¬IsUnit a<VAR>hbu : ¬IsUnit b<VAR>hnap : (norm a).natAbs = p<GOAL>a.re.natAbs ^ 2 + a.im.natAbs ^ 2 = p
<VAR>n✝ n : ℕ<VAR>n2 : 2 ≤ n<VAR>x✝ : ℕ<VAR>k : ℕ := x✝<VAR>i : ℕ<VAR>e : x✝ = 2 * i + 3<VAR>a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m<VAR>h : ¬n < k * k<GOAL>Nat.minFacProp n (if n < x✝ * x✝ then n else if x✝ ∣ n then x✝ else n.minFacAux (x✝ + 2))
<VAR>n✝ n : ℕ<VAR>n2 : 2 ≤ n<VAR>x✝ : ℕ<VAR>k : ℕ := x✝<VAR>i : ℕ<VAR>e : x✝ = 2 * i + 3<VAR>a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m<VAR>h : ¬n < k * k<VAR>k2 : 2 ≤ k<GOAL>Nat.minFacProp n (if n < x✝ * x✝ then n else if x✝ ∣ n then x✝ else n.minFacAux (x✝ + 2))
<VAR>n m : ℕ<VAR>p✝ : Fin (n + 1)<VAR>i✝ j : Fin n<VAR>p : Fin (n + 1)<VAR>i : Fin n<GOAL>p.succAbove i.rev = (p.rev.succAbove i).rev
<VAR>α✝ : Type u<VAR>β✝ : Type u_1<VAR>γ : Type u_2<VAR>r✝ : α✝ → α✝ → Prop<VAR>s✝ : β✝ → β✝ → Prop<VAR>t : γ → γ → Prop<VAR>α β : Type u<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>inst✝¹ : IsWellOrder α r<VAR>inst✝ : IsWellOrder β s<VAR>f : r ≃r s<VAR>o : Ordinal.{u}<GOAL>∀ (hr : o < type r) (hs : o < type s), f (enum r o hr) = enum s o hs
<VAR>α✝ : Type u<VAR>β✝ : Type u_1<VAR>γ : Type u_2<VAR>r✝ : α✝ → α✝ → Prop<VAR>s✝ : β✝ → β✝ → Prop<VAR>t : γ → γ → Prop<VAR>α β : Type u<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>inst✝¹ : IsWellOrder α r<VAR>inst✝ : IsWellOrder β s<VAR>f : r ≃r s<VAR>o : Ordinal.{u}<GOAL>∀ (α_1 : Type u) (r_1 : α_1 → α_1 → Prop) [inst : IsWellOrder α_1 r_1] (hr : type r_1 < type r) (hs : type r_1 < type s), f (enum r (type r_1) hr) = enum s (type r_1) hs
<VAR>α✝ : Type u<VAR>β✝ : Type u_1<VAR>γ✝ : Type u_2<VAR>r✝ : α✝ → α✝ → Prop<VAR>s✝ : β✝ → β✝ → Prop<VAR>t✝ : γ✝ → γ✝ → Prop<VAR>α β : Type u<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>inst✝¹ : IsWellOrder α r<VAR>inst✝ : IsWellOrder β s<VAR>f : r ≃r s<VAR>o : Ordinal.{u}<VAR>γ : Type u<VAR>t : γ → γ → Prop<VAR>wo : IsWellOrder γ t<VAR>g : t ≺i r<VAR>h : t ≺i s<GOAL>f (enum r (type t) ⋯) = enum s (type t) ⋯
<VAR>α✝ : Type u<VAR>β✝ : Type u_1<VAR>γ✝ : Type u_2<VAR>r✝ : α✝ → α✝ → Prop<VAR>s✝ : β✝ → β✝ → Prop<VAR>t✝ : γ✝ → γ✝ → Prop<VAR>α β : Type u<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>inst✝¹ : IsWellOrder α r<VAR>inst✝ : IsWellOrder β s<VAR>f : r ≃r s<VAR>o : Ordinal.{u}<VAR>γ : Type u<VAR>t : γ → γ → Prop<VAR>wo : IsWellOrder γ t<VAR>g : t ≺i r<VAR>h : t ≺i s<GOAL>f g.top = (g.ltEquiv f).top
<VAR>𝕜 : Type u_1<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>s : E<VAR>p q : FormalMultilinearSeries 𝕜 𝕜 E<VAR>f g : 𝕜 → E<VAR>n : ℕ<VAR>z z₀ : 𝕜<VAR>a✝ a : ℕ → E<GOAL>HasSum (fun n => 0 ^ n • a n) (a 0)
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>X Y Z : C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>inst✝ : HasPullbacks C<VAR>A B : C<VAR>f : A ⟶ B<GOAL>∀ {X Y : Subobject B}, X.Factors f ∧ Y.Factors f → (X ⊓ Y).Factors f
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>X Y Z : C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>inst✝ : HasPullbacks C<VAR>A B : C<VAR>f : A ⟶ B<GOAL>∀ (a₁ a₂ : MonoOver B), Factors (Quotient.mk'' a₁) f ∧ Factors (Quotient.mk'' a₂) f → (Quotient.mk'' a₁ ⊓ Quotient.mk'' a₂).Factors f
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>N : Type u_3<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>p : AdicCompletion I M → Prop<VAR>x : AdicCompletion I M<VAR>h : ∀ (f : AdicCauchySequence I M), p ((mk I M) f)<GOAL>p x
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>N : Type u_3<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>p : AdicCompletion I M → Prop<VAR>h : ∀ (f : AdicCauchySequence I M), p ((mk I M) f)<VAR>f : AdicCauchySequence I M<GOAL>p ((mk I M) f)
<VAR>R : Type u<VAR>inst✝³ : CommSemiring R<VAR>S : Type u_1<VAR>inst✝² : CommSemiring S<VAR>f : R →* S<VAR>g : R →+* S<VAR>p m n : ℕ<VAR>inst✝¹ : ExpChar R p<VAR>inst✝ : ExpChar S p<VAR>x y : R<GOAL>(iterateFrobenius R p (m * n)) x = (⇑(iterateFrobenius R p m))^[n] x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : Module R M<VAR>I : Ideal R<VAR>S : Type u_3<VAR>inst✝⁹ : CommSemiring S<VAR>inst✝⁸ : Algebra S R<VAR>inst✝⁷ : Module S M<VAR>inst✝⁶ : IsScalarTower S R M<VAR>R' : Type u_4<VAR>M' : Type u_5<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : AddCommGroup M'<VAR>inst✝³ : Module R' M'<VAR>inst✝² : Algebra R R'<VAR>inst✝¹ : Module R M'<VAR>inst✝ : IsScalarTower R R' M'<VAR>p : R[X]<VAR>q : PolynomialModule R M<VAR>r : R<GOAL>(eval r) ((comp p) q) = (eval (Polynomial.eval r p)) q
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : Module R M<VAR>I : Ideal R<VAR>S : Type u_3<VAR>inst✝⁹ : CommSemiring S<VAR>inst✝⁸ : Algebra S R<VAR>inst✝⁷ : Module S M<VAR>inst✝⁶ : IsScalarTower S R M<VAR>R' : Type u_4<VAR>M' : Type u_5<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : AddCommGroup M'<VAR>inst✝³ : Module R' M'<VAR>inst✝² : Algebra R R'<VAR>inst✝¹ : Module R M'<VAR>inst✝ : IsScalarTower R R' M'<VAR>p : R[X]<VAR>q : PolynomialModule R M<VAR>r : R<GOAL>(eval r ∘ₗ comp p) q = (eval (Polynomial.eval r p)) q
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : Module R M<VAR>I : Ideal R<VAR>S : Type u_3<VAR>inst✝⁹ : CommSemiring S<VAR>inst✝⁸ : Algebra S R<VAR>inst✝⁷ : Module S M<VAR>inst✝⁶ : IsScalarTower S R M<VAR>R' : Type u_4<VAR>M' : Type u_5<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : AddCommGroup M'<VAR>inst✝³ : Module R' M'<VAR>inst✝² : Algebra R R'<VAR>inst✝¹ : Module R M'<VAR>inst✝ : IsScalarTower R R' M'<VAR>p : R[X]<VAR>q : PolynomialModule R M<VAR>r : R<GOAL>(eval r ∘ₗ comp p) 0 = (eval (Polynomial.eval r p)) 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : Module R M<VAR>I : Ideal R<VAR>S : Type u_3<VAR>inst✝⁹ : CommSemiring S<VAR>inst✝⁸ : Algebra S R<VAR>inst✝⁷ : Module S M<VAR>inst✝⁶ : IsScalarTower S R M<VAR>R' : Type u_4<VAR>M' : Type u_5<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : AddCommGroup M'<VAR>inst✝³ : Module R' M'<VAR>inst✝² : Algebra R R'<VAR>inst✝¹ : Module R M'<VAR>inst✝ : IsScalarTower R R' M'<VAR>p : R[X]<VAR>q : PolynomialModule R M<VAR>r : R<GOAL>∀ (f g : PolynomialModule R M), (eval r ∘ₗ comp p) f = (eval (Polynomial.eval r p)) f → (eval r ∘ₗ comp p) g = (eval (Polynomial.eval r p)) g → (eval r ∘ₗ comp p) (f + g) = (eval (Polynomial.eval r p)) (f + g)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : Module R M<VAR>I : Ideal R<VAR>S : Type u_3<VAR>inst✝⁹ : CommSemiring S<VAR>inst✝⁸ : Algebra S R<VAR>inst✝⁷ : Module S M<VAR>inst✝⁶ : IsScalarTower S R M<VAR>R' : Type u_4<VAR>M' : Type u_5<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : AddCommGroup M'<VAR>inst✝³ : Module R' M'<VAR>inst✝² : Algebra R R'<VAR>inst✝¹ : Module R M'<VAR>inst✝ : IsScalarTower R R' M'<VAR>p : R[X]<VAR>q : PolynomialModule R M<VAR>r : R<GOAL>∀ (a : ℕ) (b : M), (eval r ∘ₗ comp p) ((single R a) b) = (eval (Polynomial.eval r p)) ((single R a) b)
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : L.Structure N<VAR>inst✝ : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>n✝ : ℕ<VAR>T : L.Theory<VAR>n : ℕ<GOAL>M ⊨ Sentence.cardGe L n ↔ ↑n ≤ #M
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : L.Structure N<VAR>inst✝ : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>n✝ : ℕ<VAR>T : L.Theory<VAR>n : ℕ<GOAL>(∃ xs, (List.foldr (fun x x_1 => x ⊓ x_1) ⊤ (List.map (fun ij => ∼((var ∘ Sum.inr) ij.1 =' (var ∘ Sum.inr) ij.2)) (List.filter (fun ij => decide (ij.1 ≠ ij.2)) (List.finRange n ×ˢ List.finRange n)))).Realize default xs) ↔ Nonempty (Fin n ↪ M)
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : L.Structure N<VAR>inst✝ : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>n✝ : ℕ<VAR>T : L.Theory<VAR>n : ℕ<GOAL>(∃ xs, ∀ φ ∈ List.map (fun ij => ∼((var ∘ Sum.inr) ij.1 =' (var ∘ Sum.inr) ij.2)) (List.filter (fun ij => decide (ij.1 ≠ ij.2)) (List.finRange n ×ˢ List.finRange n)), φ.Realize default xs) ↔ Nonempty (Fin n ↪ M)
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : L.Structure N<VAR>inst✝ : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>n✝ : ℕ<VAR>T : L.Theory<VAR>n : ℕ<GOAL>(∃ xs, ∀ (φ : L.BoundedFormula Empty n) (x x_1 : Fin n), (decide ¬x = x_1) = true → ∼(var (Sum.inr x) =' var (Sum.inr x_1)) = φ → φ.Realize default xs) ↔ Nonempty (Fin n ↪ M)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>R : Type u_4<VAR>inst✝ : Ring α<VAR>a b : α<VAR>n : ℕ<VAR>ha : Odd a<VAR>hb : Even b<GOAL>Odd (a - b)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>R : Type u_4<VAR>inst✝ : Ring α<VAR>a b : α<VAR>n : ℕ<VAR>ha : Odd a<VAR>hb : Even b<GOAL>Odd (a + -b)
<VAR>α : Type v<VAR>G : Type u<VAR>inst✝³ : Group G<VAR>inst✝² : MulAction G α<VAR>M : Type u<VAR>inst✝¹ : Monoid M<VAR>inst✝ : MulAction M α<VAR>a : G<VAR>b : α<VAR>n : ℕ<GOAL>a ^ (n % minimalPeriod (fun x => a • x) b) • b = a ^ n • b
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>W : Type v<VAR>G : SimpleGraph V<VAR>G₁ G₂ : G.Subgraph<VAR>a b : V<VAR>s : Set G.Subgraph<VAR>G' : G.Subgraph<VAR>hG' : G' ∈ s<GOAL>(∀ G' ∈ s, G'.Adj a b) → G.Adj a b
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>z w : K<VAR>x : ℝ<GOAL>↑x ≤ 0 ↔ x ≤ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>h : s ⊆ t<GOAL>(Ico s t).card = 2 ^ (t.card - s.card) - 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>G : Type u_6<VAR>inst✝ : Group G<VAR>s✝ t✝ : Set α<VAR>f✝ g✝ : α → G<VAR>a : α<VAR>g : G → β<VAR>hg : ∀ (x : G), g x⁻¹ = g x<VAR>s t : Set α<VAR>f : α → G<VAR>x : α<GOAL>g ((s ∆ t).mulIndicator f x) = g (s.mulIndicator f x / t.mulIndicator f x)
<VAR>A : Type u_1<VAR>inst✝⁵ : NormedRing A<VAR>inst✝⁴ : NormedAlgebra ℂ A<VAR>inst✝³ : CompleteSpace A<VAR>inst✝² : StarRing A<VAR>inst✝¹ : CstarRing A<VAR>inst✝ : StarModule ℂ A<VAR>a : A<VAR>ha : IsSelfAdjoint a<VAR>z : ℂ<VAR>hz : z ∈ spectrum ℂ a<GOAL>(ofReal' ∘ re) z ∈ spectrum ℂ a
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : IsCofilteredOrEmpty C<VAR>i j j' : C<VAR>f : j ⟶ i<VAR>f' : j' ⟶ i<VAR>K : C<VAR>G : K ⟶ j<VAR>G' : K ⟶ j'<VAR>h✝ : True<VAR>k : C<VAR>e : k ⟶ K<VAR>he : e ≫ G ≫ f = e ≫ G' ≫ f'<GOAL>(e ≫ G) ≫ f = (e ≫ G') ≫ f'
<VAR>α : Type u_1<VAR>M✝ : Matroid α<VAR>E B I X R J : Set α<VAR>M : Matroid α<GOAL>M ↾ ∅ = emptyOn α
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s✝ s₁ s₂ : Finset α<VAR>t✝ t₁ t₂ : α → Finset β<VAR>inst✝ : DecidableEq β<VAR>s : Finset β<VAR>t : Finset α<VAR>f : α → Finset β<GOAL>Disjoint s (t.biUnion f) ↔ ∀ i ∈ t, Disjoint s (f i)
<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>μ : Measure X<VAR>𝕜 : Type u_5<VAR>inst✝⁷ : RCLike 𝕜<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace 𝕜 E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace 𝕜 F<VAR>p : ℝ≥0∞<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace E<VAR>f : X → E × F<VAR>hf : Integrable f μ<GOAL>(∫ (x : X), f x ∂μ).2 = ∫ (x : X), (f x).2 ∂μ
<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>μ : Measure X<VAR>𝕜 : Type u_5<VAR>inst✝⁷ : RCLike 𝕜<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace 𝕜 E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace 𝕜 F<VAR>p : ℝ≥0∞<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace E<VAR>f : X → E × F<VAR>hf : Integrable f μ<GOAL>(∫ (x : X), (f x).swap ∂μ).1 = ∫ (x : X), (f x).2 ∂μ
<VAR>R : Type<VAR>inst✝ : CommRing R<VAR>d : ℤ<VAR>r : { r // r * r = ↑d }<VAR>a b : ℤ√d<GOAL>(↑{ toFun := fun a => ↑a.re + ↑a.im * ↑r, map_one' := ⋯, map_mul' := ⋯ }).toFun (a + b) = (↑{ toFun := fun a => ↑a.re + ↑a.im * ↑r, map_one' := ⋯, map_mul' := ⋯ }).toFun a + (↑{ toFun := fun a => ↑a.re + ↑a.im * ↑r, map_one' := ⋯, map_mul' := ⋯ }).toFun b
<VAR>R : Type<VAR>inst✝ : CommRing R<VAR>d : ℤ<VAR>r : { r // r * r = ↑d }<VAR>a b : ℤ√d<GOAL>↑a.re + ↑b.re + (↑a.im + ↑b.im) * ↑r = ↑a.re + ↑a.im * ↑r + (↑b.re + ↑b.im * ↑r)
<VAR>R : Type<VAR>inst✝ : CommRing R<VAR>d : ℤ<VAR>r : { r // r * r = ↑d }<VAR>a b : ℤ√d<VAR>this : (↑a.re + ↑a.im * ↑r) * (↑b.re + ↑b.im * ↑r) = ↑a.re * ↑b.re + (↑a.re * ↑b.im + ↑a.im * ↑b.re) * ↑r + ↑a.im * ↑b.im * (↑r * ↑r)<GOAL>{ toFun := fun a => ↑a.re + ↑a.im * ↑r, map_one' := ⋯ }.toFun (a * b) = { toFun := fun a => ↑a.re + ↑a.im * ↑r, map_one' := ⋯ }.toFun a * { toFun := fun a => ↑a.re + ↑a.im * ↑r, map_one' := ⋯ }.toFun b
<VAR>R : Type<VAR>inst✝ : CommRing R<VAR>d : ℤ<VAR>r : { r // r * r = ↑d }<VAR>a b : ℤ√d<VAR>this : (↑a.re + ↑a.im * ↑r) * (↑b.re + ↑b.im * ↑r) = ↑a.re * ↑b.re + (↑a.re * ↑b.im + ↑a.im * ↑b.re) * ↑r + ↑a.im * ↑b.im * (↑r * ↑r)<GOAL>↑a.re * ↑b.re + ↑d * ↑a.im * ↑b.im + (↑a.re * ↑b.im + ↑a.im * ↑b.re) * ↑r = ↑a.re * ↑b.re + (↑a.re * ↑b.im + ↑a.im * ↑b.re) * ↑r + ↑a.im * ↑b.im * ↑d
<VAR>R : Type<VAR>inst✝ : CommRing R<VAR>d : ℤ<VAR>f : ℤ√d →+* R<GOAL>f sqrtd * f sqrtd = ↑d
<VAR>R : Type<VAR>inst✝ : CommRing R<VAR>d : ℤ<VAR>f : ℤ√d →+* R<GOAL>(fun r => { toFun := fun a => ↑a.re + ↑a.im * ↑r, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }) ((fun f => ⟨f sqrtd, ⋯⟩) f) = f
<VAR>R : Type<VAR>inst✝ : CommRing R<VAR>d : ℤ<VAR>f : ℤ√d →+* R<GOAL>((fun r => { toFun := fun a => ↑a.re + ↑a.im * ↑r, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }) ((fun f => ⟨f sqrtd, ⋯⟩) f)) sqrtd = f sqrtd
<VAR>l m✝ n : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Mul α<VAR>inst✝ : AddCommMonoid α<VAR>m : ℕ<VAR>a b : Fin m → α<GOAL>dotProductᵣ a b = a ⬝ᵥ b
<VAR>R : Type u_1<VAR>inst✝⁴ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝³ : CommSemiring S<VAR>inst✝² : Algebra R S<VAR>P : Type u_3<VAR>inst✝¹ : CommSemiring P<VAR>inst✝ : IsLocalization M S<VAR>g : R →+* P<VAR>h : ∀ (y : ↥M), IsUnit (g ↑y)<VAR>y : ↥M<VAR>w z₁ z₂ : P<GOAL>w * ↑((IsUnit.liftRight ((↑g).restrict M) h) y)⁻¹ + z₁ = z₂ ↔ w + g ↑y * z₁ = g ↑y * z₂
<VAR>R : Type u_1<VAR>inst✝⁴ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝³ : CommSemiring S<VAR>inst✝² : Algebra R S<VAR>P : Type u_3<VAR>inst✝¹ : CommSemiring P<VAR>inst✝ : IsLocalization M S<VAR>g : R →+* P<VAR>h : ∀ (y : ↥M), IsUnit (g ↑y)<VAR>y : ↥M<VAR>w z₁ z₂ : P<GOAL>w + ((↑g).restrict M) y * z₁ = ((↑g).restrict M) y * z₂ ↔ w + g ↑y * z₁ = g ↑y * z₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>E : Type u_3<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f g : α → E<VAR>hf : Integrable f μ<VAR>hg : Integrable g μ<GOAL>μ.withDensityᵥ (f - g) = μ.withDensityᵥ f - μ.withDensityᵥ g
<VAR>m n a b : ℕ<GOAL>↑a = 0 ↔ b ∣ a
<VAR>α : Sort u_1<VAR>A : Sort u_2<VAR>B : Sort u_3<VAR>inst✝¹ : Unique A<VAR>inst✝ : Unique B<VAR>f : A → B<GOAL>Function.Bijective f
<VAR>α : Sort u_1<VAR>A : Sort u_2<VAR>B : Sort u_3<VAR>inst✝¹ : Unique A<VAR>inst✝ : Unique B<VAR>f : A → B<GOAL>∃ g, Function.LeftInverse g f ∧ Function.RightInverse g f
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>α : Type u_7<VAR>inst✝⁹ : LinearOrderedField R<VAR>inst✝⁸ : LinearOrderedField R'<VAR>inst✝⁷ : AddCommGroup E<VAR>inst✝⁶ : AddCommGroup F<VAR>inst✝⁵ : LinearOrderedAddCommGroup α<VAR>inst✝⁴ : Module R E<VAR>inst✝³ : Module R F<VAR>inst✝² : Module R α<VAR>inst✝¹ : OrderedSMul R α<VAR>s✝ : Set E<VAR>i j : ι<VAR>c : R<VAR>t : Finset ι<VAR>w : ι → R<VAR>z : ι → E<VAR>inst✝ : Fintype ι<VAR>f : ι → R<VAR>s : Set E<VAR>hs : s.Finite<VAR>this : Fintype ↑s := hs.fintype<GOAL>(convexHull R) s = ⇑(∑ x : ↑s, (LinearMap.proj x).smulRight ↑x) '' stdSimplex R ↑s
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>α : Type u_7<VAR>inst✝⁹ : LinearOrderedField R<VAR>inst✝⁸ : LinearOrderedField R'<VAR>inst✝⁷ : AddCommGroup E<VAR>inst✝⁶ : AddCommGroup F<VAR>inst✝⁵ : LinearOrderedAddCommGroup α<VAR>inst✝⁴ : Module R E<VAR>inst✝³ : Module R F<VAR>inst✝² : Module R α<VAR>inst✝¹ : OrderedSMul R α<VAR>s✝ : Set E<VAR>i j : ι<VAR>c : R<VAR>t : Finset ι<VAR>w : ι → R<VAR>z : ι → E<VAR>inst✝ : Fintype ι<VAR>f : ι → R<VAR>s : Set E<VAR>hs : s.Finite<VAR>this : Fintype ↑s := hs.fintype<GOAL>(convexHull R) s = (convexHull R) (range (⇑(∑ x : ↑s, (LinearMap.proj x).smulRight ↑x) ∘ fun i j => if i = j then 1 else 0))
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>α : Type u_7<VAR>inst✝⁹ : LinearOrderedField R<VAR>inst✝⁸ : LinearOrderedField R'<VAR>inst✝⁷ : AddCommGroup E<VAR>inst✝⁶ : AddCommGroup F<VAR>inst✝⁵ : LinearOrderedAddCommGroup α<VAR>inst✝⁴ : Module R E<VAR>inst✝³ : Module R F<VAR>inst✝² : Module R α<VAR>inst✝¹ : OrderedSMul R α<VAR>s✝ : Set E<VAR>i j : ι<VAR>c : R<VAR>t : Finset ι<VAR>w : ι → R<VAR>z : ι → E<VAR>inst✝ : Fintype ι<VAR>f : ι → R<VAR>s : Set E<VAR>hs : s.Finite<VAR>this : Fintype ↑s := hs.fintype<GOAL>s = range fun x => (∑ x : ↑s, (LinearMap.proj x).smulRight ↑x) fun j => if x = j then 1 else 0
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>α : Type u_7<VAR>inst✝⁹ : LinearOrderedField R<VAR>inst✝⁸ : LinearOrderedField R'<VAR>inst✝⁷ : AddCommGroup E<VAR>inst✝⁶ : AddCommGroup F<VAR>inst✝⁵ : LinearOrderedAddCommGroup α<VAR>inst✝⁴ : Module R E<VAR>inst✝³ : Module R F<VAR>inst✝² : Module R α<VAR>inst✝¹ : OrderedSMul R α<VAR>s✝ : Set E<VAR>i j : ι<VAR>c : R<VAR>t : Finset ι<VAR>w : ι → R<VAR>z : ι → E<VAR>inst✝ : Fintype ι<VAR>f : ι → R<VAR>s : Set E<VAR>hs : s.Finite<VAR>this : Fintype ↑s := hs.fintype<VAR>x✝ : ↑s<GOAL>((∑ x : ↑s, (LinearMap.proj x).smulRight ↑x) fun j => if x✝ = j then 1 else 0) = ↑x✝
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>f : ι → α → β<VAR>μ : Measure α<VAR>p : α → (ι → β) → Prop<VAR>inst✝ : Countable ι<VAR>hf : ∀ (i : ι), AEMeasurable (f i) μ<VAR>hp : ∀ᵐ (x : α) ∂μ, p x fun n => f n x<GOAL>μ (aeSeqSet hf p)ᶜ = 0
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>f : ι → α → β<VAR>μ : Measure α<VAR>p : α → (ι → β) → Prop<VAR>inst✝ : Countable ι<VAR>hf : ∀ (i : ι), AEMeasurable (f i) μ<VAR>hp : ∀ᵐ (x : α) ∂μ, p x fun n => f n x<GOAL>μ {x | (∀ (i : ι), f i x = AEMeasurable.mk (f i) ⋯ x) ∧ p x fun n => f n x}ᶜ = 0
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>f : ι → α → β<VAR>μ : Measure α<VAR>p : α → (ι → β) → Prop<VAR>inst✝ : Countable ι<VAR>hf : ∀ (i : ι), AEMeasurable (f i) μ<VAR>hp : ∀ᵐ (x : α) ∂μ, p x fun n => f n x<VAR>hf_eq : ∀ (i : ι), f i =ᶠ[ae μ] AEMeasurable.mk (f i) ⋯<GOAL>μ {x | (∀ (i : ι), f i x = AEMeasurable.mk (f i) ⋯ x) ∧ p x fun n => f n x}ᶜ = 0
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>f : ι → α → β<VAR>μ : Measure α<VAR>p : α → (ι → β) → Prop<VAR>inst✝ : Countable ι<VAR>hf : ∀ (i : ι), AEMeasurable (f i) μ<VAR>hp : ∀ᵐ (x : α) ∂μ, p x fun n => f n x<VAR>hf_eq : ∀ᵐ (a : α) ∂μ, ∀ (i : ι), f i a = AEMeasurable.mk (f i) ⋯ a<GOAL>μ {x | (∀ (i : ι), f i x = AEMeasurable.mk (f i) ⋯ x) ∧ p x fun n => f n x}ᶜ = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>M₂ : Type u_3<VAR>M₃ : Type u_4<VAR>inst✝⁶ : Ring R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : AddCommGroup M₂<VAR>inst✝³ : AddCommGroup M₃<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M₂<VAR>inst✝ : Module R M₃<VAR>f : M →ₗ[R] M₂<VAR>p p' : Submodule R M<GOAL>Function.Injective ⇑(quotientInfToSupQuotient p p')
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>M₂ : Type u_3<VAR>M₃ : Type u_4<VAR>inst✝⁶ : Ring R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : AddCommGroup M₂<VAR>inst✝³ : AddCommGroup M₃<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M₂<VAR>inst✝ : Module R M₃<VAR>f : M →ₗ[R] M₂<VAR>p p' : Submodule R M<GOAL>ker (subToSupQuotient p p') ≤ comap p.subtype (p ⊓ p')