ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>inst✝³ : Semiring R<VAR>S : Submonoid R<VAR>inst✝² : OreSet S<VAR>X : Type u_2<VAR>inst✝¹ : AddCommMonoid X<VAR>inst✝ : Module R X<VAR>r₁ : X<VAR>s₁ : ↥S<VAR>r₂ : R<VAR>s₂ : ↥S<VAR>r₃ : R<VAR>s₃ : ↥S<VAR>ra : R<VAR>sa : ↥S<VAR>ha : ↑sa * ↑s₂ = ra * ↑s₃<VAR>rb : R<VAR>sb : ↥S<VAR>hb : ↑sb * sa • r₂ = rb * ↑s₁<VAR>hs₃rasb : ↑sb * ra * ↑s₃ ∈ S<VAR>ha' : ↑(sb * sa * s₂) = ↑sb * ra * ↑s₃<VAR>rc : R<VAR>sc : ↥S<VAR>hc : ↑sc * (↑sb * ra) • r₃ = rc * ↑s₁<VAR>hc' : ((↑sb * ra) • r₃ /ₒ (sb * sa * s₂)) • (r₁ /ₒ s₁) = rc • r₁ /ₒ (sc * (sb * sa * s₂))<GOAL>((sc * sb) • (sa • r₂ + ra • r₃) /ₒ (sc * sb * (sa * s₂))) • (r₁ /ₒ s₁) = (sc • rb • r₁ + 1 • rc • r₁) /ₒ (sc * (sb * (sa * s₂)))
<VAR>R : Type u_1<VAR>inst✝³ : Semiring R<VAR>S : Submonoid R<VAR>inst✝² : OreSet S<VAR>X : Type u_2<VAR>inst✝¹ : AddCommMonoid X<VAR>inst✝ : Module R X<VAR>r₁ : X<VAR>s₁ : ↥S<VAR>r₂ : R<VAR>s₂ : ↥S<VAR>r₃ : R<VAR>s₃ : ↥S<VAR>ra : R<VAR>sa : ↥S<VAR>ha : ↑sa * ↑s₂ = ra * ↑s₃<VAR>rb : R<VAR>sb : ↥S<VAR>hb : ↑sb * (↑sa * r₂) = rb * ↑s₁<VAR>hs₃rasb : ↑sb * ra * ↑s₃ ∈ S<VAR>ha' : ↑(sb * sa * s₂) = ↑sb * ra * ↑s₃<VAR>rc : R<VAR>sc : ↥S<VAR>hc : ↑sc * (↑sb * ra * r₃) = rc * ↑s₁<VAR>hc' : ((↑sb * ra) • r₃ /ₒ (sb * sa * s₂)) • (r₁ /ₒ s₁) = rc • r₁ /ₒ (sc * (sb * sa * s₂))<GOAL>((↑sc * ↑sb * (↑sa * r₂) + ↑sc * ↑sb * (ra * r₃)) /ₒ (sc * sb * (sa * s₂))) • (r₁ /ₒ s₁) = (↑sc • rb • r₁ + rc • r₁) /ₒ (sc * (sb * (sa * s₂)))
<VAR>R : Type u_1<VAR>inst✝³ : Semiring R<VAR>S : Submonoid R<VAR>inst✝² : OreSet S<VAR>X : Type u_2<VAR>inst✝¹ : AddCommMonoid X<VAR>inst✝ : Module R X<VAR>r₁ : X<VAR>s₁ : ↥S<VAR>r₂ : R<VAR>s₂ : ↥S<VAR>r₃ : R<VAR>s₃ : ↥S<VAR>ra : R<VAR>sa : ↥S<VAR>ha : ↑sa * ↑s₂ = ra * ↑s₃<VAR>rb : R<VAR>sb : ↥S<VAR>hb : ↑sb * (↑sa * r₂) = rb * ↑s₁<VAR>hs₃rasb : ↑sb * ra * ↑s₃ ∈ S<VAR>ha' : ↑(sb * sa * s₂) = ↑sb * ra * ↑s₃<VAR>rc : R<VAR>sc : ↥S<VAR>hc : ↑sc * (↑sb * ra * r₃) = rc * ↑s₁<VAR>hc' : ((↑sb * ra) • r₃ /ₒ (sb * sa * s₂)) • (r₁ /ₒ s₁) = rc • r₁ /ₒ (sc * (sb * sa * s₂))<GOAL>((↑sc * rb + rc) * ↑s₁ /ₒ (sc * sb * (sa * s₂))) • (r₁ /ₒ s₁) = (↑sc • rb • r₁ + rc • r₁) /ₒ (sc * (sb * (sa * s₂)))
<VAR>R : Type u_1<VAR>inst✝³ : Semiring R<VAR>S : Submonoid R<VAR>inst✝² : OreSet S<VAR>X : Type u_2<VAR>inst✝¹ : AddCommMonoid X<VAR>inst✝ : Module R X<VAR>r₁ : X<VAR>s₁ : ↥S<VAR>r₂ : R<VAR>s₂ : ↥S<VAR>r₃ : R<VAR>s₃ : ↥S<VAR>ra : R<VAR>sa : ↥S<VAR>ha : ↑sa * ↑s₂ = ra * ↑s₃<VAR>rb : R<VAR>sb : ↥S<VAR>hb : ↑sb * (↑sa * r₂) = rb * ↑s₁<VAR>hs₃rasb : ↑sb * ra * ↑s₃ ∈ S<VAR>ha' : ↑(sb * sa * s₂) = ↑sb * ra * ↑s₃<VAR>rc : R<VAR>sc : ↥S<VAR>hc : ↑sc * (↑sb * ra * r₃) = rc * ↑s₁<VAR>hc' : ((↑sb * ra) • r₃ /ₒ (sb * sa * s₂)) • (r₁ /ₒ s₁) = rc • r₁ /ₒ (sc * (sb * sa * s₂))<GOAL>(↑sc * rb + rc) • r₁ /ₒ (sc * sb * (sa * s₂)) = (↑sc • rb • r₁ + rc • r₁) /ₒ (sc * (sb * (sa * s₂)))
<VAR>K✝ : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝³ : DivisionRing K✝<VAR>inst✝² : DivisionRing L<VAR>inst✝¹ : DivisionRing M<VAR>s✝¹ : Set K✝<VAR>K : Type u<VAR>inst✝ : Field K<VAR>s✝ : Subfield K<VAR>s : Set K<VAR>x : K<GOAL>x ∈ closure s ↔ ∃ y ∈ Subring.closure s, ∃ z ∈ Subring.closure s, y / z = x
<VAR>K✝ : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝³ : DivisionRing K✝<VAR>inst✝² : DivisionRing L<VAR>inst✝¹ : DivisionRing M<VAR>s✝¹ : Set K✝<VAR>K : Type u<VAR>inst✝ : Field K<VAR>s✝ : Subfield K<VAR>s : Set K<VAR>x : K<GOAL>x ∈ Subfield.commClosure s ↔ ∃ y ∈ Subring.closure s, ∃ z ∈ Subring.closure s, y / z = x
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝ : Group α<VAR>s t : Set α<VAR>a b : α<GOAL>(fun x => a * x) ⁻¹' 1 = {a⁻¹}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>A✝ : Matrix n n α<VAR>inst✝³ : CommRing α<VAR>inst✝² : StarRing α<VAR>inst✝¹ : Fintype m<VAR>inst✝ : DecidableEq m<VAR>A : Matrix m m α<VAR>h : A.IsHermitian<VAR>k : ℤ<GOAL>(A ^ k).IsHermitian
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>t : ℝ≥0∞<VAR>t_ne_top : t ≠ ⊤<VAR>x y : ℝ≥0∞<VAR>x_le_y : x ≤ y<GOAL>t.truncateToReal x ≤ t.truncateToReal y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>t : ℝ≥0∞<VAR>t_ne_top : t ≠ ⊤<VAR>x y : ℝ≥0∞<VAR>x_le_y : x ≤ y<VAR>obs_x : min t x ≠ ⊤<GOAL>t.truncateToReal x ≤ t.truncateToReal y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>t : ℝ≥0∞<VAR>t_ne_top : t ≠ ⊤<VAR>x y : ℝ≥0∞<VAR>x_le_y : x ≤ y<VAR>obs_x : min t x ≠ ⊤<VAR>obs_y : min t y ≠ ⊤<GOAL>t.truncateToReal x ≤ t.truncateToReal y
<VAR>α : Type u_1<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<GOAL>⋃ n, Ioo a ↑n = Ioi a \ {⊤}
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C fun x => ord I x < o)))<GOAL>LinearIndependent ℤ (eval (C' C ho)) → LinearIndependent (ι := ↑(MaxProducts C ho)) ℤ (⇑(Linear_CC' C hsC ho) ∘ fun l => Products.eval C ↑l)
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C fun x => ord I x < o)))<GOAL>LinearIndependent ℤ (eval (C' C ho)) → LinearIndependent ℤ fun (l : ↑(MaxProducts C ho)) => Products.eval (C' C ho) (↑l).Tail
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C fun x => ord I x < o)))<VAR>h : LinearIndependent ℤ (eval (C' C ho))<VAR>f : ↑(MaxProducts C ho) → ↑(GoodProducts (C' C ho)) := MaxToGood C hC hsC ho h₁<GOAL>LinearIndependent ℤ fun (l : ↑(MaxProducts C ho)) => Products.eval (C' C ho) (↑l).Tail
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C fun x => ord I x < o)))<VAR>h : LinearIndependent ℤ (eval (C' C ho))<VAR>f : ↑(MaxProducts C ho) → ↑(GoodProducts (C' C ho)) := MaxToGood C hC hsC ho h₁<VAR>hf : Function.Injective f<GOAL>LinearIndependent ℤ fun (l : ↑(MaxProducts C ho)) => Products.eval (C' C ho) (↑l).Tail
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C fun x => ord I x < o)))<VAR>h : LinearIndependent ℤ (eval (C' C ho))<VAR>f : ↑(MaxProducts C ho) → ↑(GoodProducts (C' C ho)) := MaxToGood C hC hsC ho h₁<VAR>hf : Function.Injective f<VAR>hh : (fun l => Products.eval (C' C ho) (↑l).Tail) = eval (C' C ho) ∘ f<GOAL>LinearIndependent (ι := ↑(MaxProducts C ho)) ℤ (eval (C' C ho) ∘ f)
<VAR>R : Type u_2<VAR>K : Type ?u.52420<VAR>L : Type ?u.52423<VAR>S : Type u_1<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : Field L<VAR>inst✝⁴ : CommRing S<VAR>inst✝³ : Algebra R S<VAR>inst✝² : Algebra K L<VAR>x : S<VAR>hx : IsIntegral R x<VAR>inst✝¹ : IsDomain S<VAR>inst✝ : DecidableEq S<VAR>y : S<VAR>hy : (aeval y) (minpoly R x) = 0<GOAL>eval y (minpolyDiv R x) = if x = y then (aeval x) (derivative (minpoly R x)) else 0
<VAR>R : Type u_2<VAR>K : Type ?u.52420<VAR>L : Type ?u.52423<VAR>S : Type u_1<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : Field L<VAR>inst✝⁴ : CommRing S<VAR>inst✝³ : Algebra R S<VAR>inst✝² : Algebra K L<VAR>x : S<VAR>hx : IsIntegral R x<VAR>inst✝¹ : IsDomain S<VAR>inst✝ : DecidableEq S<VAR>y : S<VAR>hy : (aeval y) (minpoly R x) = 0<GOAL>eval₂ ((RingHom.id S).comp (algebraMap R S)) y (minpoly R x) = 0
<VAR>E : Type u_1<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>x : E<GOAL>‖x‖⁻¹ • x ∈ closedBall 0 1
<VAR>𝓕 : Type u_1<VAR>𝕜 : Type u_2<VAR>α : Type u_3<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>E : Type u_6<VAR>F : Type u_7<VAR>G : Type u_8<VAR>inst✝¹ : SeminormedCommGroup E<VAR>inst✝ : SeminormedCommGroup F<VAR>a✝ a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>n : ℕ<VAR>a : E<GOAL>‖a ^ n‖₊ ≤ ↑n * ‖a‖₊
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>L' : Type u_3<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : Field L<VAR>inst✝³ : Field L'<VAR>inst✝² : Algebra K L<VAR>inst✝¹ : Algebra K L'<VAR>S F E : IntermediateField K L<VAR>inst✝ : FiniteDimensional (↥F) L<VAR>h_le : F ≤ E<VAR>h_finrank : finrank (↥F) L ≤ finrank (↥E) L<GOAL>F = E
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>L' : Type u_3<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : Field L<VAR>inst✝³ : Field L'<VAR>inst✝² : Algebra K L<VAR>inst✝¹ : Algebra K L'<VAR>S F E : IntermediateField K L<VAR>inst✝ : FiniteDimensional (↥F) L<VAR>h_le : F ≤ E<VAR>h_finrank : finrank (↥F) L ≤ finrank (↥E) L<VAR>l : L<VAR>hl : l ∈ E<GOAL>l ∈ F
<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>x : R<VAR>inst✝¹⁶ : Away x S<VAR>g : R →+* P<VAR>Q : Type u_4<VAR>inst✝¹⁵ : CommSemiring Q<VAR>inst✝¹⁴ : Algebra P Q<VAR>A : Type u_5<VAR>inst✝¹³ : CommRing A<VAR>inst✝¹² : Algebra R A<VAR>B : Type u_6<VAR>inst✝¹¹ : CommRing B<VAR>inst✝¹⁰ : Algebra R B<VAR>Aₚ : Type u_7<VAR>inst✝⁹ : CommRing Aₚ<VAR>inst✝⁸ : Algebra A Aₚ<VAR>inst✝⁷ : Algebra R Aₚ<VAR>inst✝⁶ : IsScalarTower R A Aₚ<VAR>Bₚ : Type u_8<VAR>inst✝⁵ : CommRing Bₚ<VAR>inst✝⁴ : Algebra B Bₚ<VAR>inst✝³ : Algebra R Bₚ<VAR>inst✝² : IsScalarTower R B Bₚ<VAR>f : A →ₐ[R] B<VAR>a : A<VAR>inst✝¹ : Away a Aₚ<VAR>inst✝ : Away (f a) Bₚ<VAR>hf : Function.Surjective ⇑f<GOAL>IsLocalization (Submonoid.map f.toRingHom (Submonoid.powers 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>x : R<VAR>inst✝¹⁶ : Away x S<VAR>g : R →+* P<VAR>Q : Type u_4<VAR>inst✝¹⁵ : CommSemiring Q<VAR>inst✝¹⁴ : Algebra P Q<VAR>A : Type u_5<VAR>inst✝¹³ : CommRing A<VAR>inst✝¹² : Algebra R A<VAR>B : Type u_6<VAR>inst✝¹¹ : CommRing B<VAR>inst✝¹⁰ : Algebra R B<VAR>Aₚ : Type u_7<VAR>inst✝⁹ : CommRing Aₚ<VAR>inst✝⁸ : Algebra A Aₚ<VAR>inst✝⁷ : Algebra R Aₚ<VAR>inst✝⁶ : IsScalarTower R A Aₚ<VAR>Bₚ : Type u_8<VAR>inst✝⁵ : CommRing Bₚ<VAR>inst✝⁴ : Algebra B Bₚ<VAR>inst✝³ : Algebra R Bₚ<VAR>inst✝² : IsScalarTower R B Bₚ<VAR>f : A →ₐ[R] B<VAR>a : A<VAR>inst✝¹ : Away a Aₚ<VAR>inst✝ : Away (f a) Bₚ<VAR>hf : Function.Surjective ⇑f<GOAL>IsLocalization (Submonoid.powers (f a)) Bₚ
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f g : Perm α<VAR>x y : α<VAR>inst✝ : Finite α<VAR>hf : f.IsCycle<VAR>hx : f x ≠ x<VAR>hy : f y ≠ y<GOAL>∃ i, (f ^ i) x = y
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f g : Perm α<VAR>x y : α<VAR>inst✝ : Finite α<VAR>hf : f.IsCycle<VAR>hx : f x ≠ x<VAR>hy : f y ≠ y<VAR>n : ℤ<VAR>hn : (f ^ n) x = y<GOAL>∃ i, (f ^ i) x = y
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α✝<VAR>inst✝¹ : MeasurableSpace β<VAR>μ✝ ν✝ ν₁ ν₂ : Measure α✝<VAR>s✝ t : Set α✝<VAR>α : Type u_5<VAR>m₀ : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝ : IsFiniteMeasure μ<VAR>C : Set (Set α)<VAR>hμν : ∀ s ∈ C, μ s = ν s<VAR>m : MeasurableSpace α<VAR>h : m ≤ m₀<VAR>hA : m = generateFrom C<VAR>hC : IsPiSystem C<VAR>h_univ : μ univ = ν univ<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>μ s = ν s
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α✝<VAR>inst✝¹ : MeasurableSpace β<VAR>μ✝ ν✝ ν₁ ν₂ : Measure α✝<VAR>s✝ t : Set α✝<VAR>α : Type u_5<VAR>m₀ : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝ : IsFiniteMeasure μ<VAR>C : Set (Set α)<VAR>hμν : ∀ s ∈ C, μ s = ν s<VAR>m : MeasurableSpace α<VAR>h : m ≤ m₀<VAR>hA : m = generateFrom C<VAR>hC : IsPiSystem C<VAR>h_univ : μ univ = ν univ<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>this : IsFiniteMeasure ν<GOAL>μ s = ν s
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α✝<VAR>inst✝¹ : MeasurableSpace β<VAR>μ✝ ν✝ ν₁ ν₂ : Measure α✝<VAR>s✝ t : Set α✝<VAR>α : Type u_5<VAR>m₀ : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝ : IsFiniteMeasure μ<VAR>C : Set (Set α)<VAR>hμν : ∀ s ∈ C, μ s = ν s<VAR>m : MeasurableSpace α<VAR>h : m ≤ m₀<VAR>hA : m = generateFrom C<VAR>hC : IsPiSystem C<VAR>h_univ : μ univ = ν univ<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>this : IsFiniteMeasure ν<GOAL>∀ (t : Set α), MeasurableSet t → μ t = ν t → μ tᶜ = ν tᶜ
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α✝<VAR>inst✝¹ : MeasurableSpace β<VAR>μ✝ ν✝ ν₁ ν₂ : Measure α✝<VAR>s✝ t : Set α✝<VAR>α : Type u_5<VAR>m₀ : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝ : IsFiniteMeasure μ<VAR>C : Set (Set α)<VAR>hμν : ∀ s ∈ C, μ s = ν s<VAR>m : MeasurableSpace α<VAR>h : m ≤ m₀<VAR>hA : m = generateFrom C<VAR>hC : IsPiSystem C<VAR>h_univ : μ univ = ν univ<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>this : IsFiniteMeasure ν<GOAL>∀ (f : ℕ → Set α), Pairwise (Disjoint on f) → (∀ (i : ℕ), MeasurableSet (f i)) → (∀ (i : ℕ), μ (f i) = ν (f i)) → μ (⋃ i, f i) = ν (⋃ i, f i)
<VAR>Ω : Type u_1<VAR>Ω' : Type u_2<VAR>inst✝⁵ : MeasurableSpace Ω<VAR>inst✝⁴ : MeasurableSpace Ω'<VAR>inst✝³ : TopologicalSpace Ω<VAR>inst✝² : OpensMeasurableSpace Ω<VAR>inst✝¹ : TopologicalSpace Ω'<VAR>inst✝ : BorelSpace Ω'<VAR>ι : Type u_3<VAR>L : Filter ι<VAR>νs : ι → FiniteMeasure Ω<VAR>ν : FiniteMeasure Ω<VAR>lim : Tendsto νs L (𝓝 ν)<VAR>f : Ω → Ω'<VAR>f_cont : Continuous f<GOAL>Tendsto (fun i => (νs i).map f) L (𝓝 (ν.map f))
<VAR>Ω : Type u_1<VAR>Ω' : Type u_2<VAR>inst✝⁵ : MeasurableSpace Ω<VAR>inst✝⁴ : MeasurableSpace Ω'<VAR>inst✝³ : TopologicalSpace Ω<VAR>inst✝² : OpensMeasurableSpace Ω<VAR>inst✝¹ : TopologicalSpace Ω'<VAR>inst✝ : BorelSpace Ω'<VAR>ι : Type u_3<VAR>L : Filter ι<VAR>νs : ι → FiniteMeasure Ω<VAR>ν : FiniteMeasure Ω<VAR>lim : ∀ (f : Ω →ᵇ ℝ≥0), Tendsto (fun i => ∫⁻ (x : Ω), ↑(f x) ∂↑(νs i)) L (𝓝 (∫⁻ (x : Ω), ↑(f x) ∂↑ν))<VAR>f : Ω → Ω'<VAR>f_cont : Continuous f<GOAL>∀ (f_1 : Ω' →ᵇ ℝ≥0), Tendsto (fun i => ∫⁻ (x : Ω'), ↑(f_1 x) ∂↑((νs i).map f)) L (𝓝 (∫⁻ (x : Ω'), ↑(f_1 x) ∂↑(ν.map f)))
<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>r : ℝ<GOAL>(o.oangle x (r • y)).sign = SignType.sign r * (o.oangle x y).sign
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>A : Type z<VAR>a✝ b : R<VAR>n : ℕ<VAR>inst✝ : Semiring R<VAR>a : R<VAR>p : R[X]<VAR>k : ℕ<GOAL>(⇑derivative)^[k] (C a * p) = C a * (⇑derivative)^[k] p
<VAR>R : Type u_1<VAR>inst✝¹² : CommRing R<VAR>M : Type u_2<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : Module R M<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝⁹ : AddCommGroup N<VAR>inst✝⁸ : Module R N<VAR>inst✝⁷ : AddCommGroup P<VAR>inst✝⁶ : Module R P<VAR>ι : Type u_5<VAR>inst✝⁵ : Module.Free R M<VAR>inst✝⁴ : Module.Finite R M<VAR>inst✝³ : Module.Free R N<VAR>inst✝² : Module.Finite R N<VAR>inst✝¹ : Module.Free R P<VAR>inst✝ : Module.Finite R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] M<GOAL>(trace R M) (g ∘ₗ f) = (trace R N) (f ∘ₗ g)
<VAR>R : Type u_1<VAR>inst✝¹² : CommRing R<VAR>M : Type u_2<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : Module R M<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝⁹ : AddCommGroup N<VAR>inst✝⁸ : Module R N<VAR>inst✝⁷ : AddCommGroup P<VAR>inst✝⁶ : Module R P<VAR>ι : Type u_5<VAR>inst✝⁵ : Module.Free R M<VAR>inst✝⁴ : Module.Finite R M<VAR>inst✝³ : Module.Free R N<VAR>inst✝² : Module.Finite R N<VAR>inst✝¹ : Module.Free R P<VAR>inst✝ : Module.Finite R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] M<VAR>h : (((llcomp R M N M).compr₂ (trace R M)) g) f = (((llcomp R N M N).flip.compr₂ (trace R N)) g) f<GOAL>(trace R M) (g ∘ₗ f) = (trace R N) (f ∘ₗ g)
<VAR>R : Type u_1<VAR>inst✝¹² : CommRing R<VAR>M : Type u_2<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : Module R M<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝⁹ : AddCommGroup N<VAR>inst✝⁸ : Module R N<VAR>inst✝⁷ : AddCommGroup P<VAR>inst✝⁶ : Module R P<VAR>ι : Type u_5<VAR>inst✝⁵ : Module.Free R M<VAR>inst✝⁴ : Module.Finite R M<VAR>inst✝³ : Module.Free R N<VAR>inst✝² : Module.Finite R N<VAR>inst✝¹ : Module.Free R P<VAR>inst✝ : Module.Finite R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] M<VAR>h : (trace R M) (g ∘ₗ f) = (trace R N) (f ∘ₗ g)<GOAL>(trace R M) (g ∘ₗ f) = (trace R N) (f ∘ₗ g)
<VAR>α β : Type u<VAR>m n : ℕ<GOAL>↑m ≤ ↑n ↔ m ≤ n
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I B X : Set α<VAR>h : M✶.RkPos<VAR>hI : M.Indep I<GOAL>I ⊂ M.E
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I B✝ X : Set α<VAR>h : M✶.RkPos<VAR>hI : M.Indep I<VAR>B : Set α<VAR>hB : M.Base B ∧ I ⊆ B<GOAL>I ⊂ M.E
<VAR>ι : Type u<VAR>X : Type v<VAR>inst✝ : TopologicalSpace X<VAR>s : Set X<VAR>f : BumpCovering ι X s<VAR>i : ι<VAR>x : X<GOAL>∃ t, f.toPOUFun i =ᶠ[𝓝 x] ⇑(f i) * ⇑(∏ j ∈ Finset.filter (fun j => WellOrderingRel j i) t, (1 - f j))
<VAR>ι : Type u<VAR>X : Type v<VAR>inst✝ : TopologicalSpace X<VAR>s : Set X<VAR>f : BumpCovering ι X s<VAR>i : ι<VAR>x : X<VAR>U : Set X<VAR>hU : U ∈ 𝓝 x<VAR>hf : {i | ((fun i => support ⇑(f i)) i ∩ U).Nonempty}.Finite<GOAL>∃ t, f.toPOUFun i =ᶠ[𝓝 x] ⇑(f i) * ⇑(∏ j ∈ Finset.filter (fun j => WellOrderingRel j i) t, (1 - f j))
<VAR>ι : Type u<VAR>X : Type v<VAR>inst✝ : TopologicalSpace X<VAR>s : Set X<VAR>f : BumpCovering ι X s<VAR>i : ι<VAR>x : X<VAR>U : Set X<VAR>hU : U ∈ 𝓝 x<VAR>hf : {i | ((fun i => support ⇑(f i)) i ∩ U).Nonempty}.Finite<GOAL>f.toPOUFun i =ᶠ[𝓝 x] ⇑(f i) * ⇑(∏ j ∈ Finset.filter (fun j => WellOrderingRel j i) hf.toFinset, (1 - f j))
<VAR>ι : Type u<VAR>X : Type v<VAR>inst✝ : TopologicalSpace X<VAR>s : Set X<VAR>f : BumpCovering ι X s<VAR>i : ι<VAR>x : X<VAR>U : Set X<VAR>hU : U ∈ 𝓝 x<VAR>hf : {i | ((fun i => support ⇑(f i)) i ∩ U).Nonempty}.Finite<VAR>y : X<VAR>hyU : y ∈ U<GOAL>f.toPOUFun i y = (⇑(f i) * ⇑(∏ j ∈ Finset.filter (fun j => WellOrderingRel j i) hf.toFinset, (1 - f j))) y
<VAR>ι : Type u<VAR>X : Type v<VAR>inst✝ : TopologicalSpace X<VAR>s : Set X<VAR>f : BumpCovering ι X s<VAR>i : ι<VAR>x : X<VAR>U : Set X<VAR>hU : U ∈ 𝓝 x<VAR>hf : {i | ((fun i => support ⇑(f i)) i ∩ U).Nonempty}.Finite<VAR>y : X<VAR>hyU : y ∈ U<GOAL>f.toPOUFun i y = (f i) y * ∏ c ∈ Finset.filter (fun j => WellOrderingRel j i) hf.toFinset, (1 - f c) y
<VAR>ι : Type u<VAR>X : Type v<VAR>inst✝ : TopologicalSpace X<VAR>s : Set X<VAR>f : BumpCovering ι X s<VAR>i : ι<VAR>x : X<VAR>U : Set X<VAR>hU : U ∈ 𝓝 x<VAR>hf : {i | ((fun i => support ⇑(f i)) i ∩ U).Nonempty}.Finite<VAR>y : X<VAR>hyU : y ∈ U<GOAL>∀ (j : ι), WellOrderingRel j i → (f j) y ≠ 0 → j ∈ hf.toFinset
<VAR>ι : Type u<VAR>X : Type v<VAR>inst✝ : TopologicalSpace X<VAR>s : Set X<VAR>f : BumpCovering ι X s<VAR>i : ι<VAR>x : X<VAR>U : Set X<VAR>hU : U ∈ 𝓝 x<VAR>hf : {i | ((fun i => support ⇑(f i)) i ∩ U).Nonempty}.Finite<VAR>y : X<VAR>hyU : y ∈ U<VAR>j : ι<VAR>a✝ : WellOrderingRel j i<VAR>hj : (f j) y ≠ 0<GOAL>j ∈ hf.toFinset
<VAR>R : Type u<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>ι : Type w<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>inst✝³ : Nontrivial R<VAR>inst✝² : NoZeroSMulDivisors R M<VAR>inst✝¹ : Nontrivial R<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>S : Submodule R M<VAR>h : S = ⊥<GOAL>Module.rank R ↥S = 0
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_2<VAR>π : ι → Type u_3<VAR>r : α → α → Prop<VAR>inst✝ : Preorder α<VAR>f : ℕ → α<VAR>hf : Antitone f<VAR>n a : ℕ<VAR>h1 : f (n + 1) < f a<VAR>h2 : f a < f n<GOAL>False
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝² : PseudoEMetricSpace α<VAR>inst✝¹ : PseudoEMetricSpace β<VAR>inst✝ : PseudoEMetricSpace γ<VAR>K : ℝ≥0<VAR>s✝ : Set α<VAR>f✝ : α → β<VAR>f : α → β → γ<VAR>K₁ K₂ : ℝ≥0<VAR>s : Set α<VAR>t : Set β<VAR>hf₁ : ∀ b ∈ t, LipschitzOnWith K₁ (fun x => f x b) s<VAR>hf₂ : ∀ a ∈ s, LipschitzOnWith K₂ (f a) t<GOAL>EMetric.diam (image2 f s t) ≤ ↑K₁ * EMetric.diam s + ↑K₂ * EMetric.diam t
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝² : PseudoEMetricSpace α<VAR>inst✝¹ : PseudoEMetricSpace β<VAR>inst✝ : PseudoEMetricSpace γ<VAR>K : ℝ≥0<VAR>s✝ : Set α<VAR>f✝ : α → β<VAR>f : α → β → γ<VAR>K₁ K₂ : ℝ≥0<VAR>s : Set α<VAR>t : Set β<VAR>hf₁ : ∀ b ∈ t, LipschitzOnWith K₁ (fun x => f x b) s<VAR>hf₂ : ∀ a ∈ s, LipschitzOnWith K₂ (f a) t<GOAL>∀ x ∈ s, ∀ y ∈ t, ∀ x_1 ∈ s, ∀ y_1 ∈ t, edist (f x y) (f x_1 y_1) ≤ ↑K₁ * EMetric.diam s + ↑K₂ * EMetric.diam t
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝² : PseudoEMetricSpace α<VAR>inst✝¹ : PseudoEMetricSpace β<VAR>inst✝ : PseudoEMetricSpace γ<VAR>K : ℝ≥0<VAR>s✝ : Set α<VAR>f✝ : α → β<VAR>f : α → β → γ<VAR>K₁ K₂ : ℝ≥0<VAR>s : Set α<VAR>t : Set β<VAR>hf₁ : ∀ b ∈ t, LipschitzOnWith K₁ (fun x => f x b) s<VAR>hf₂ : ∀ a ∈ s, LipschitzOnWith K₂ (f a) t<VAR>a₁ : α<VAR>ha₁ : a₁ ∈ s<VAR>b₁ : β<VAR>hb₁ : b₁ ∈ t<VAR>a₂ : α<VAR>ha₂ : a₂ ∈ s<VAR>b₂ : β<VAR>hb₂ : b₂ ∈ t<GOAL>edist (f a₁ b₁) (f a₂ b₂) ≤ ↑K₁ * EMetric.diam s + ↑K₂ * EMetric.diam t
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝² : PseudoEMetricSpace α<VAR>inst✝¹ : PseudoEMetricSpace β<VAR>inst✝ : PseudoEMetricSpace γ<VAR>K : ℝ≥0<VAR>s✝ : Set α<VAR>f✝ : α → β<VAR>f : α → β → γ<VAR>K₁ K₂ : ℝ≥0<VAR>s : Set α<VAR>t : Set β<VAR>hf₁ : ∀ b ∈ t, LipschitzOnWith K₁ (fun x => f x b) s<VAR>hf₂ : ∀ a ∈ s, LipschitzOnWith K₂ (f a) t<VAR>a₁ : α<VAR>ha₁ : a₁ ∈ s<VAR>b₁ : β<VAR>hb₁ : b₁ ∈ t<VAR>a₂ : α<VAR>ha₂ : a₂ ∈ s<VAR>b₂ : β<VAR>hb₂ : b₂ ∈ t<GOAL>edist (f a₁ b₁) (f a₂ b₁) + edist (f a₂ b₁) (f a₂ b₂) ≤ ↑K₁ * EMetric.diam s + ↑K₂ * EMetric.diam t
<VAR>L : Language<VAR>T✝ : L.Theory<VAR>α : Type w<VAR>n : ℕ<VAR>T' T : L.Theory<VAR>h : T.IsFinitelySatisfiable<GOAL>T.IsSatisfiable
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s✝ s₁ s₂ : Finset α<VAR>a : α<VAR>f✝ g : α → β<VAR>inst✝ : CommMonoid β<VAR>s : Finset α<VAR>f : α → β<VAR>this✝ : DecidableEq α<VAR>this : DecidableEq β<GOAL>∀ (g : (a : α) → a ∈ s → α), (∀ (a : α) (ha : a ∈ s), f a * f (g a ha) = 1) → (∀ (a : α) (ha : a ∈ s), f a ≠ 1 → g a ha ≠ a) → ∀ (g_mem : ∀ (a : α) (ha : a ∈ s), g a ha ∈ s), (∀ (a : α) (ha : a ∈ s), g (g a ha) ⋯ = a) → ∏ x ∈ s, f x = 1
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : SeminormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>x : E<GOAL>‖(inclusionInDoubleDual 𝕜 E) x‖ ≤ ‖x‖
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>A : Type u₂<VAR>inst✝² : Category.{v₂, u₂} A<VAR>A' : Type u₂<VAR>inst✝¹ : Category.{max v₁ u₁, u₂} A'<VAR>B : Type u₃<VAR>inst✝ : Category.{v₃, u₃} B<VAR>J : GrothendieckTopology C<VAR>U : C<VAR>R : Presieve U<VAR>P : Cᵒᵖ ⥤ A<VAR>P' : Cᵒᵖ ⥤ A'<VAR>h : ∀ (X : C) (S : J.Cover X), Nonempty (IsLimit (S.multifork P))<VAR>E : A<VAR>X : C<VAR>S : Sieve X<VAR>hS : S ∈ J.sieves X<VAR>x : Presieve.FamilyOfElements (P ⋙ coyoneda.obj (op E)) S.arrows<VAR>hx : x.Compatible<VAR>T : J.Cover X := ⟨S, hS⟩<VAR>hh : IsLimit (T.multifork P)<GOAL>∃! t, x.IsAmalgamation t
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>A : Type u₂<VAR>inst✝² : Category.{v₂, u₂} A<VAR>A' : Type u₂<VAR>inst✝¹ : Category.{max v₁ u₁, u₂} A'<VAR>B : Type u₃<VAR>inst✝ : Category.{v₃, u₃} B<VAR>J : GrothendieckTopology C<VAR>U : C<VAR>R : Presieve U<VAR>P : Cᵒᵖ ⥤ A<VAR>P' : Cᵒᵖ ⥤ A'<VAR>h : ∀ (X : C) (S : J.Cover X), Nonempty (IsLimit (S.multifork P))<VAR>E : A<VAR>X : C<VAR>S : Sieve X<VAR>hS : S ∈ J.sieves X<VAR>x : Presieve.FamilyOfElements (P ⋙ coyoneda.obj (op E)) S.arrows<VAR>hx : x.Compatible<VAR>T : J.Cover X := ⟨S, hS⟩<VAR>hh : IsLimit (T.multifork P)<VAR>K : Multifork (T.index P) := Multifork.ofι (T.index P) E (fun I => x I.f ⋯) ⋯<GOAL>∃! t, x.IsAmalgamation t