ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>x y y₁ y₂ : PGame<VAR>hx : x.Numeric<VAR>hy✝ : y.Numeric<VAR>hy₁ : y₁.Numeric<VAR>hy₂ : y₂.Numeric<VAR>hy : y₁ < y₂<GOAL>∀ (x : PGame × PGame), (∀ (y : PGame × PGame), Prod.GameAdd IsOption IsOption y x → y.1.Numeric → y.2.Numeric → y.1 < y.2 → P3 y.1 y.2 y₁ y₂) → x.1.Numeric → x.2.Numeric → x.1 < x.2 → P3 x.1 x.2 y₁ y₂
<VAR>x y y₁ y₂ : PGame<VAR>hx✝ : x.Numeric<VAR>hy✝ : y.Numeric<VAR>hy₁ : y₁.Numeric<VAR>hy₂ : y₂.Numeric<VAR>hy : y₁ < y₂<VAR>x₁ x₂ : PGame<VAR>ih : ∀ (y : PGame × PGame), Prod.GameAdd IsOption IsOption y (x₁, x₂) → y.1.Numeric → y.2.Numeric → y.1 < y.2 → P3 y.1 y.2 y₁ y₂<VAR>hx₁ : (x₁, x₂).1.Numeric<VAR>hx₂ : (x₁, x₂).2.Numeric<VAR>hx : (x₁, x₂).1 < (x₁, x₂).2<GOAL>P3 (x₁, x₂).1 (x₁, x₂).2 y₁ y₂
<VAR>x y y₁ y₂ : PGame<VAR>hx✝ : x.Numeric<VAR>hy✝ : y.Numeric<VAR>hy₁ : y₁.Numeric<VAR>hy₂ : y₂.Numeric<VAR>hy : y₁ < y₂<VAR>x₁ x₂ : PGame<VAR>ih : ∀ (y : PGame × PGame), Prod.GameAdd IsOption IsOption y (x₁, x₂) → y.1.Numeric → y.2.Numeric → y.1 < y.2 → P3 y.1 y.2 y₁ y₂<VAR>hx₁ : (x₁, x₂).1.Numeric<VAR>hx₂ : (x₁, x₂).2.Numeric<VAR>hx : (x₁, x₂).1 < (x₁, x₂).2<VAR>i : (x₁, x₂).2.LeftMoves<GOAL>IH3 (x₁, x₂).1 ((x₁, x₂).2.moveLeft i) (x₁, x₂).2 y₁ y₂
<VAR>x y y₁ y₂ : PGame<VAR>hx✝ : x.Numeric<VAR>hy✝ : y.Numeric<VAR>hy₁ : y₁.Numeric<VAR>hy₂ : y₂.Numeric<VAR>hy : y₁ < y₂<VAR>x₁ x₂ : PGame<VAR>ih : ∀ (y : PGame × PGame), Prod.GameAdd IsOption IsOption y (x₁, x₂) → y.1.Numeric → y.2.Numeric → y.1 < y.2 → P3 y.1 y.2 y₁ y₂<VAR>hx₁ : (x₁, x₂).1.Numeric<VAR>hx₂ : (x₁, x₂).2.Numeric<VAR>hx : (x₁, x₂).1 < (x₁, x₂).2<VAR>i : (-(x₁, x₂).1).LeftMoves<GOAL>IH3 (-(x₁, x₂).2) ((-(x₁, x₂).1).moveLeft i) (-(x₁, x₂).1) y₁ y₂
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁶ : OrderedSemiring 𝕜<VAR>inst✝⁵ : AddCommMonoid E<VAR>inst✝⁴ : AddCommMonoid F<VAR>inst✝³ : LinearOrderedAddCommMonoid β<VAR>inst✝² : SMul 𝕜 E<VAR>inst✝¹ : Module 𝕜 β<VAR>inst✝ : OrderedSMul 𝕜 β<VAR>s : Set E<VAR>f g : E → β<VAR>hf : StrictConvexOn 𝕜 s f<VAR>hg : StrictConvexOn 𝕜 s g<VAR>x : E<VAR>hx : x ∈ s<VAR>y : E<VAR>hy : y ∈ s<VAR>hxy : x ≠ y<VAR>a b : 𝕜<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<GOAL>a • f x + b • f y ≤ a • (f x ⊔ g x) + b • (f y ⊔ g y)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁶ : OrderedSemiring 𝕜<VAR>inst✝⁵ : AddCommMonoid E<VAR>inst✝⁴ : AddCommMonoid F<VAR>inst✝³ : LinearOrderedAddCommMonoid β<VAR>inst✝² : SMul 𝕜 E<VAR>inst✝¹ : Module 𝕜 β<VAR>inst✝ : OrderedSMul 𝕜 β<VAR>s : Set E<VAR>f g : E → β<VAR>hf : StrictConvexOn 𝕜 s f<VAR>hg : StrictConvexOn 𝕜 s g<VAR>x : E<VAR>hx : x ∈ s<VAR>y : E<VAR>hy : y ∈ s<VAR>hxy : x ≠ y<VAR>a b : 𝕜<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<GOAL>a • g x + b • g y ≤ a • (f x ⊔ g x) + b • (f y ⊔ g y)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : C<VAR>S✝ R✝ : Sieve X<VAR>J : GrothendieckTopology C<VAR>f : Y ⟶ X<VAR>S R : Sieve X<VAR>h : J.Covers S f<VAR>k : ∀ {Z : C} (g : Z ⟶ X), S.arrows g → J.Covers R g<GOAL>J.Covers R f
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : C<VAR>S✝ R✝ : Sieve X<VAR>J : GrothendieckTopology C<VAR>f : Y ⟶ X<VAR>S R : Sieve X<VAR>h : J.Covers S f<VAR>k : ∀ {Z : C} (g : Z ⟶ X), S.arrows g → J.Covers R g<GOAL>∀ ⦃Y_1 : C⦄ ⦃f_1 : Y_1 ⟶ Y⦄, (Sieve.pullback f S).arrows f_1 → Sieve.pullback f_1 (Sieve.pullback f R) ∈ J.sieves Y_1
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : C<VAR>S✝ R✝ : Sieve X<VAR>J : GrothendieckTopology C<VAR>f : Y ⟶ X<VAR>S R : Sieve X<VAR>h : J.Covers S f<VAR>k : ∀ {Z : C} (g : Z ⟶ X), S.arrows g → J.Covers R g<VAR>Z : C<VAR>g : Z ⟶ Y<VAR>hg : (Sieve.pullback f S).arrows g<GOAL>Sieve.pullback g (Sieve.pullback f R) ∈ J.sieves Z
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : C<VAR>S✝ R✝ : Sieve X<VAR>J : GrothendieckTopology C<VAR>f : Y ⟶ X<VAR>S R : Sieve X<VAR>h : J.Covers S f<VAR>k : ∀ {Z : C} (g : Z ⟶ X), S.arrows g → J.Covers R g<VAR>Z : C<VAR>g : Z ⟶ Y<VAR>hg : (Sieve.pullback f S).arrows g<GOAL>Sieve.pullback (g ≫ f) R ∈ J.sieves Z
<VAR>k : Type u_1<VAR>E : Type u_2<VAR>PE : Type u_3<VAR>inst✝³ : OrderedRing k<VAR>inst✝² : OrderedAddCommGroup E<VAR>inst✝¹ : Module k E<VAR>inst✝ : OrderedSMul k E<VAR>a a' b b' : E<VAR>r r' : k<VAR>h : 0 < r<GOAL>a < (lineMap a b) r ↔ (lineMap a b) 0 < (lineMap a b) r
<VAR>R : Type u<VAR>inst✝⁴ : Ring R<VAR>ι : Type v<VAR>inst✝³ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝² : Nonempty ι<VAR>inst✝¹ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>inst✝ : (i : ι) → Field (G i)<VAR>f : (i j : ι) → i ≤ j → G i → G j<VAR>f' : (i j : ι) → i ≤ j → G i →+* G j<VAR>p : Ring.DirectLimit G f<VAR>hp : p ≠ 0<GOAL>inv G f p * p = 1
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁸ : _root_.RCLike 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : InnerProductSpace 𝕜 E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : InnerProductSpace ℝ F<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>ι'' : Type u_6<VAR>E' : Type u_7<VAR>inst✝³ : NormedAddCommGroup E'<VAR>inst✝² : InnerProductSpace 𝕜 E'<VAR>E'' : Type u_8<VAR>inst✝¹ : NormedAddCommGroup E''<VAR>inst✝ : InnerProductSpace 𝕜 E''<VAR>v : ι → E<VAR>hv : Orthonormal 𝕜 v<VAR>f : E →ₗᵢ[𝕜] E'<GOAL>Orthonormal 𝕜 (⇑f ∘ v)
<VAR>R M : Type u<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Flat R M<VAR>P : Type u<VAR>inst✝² : AddCommGroup P<VAR>inst✝¹ : Module R P<VAR>inst✝ : FinitePresentation R P<VAR>h₁ : P →ₗ[R] M<GOAL>∃ κ x h₂ h₃, h₁ = h₃ ∘ₗ h₂
<VAR>R M : Type u<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Flat R M<VAR>P : Type u<VAR>inst✝² : AddCommGroup P<VAR>inst✝¹ : Module R P<VAR>inst✝ : FinitePresentation R P<VAR>h₁ : P →ₗ[R] M<VAR>L : Type u<VAR>w✝¹ : AddCommGroup L<VAR>w✝ : Module R L<VAR>K : Submodule R L<VAR>ϕ : P ≃ₗ[R] L ⧸ K<VAR>left✝¹ : Free R L<VAR>left✝ : Finite R L<VAR>hK : K.FG<GOAL>∃ κ x h₂ h₃, h₁ = h₃ ∘ₗ h₂
<VAR>R M : Type u<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Flat R M<VAR>P : Type u<VAR>inst✝² : AddCommGroup P<VAR>inst✝¹ : Module R P<VAR>inst✝ : FinitePresentation R P<VAR>h₁ : P →ₗ[R] M<VAR>L : Type u<VAR>w✝¹ : AddCommGroup L<VAR>w✝ : Module R L<VAR>K : Submodule R L<VAR>ϕ : P ≃ₗ[R] L ⧸ K<VAR>left✝¹ : Free R L<VAR>left✝ : Finite R L<VAR>hK : K.FG<VAR>this : Finite R ↥K<GOAL>∃ κ x h₂ h₃, h₁ = h₃ ∘ₗ h₂
<VAR>R M : Type u<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Flat R M<VAR>P : Type u<VAR>inst✝² : AddCommGroup P<VAR>inst✝¹ : Module R P<VAR>inst✝ : FinitePresentation R P<VAR>h₁ : P →ₗ[R] M<VAR>L : Type u<VAR>w✝¹ : AddCommGroup L<VAR>w✝ : Module R L<VAR>K : Submodule R L<VAR>ϕ : P ≃ₗ[R] L ⧸ K<VAR>left✝¹ : Free R L<VAR>left✝ : Finite R L<VAR>hK : K.FG<VAR>this✝ : Finite R ↥K<VAR>this : (h₁ ∘ₗ ↑ϕ.symm ∘ₗ K.mkQ) ∘ₗ K.subtype = 0<GOAL>∃ κ x h₂ h₃, h₁ = h₃ ∘ₗ h₂
<VAR>R M : Type u<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Flat R M<VAR>P : Type u<VAR>inst✝² : AddCommGroup P<VAR>inst✝¹ : Module R P<VAR>inst✝ : FinitePresentation R P<VAR>h₁ : P →ₗ[R] M<VAR>L : Type u<VAR>w✝¹ : AddCommGroup L<VAR>w✝ : Module R L<VAR>K : Submodule R L<VAR>ϕ : P ≃ₗ[R] L ⧸ K<VAR>left✝¹ : Free R L<VAR>left✝ : Finite R L<VAR>hK : K.FG<VAR>this✝ : Finite R ↥K<VAR>this : (h₁ ∘ₗ ↑ϕ.symm ∘ₗ K.mkQ) ∘ₗ K.subtype = 0<VAR>κ : Type u<VAR>hκ : Fintype κ<VAR>a : L →ₗ[R] κ →₀ R<VAR>y : (κ →₀ R) →ₗ[R] M<VAR>hay : h₁ ∘ₗ ↑ϕ.symm ∘ₗ K.mkQ = y ∘ₗ a<VAR>ha : a ∘ₗ K.subtype = 0<GOAL>∃ κ x h₂ h₃, h₁ = h₃ ∘ₗ h₂
<VAR>R M : Type u<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Flat R M<VAR>P : Type u<VAR>inst✝² : AddCommGroup P<VAR>inst✝¹ : Module R P<VAR>inst✝ : FinitePresentation R P<VAR>h₁ : P →ₗ[R] M<VAR>L : Type u<VAR>w✝¹ : AddCommGroup L<VAR>w✝ : Module R L<VAR>K : Submodule R L<VAR>ϕ : P ≃ₗ[R] L ⧸ K<VAR>left✝¹ : Free R L<VAR>left✝ : Finite R L<VAR>hK : K.FG<VAR>this✝ : Finite R ↥K<VAR>this : (h₁ ∘ₗ ↑ϕ.symm ∘ₗ K.mkQ) ∘ₗ K.subtype = 0<VAR>κ : Type u<VAR>hκ : Fintype κ<VAR>a : L →ₗ[R] κ →₀ R<VAR>y : (κ →₀ R) →ₗ[R] M<VAR>hay : h₁ ∘ₗ ↑ϕ.symm ∘ₗ K.mkQ = y ∘ₗ a<VAR>ha : a ∘ₗ K.subtype = 0<GOAL>h₁ = y ∘ₗ K.liftQ a ⋯ ∘ₗ ↑ϕ
<VAR>R M : Type u<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Flat R M<VAR>P : Type u<VAR>inst✝² : AddCommGroup P<VAR>inst✝¹ : Module R P<VAR>inst✝ : FinitePresentation R P<VAR>h₁ : P →ₗ[R] M<VAR>L : Type u<VAR>w✝¹ : AddCommGroup L<VAR>w✝ : Module R L<VAR>K : Submodule R L<VAR>ϕ : P ≃ₗ[R] L ⧸ K<VAR>left✝¹ : Free R L<VAR>left✝ : Finite R L<VAR>hK : K.FG<VAR>this✝ : Finite R ↥K<VAR>this : (h₁ ∘ₗ ↑ϕ.symm ∘ₗ K.mkQ) ∘ₗ K.subtype = 0<VAR>κ : Type u<VAR>hκ : Fintype κ<VAR>a : L →ₗ[R] κ →₀ R<VAR>y : (κ →₀ R) →ₗ[R] M<VAR>hay : h₁ ∘ₗ ↑ϕ.symm ∘ₗ K.mkQ = y ∘ₗ a<VAR>ha : a ∘ₗ K.subtype = 0<GOAL>h₁ ∘ₗ ↑ϕ.symm = (y ∘ₗ K.liftQ a ⋯ ∘ₗ ↑ϕ) ∘ₗ ↑ϕ.symm
<VAR>R M : Type u<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Flat R M<VAR>P : Type u<VAR>inst✝² : AddCommGroup P<VAR>inst✝¹ : Module R P<VAR>inst✝ : FinitePresentation R P<VAR>h₁ : P →ₗ[R] M<VAR>L : Type u<VAR>w✝¹ : AddCommGroup L<VAR>w✝ : Module R L<VAR>K : Submodule R L<VAR>ϕ : P ≃ₗ[R] L ⧸ K<VAR>left✝¹ : Free R L<VAR>left✝ : Finite R L<VAR>hK : K.FG<VAR>this✝ : Finite R ↥K<VAR>this : (h₁ ∘ₗ ↑ϕ.symm ∘ₗ K.mkQ) ∘ₗ K.subtype = 0<VAR>κ : Type u<VAR>hκ : Fintype κ<VAR>a : L →ₗ[R] κ →₀ R<VAR>y : (κ →₀ R) →ₗ[R] M<VAR>hay : h₁ ∘ₗ ↑ϕ.symm ∘ₗ K.mkQ = y ∘ₗ a<VAR>ha : a ∘ₗ K.subtype = 0<GOAL>(h₁ ∘ₗ ↑ϕ.symm) ∘ₗ K.mkQ = ((y ∘ₗ K.liftQ a ⋯ ∘ₗ ↑ϕ) ∘ₗ ↑ϕ.symm) ∘ₗ K.mkQ
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : Ring α<VAR>inst✝¹ : IsDomain α<VAR>inst✝ : Ring β<VAR>f : β →+* α<VAR>hf : Injective ⇑f<GOAL>IsDomain β
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : Ring α<VAR>inst✝¹ : IsDomain α<VAR>inst✝ : Ring β<VAR>f : β →+* α<VAR>hf : Injective ⇑f<VAR>this : Nontrivial β<GOAL>IsDomain β
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : Ring α<VAR>inst✝¹ : IsDomain α<VAR>inst✝ : Ring β<VAR>f : β →+* α<VAR>hf : Injective ⇑f<VAR>this✝ : Nontrivial β<VAR>this : NoZeroDivisors α<GOAL>IsDomain β
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : Ring α<VAR>inst✝¹ : IsDomain α<VAR>inst✝ : Ring β<VAR>f : β →+* α<VAR>hf : Injective ⇑f<VAR>this✝¹ : Nontrivial β<VAR>this✝ : NoZeroDivisors α<VAR>this : NoZeroDivisors β<GOAL>IsDomain β
<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 : α<VAR>m : ℤ<GOAL>toIcoMod hp a (b - m • p) = toIcoMod hp a b
<VAR>R : Type u<VAR>ι : Type w<VAR>s : Finset ι<VAR>inst✝ : CommSemiring R<VAR>f : ι → R[X]<VAR>t : Multiset R[X]<GOAL>(Multiset.map (fun f => f.leadingCoeff) t).prod ≠ 0 → t.prod.natDegree = (Multiset.map (fun f => f.natDegree) t).sum
<VAR>R : Type u<VAR>ι : Type w<VAR>s : Finset ι<VAR>inst✝ : CommSemiring R<VAR>f : ι → R[X]<VAR>t : Multiset R[X]<GOAL>(Multiset.map (fun f => f.leadingCoeff) 0).prod ≠ 0 → (prod 0).natDegree = (Multiset.map (fun f => f.natDegree) 0).sum
<VAR>R : Type u<VAR>ι : Type w<VAR>s : Finset ι<VAR>inst✝ : CommSemiring R<VAR>f : ι → R[X]<VAR>t✝ : Multiset R[X]<VAR>a : R[X]<VAR>t : Multiset R[X]<VAR>ih : (Multiset.map (fun f => f.leadingCoeff) t).prod ≠ 0 → t.prod.natDegree = (Multiset.map (fun f => f.natDegree) t).sum<VAR>ht : (Multiset.map (fun f => f.leadingCoeff) (a ::ₘ t)).prod ≠ 0<GOAL>(a ::ₘ t).prod.natDegree = (Multiset.map (fun f => f.natDegree) (a ::ₘ t)).sum
<VAR>R : Type u<VAR>ι : Type w<VAR>s : Finset ι<VAR>inst✝ : CommSemiring R<VAR>f : ι → R[X]<VAR>t✝ : Multiset R[X]<VAR>a : R[X]<VAR>t : Multiset R[X]<VAR>ih : (Multiset.map (fun f => f.leadingCoeff) t).prod ≠ 0 → t.prod.natDegree = (Multiset.map (fun f => f.natDegree) t).sum<VAR>ht : a.leadingCoeff * (Multiset.map (fun f => f.leadingCoeff) t).prod ≠ 0<GOAL>(a * t.prod).natDegree = (a.natDegree ::ₘ Multiset.map (fun f => f.natDegree) t).sum
<VAR>R : Type u<VAR>ι : Type w<VAR>s : Finset ι<VAR>inst✝ : CommSemiring R<VAR>f : ι → R[X]<VAR>t✝ : Multiset R[X]<VAR>a : R[X]<VAR>t : Multiset R[X]<VAR>ih : (Multiset.map (fun f => f.leadingCoeff) t).prod ≠ 0 → t.prod.natDegree = (Multiset.map (fun f => f.natDegree) t).sum<VAR>ht : a.leadingCoeff * (Multiset.map (fun f => f.leadingCoeff) t).prod ≠ 0<GOAL>(Multiset.map (fun f => f.leadingCoeff) t).prod ≠ 0
<VAR>R : Type u<VAR>ι : Type w<VAR>s : Finset ι<VAR>inst✝ : CommSemiring R<VAR>f : ι → R[X]<VAR>t✝ : Multiset R[X]<VAR>a : R[X]<VAR>t : Multiset R[X]<VAR>ih : (Multiset.map (fun f => f.leadingCoeff) t).prod ≠ 0 → t.prod.natDegree = (Multiset.map (fun f => f.natDegree) t).sum<VAR>ht : a.leadingCoeff * (Multiset.map (fun f => f.leadingCoeff) t).prod ≠ 0<GOAL>a.leadingCoeff * t.prod.leadingCoeff ≠ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ η : Kernel α β<GOAL>κ = η ↔ ∀ (a : α) (s : Set β), MeasurableSet s → (κ a) s = (η a) s
<VAR>a b : Nat<GOAL>range (a + b) = range a ++ map (fun x => a + x) (range b)
<VAR>a b : Nat<GOAL>range (a + b) = range a ++ range' a b
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝ : LinearOrderedField 𝕜<VAR>x y z✝ z : 𝕜<VAR>hxz : x ≤ z<VAR>hyz : z ≤ y<VAR>h : x < y<GOAL>z ∈ [x-[𝕜]y]
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝ : LinearOrderedField 𝕜<VAR>x y z✝ z : 𝕜<VAR>hxz : 0 ≤ z - x<VAR>hyz : 0 ≤ y - z<VAR>h : x < y<GOAL>z ∈ [x-[𝕜]y]
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝ : LinearOrderedField 𝕜<VAR>x y z✝ z : 𝕜<VAR>hxz : 0 ≤ z - x<VAR>hyz : 0 ≤ y - z<VAR>h : 0 < y - x<GOAL>z ∈ [x-[𝕜]y]
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝ : LinearOrderedField 𝕜<VAR>x y z✝ z : 𝕜<VAR>hxz : 0 ≤ z - x<VAR>hyz : 0 ≤ y - z<VAR>h : 0 < y - x<GOAL>(y - z) / (y - x) + (z - x) / (y - x) = 1
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝ : LinearOrderedField 𝕜<VAR>x y z✝ z : 𝕜<VAR>hxz : 0 ≤ z - x<VAR>hyz : 0 ≤ y - z<VAR>h : 0 < y - x<GOAL>((y - z) / (y - x)) • x + ((z - x) / (y - x)) • y = z
<VAR>α✝ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝⁴ : LinearOrder α<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : CompactIccSpace α<GOAL>cocompact α ≤ atBot ⊔ atTop
<VAR>α✝ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝⁴ : LinearOrder α<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : CompactIccSpace α<VAR>s : Set α<VAR>hs : s ∈ atBot ⊔ atTop<VAR>h✝ : IsEmpty α<GOAL>∃ t, IsCompact t ∧ tᶜ ⊆ s
<VAR>α✝ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝⁴ : LinearOrder α<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : CompactIccSpace α<VAR>s : Set α<VAR>hs : s ∈ atBot ⊔ atTop<VAR>h✝ : Nonempty α<GOAL>∃ t, IsCompact t ∧ tᶜ ⊆ s
<VAR>R : Type u<VAR>inst✝³ : Semiring R<VAR>inst✝² : StrongRankCondition R<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Fintype β<VAR>f : (α → R) →ₗ[R] β → R<VAR>i : Injective ⇑f<VAR>P : (Fin (Fintype.card α) → R) ≃ₗ[R] α → R := LinearEquiv.funCongrLeft R R (Fintype.equivFin α)<VAR>Q : (Fin (Fintype.card β) → R) ≃ₗ[R] β → R := LinearEquiv.funCongrLeft R R (Fintype.equivFin β)<GOAL>Fintype.card α ≤ Fintype.card β
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝³ : Group G<VAR>inst✝² : Group G'<VAR>inst✝¹ : Group G''<VAR>A : Type u_4<VAR>inst✝ : AddGroup A<VAR>s : Set G<VAR>x : G<GOAL>x ∈ conjugatesOfSet s ↔ ∃ a ∈ s, IsConj a x
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝³ : Group G<VAR>inst✝² : Group G'<VAR>inst✝¹ : Group G''<VAR>A : Type u_4<VAR>inst✝ : AddGroup A<VAR>s : Set G<VAR>x : G<GOAL>(∃ i, ∃ (_ : i ∈ s), x ∈ conjugatesOf i) ↔ ∃ a ∈ s, IsConj a x
<VAR>K R : Type v<VAR>V M : Type w<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>f : End R M<VAR>μ : R<VAR>m : M<GOAL>m ∈ f.maxGenEigenspace μ ↔ ∃ k, ((f - μ • 1) ^ k) m = 0
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>κ✝ η✝ : Kernel α γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>κ η : Kernel α γ<VAR>inst✝¹ : IsFiniteKernel κ<VAR>inst✝ : IsFiniteKernel η<GOAL>MeasurableSet {a | κ a ≪ η a}
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>κ✝ η✝ : Kernel α γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>κ η : Kernel α γ<VAR>inst✝¹ : IsFiniteKernel κ<VAR>inst✝ : IsFiniteKernel η<GOAL>MeasurableSet {a | (κ a) (κ.mutuallySingularSetSlice η a) = 0}
<VAR>V : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝³ : DecidableEq α<VAR>inst✝² : DecidableEq V<VAR>A : Matrix V V α<VAR>inst✝¹ : Zero α<VAR>inst✝ : One α<VAR>h : A.IsSymm<VAR>i✝ j✝ : V<GOAL>A.complᵀ i✝ j✝ = A.compl i✝ j✝
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝ : Group α<VAR>s t : Finset α<VAR>a b : α<GOAL>{b}.preimage (fun x => x * a) ⋯ = {b * a⁻¹}
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>f : ↥(Lp ℂ 2 haarAddCircle)<GOAL>∑' (i : ℤ), ‖fourierCoeff (↑↑f) i‖ ^ 2 = ∫ (t : AddCircle T), ‖↑↑f t‖ ^ 2 ∂haarAddCircle
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>f : ↥(Lp ℂ 2 haarAddCircle)<GOAL>∑' (i : ℤ), ‖↑(fourierBasis.repr f) i‖ ^ 2 = ∫ (t : AddCircle T), ‖↑↑f t‖ ^ 2 ∂haarAddCircle
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>f : ↥(Lp ℂ 2 haarAddCircle)<VAR>H₁ : ‖fourierBasis.repr f‖ ^ 2 = ∑' (i : ℤ), ‖↑(fourierBasis.repr f) i‖ ^ 2<GOAL>∑' (i : ℤ), ‖↑(fourierBasis.repr f) i‖ ^ 2 = ∫ (t : AddCircle T), ‖↑↑f t‖ ^ 2 ∂haarAddCircle
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>f : ↥(Lp ℂ 2 haarAddCircle)<VAR>H₁ : ‖fourierBasis.repr f‖ ^ 2 = ∑' (i : ℤ), ‖↑(fourierBasis.repr f) i‖ ^ 2<VAR>H₂ : ‖fourierBasis.repr f‖ ^ 2 = ‖f‖ ^ 2<GOAL>∑' (i : ℤ), ‖↑(fourierBasis.repr f) i‖ ^ 2 = ∫ (t : AddCircle T), ‖↑↑f t‖ ^ 2 ∂haarAddCircle
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>f : ↥(Lp ℂ 2 haarAddCircle)<VAR>H₁ : ‖fourierBasis.repr f‖ ^ 2 = ∑' (i : ℤ), ‖↑(fourierBasis.repr f) i‖ ^ 2<VAR>H₂ : ‖fourierBasis.repr f‖ ^ 2 = ‖f‖ ^ 2<VAR>H₃ : RCLike.re ⟪f, f⟫_ℂ = RCLike.re (∫ (a : AddCircle T), ⟪↑↑f a, ↑↑f a⟫_ℂ ∂haarAddCircle)<GOAL>∑' (i : ℤ), ‖↑(fourierBasis.repr f) i‖ ^ 2 = ∫ (t : AddCircle T), ‖↑↑f t‖ ^ 2 ∂haarAddCircle
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>f : ↥(Lp ℂ 2 haarAddCircle)<VAR>H₁ : ‖fourierBasis.repr f‖ ^ 2 = ∑' (i : ℤ), ‖↑(fourierBasis.repr f) i‖ ^ 2<VAR>H₂ : ‖fourierBasis.repr f‖ ^ 2 = ‖f‖ ^ 2<VAR>H₃ : RCLike.re ⟪f, f⟫_ℂ = ∫ (x : AddCircle T), RCLike.re ⟪↑↑f x, ↑↑f x⟫_ℂ ∂haarAddCircle<GOAL>∑' (i : ℤ), ‖↑(fourierBasis.repr f) i‖ ^ 2 = ∫ (t : AddCircle T), ‖↑↑f t‖ ^ 2 ∂haarAddCircle
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>f : ↥(Lp ℂ 2 haarAddCircle)<VAR>H₁ : ‖fourierBasis.repr f‖ ^ 2 = ∑' (i : ℤ), ‖↑(fourierBasis.repr f) i‖ ^ 2<VAR>H₂ : ‖fourierBasis.repr f‖ ^ 2 = ‖f‖ ^ 2<VAR>H₃ : RCLike.re ⟪f, f⟫_ℂ = RCLike.re (∫ (a : AddCircle T), ⟪↑↑f a, ↑↑f a⟫_ℂ ∂haarAddCircle)<GOAL>Integrable (fun a => ⟪↑↑f a, ↑↑f a⟫_ℂ) haarAddCircle
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝⁴ : CommMonoid M<VAR>inst✝³ : CommMonoid N<VAR>inst✝² : DivisionCommMonoid G<VAR>k✝ l : ℕ<VAR>inst✝¹ : CommRing R<VAR>ζ✝ : Rˣ<VAR>h✝ : IsPrimitiveRoot ζ✝ k✝<VAR>inst✝ : IsDomain R<VAR>k : ℕ+<VAR>ζ : Rˣ<VAR>h : IsPrimitiveRoot ζ ↑k<GOAL>Subgroup.zpowers ζ = rootsOfUnity k R
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝⁴ : CommMonoid M<VAR>inst✝³ : CommMonoid N<VAR>inst✝² : DivisionCommMonoid G<VAR>k✝ l : ℕ<VAR>inst✝¹ : CommRing R<VAR>ζ✝ : Rˣ<VAR>h✝ : IsPrimitiveRoot ζ✝ k✝<VAR>inst✝ : IsDomain R<VAR>k : ℕ+<VAR>ζ : Rˣ<VAR>h : IsPrimitiveRoot ζ ↑k<GOAL>↑(Subgroup.zpowers ζ) = ↑(rootsOfUnity k R)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F✝ : Type u_6<VAR>inst✝⁴ : CommMonoid M<VAR>inst✝³ : CommMonoid N<VAR>inst✝² : DivisionCommMonoid G<VAR>k✝ l : ℕ<VAR>inst✝¹ : CommRing R<VAR>ζ✝ : Rˣ<VAR>h✝ : IsPrimitiveRoot ζ✝ k✝<VAR>inst✝ : IsDomain R<VAR>k : ℕ+<VAR>ζ : Rˣ<VAR>h : IsPrimitiveRoot ζ ↑k<VAR>F : Fintype ↥(Subgroup.zpowers ζ)<GOAL>↑(Subgroup.zpowers ζ) = ↑(rootsOfUnity k R)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F✝ : Type u_6<VAR>inst✝⁴ : CommMonoid M<VAR>inst✝³ : CommMonoid N<VAR>inst✝² : DivisionCommMonoid G<VAR>k✝ l : ℕ<VAR>inst✝¹ : CommRing R<VAR>ζ✝ : Rˣ<VAR>h✝ : IsPrimitiveRoot ζ✝ k✝<VAR>inst✝ : IsDomain R<VAR>k : ℕ+<VAR>ζ : Rˣ<VAR>h : IsPrimitiveRoot ζ ↑k<VAR>F : Fintype ↥(Subgroup.zpowers ζ)<GOAL>Fintype.card ↑↑(rootsOfUnity k R) ≤ Fintype.card ↑↑(Subgroup.zpowers ζ)
<VAR>K : Type u_1<VAR>inst✝² : DecidableEq K<VAR>Γ : K → Type u_2<VAR>Λ : Type u_3<VAR>inst✝¹ : Inhabited Λ<VAR>σ : Type u_4<VAR>inst✝ : Inhabited σ<VAR>k : K<VAR>q : Stmt₂<VAR>v : σ<VAR>S : (k : K) → List (Γ k)<VAR>f : σ → Option (Γ k) → σ<GOAL>TM2.stepAux (stRun (StAct.peek f) q) v S = TM2.stepAux q (stVar v (S k) (StAct.peek f)) (update S k (match StAct.peek f with | StAct.push f => f v :: S k | StAct.peek a => S k | StAct.pop a => (S k).tail))
<VAR>K : Type u_1<VAR>inst✝² : DecidableEq K<VAR>Γ : K → Type u_2<VAR>Λ : Type u_3<VAR>inst✝¹ : Inhabited Λ<VAR>σ : Type u_4<VAR>inst✝ : Inhabited σ<VAR>k : K<VAR>q : Stmt₂<VAR>v : σ<VAR>S : (k : K) → List (Γ k)<VAR>f : σ → Option (Γ k) → σ<GOAL>TM2.stepAux (stRun (StAct.peek f) q) v S = TM2.stepAux q (stVar v (S k) (StAct.peek f)) S
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝ : LinearOrderedRing G<VAR>a x : G<VAR>h : |x| ≠ 1<GOAL>orderOf x = 0
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝ : LinearOrderedRing G<VAR>a x : G<VAR>h : |x| ≠ 1<GOAL>∀ (n : ℕ), 0 < n → x ^ n ≠ 1
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝ : LinearOrderedRing G<VAR>a x : G<VAR>h : |x| ≠ 1<VAR>n : ℕ<VAR>hn : 0 < n<VAR>hx : x ^ n = 1<GOAL>False
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝ : LinearOrderedRing G<VAR>a x : G<VAR>h : |x| ≠ 1<VAR>n : ℕ<VAR>hn : 0 < n<VAR>hx : |x| ^ n = 1<GOAL>False
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝ : LinearOrderedRing G<VAR>a x : G<VAR>h✝ : |x| ≠ 1<VAR>n : ℕ<VAR>hn : 0 < n<VAR>hx : |x| ^ n = 1<VAR>h : |x| < 1<GOAL>False
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝ : LinearOrderedRing G<VAR>a x : G<VAR>h✝ : |x| ≠ 1<VAR>n : ℕ<VAR>hn : 0 < n<VAR>hx : |x| ^ n = 1<VAR>h : 1 < |x|<GOAL>False
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>n i j : ℕ<VAR>hi : i ≤ n<VAR>hj : j < p ^ (n - i)<GOAL>j - v p ⟨j + 1, ⋯⟩ + n = i + j + (n - i - v p ⟨j + 1, ⋯⟩)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>n i j : ℕ<VAR>hi : i ≤ n<VAR>hj : j < p ^ (n - i)<VAR>m : ℕ<VAR>h : v p ⟨j + 1, ⋯⟩ = m<GOAL>j - m + n = i + j + (n - i - m)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>n i j : ℕ<VAR>hi : i ≤ n<VAR>hj : j < p ^ (n - i)<VAR>m : ℕ<VAR>h : v p ⟨j + 1, ⋯⟩ = m<GOAL>m ≤ n - i ∧ m ≤ j
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>n i j : ℕ<VAR>hi : i ≤ n<VAR>hj : j < p ^ (n - i)<VAR>m : ℕ<VAR>h : v p ⟨j + 1, ⋯⟩ = m<VAR>hle : p ^ m ≤ j + 1<GOAL>m ≤ n - i ∧ m ≤ j
<VAR>α : Type u<VAR>β : α → Type v<VAR>l✝ l₁ l₂ : List (Sigma β)<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>b : β a<VAR>l : List (Sigma β)<GOAL>(kreplace a b l).NodupKeys ↔ l.NodupKeys