ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>E : Type u<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : E → ℝ<VAR>f' : E →L[ℝ] ℝ<VAR>s : Set E<VAR>a x y : E<VAR>h : [x-[ℝ]x + y] ⊆ s<VAR>t : ℝ<VAR>ht₁ : t ≤ 1<VAR>ht₀ : t ∈ Ioi 0<GOAL>x + t • y ∈ s
<VAR>E : Type u<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : E → ℝ<VAR>f' : E →L[ℝ] ℝ<VAR>s : Set E<VAR>a x y : E<VAR>h : [x-[ℝ]x + y] ⊆ s<VAR>t : ℝ<VAR>ht₁ : t ≤ 1<VAR>ht₀ : t ∈ Ioi 0<GOAL>x + t • y ∈ [x-[ℝ]x + y]
<VAR>E : Type u<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : E → ℝ<VAR>f' : E →L[ℝ] ℝ<VAR>s : Set E<VAR>a x y : E<VAR>h : [x-[ℝ]x + y] ⊆ s<VAR>t : ℝ<VAR>ht₁ : t ≤ 1<VAR>ht₀ : t ∈ Ioi 0<GOAL>x + t • y ∈ (fun θ => x + θ • y) '' Icc 0 1
<VAR>μ ν : YoungDiagram<VAR>h : μ.transpose ≤ ν.transpose<GOAL>μ ≤ ν
<VAR>μ ν : YoungDiagram<VAR>h : μ.transpose ≤ ν.transpose<GOAL>ν = ν.transpose.transpose
<VAR>μ ν : YoungDiagram<VAR>h : μ ≤ ν<GOAL>μ.transpose ≤ ν.transpose
<VAR>μ ν : YoungDiagram<VAR>h : μ.transpose.transpose ≤ ν<GOAL>μ.transpose ≤ ν.transpose
<VAR>E : ℕ → Type u_1<VAR>x y : (n : ℕ) → E n<GOAL>0 ≤ dist x y
<VAR>E : ℕ → Type u_1<VAR>x : (n : ℕ) → E n<GOAL>0 ≤ dist x x
<VAR>E : ℕ → Type u_1<VAR>x y : (n : ℕ) → E n<VAR>h : x ≠ y<GOAL>0 ≤ dist x y
<VAR>θ : Angle<GOAL>θ.toReal < 0 ↔ θ.sign = -1
<VAR>θ : Angle<GOAL>θ.toReal < 0 ↔ Real.sin θ.toReal < 0
<VAR>θ : Angle<VAR>h : θ.toReal < 0<GOAL>θ.toReal < 0 ↔ Real.sin θ.toReal < 0
<VAR>θ : Angle<VAR>h : θ.toReal = 0<GOAL>θ.toReal < 0 ↔ Real.sin θ.toReal < 0
<VAR>θ : Angle<VAR>h : 0 < θ.toReal<GOAL>θ.toReal < 0 ↔ Real.sin θ.toReal < 0
<VAR>α : Type u_1<VAR>inst✝ : HeytingAlgebra α<VAR>a b : α<VAR>ha : IsRegular a<VAR>hb : IsRegular b<GOAL>IsRegular (a ⇨ b)
<VAR>X Y : Scheme<VAR>U : X.Opens<VAR>hU : IsAffineOpen U<VAR>f : ↑Γ(X, U)<VAR>s : Set ↑Γ(X, U)<GOAL>U ≤ ⨆ f, X.basicOpen ↑f ↔ Ideal.span s = ⊤
<VAR>X Y : Scheme<VAR>U : X.Opens<VAR>hU : IsAffineOpen U<VAR>f : ↑Γ(X, U)<VAR>s : Set ↑Γ(X, U)<GOAL>U ≤ ⨆ f, X.basicOpen ↑f ↔ U = ⨆ f, X.basicOpen ↑f
<VAR>X Y : Scheme<VAR>U : X.Opens<VAR>hU : IsAffineOpen U<VAR>f : ↑Γ(X, U)<VAR>s : Set ↑Γ(X, U)<VAR>h : U ≤ ⨆ f, X.basicOpen ↑f<GOAL>⨆ f, X.basicOpen ↑f ≤ U
<VAR>X Y : Scheme<VAR>U : X.Opens<VAR>hU : IsAffineOpen U<VAR>f : ↑Γ(X, U)<VAR>s : Set ↑Γ(X, U)<VAR>h : U ≤ ⨆ f, X.basicOpen ↑f<GOAL>∀ x ∈ s, X.basicOpen x ≤ U
<VAR>X Y : Scheme<VAR>U : X.Opens<VAR>hU : IsAffineOpen U<VAR>f : ↑Γ(X, U)<VAR>s : Set ↑Γ(X, U)<VAR>h : U ≤ ⨆ f, X.basicOpen ↑f<VAR>x : ↑Γ(X, U)<VAR>h✝ : x ∈ s<GOAL>X.basicOpen x ≤ U
<VAR>R : Type u<VAR>S : Type v<VAR>A : Type w<VAR>B : Type u₁<VAR>M : Type v₁<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : CommSemiring S<VAR>inst✝⁸ : Semiring A<VAR>inst✝⁷ : Semiring B<VAR>inst✝⁶ : Algebra R S<VAR>inst✝⁵ : Algebra S A<VAR>inst✝⁴ : Algebra S B<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra R B<VAR>inst✝¹ : IsScalarTower R S A<VAR>inst✝ : IsScalarTower R S B<VAR>f : A →ₐ[S] B<VAR>r : R<GOAL>f ((algebraMap R A) r) = (algebraMap R B) r
<VAR>α : Type u<VAR>inst✝ : Monoid α<VAR>a b : α<VAR>x✝ : Invertible a<GOAL>⅟a * (a * b) = b
<VAR>d : ℕ<VAR>x y a b : ℤ<VAR>h₁ : ↑d ∣ x<VAR>h₂ : ↑d ∣ y<VAR>h₃ : x * a + y * b = ↑d<GOAL>x.gcd y = d
<VAR>d : ℕ<VAR>x y a b : ℤ<VAR>h₁ : ↑d ∣ x<VAR>h₂ : ↑d ∣ y<VAR>h₃ : x * a + y * b = ↑d<GOAL>x.gcd y ∣ d
<VAR>d : ℕ<VAR>x y a b : ℤ<VAR>h₁ : ↑d ∣ x<VAR>h₂ : ↑d ∣ y<VAR>h₃ : x * a + y * b = ↑d<GOAL>↑(x.gcd y) ∣ x * a + y * b
<VAR>d : ℕ<VAR>x y a b : ℤ<VAR>h₁ : ↑d ∣ x<VAR>h₂ : ↑d ∣ y<VAR>h₃ : x * a + y * b = ↑d<GOAL>↑(x.gcd y) ∣ x * a
<VAR>d : ℕ<VAR>x y a b : ℤ<VAR>h₁ : ↑d ∣ x<VAR>h₂ : ↑d ∣ y<VAR>h₃ : x * a + y * b = ↑d<GOAL>↑(x.gcd y) ∣ y * b
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Preadditive C<VAR>J : C<GOAL>Injective J ↔ (preadditiveYoneda.obj J).PreservesEpimorphisms
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Preadditive C<VAR>J : C<GOAL>(yoneda.obj J).PreservesEpimorphisms ↔ (preadditiveYoneda.obj J).PreservesEpimorphisms
<VAR>a b c : PartENat<VAR>hc : c ≠ ⊤<GOAL>a + c = b + c ↔ a = b
<VAR>a b : PartENat<VAR>c : ℕ<VAR>hc : ↑c ≠ ⊤<GOAL>a + ↑c = b + ↑c ↔ a = b
<VAR>a b : PartENat<VAR>c : ℕ<VAR>hc : ↑c ≠ ⊤<GOAL>∀ (n n_1 : ℕ), ↑n_1 + ↑c = ↑n + ↑c ↔ n_1 = n
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>inst✝⁹ : NontriviallyNormedField R<VAR>inst✝⁸ : (x : B) → AddCommMonoid (E x)<VAR>inst✝⁷ : (x : B) → Module R (E x)<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace R F<VAR>inst✝⁴ : TopologicalSpace B<VAR>inst✝³ : TopologicalSpace (TotalSpace F E)<VAR>inst✝² : (x : B) → TopologicalSpace (E x)<VAR>inst✝¹ : FiberBundle F E<VAR>e : Trivialization F TotalSpace.proj<VAR>inst✝ : Trivialization.IsLinear R e<VAR>b : B<VAR>hb : b ∈ e.baseSet<VAR>z : F<GOAL>↑e.symm (b, z) = { proj := b, snd := (continuousLinearEquivAt R e b hb).symm z }
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>inst✝⁹ : NontriviallyNormedField R<VAR>inst✝⁸ : (x : B) → AddCommMonoid (E x)<VAR>inst✝⁷ : (x : B) → Module R (E x)<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace R F<VAR>inst✝⁴ : TopologicalSpace B<VAR>inst✝³ : TopologicalSpace (TotalSpace F E)<VAR>inst✝² : (x : B) → TopologicalSpace (E x)<VAR>inst✝¹ : FiberBundle F E<VAR>e : Trivialization F TotalSpace.proj<VAR>inst✝ : Trivialization.IsLinear R e<VAR>b : B<VAR>hb : b ∈ e.baseSet<VAR>z : F<VAR>h : (b, z) ∈ e.target<GOAL>↑e.symm (b, z) = { proj := b, snd := (continuousLinearEquivAt R e b hb).symm z }
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>inst✝⁹ : NontriviallyNormedField R<VAR>inst✝⁸ : (x : B) → AddCommMonoid (E x)<VAR>inst✝⁷ : (x : B) → Module R (E x)<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace R F<VAR>inst✝⁴ : TopologicalSpace B<VAR>inst✝³ : TopologicalSpace (TotalSpace F E)<VAR>inst✝² : (x : B) → TopologicalSpace (E x)<VAR>inst✝¹ : FiberBundle F E<VAR>e : Trivialization F TotalSpace.proj<VAR>inst✝ : Trivialization.IsLinear R e<VAR>b : B<VAR>hb : b ∈ e.baseSet<VAR>z : F<VAR>h : (b, z) ∈ e.target<GOAL>{ proj := b, snd := (continuousLinearEquivAt R e b hb).symm z } ∈ e.source
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>inst✝⁹ : NontriviallyNormedField R<VAR>inst✝⁸ : (x : B) → AddCommMonoid (E x)<VAR>inst✝⁷ : (x : B) → Module R (E x)<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace R F<VAR>inst✝⁴ : TopologicalSpace B<VAR>inst✝³ : TopologicalSpace (TotalSpace F E)<VAR>inst✝² : (x : B) → TopologicalSpace (E x)<VAR>inst✝¹ : FiberBundle F E<VAR>e : Trivialization F TotalSpace.proj<VAR>inst✝ : Trivialization.IsLinear R e<VAR>b : B<VAR>hb : b ∈ e.baseSet<VAR>z : F<VAR>h : (b, z) ∈ e.target<GOAL>↑e.toPartialHomeomorph (↑e.symm (b, z)) = ↑e.toPartialHomeomorph { proj := b, snd := (continuousLinearEquivAt R e b hb).symm z }
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>inst✝² : Semiring k<VAR>inst✝¹ : DecidableEq G<VAR>inst✝ : Mul G<VAR>f : MonoidAlgebra k G<VAR>r : k<VAR>hr : ∀ (y : k), r * y = 0 ↔ y = 0<VAR>x : G<VAR>lx : IsLeftRegular x<GOAL>(single x r * f).support = image (fun x_1 => x * x_1) f.support
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>inst✝² : Semiring k<VAR>inst✝¹ : DecidableEq G<VAR>inst✝ : Mul G<VAR>f : MonoidAlgebra k G<VAR>r : k<VAR>hr : ∀ (y : k), r * y = 0 ↔ y = 0<VAR>x : G<VAR>lx : IsLeftRegular x<VAR>y : G<VAR>hy : y ∈ image (fun x_1 => x * x_1) f.support<GOAL>y ∈ (single x r * f).support
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>inst✝² : Semiring k<VAR>inst✝¹ : DecidableEq G<VAR>inst✝ : Mul G<VAR>f : MonoidAlgebra k G<VAR>r : k<VAR>hr : ∀ (y : k), r * y = 0 ↔ y = 0<VAR>x : G<VAR>lx : IsLeftRegular x<VAR>y : G<VAR>yf : y ∈ f.support<VAR>hy : x * y ∈ image (fun x_1 => x * x_1) f.support<GOAL>x * y ∈ (single x r * f).support
<VAR>l m r : List Char<VAR>c : Char<VAR>x✝ : Substring<VAR>h : ValidFor l m r x✝<GOAL>x✝.contains c = true ↔ c ∈ m
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>𝔹 : Type u_3<VAR>inst✝⁷ : RCLike 𝕂<VAR>inst✝⁶ : NormedRing 𝔸<VAR>inst✝⁵ : NormedAlgebra 𝕂 𝔸<VAR>inst✝⁴ : NormedRing 𝔹<VAR>inst✝³ : NormedAlgebra 𝕂 𝔹<VAR>inst✝² : CompleteSpace 𝔸<VAR>inst✝¹ : StarRing 𝔸<VAR>inst✝ : ContinuousStar 𝔸<VAR>x : 𝔸<VAR>h : x ∈ skewAdjoint 𝔸<GOAL>exp 𝕂 x ∈ unitary 𝔸
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>Z : Type u_5<VAR>inst✝¹ : TopologicalSpace B<VAR>inst✝ : TopologicalSpace F<VAR>proj : Z → B<VAR>e : Pretrivialization F proj<VAR>x : Z<GOAL>↑e.symm ⁻¹' (proj ⁻¹' e.baseSet) ∩ e.target = e.target
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>Z : Type u_5<VAR>inst✝¹ : TopologicalSpace B<VAR>inst✝ : TopologicalSpace F<VAR>proj : Z → B<VAR>e : Pretrivialization F proj<VAR>x✝ : Z<VAR>x : B × F<VAR>hx : x ∈ e.target<GOAL>x ∈ ↑e.symm ⁻¹' (proj ⁻¹' e.baseSet)
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>Z : Type u_5<VAR>inst✝¹ : TopologicalSpace B<VAR>inst✝ : TopologicalSpace F<VAR>proj : Z → B<VAR>e : Pretrivialization F proj<VAR>x✝ : Z<VAR>x : B × F<VAR>hx : x ∈ e.target<GOAL>x.1 ∈ e.baseSet
<VAR>R✝ : Type u<VAR>inst✝¹¹ : CommRing R✝<VAR>W✝ : Affine R✝<VAR>R : Type r<VAR>inst✝¹⁰ : CommRing R<VAR>W : Affine R<VAR>S : Type s<VAR>inst✝⁹ : CommRing S<VAR>inst✝⁸ : Algebra R S<VAR>A : Type u<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : Algebra S A<VAR>inst✝⁴ : IsScalarTower R S A<VAR>B : Type v<VAR>inst✝³ : CommRing B<VAR>inst✝² : Algebra R B<VAR>inst✝¹ : Algebra S B<VAR>inst✝ : IsScalarTower R S B<VAR>f : A →ₐ[S] B<VAR>x₁ x₂ y₁ L : A<GOAL>(baseChange W B).toAffine.addY (f x₁) (f x₂) (f y₁) (f L) = f ((baseChange W A).toAffine.addY x₁ x₂ y₁ L)
<VAR>R✝ : Type u<VAR>inst✝¹¹ : CommRing R✝<VAR>W✝ : Affine R✝<VAR>R : Type r<VAR>inst✝¹⁰ : CommRing R<VAR>W : Affine R<VAR>S : Type s<VAR>inst✝⁹ : CommRing S<VAR>inst✝⁸ : Algebra R S<VAR>A : Type u<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : Algebra S A<VAR>inst✝⁴ : IsScalarTower R S A<VAR>B : Type v<VAR>inst✝³ : CommRing B<VAR>inst✝² : Algebra R B<VAR>inst✝¹ : Algebra S B<VAR>inst✝ : IsScalarTower R S B<VAR>f : A →ₐ[S] B<VAR>x₁ x₂ y₁ L : A<GOAL>(baseChange W B).toAffine.addY (f x₁) (f x₂) (f y₁) (f L) = (baseChange W B).toAffine.addY (f.toRingHom x₁) (f.toRingHom x₂) (f.toRingHom y₁) (f.toRingHom L)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>k : Type u_3<VAR>V : Type u_4<VAR>P : Type u_5<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : AffineSpace V P<VAR>inst✝² : Ring k<VAR>inst✝¹ : Module k V<VAR>b : AffineBasis ι k P<VAR>s : Finset ι<VAR>i j : ι<VAR>e : ι ≃ ι'<VAR>inst✝ : Finite ι<VAR>q₁ q₂ : P<VAR>h : ∀ (i : ι), (b.coord i) q₁ = (b.coord i) q₂<GOAL>q₁ = q₂
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>k : Type u_3<VAR>V : Type u_4<VAR>P : Type u_5<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : AffineSpace V P<VAR>inst✝² : Ring k<VAR>inst✝¹ : Module k V<VAR>b : AffineBasis ι k P<VAR>s : Finset ι<VAR>i j : ι<VAR>e : ι ≃ ι'<VAR>inst✝ : Finite ι<VAR>q₁ q₂ : P<VAR>h : ∀ (i : ι), (b.coord i) q₁ = (b.coord i) q₂<VAR>val✝ : Fintype ι<GOAL>q₁ = q₂
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>k : Type u_3<VAR>V : Type u_4<VAR>P : Type u_5<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : AffineSpace V P<VAR>inst✝² : Ring k<VAR>inst✝¹ : Module k V<VAR>b : AffineBasis ι k P<VAR>s : Finset ι<VAR>i j : ι<VAR>e : ι ≃ ι'<VAR>inst✝ : Finite ι<VAR>q₁ q₂ : P<VAR>h : ∀ (i : ι), (b.coord i) q₁ = (b.coord i) q₂<VAR>val✝ : Fintype ι<GOAL>((Finset.affineCombination k Finset.univ ⇑b) fun i => (b.coord i) q₁) = (Finset.affineCombination k Finset.univ ⇑b) fun i => (b.coord i) q₂
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>t : ι → Set α<VAR>inst✝ : Countable ι<VAR>ht : ∀ (i : ι), (t i).Countable<VAR>this : ∀ (i : ι), Countable ↑(t i)<GOAL>(⋃ i, t i).Countable
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>t : ι → Set α<VAR>inst✝ : Countable ι<VAR>ht : ∀ (i : ι), (t i).Countable<VAR>this : ∀ (i : ι), Countable ↑(t i)<GOAL>(range fun a => ↑a.snd).Countable
<VAR>α : Type u_1<VAR>β : Type u_2<GOAL>Nat.card α = 0 ↔ IsEmpty α ∨ Infinite α
<VAR>α : Type u_1<VAR>inst✝ : Group α<VAR>s : Subgroup α<VAR>a : α<VAR>ha : a ∈ s<VAR>b : α<GOAL>b ∈ op a • ↑s ↔ b ∈ ↑s
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>p : R[X]<VAR>h : ¬p = 0<GOAL>p = C p.content * p.primPart
<VAR>ι : Sort u<VAR>α : Type v<VAR>β : Type w<VAR>inst✝ : LinearOrder α<VAR>a₁ a₂ b₁ b₂ x₁ x₂ y₁ y₂ : α<VAR>h : Disjoint (Ico x₁ x₂) (Ico y₁ y₂)<VAR>hx : x₁ < x₂<VAR>h2 : x₂ ∈ Ico y₁ y₂<GOAL>y₁ = x₂
<VAR>ι : Sort u<VAR>α : Type v<VAR>β : Type w<VAR>inst✝ : LinearOrder α<VAR>a₁ a₂ b₁ b₂ x₁ x₂ y₁ y₂ : α<VAR>h : x₂ ≤ x₁ ∨ x₂ ≤ y₁<VAR>hx : x₁ < x₂<VAR>h2 : x₂ ∈ Ico y₁ y₂<GOAL>y₁ = x₂
<VAR>ι : Sort u<VAR>α : Type v<VAR>β : Type w<VAR>inst✝ : LinearOrder α<VAR>a₁ a₂ b₁ b₂ x₁ x₂ y₁ y₂ : α<VAR>h : x₂ ≤ x₁ ∨ x₂ ≤ y₁<VAR>hx : x₁ < x₂<VAR>h2 : x₂ ∈ Ico y₁ y₂<GOAL>x₂ ≤ y₁
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : Ring R<VAR>inst✝ : Nontrivial R<GOAL>-1 = 1 ↔ ringChar R = 2
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : Ring R<VAR>inst✝ : Nontrivial R<VAR>h : -1 = 1<GOAL>ringChar R = 2
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : Ring R<VAR>inst✝ : Nontrivial R<VAR>h : ↑(1 + 1) = 0<GOAL>ringChar R = 2
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : OrderedRing R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>x z : P<VAR>t : R<VAR>ht : t ∈ Set.Icc 0 1<VAR>hyx : (lineMap x z) t ≠ x<VAR>hyz : (lineMap x z) t ≠ z<GOAL>(lineMap x z) t ∈ ⇑(lineMap x z) '' Set.Ioo 0 1
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : OrderedRing R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>x z : P<VAR>ht : 0 ∈ Set.Icc 0 1<VAR>hyx : (lineMap x z) 0 ≠ x<VAR>hyz : (lineMap x z) 0 ≠ z<GOAL>(lineMap x z) 0 ∈ ⇑(lineMap x z) '' Set.Ioo 0 1
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : OrderedRing R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>x z : P<VAR>ht : 1 ∈ Set.Icc 0 1<VAR>hyx : (lineMap x z) 1 ≠ x<VAR>hyz : (lineMap x z) 1 ≠ z<GOAL>(lineMap x z) 1 ∈ ⇑(lineMap x z) '' Set.Ioo 0 1
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : OrderedRing R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>x z : P<VAR>t : R<VAR>ht : t ∈ Set.Icc 0 1<VAR>hyx : (lineMap x z) t ≠ x<VAR>hyz : (lineMap x z) t ≠ z<VAR>ho : t ∈ Set.Ioo 0 1<GOAL>(lineMap x z) t ∈ ⇑(lineMap x z) '' Set.Ioo 0 1
<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>S✝ : L.Substructure M<VAR>s : Set M<VAR>φ : M →[L] N<VAR>S : L.Substructure M<VAR>n : ℕ<VAR>f : L.Functions n<VAR>x : Fin n → N<VAR>hx : ∀ (i : Fin n), x i ∈ ⇑φ '' ↑S<GOAL>φ (funMap f fun i => Classical.choose ⋯) = funMap f x
<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>S✝ : L.Substructure M<VAR>s : Set M<VAR>φ : M →[L] N<VAR>S : L.Substructure M<VAR>n : ℕ<VAR>f : L.Functions n<VAR>x : Fin n → N<VAR>hx : ∀ (i : Fin n), x i ∈ ⇑φ '' ↑S<GOAL>funMap f (⇑φ ∘ fun i => Classical.choose ⋯) = funMap f x
<VAR>α : Type u_1<VAR>t t₁ t₂ : TopologicalSpace α<VAR>s✝ : Set α<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : DiscreteTopology α<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : DiscreteTopology β<VAR>f : α → β<VAR>h : ∀ (b : β), IsOpen (f ⁻¹' {b})<VAR>s : Set β<VAR>x✝ : IsOpen s<GOAL>IsOpen (f ⁻¹' s)
<VAR>α : Type u_1<VAR>t t₁ t₂ : TopologicalSpace α<VAR>s✝ : Set α<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : DiscreteTopology α<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : DiscreteTopology β<VAR>f : α → β<VAR>h : ∀ (b : β), IsOpen (f ⁻¹' {b})<VAR>s : Set β<VAR>x✝ : IsOpen s<GOAL>IsOpen (⋃ i ∈ s, f ⁻¹' {i})
<VAR>α : Type u_1<VAR>a b c d : α<VAR>inst✝³ : MulZeroClass α<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : PosMulStrictMono α<VAR>inst✝ : MulPosStrictMono α<VAR>hab : a ≤ b<VAR>hcd : c ≤ d<VAR>b0 : 0 < b<VAR>c0 : 0 < c<VAR>h : a * c = b * d<GOAL>a = b ∧ c = d
<VAR>α : Type u_1<VAR>a b c d : α<VAR>inst✝³ : MulZeroClass α<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : PosMulStrictMono α<VAR>inst✝ : MulPosStrictMono α<VAR>hab : a ≤ b<VAR>hcd : c ≤ d<VAR>b0 : 0 < b<VAR>c0 : 0 < c<VAR>h : a * c = b * d<GOAL>¬a < b ∧ ¬c < d
<VAR>α : Type u_1<VAR>a b c d : α<VAR>inst✝³ : MulZeroClass α<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : PosMulStrictMono α<VAR>inst✝ : MulPosStrictMono α<VAR>hab✝ : a ≤ b<VAR>hcd : c ≤ d<VAR>b0 : 0 < b<VAR>c0 : 0 < c<VAR>h : a * c = b * d<VAR>hab : a < b<GOAL>a * c < b * d
<VAR>α : Type u_1<VAR>a b c d : α<VAR>inst✝³ : MulZeroClass α<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : PosMulStrictMono α<VAR>inst✝ : MulPosStrictMono α<VAR>hab : a ≤ b<VAR>hcd✝ : c ≤ d<VAR>b0 : 0 < b<VAR>c0 : 0 < c<VAR>h : a * c = b * d<VAR>hcd : c < d<GOAL>a * c < b * d
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>r : R<VAR>e : ℕ<VAR>n m : σ<VAR>s✝ : σ →₀ ℕ<VAR>inst✝ : CommSemiring R<VAR>p q : MvPolynomial σ R<VAR>ι : Type u_3<VAR>s : Finset ι<VAR>f : ι → MvPolynomial σ R<GOAL>(s.sum f).totalDegree ≤ s.sup fun i => (f i).totalDegree
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>r : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝ : CommSemiring R<VAR>p q : MvPolynomial σ R<VAR>ι : Type u_3<VAR>f : ι → MvPolynomial σ R<GOAL>(∅.sum f).totalDegree ≤ ∅.sup fun i => (f i).totalDegree
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>r : R<VAR>e : ℕ<VAR>n m : σ<VAR>s✝ : σ →₀ ℕ<VAR>inst✝ : CommSemiring R<VAR>p q : MvPolynomial σ R<VAR>ι : Type u_3<VAR>f : ι → MvPolynomial σ R<VAR>a : ι<VAR>s : Finset ι<VAR>has : a ∉ s<VAR>hind : (s.sum f).totalDegree ≤ s.sup fun i => (f i).totalDegree<GOAL>((Finset.cons a s has).sum f).totalDegree ≤ (Finset.cons a s has).sup fun i => (f i).totalDegree
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : Ring S<VAR>inst✝⁶ : Algebra R S<VAR>A : Type u_4<VAR>B : Type u_5<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing B<VAR>inst✝³ : IsDomain B<VAR>inst✝² : Algebra A B<VAR>K : Type u_6<VAR>inst✝¹ : Field K<VAR>inst✝ : StrongRankCondition R<VAR>pb : PowerBasis R S<GOAL>FiniteDimensional.finrank R S = pb.dim
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>R₂ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>M'' : Type u_8<VAR>V : Type u<VAR>V' : Type u_9<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>b b₁ : Basis ι R M<VAR>i : ι<VAR>c : R<VAR>x : M<GOAL>b.repr.symm (Finsupp.single i c) = b.repr.symm (c • Finsupp.single i 1)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>R₂ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>M'' : Type u_8<VAR>V : Type u<VAR>V' : Type u_9<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>b b₁ : Basis ι R M<VAR>i : ι<VAR>c : R<VAR>x : M<GOAL>b.repr.symm (c • Finsupp.single i 1) = c • b i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p : PMF α<VAR>s t : Set α<GOAL>p.toOuterMeasure s = 0 ↔ Disjoint p.support s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p : PMF α<VAR>s t : Set α<GOAL>(∀ (i : α), s.indicator (⇑p) i = 0) ↔ Disjoint p.support s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : Preorder β<VAR>a b : α<VAR>a' b' : β<VAR>h : ∀ {o : Ordering}, o.Compares a b → o.Compares a' b'<VAR>o : Ordering<VAR>ho : o.Compares a' b'<GOAL>o.Compares a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : Preorder β<VAR>a b : α<VAR>a' b' : β<VAR>h : ∀ {o : Ordering}, o.Compares a b → o.Compares a' b'<VAR>o : Ordering<VAR>ho : o.Compares a' b'<VAR>hab : a < b<GOAL>o.Compares a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : Preorder β<VAR>a b : α<VAR>a' b' : β<VAR>h : ∀ {o : Ordering}, o.Compares a b → o.Compares a' b'<VAR>o : Ordering<VAR>ho : o.Compares a' b'<VAR>hab : a = b ∨ b < a<GOAL>o.Compares a b
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : OrderedSemiring 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : AddCommMonoid F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>x y✝ z : E<VAR>s : Set E<VAR>hs : StarConvex 𝕜 x s<VAR>f : E →ₗ[𝕜] F<VAR>y : E<VAR>hy : y ∈ s<VAR>a b : 𝕜<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>hab : a + b = 1<GOAL>a • f x + b • f y ∈ ⇑f '' s
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : (i : ι) → DecidableEq (α i)<VAR>inst✝¹ : (i : ι) → CanonicallyOrderedAddCommMonoid (α i)<VAR>inst✝ : (i : ι) → LocallyFiniteOrder (α i)<VAR>f : Π₀ (i : ι), α i<GOAL>(Iio f).card = ∏ i ∈ f.support, (Iic (f i)).card - 1
<VAR>R : Type u<VAR>S : Type v<VAR>k : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Field R<VAR>p✝ q p : R[X]<VAR>hq : q.Monic<GOAL>p /ₘ q = C q.leadingCoeff⁻¹ * (p /ₘ (q * C q.leadingCoeff⁻¹))
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>W : MorphismProperty C<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>D' : Type u₃<VAR>inst✝² : Category.{v₃, u₃} D'<VAR>X Y Z T : C<VAR>inst✝¹ : HasSmallLocalizedHom W X Y<VAR>inst✝ : HasSmallLocalizedHom W Y Y<VAR>α : SmallHom W X Y<GOAL>(equiv W W.Q) (α.comp (mk W (𝟙 Y))) = (equiv W W.Q) α
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>m : ℕ<GOAL>padicNorm p ↑m = 1 ↔ ¬p ∣ m
<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>s : Submodule R M<VAR>h : 0 < Module.rank R ↥s<VAR>eq : s = ⊥<GOAL>False
<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>s : Submodule R M<VAR>h : 0 < 0<VAR>eq : s = ⊥<GOAL>False
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f : R[X]<VAR>N n : ℕ<GOAL>reflect N (X ^ n) = X ^ (revAt N) n
<VAR>M : Type u_1<VAR>S T : Set M<VAR>a b✝ c✝ : M<VAR>inst✝ : Mul M<VAR>h : IsMulCentral a<VAR>b c : M<GOAL>a * (b * c) = b * (a * c)
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedSemifield α<VAR>a : α<VAR>q : ℚ≥0<GOAL>0 ≤ ↑q
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedSemifield α<VAR>a : α<VAR>q : ℚ≥0<GOAL>0 ≤ ↑q.num / ↑q.den
<VAR>α✝ β α : Type u<GOAL>#(Option α) = #α + 1
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s✝ t✝ u : Multiset α<VAR>a b : α<VAR>s t : Multiset α<VAR>l₁ l₂ : List α<GOAL>⟦l₁⟧ - ⟦l₂⟧ = foldl erase ⋯ ⟦l₁⟧ ⟦l₂⟧
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s✝ t✝ u : Multiset α<VAR>a b : α<VAR>s t : Multiset α<VAR>l₁ l₂ : List α<GOAL>↑(l₁.diff l₂) = foldl erase ⋯ ↑l₁ ↑l₂
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s✝ t✝ u : Multiset α<VAR>a b : α<VAR>s t : Multiset α<VAR>l₁ l₂ : List α<GOAL>↑(List.foldl List.erase l₁ l₂) = foldl erase ⋯ ↑l₁ ↑l₂
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s✝ t✝ u : Multiset α<VAR>a b : α<VAR>s t : Multiset α<VAR>l₁ l₂ : List α<GOAL>foldl erase ⋯ ↑l₁ ↑l₂ = ↑(List.foldl List.erase l₁ l₂)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>ι : Type u_4<VAR>f : X → Y<VAR>g : Y → Z<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>hf : Inducing f<VAR>s : Set X<GOAL>𝓝ˢ s = comap f (𝓝ˢ (f '' s))
<VAR>n m d b : ℕ<VAR>hd : d ∈ (b + 1 + 1).digits m<GOAL>d < b + 1 + 1