ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>f✝¹ : ℝ → E<VAR>g'✝ g✝ φ : ℝ → ℝ<VAR>a b : ℝ<VAR>inst✝ : CompleteSpace E<VAR>f✝ f'✝ : ℝ → E<VAR>f f' g g' : ℝ → ℝ<VAR>hf : ∀ x ∈ [[a, b]], HasDerivAt f (f' x) x<VAR>hg : ∀ x ∈ [[a, b]], HasDerivAt g (g' (f x)) (f x)<VAR>hf' : ContinuousOn f' [[a, b]]<VAR>hg' : Continuous g'<GOAL>∫ (x : ℝ) in a..b, (g' ∘ f) x * f' x = (g ∘ f) b - (g ∘ f) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s t u : Set α<GOAL>borel ℝ = generateFrom (⋃ a, {Ici ↑a})
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s t u : Set α<GOAL>generateFrom (range fun a => Iio ↑a) = generateFrom (range fun a => Ici ↑a)
<VAR>R : Type u<VAR>R' : Type u'<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>inst✝⁹ : Ring R<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✝¹ : Module R' M'<VAR>inst✝ : Module R' M₁<VAR>i : ZeroHom R R'<VAR>j : M ≃+ M'<VAR>hi : Bijective ⇑i<VAR>hc : ∀ (r : R) (m : M), j (r • m) = i r • j m<VAR>x✝¹ : R<VAR>x✝ : i x✝¹ = 0<GOAL>i x✝¹ = i 0
<VAR>R : Type u<VAR>R' : Type u'<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>inst✝⁹ : Ring R<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✝¹ : Module R' M'<VAR>inst✝ : Module R' M₁<VAR>i : ZeroHom R R'<VAR>j : M ≃+ M'<VAR>hi : Bijective ⇑i<VAR>hc : ∀ (r : R) (m : M), j (r • m) = i r • j m<VAR>x✝¹ : R<VAR>x✝ : M'<GOAL>i x✝¹ • x✝ = j (x✝¹ • ↑j.symm x✝)
<VAR>R : Type u_1<VAR>inst✝¹⁶ : CommSemiring R<VAR>R' : Type u_2<VAR>inst✝¹⁵ : Monoid R'<VAR>R'' : Type u_3<VAR>inst✝¹⁴ : Semiring R''<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>S : Type u_8<VAR>T : Type u_9<VAR>inst✝¹³ : AddCommMonoid M<VAR>inst✝¹² : AddCommMonoid N<VAR>inst✝¹¹ : AddCommMonoid P<VAR>inst✝¹⁰ : AddCommMonoid Q<VAR>inst✝⁹ : AddCommMonoid S<VAR>inst✝⁸ : AddCommMonoid T<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R N<VAR>inst✝⁵ : Module R P<VAR>inst✝⁴ : Module R Q<VAR>inst✝³ : Module R S<VAR>inst✝² : Module R T<VAR>inst✝¹ : DistribMulAction R' M<VAR>inst✝ : Module R'' M<VAR>g : P →ₗ[R] Q<VAR>f : N →ₗ[R] P<GOAL>Function.Bijective ⇑(lTensor M f) ↔ Function.Bijective ⇑(rTensor M f)
<VAR>p q : ℤ[X]<VAR>k m n : ℕ<VAR>hkm : k < m<VAR>hmn : m < n<VAR>u v w : ℤˣ<VAR>hp : p = trinomial k m n ↑u ↑v ↑w<GOAL>C ↑v * (C ↑u * X ^ (m + n) + C ↑w * X ^ (n - m + k + n)) = { toFinsupp := Finsupp.filter (fun x => x ∈ Set.Ioo (k + n) (n + n)) (p * p.mirror).toFinsupp }
<VAR>p q : ℤ[X]<VAR>k m n : ℕ<VAR>hkm : k < m<VAR>hmn : m < n<VAR>u v w : ℤˣ<VAR>hp : p = trinomial k m n ↑u ↑v ↑w<VAR>key : n - m + k < n<GOAL>C ↑v * (C ↑u * X ^ (m + n) + C ↑w * X ^ (n - m + k + n)) = { toFinsupp := Finsupp.filter (fun x => x ∈ Set.Ioo (k + n) (n + n)) (p * p.mirror).toFinsupp }
<VAR>p q : ℤ[X]<VAR>k m n : ℕ<VAR>hkm : k < m<VAR>hmn : m < n<VAR>u v w : ℤˣ<VAR>hp : p = trinomial k m n ↑u ↑v ↑w<VAR>key : n - m + k < n<GOAL>C ↑v * (C ↑u * X ^ (m + n) + C ↑w * X ^ (n - m + k + n)) = { toFinsupp := Finsupp.filter (fun x => x ∈ Set.Ioo (k + n) (n + n)) (trinomial k m n ↑u ↑v ↑w * trinomial k (n - m + k) n ↑w ↑v ↑u).toFinsupp }
<VAR>p q : ℤ[X]<VAR>k m n : ℕ<VAR>hkm : k < m<VAR>hmn : m < n<VAR>u v w : ℤˣ<VAR>hp : p = trinomial k m n ↑u ↑v ↑w<VAR>key : n - m + k < n<GOAL>C ↑v * (monomial (m + n)) ↑u + C ↑v * (monomial (n - m + k + n)) ↑w = { toFinsupp := Finsupp.filter (fun x => x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (k + k) (↑u * ↑w) + Finsupp.single (k + (n - m + k)) (↑u * ↑v) + Finsupp.single (k + n) (↑u * ↑u) + (Finsupp.single (m + k) (↑v * ↑w) + Finsupp.single (m + (n - m + k)) (↑v * ↑v) + Finsupp.single (m + n) (↑v * ↑u)) + (Finsupp.single (n + k) (↑w * ↑w) + Finsupp.single (n + (n - m + k)) (↑w * ↑v) + Finsupp.single (n + n) (↑w * ↑u))) }
<VAR>p q : ℤ[X]<VAR>k m n : ℕ<VAR>hkm : k < m<VAR>hmn : m < n<VAR>u v w : ℤˣ<VAR>hp : p = trinomial k m n ↑u ↑v ↑w<VAR>key : n - m + k < n<GOAL>C ↑v * (monomial (m + n)) ↑u + C ↑v * (monomial (n - m + k + n)) ↑w = { toFinsupp := Finsupp.filter (fun x => x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (k + k) (↑u * ↑w)) + Finsupp.filter (fun x => x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (k + (n - m + k)) (↑u * ↑v)) + Finsupp.filter (fun x => x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (k + n) (↑u * ↑u)) + (Finsupp.filter (fun x => x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (m + k) (↑v * ↑w)) + Finsupp.filter (fun x => x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (m + (n - m + k)) (↑v * ↑v)) + Finsupp.filter (fun x => x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (m + n) (↑v * ↑u))) + (Finsupp.filter (fun x => x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (n + k) (↑w * ↑w)) + Finsupp.filter (fun x => x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (n + (n - m + k)) (↑w * ↑v)) + Finsupp.filter (fun x => x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (n + n) (↑w * ↑u))) }
<VAR>p q : ℤ[X]<VAR>k m n : ℕ<VAR>hkm : k < m<VAR>hmn : m < n<VAR>u v w : ℤˣ<VAR>hp : p = trinomial k m n ↑u ↑v ↑w<VAR>key : n - m + k < n<GOAL>C ↑v * (monomial (m + n)) ↑u + C ↑v * (monomial (n - m + k + n)) ↑w = { toFinsupp := 0 + 0 + 0 + (0 + 0 + Finsupp.single (m + n) (↑v * ↑u)) + (0 + Finsupp.single (n + (n - m + k)) (↑w * ↑v) + 0) }
<VAR>p q : ℤ[X]<VAR>k m n : ℕ<VAR>hkm : k < m<VAR>hmn : m < n<VAR>u v w : ℤˣ<VAR>hp : p = trinomial k m n ↑u ↑v ↑w<VAR>key : n - m + k < n<GOAL>n + n ∉ Set.Ioo (k + n) (n + n)
<VAR>p q : ℤ[X]<VAR>k m n : ℕ<VAR>hkm : k < m<VAR>hmn : m < n<VAR>u v w : ℤˣ<VAR>hp : p = trinomial k m n ↑u ↑v ↑w<VAR>key : n - m + k < n<GOAL>n + (n - m + k) ∈ Set.Ioo (k + n) (n + n)
<VAR>p q : ℤ[X]<VAR>k m n : ℕ<VAR>hkm : k < m<VAR>hmn : m < n<VAR>u v w : ℤˣ<VAR>hp : p = trinomial k m n ↑u ↑v ↑w<VAR>key : n - m + k < n<GOAL>n + k ∉ Set.Ioo (k + n) (n + n)
<VAR>p q : ℤ[X]<VAR>k m n : ℕ<VAR>hkm : k < m<VAR>hmn : m < n<VAR>u v w : ℤˣ<VAR>hp : p = trinomial k m n ↑u ↑v ↑w<VAR>key : n - m + k < n<GOAL>m + n ∈ Set.Ioo (k + n) (n + n)
<VAR>p q : ℤ[X]<VAR>k m n : ℕ<VAR>hkm : k < m<VAR>hmn : m < n<VAR>u v w : ℤˣ<VAR>hp : p = trinomial k m n ↑u ↑v ↑w<VAR>key : n - m + k < n<GOAL>m + (n - m + k) ∉ Set.Ioo (k + n) (n + n)
<VAR>p q : ℤ[X]<VAR>k m n : ℕ<VAR>hkm : k < m<VAR>hmn : m < n<VAR>u v w : ℤˣ<VAR>hp : p = trinomial k m n ↑u ↑v ↑w<VAR>key : n - m + k < n<GOAL>m + k ∉ Set.Ioo (k + n) (n + n)
<VAR>p q : ℤ[X]<VAR>k m n : ℕ<VAR>hkm : k < m<VAR>hmn : m < n<VAR>u v w : ℤˣ<VAR>hp : p = trinomial k m n ↑u ↑v ↑w<VAR>key : n - m + k < n<GOAL>k + n ∉ Set.Ioo (k + n) (n + n)
<VAR>p q : ℤ[X]<VAR>k m n : ℕ<VAR>hkm : k < m<VAR>hmn : m < n<VAR>u v w : ℤˣ<VAR>hp : p = trinomial k m n ↑u ↑v ↑w<VAR>key : n - m + k < n<GOAL>k + (n - m + k) ∉ Set.Ioo (k + n) (n + n)
<VAR>p q : ℤ[X]<VAR>k m n : ℕ<VAR>hkm : k < m<VAR>hmn : m < n<VAR>u v w : ℤˣ<VAR>hp : p = trinomial k m n ↑u ↑v ↑w<VAR>key : n - m + k < n<GOAL>k + k ∉ Set.Ioo (k + n) (n + n)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : C<VAR>S R : Sieve X<VAR>J : GrothendieckTopology C<VAR>rj : R ∈ J.sieves X<VAR>sj : S ∈ J.sieves X<GOAL>R ⊓ S ∈ J.sieves X
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : C<VAR>S R : Sieve X<VAR>J : GrothendieckTopology C<VAR>rj : R ∈ J.sieves X<VAR>sj : S ∈ J.sieves X<GOAL>∀ (Y : C) (f : Y ⟶ X), R.arrows f → Sieve.pullback f (R ⊓ S) ∈ J.sieves 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>rj : R ∈ J.sieves X<VAR>sj : S ∈ J.sieves X<VAR>Y : C<VAR>f : Y ⟶ X<VAR>hf : R.arrows f<GOAL>Sieve.pullback f (R ⊓ S) ∈ J.sieves 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>rj : R ∈ J.sieves X<VAR>sj : S ∈ J.sieves X<VAR>Y : C<VAR>f : Y ⟶ X<VAR>hf : R.arrows f<GOAL>⊤ ⊓ Sieve.pullback f S ∈ J.sieves Y
<VAR>n : ℕ<VAR>i : Fin (n + 2)<VAR>j : Fin (n + 1)<VAR>H : i ≤ j.castSucc<VAR>k : Fin ([n + 1].len + 1)<GOAL>j.succ.predAbove (i.castSucc.succAbove k) = i.succAbove (j.predAbove k)
<VAR>n : ℕ<VAR>i : Fin (n + 2)<VAR>j : Fin (n + 1)<VAR>H : i ≤ j.castSucc<VAR>k : Fin ([n + 1].len + 1)<VAR>hik : i ≤ k<GOAL>j.succ.predAbove (i.castSucc.succAbove k) = i.succAbove (j.predAbove k)
<VAR>n : ℕ<VAR>i : Fin (n + 2)<VAR>j : Fin (n + 1)<VAR>H : i ≤ j.castSucc<VAR>k : Fin ([n + 1].len + 1)<VAR>hik : k < i<GOAL>j.succ.predAbove (i.castSucc.succAbove k) = i.succAbove (j.predAbove k)
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : NonPreadditiveAbelian C<VAR>X Y : C<VAR>a b : X ⟶ Y<GOAL>a + -b = a - b
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝ : ConditionallyCompleteLattice α<VAR>s : Finset α<VAR>hs : s.Nonempty<GOAL>s.sup' hs id = sSup ↑s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝² : PseudoEMetricSpace α<VAR>inst✝¹ : PseudoEMetricSpace β<VAR>inst✝ : PseudoEMetricSpace γ<VAR>K : ℝ≥0<VAR>f : α → β<VAR>hf : AntilipschitzWith K f<VAR>x y : α<GOAL>(↑K)⁻¹ * edist x y ≤ edist (f x) (f y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝² : PseudoEMetricSpace α<VAR>inst✝¹ : PseudoEMetricSpace β<VAR>inst✝ : PseudoEMetricSpace γ<VAR>K : ℝ≥0<VAR>f : α → β<VAR>hf : AntilipschitzWith K f<VAR>x y : α<GOAL>edist x y / ↑K ≤ edist (f x) (f y)
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v, u₁} C<VAR>D : Type u₂<VAR>inst✝² : Category.{v, u₂} D<VAR>S : D<VAR>T : C ⥤ D<VAR>inst✝¹ : HasLimits C<VAR>inst✝ : PreservesLimits T<VAR>A : StructuredArrow S T<VAR>P : { P // ∃ q, q ≫ T.map P.arrow = A.hom }<GOAL>↑((fun P => ⟨projectSubobject P, ⋯⟩) ((fun P => liftSubobject ↑P ⋯) P)) = ↑P
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v, u₁} C<VAR>D : Type u₂<VAR>inst✝² : Category.{v, u₂} D<VAR>S : D<VAR>T : C ⥤ D<VAR>inst✝¹ : HasLimits C<VAR>inst✝ : PreservesLimits T<VAR>A : StructuredArrow S T<GOAL>∀ {a b : Subobject A}, { toFun := fun P => ⟨projectSubobject P, ⋯⟩, invFun := fun P => liftSubobject ↑P ⋯, left_inv := ⋯, right_inv := ⋯ } a ≤ { toFun := fun P => ⟨projectSubobject P, ⋯⟩, invFun := fun P => liftSubobject ↑P ⋯, left_inv := ⋯, right_inv := ⋯ } b ↔ a ≤ b
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v, u₁} C<VAR>D : Type u₂<VAR>inst✝² : Category.{v, u₂} D<VAR>S : D<VAR>T : C ⥤ D<VAR>inst✝¹ : HasLimits C<VAR>inst✝ : PreservesLimits T<VAR>A : StructuredArrow S T<GOAL>∀ ⦃A_1 B : StructuredArrow S T⦄ (f : A_1 ⟶ A) (g : B ⟶ A) [inst : Mono f] [inst_1 : Mono g], { toFun := fun P => ⟨projectSubobject P, ⋯⟩, invFun := fun P => liftSubobject ↑P ⋯, left_inv := ⋯, right_inv := ⋯ } (Subobject.mk f) ≤ { toFun := fun P => ⟨projectSubobject P, ⋯⟩, invFun := fun P => liftSubobject ↑P ⋯, left_inv := ⋯, right_inv := ⋯ } (Subobject.mk g) ↔ Subobject.mk f ≤ Subobject.mk g
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v, u₁} C<VAR>D : Type u₂<VAR>inst✝² : Category.{v, u₂} D<VAR>S : D<VAR>T : C ⥤ D<VAR>inst✝¹ : HasLimits C<VAR>inst✝ : PreservesLimits T<VAR>A P Q : StructuredArrow S T<VAR>f : P ⟶ A<VAR>g : Q ⟶ A<VAR>hf : Mono f<VAR>hg : Mono g<GOAL>{ toFun := fun P => ⟨projectSubobject P, ⋯⟩, invFun := fun P => liftSubobject ↑P ⋯, left_inv := ⋯, right_inv := ⋯ } (Subobject.mk f) ≤ { toFun := fun P => ⟨projectSubobject P, ⋯⟩, invFun := fun P => liftSubobject ↑P ⋯, left_inv := ⋯, right_inv := ⋯ } (Subobject.mk g) ↔ Subobject.mk f ≤ Subobject.mk g
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v, u₁} C<VAR>D : Type u₂<VAR>inst✝² : Category.{v, u₂} D<VAR>S : D<VAR>T : C ⥤ D<VAR>inst✝¹ : HasLimits C<VAR>inst✝ : PreservesLimits T<VAR>A P Q : StructuredArrow S T<VAR>f : P ⟶ A<VAR>g : Q ⟶ A<VAR>hf : Mono f<VAR>hg : Mono g<VAR>h : { toFun := fun P => ⟨projectSubobject P, ⋯⟩, invFun := fun P => liftSubobject ↑P ⋯, left_inv := ⋯, right_inv := ⋯ } (Subobject.mk f) ≤ { toFun := fun P => ⟨projectSubobject P, ⋯⟩, invFun := fun P => liftSubobject ↑P ⋯, left_inv := ⋯, right_inv := ⋯ } (Subobject.mk g)<GOAL>P ⟶ Q
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v, u₁} C<VAR>D : Type u₂<VAR>inst✝² : Category.{v, u₂} D<VAR>S : D<VAR>T : C ⥤ D<VAR>inst✝¹ : HasLimits C<VAR>inst✝ : PreservesLimits T<VAR>A P Q : StructuredArrow S T<VAR>f : P ⟶ A<VAR>g : Q ⟶ A<VAR>hf : Mono f<VAR>hg : Mono g<VAR>h : { toFun := fun P => ⟨projectSubobject P, ⋯⟩, invFun := fun P => liftSubobject ↑P ⋯, left_inv := ⋯, right_inv := ⋯ } (Subobject.mk f) ≤ { toFun := fun P => ⟨projectSubobject P, ⋯⟩, invFun := fun P => liftSubobject ↑P ⋯, left_inv := ⋯, right_inv := ⋯ } (Subobject.mk g)<GOAL>?h.refine_1 ≫ g = f
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v, u₁} C<VAR>D : Type u₂<VAR>inst✝² : Category.{v, u₂} D<VAR>S : D<VAR>T : C ⥤ D<VAR>inst✝¹ : HasLimits C<VAR>inst✝ : PreservesLimits T<VAR>A P Q : StructuredArrow S T<VAR>f : P ⟶ A<VAR>g : Q ⟶ A<VAR>hf : Mono f<VAR>hg : Mono g<VAR>h : Subobject.mk f ≤ Subobject.mk g<GOAL>{ toFun := fun P => ⟨projectSubobject P, ⋯⟩, invFun := fun P => liftSubobject ↑P ⋯, left_inv := ⋯, right_inv := ⋯ } (Subobject.mk f) ≤ { toFun := fun P => ⟨projectSubobject P, ⋯⟩, invFun := fun P => liftSubobject ↑P ⋯, left_inv := ⋯, right_inv := ⋯ } (Subobject.mk g)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s t : Multiset α<VAR>a : α<GOAL>{a}.toFinset = {a}
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>m n : ℕ<VAR>ι : Type y<VAR>inst✝ : Semiring R<VAR>p : R[X]<VAR>h : p.Monic<VAR>q : R[X]<GOAL>q * p = 0 ↔ q = 0
<VAR>l✝ r : List Char<VAR>it : Iterator<VAR>n : Nat<VAR>a : Char<VAR>l : List Char<VAR>h : ValidFor (a :: l) r it<VAR>hn : n + 1 ≤ (a :: l).length<GOAL>ValidFor (List.drop (n + 1) (a :: l)) ((List.take (n + 1) (a :: l)).reverse ++ r) (it.prev.prevn n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>r : α → α → Prop<VAR>f g : Filter α<GOAL>IsCobounded r ⊤ ↔ Nonempty α
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : Module α ℝ<VAR>inst✝ : OrderedSMul α ℝ<VAR>a : α<VAR>ha : a ≤ 0<VAR>s : Set ℝ<GOAL>sSup (a • s) = a • sInf s
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : Module α ℝ<VAR>inst✝ : OrderedSMul α ℝ<VAR>a : α<VAR>ha : a ≤ 0<GOAL>sSup (a • ∅) = a • sInf ∅
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : Module α ℝ<VAR>inst✝ : OrderedSMul α ℝ<VAR>a : α<VAR>ha : a ≤ 0<VAR>s : Set ℝ<VAR>hs : s.Nonempty<GOAL>sSup (a • s) = a • sInf s
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>f g : End R M<VAR>inst✝ : IsSemisimpleModule R M<GOAL>IsSemisimple 0
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>f : Filter α<VAR>P : α → Prop<GOAL>(∃ᶠ (x : α) in f, P x) ↔ ∀ {U : Set α}, U ∈ f → ∃ x ∈ U, P x
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>f : Filter α<VAR>P : α → Prop<GOAL>(∀ {q : α → Prop}, (∀ᶠ (x : α) in f, q x) → ∃ x, q x ∧ P x) ↔ ∀ {U : Set α}, U ∈ f → ∃ x ∈ U, P x
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁹ : Category.{u_3, u_1} C<VAR>inst✝⁸ : Category.{u_4, u_2} D<VAR>inst✝⁷ : HasZeroMorphisms C<VAR>inst✝⁶ : HasZeroMorphisms D<VAR>S : ShortComplex C<VAR>h₁✝ : S.LeftHomologyData<VAR>h₂✝ : S.RightHomologyData<VAR>F✝ : C ⥤ D<VAR>inst✝⁵ : F✝.PreservesZeroMorphisms<VAR>hl : S.LeftHomologyData<VAR>hr : S.RightHomologyData<VAR>S₁ S₂ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>hl₁ : S₁.LeftHomologyData<VAR>hr₁ : S₁.RightHomologyData<VAR>hl₂ : S₂.LeftHomologyData<VAR>hr₂ : S₂.RightHomologyData<VAR>h₁ : S₁.HomologyData<VAR>h₂ : S₂.HomologyData<VAR>F : C ⥤ D<VAR>inst✝⁴ : F.PreservesZeroMorphisms<VAR>inst✝³ : S₁.HasLeftHomology<VAR>inst✝² : S₂.HasLeftHomology<VAR>inst✝¹ : F.PreservesLeftHomologyOf S₁<VAR>inst✝ : F.PreservesLeftHomologyOf S₂<GOAL>F.map (cyclesMap φ) ≫ (S₂.mapCyclesIso F).inv = (S₁.mapCyclesIso F).inv ≫ cyclesMap (F.mapShortComplex.map φ)
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f : R[X]<VAR>i : ℕ<VAR>hi : i ≠ f.natDegree<GOAL>f.eraseLead.coeff i = f.coeff i
<VAR>p : ℕ → Prop<VAR>inst✝ : DecidablePred p<VAR>a b : ℕ<GOAL>count p (a + b) = count p a + count (fun k => p (a + k)) b
<VAR>p : ℕ → Prop<VAR>inst✝ : DecidablePred p<VAR>a b : ℕ<VAR>this : Disjoint (filter p (range a)) (filter p (map (addLeftEmbedding a) (range b)))<GOAL>count p (a + b) = count p a + count (fun k => p (a + k)) b
<VAR>p : ℕ → Prop<VAR>inst✝ : DecidablePred p<VAR>a b : ℕ<VAR>this : Disjoint (filter p (range a)) (filter p (map (addLeftEmbedding a) (range b)))<GOAL>(filter p (range a)).card + (filter (p ∘ ⇑{ toFun := fun h => a + h, inj' := ⋯ }) (range b)).card = (filter p (range a)).card + (filter (fun k => p (a + k)) (range b)).card
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l f f₁ f₂ : Filter α<VAR>g g₁ g₂ : Filter β<VAR>m : α → β<VAR>m' : β → γ<VAR>s : Set α<VAR>t : Set β<VAR>h : Disjoint g₁ g₂<GOAL>Disjoint (comap m g₁) (comap m g₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : Preorder α<VAR>a a₁ a₂ b b₁ b₂ c x : α<GOAL>b ∈ Ioc a b ↔ a < b
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<VAR>inst✝ : IsIso f<GOAL>pushout.inl f g ≫ inv (pushout.inr f g) = inv f ≫ g
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>inst✝³ : NonUnitalNormedRing A<VAR>inst✝² : NormedSpace 𝕜 A<VAR>inst✝¹ : SMulCommClass 𝕜 A A<VAR>inst✝ : IsScalarTower 𝕜 A A<VAR>a : 𝓜(𝕜, A)<GOAL>a.toProdMulOpposite ∈ {lr | ∀ (x y : A), (unop lr.2) x * y = x * lr.1 y}
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>G : SimpleGraph α<VAR>inst✝¹ : MulZeroOneClass R<VAR>a b : α<VAR>e : Sym2 α<VAR>inst✝ : Nontrivial R<GOAL>incMatrix R G a e = 0 ↔ e ∉ G.incidenceSet a
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝¹ : SeminormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>x : F<VAR>s : Set F<VAR>hx : x ∈ s<GOAL>closedBall x (infDist x sᶜ) ⊆ closure s
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝¹ : SeminormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>x : F<VAR>s : Set F<VAR>hx : x ∈ s<VAR>h₀ : infDist x sᶜ = 0<GOAL>closedBall x (infDist x sᶜ) ⊆ closure s
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝¹ : SeminormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>x : F<VAR>s : Set F<VAR>hx : x ∈ s<VAR>h₀ : infDist x sᶜ ≠ 0<GOAL>closedBall x (infDist x sᶜ) ⊆ closure s
<VAR>z : ℍ<GOAL>ModularGroup.T • z = 1 +ᵥ z
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : Type u_6<VAR>α : Type u_7<VAR>α' : Type u_8<VAR>β : Type u_9<VAR>β' : Type u_10<VAR>γ : Type u_11<VAR>𝓕 : Type u_12<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>F : ι → X → α<VAR>S : Set X<VAR>u : α → β<VAR>hu : UniformInducing u<VAR>x : X<GOAL>EquicontinuousWithinAt F S x ↔ EquicontinuousWithinAt ((fun x => u ∘ x) ∘ F) S x
<VAR>a : ℚ<VAR>tr : Transcendental ℚ ↑a<GOAL>False
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>E' : Type u_5<VAR>M' : Type u_6<VAR>H' : Type u_7<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : TopologicalSpace H<VAR>inst✝⁵ : TopologicalSpace M<VAR>f f' : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>inst✝⁴ : NormedAddCommGroup E'<VAR>inst✝³ : NormedSpace 𝕜 E'<VAR>inst✝² : TopologicalSpace H'<VAR>inst✝¹ : TopologicalSpace M'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>s t : Set M<VAR>inst✝ : I.Boundaryless<GOAL>IsOpen (f.extend I).target
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>E' : Type u_5<VAR>M' : Type u_6<VAR>H' : Type u_7<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : TopologicalSpace H<VAR>inst✝⁵ : TopologicalSpace M<VAR>f f' : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>inst✝⁴ : NormedAddCommGroup E'<VAR>inst✝³ : NormedSpace 𝕜 E'<VAR>inst✝² : TopologicalSpace H'<VAR>inst✝¹ : TopologicalSpace M'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>s t : Set M<VAR>inst✝ : I.Boundaryless<GOAL>IsOpen (↑I.symm ⁻¹' f.target)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → Option β<VAR>s' s t : Finset α<VAR>f_inj : ∀ (a a' : α), ∀ b ∈ f a, b ∈ f a' → a = a'<VAR>x✝ : α<GOAL>x✝ ∈ filterMap some s ⋯ ↔ x✝ ∈ s
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>m' : o → Type u_5<VAR>n' : o → Type u_6<VAR>R : Type u_7<VAR>S : Type u_8<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>inst✝¹ : NonUnitalNonAssocRing α<VAR>inst✝ : Fintype n<VAR>v : n → α<VAR>A : Matrix m n α<GOAL>-A *ᵥ -v = A *ᵥ v
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B I J X Y : Set α<VAR>e : α<VAR>hI : M.Basis I X<VAR>hJ : M.Indep J<VAR>hIJ : I ⊆ J<GOAL>M.Basis J (J ∪ X)
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B I J X Y : Set α<VAR>e : α<VAR>hI : M.Basis I X<VAR>hJ : M.Indep J<VAR>hIJ : I ⊆ J<GOAL>M.Indep J
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>X : Type u_4<VAR>Y : Type u_5<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>f g : ι → Set X<VAR>hf : LocallyFinite f<VAR>a : X<VAR>U : Set X<VAR>haU : U ∈ 𝓝 a<VAR>hfin : {i | (f i ∩ U).Nonempty}.Finite<GOAL>𝓝[⋃ i, f i] a = ⨆ i, 𝓝[f i] a
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>X : Type u_4<VAR>Y : Type u_5<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>f g : ι → Set X<VAR>hf : LocallyFinite f<VAR>a : X<VAR>U : Set X<VAR>haU : U ∈ 𝓝 a<VAR>hfin : {i | (f i ∩ U).Nonempty}.Finite<GOAL>𝓝[⋃ i, f i] a ≤ ⨆ i, 𝓝[f i] a
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝² : Category.{v', u'} D<VAR>inst✝¹ : ConcreteCategory D<VAR>J : GrothendieckTopology C<VAR>F₁ F₂ F₃ : Cᵒᵖ ⥤ D<VAR>φ : F₁ ⟶ F₂<VAR>ψ : F₂ ⟶ F₃<VAR>inst✝ : IsLocallyInjective J (φ ≫ ψ)<GOAL>IsLocallyInjective J φ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : Nontrivial β<VAR>f : α → β<VAR>hf : Surjective f<GOAL>Nontrivial α
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : Nontrivial β<VAR>f : α → β<VAR>hf : Surjective f<VAR>x y : β<VAR>h : x ≠ y<GOAL>Nontrivial α
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>a b c d : Ordinal.{u_4}<GOAL>a - b - c ≤ d ↔ a - (b + c) ≤ d
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDedekindDomain R<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>v : HeightOneSpectrum R<VAR>x y : R_hat R K<GOAL>{ toFun := fun x v => ↑(x v), map_zero' := ⋯ }.toFun (x + y) = { toFun := fun x v => ↑(x v), map_zero' := ⋯ }.toFun x + { toFun := fun x v => ↑(x v), map_zero' := ⋯ }.toFun y
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDedekindDomain R<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>v✝ : HeightOneSpectrum R<VAR>x y : R_hat R K<VAR>v : HeightOneSpectrum R<GOAL>{ toFun := fun x v => ↑(x v), map_zero' := ⋯ }.toFun (x + y) v = ({ toFun := fun x v => ↑(x v), map_zero' := ⋯ }.toFun x + { toFun := fun x v => ↑(x v), map_zero' := ⋯ }.toFun y) v
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDedekindDomain R<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>v✝ : HeightOneSpectrum R<VAR>x y : R_hat R K<VAR>v : HeightOneSpectrum R<GOAL>↑((x + y) v) = ((fun v => ↑(x v)) + fun v => ↑(y v)) v
<VAR>ι : Sort u_1<VAR>κ : ι → Sort u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : TopologicalSpace β<VAR>s✝ t✝ : Set α<VAR>a x y : α<VAR>inst✝¹ : AlexandrovDiscrete α<VAR>inst✝ : AlexandrovDiscrete β<VAR>s t : Set α<GOAL>t ∈ 𝓝ˢ (exterior s) ↔ t ∈ 𝓝ˢ s
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>σ : Perm α<GOAL>σ.cycleType = 0 ↔ σ = 1
<VAR>ξ : ℝ<VAR>u v : ℤ<VAR>hv : 2 ≤ v<VAR>h : ContfracLegendre.Ass ξ u v<GOAL>|(fract ξ)⁻¹ - ↑v / (↑u - ↑⌊ξ⌋ * ↑v)| < ((↑u - ↑⌊ξ⌋ * ↑v) * (2 * (↑u - ↑⌊ξ⌋ * ↑v) - 1))⁻¹