ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type uX<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x✝ x₀ : E<VAR>c : F<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>h : HasFTaylorSeriesUpTo n f p<VAR>x : E<GOAL>p x 0 = (continuousMultilinearCurryFin0 𝕜 E F).symm (p x 0).uncurry0
<VAR>a✝ b✝ : ℤ<VAR>n : ℕ<VAR>a : ℤ<VAR>x✝ : a ∈ Iic 0<VAR>b : ℤ<VAR>hb : b ∈ Iic 0<VAR>hab : a < b<GOAL>b.natAbs < a.natAbs
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P : Fin 3 → F<VAR>hPz : P z ≠ 0<GOAL>P x * ![P x / P z ^ 2, P y / P z ^ 3, 1] z ^ 2 = ![P x / P z ^ 2, P y / P z ^ 3, 1] x * P z ^ 2
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P : Fin 3 → F<VAR>hPz : P z ≠ 0<GOAL>P y * ![P x / P z ^ 2, P y / P z ^ 3, 1] z ^ 3 = ![P x / P z ^ 2, P y / P z ^ 3, 1] y * P z ^ 3
<VAR>n m : ℕ<VAR>i : Fin (n + 1)<GOAL>i.predAbove (last (n + 1)) = last n
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : CommRing S<VAR>inst✝⁶ : Algebra R S<VAR>P✝ : Generators R S<VAR>T✝ : Type ?u.93774<VAR>inst✝⁵ : CommRing T✝<VAR>inst✝⁴ : Algebra R T✝<VAR>inst✝³ : Algebra S T✝<VAR>inst✝² : IsScalarTower R S T✝<VAR>T : Type ?u.94985<VAR>inst✝¹ : CommRing T<VAR>inst✝ : Algebra R T<VAR>P : Generators R S<VAR>x : T ⊗[R] S<GOAL>∃ a, (aeval fun x => 1 ⊗ₜ[R] P.val x) a = x
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>G : Type u_6<VAR>k : Type u_7<VAR>R : Type u_8<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : OrderedCommMonoid N<VAR>f : M → N<VAR>h_one : f 1 = 1<VAR>h_mul : ∀ (x y : M), f (x * y) ≤ f x * f y<VAR>s : Finset ι<VAR>g : ι → M<GOAL>f (∏ i ∈ s, g i) ≤ ∏ i ∈ s, f (g i)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>G : Type u_6<VAR>k : Type u_7<VAR>R : Type u_8<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : OrderedCommMonoid N<VAR>f : M → N<VAR>h_one : f 1 = 1<VAR>h_mul : ∀ (x y : M), f (x * y) ≤ f x * f y<VAR>s : Finset ι<VAR>g : ι → M<GOAL>(Multiset.map f (Multiset.map (fun i => g i) s.val)).prod ≤ ∏ i ∈ s, f (g i)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>G : Type u_6<VAR>k : Type u_7<VAR>R : Type u_8<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : OrderedCommMonoid N<VAR>f : M → N<VAR>h_one : f 1 = 1<VAR>h_mul : ∀ (x y : M), f (x * y) ≤ f x * f y<VAR>s : Finset ι<VAR>g : ι → M<GOAL>(Multiset.map (f ∘ fun i => g i) s.val).prod ≤ ∏ i ∈ s, f (g i)
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>A✝ A B : ValuationSubring K<VAR>h : A.principalUnitGroup = B.principalUnitGroup<GOAL>A = B
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<GOAL>(o.oangle (x + y) y).tan * ‖y‖ = ‖x‖
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : (-o).oangle y x = ↑(π / 2)<GOAL>((-o).oangle y (x + y)).tan * ‖y‖ = ‖x‖
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : (-o).oangle y x = ↑(π / 2)<GOAL>((-o).oangle y (y + x)).tan * ‖y‖ = ‖x‖
<VAR>α : Type u_1<VAR>Γ₀ : Type u_2<VAR>inst✝ : LinearOrderedCommGroupWithZero Γ₀<VAR>γ γ₁ γ₂ : Γ₀<VAR>l : Filter α<VAR>f : α → Γ₀<VAR>h : γ₁ < γ₂<GOAL>Iio γ₂ ∈ 𝓝 γ₁
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : Type x<VAR>inst✝ : Ring α<VAR>a✝ b✝ a b : α<VAR>u : αˣ<GOAL>a - b /ₚ u = (a * ↑u - b) /ₚ u
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>q : Semiquot α<VAR>p : q.IsPure<VAR>a : α<GOAL>a ∈ q ↔ a ∈ pure (q.get p)
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<GOAL>‖y‖ / (o.oangle (x - y) x).tan = ‖x‖
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : (-o).oangle y x = ↑(π / 2)<GOAL>‖y‖ / ((-o).oangle x (x - y)).tan = ‖x‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>M : Type u_3<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : OrderedAddCommMonoid M<VAR>s : SignedMeasure α<VAR>i j : Set α<VAR>hi : ¬restrict s i ≤ restrict 0 i<GOAL>MeasureTheory.SignedMeasure.someExistsOneDivLT s i ⊆ i ∧ MeasurableSet (MeasureTheory.SignedMeasure.someExistsOneDivLT s i) ∧ 1 / (↑(MeasureTheory.SignedMeasure.findExistsOneDivLT s i) + 1) < ↑s (MeasureTheory.SignedMeasure.someExistsOneDivLT s i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>M : Type u_3<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : OrderedAddCommMonoid M<VAR>s : SignedMeasure α<VAR>i j : Set α<VAR>hi : ¬restrict s i ≤ restrict 0 i<GOAL>Classical.choose ⋯ ⊆ i ∧ MeasurableSet (Classical.choose ⋯) ∧ 1 / (↑(MeasureTheory.SignedMeasure.findExistsOneDivLT s i) + 1) < ↑s (Classical.choose ⋯)
<VAR>x x₁ x₂ x₃ x' y y₁ y₂ y₃ y' : PGame<GOAL>P24 x₁ x₂ y ↔ P24 (-x₂) (-x₁) y
<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<VAR>S : Type u_10<VAR>inst✝² : Semiring S<VAR>inst✝¹ : Module S M'<VAR>inst✝ : SMulCommClass R S M'<VAR>f : ι → M'<GOAL>LinearMap.range ((b.constr S) f) = span R (range f)
<VAR>X : Type u_1<VAR>inst✝³ : MeasurableSpace X<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : OpensMeasurableSpace X<VAR>inst✝ : T0Space X<VAR>x : X<VAR>μ : ↑(range diracProba)<VAR>h : ↑μ = diracProba x<GOAL>diracProbaInverse μ = x
<VAR>X : Type u_1<VAR>inst✝³ : MeasurableSpace X<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : OpensMeasurableSpace X<VAR>inst✝ : T0Space X<VAR>x : X<VAR>μ : ↑(range diracProba)<VAR>h : ↑μ = diracProba x<GOAL>(fun x => diracProba x) (diracProbaInverse μ) = (fun x => diracProba x) x
<VAR>X : Type u_1<VAR>inst✝³ : MeasurableSpace X<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : OpensMeasurableSpace X<VAR>inst✝ : T0Space X<VAR>x : X<VAR>μ : ↑(range diracProba)<VAR>h : ↑μ = diracProba x<GOAL>diracProba (diracProbaInverse μ) = ↑μ
<VAR>C : Type u<VAR>𝒞 : Category.{v, u} C<VAR>inst✝ : MonoidalCategory C<VAR>X Y : C<VAR>f : X ≅ Y<VAR>Z : C<GOAL>f.inv ▷ Z ≫ f.hom ▷ Z = 𝟙 (Y ⊗ Z)
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>n✝ n' m : ℕ<VAR>s✝ : Sym α✝ n✝<VAR>a b : α✝<VAR>α : Type u_3<VAR>n : ℕ<VAR>s : Sym α n<GOAL>↑(map (fun x => x) s) = ↑s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedDivisionRing 𝕜<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : BoundedSMul 𝕜 E<VAR>c : 𝕜<VAR>x : Set E<GOAL>diam (c • x) = ‖c‖ * diam x
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hff' : ∀ᶠ (x : ℝ) in 𝓝[<] a, HasDerivAt f (f' x) x<VAR>hgg' : ∀ᶠ (x : ℝ) in 𝓝[<] a, HasDerivAt g (g' x) x<VAR>hg' : ∀ᶠ (x : ℝ) in 𝓝[<] a, g' x ≠ 0<VAR>hfa : Tendsto f (𝓝[<] a) (𝓝 0)<VAR>hga : Tendsto g (𝓝[<] a) (𝓝 0)<VAR>hdiv : Tendsto (fun x => f' x / g' x) (𝓝[<] a) l<GOAL>Tendsto (fun x => f x / g x) (𝓝[<] a) l
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hff' : ∃ v ∈ 𝓝[<] a, ∀ y ∈ v, HasDerivAt f (f' y) y<VAR>hgg' : ∃ v ∈ 𝓝[<] a, ∀ y ∈ v, HasDerivAt g (g' y) y<VAR>hg' : ∃ v ∈ 𝓝[<] a, ∀ y ∈ v, g' y ≠ 0<VAR>hfa : Tendsto f (𝓝[<] a) (𝓝 0)<VAR>hga : Tendsto g (𝓝[<] a) (𝓝 0)<VAR>hdiv : Tendsto (fun x => f' x / g' x) (𝓝[<] a) l<GOAL>Tendsto (fun x => f x / g x) (𝓝[<] a) l
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hfa : Tendsto f (𝓝[<] a) (𝓝 0)<VAR>hga : Tendsto g (𝓝[<] a) (𝓝 0)<VAR>hdiv : Tendsto (fun x => f' x / g' x) (𝓝[<] a) l<VAR>s₁ : Set ℝ<VAR>hs₁ : s₁ ∈ 𝓝[<] a<VAR>hff' : ∀ y ∈ s₁, HasDerivAt f (f' y) y<VAR>s₂ : Set ℝ<VAR>hs₂ : s₂ ∈ 𝓝[<] a<VAR>hgg' : ∀ y ∈ s₂, HasDerivAt g (g' y) y<VAR>s₃ : Set ℝ<VAR>hs₃ : s₃ ∈ 𝓝[<] a<VAR>hg' : ∀ y ∈ s₃, g' y ≠ 0<VAR>s : Set ℝ := s₁ ∩ s₂ ∩ s₃<GOAL>Tendsto (fun x => f x / g x) (𝓝[<] a) l
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hfa : Tendsto f (𝓝[<] a) (𝓝 0)<VAR>hga : Tendsto g (𝓝[<] a) (𝓝 0)<VAR>hdiv : Tendsto (fun x => f' x / g' x) (𝓝[<] a) l<VAR>s₁ : Set ℝ<VAR>hs₁ : s₁ ∈ 𝓝[<] a<VAR>hff' : ∀ y ∈ s₁, HasDerivAt f (f' y) y<VAR>s₂ : Set ℝ<VAR>hs₂ : s₂ ∈ 𝓝[<] a<VAR>hgg' : ∀ y ∈ s₂, HasDerivAt g (g' y) y<VAR>s₃ : Set ℝ<VAR>hs₃ : s₃ ∈ 𝓝[<] a<VAR>hg' : ∀ y ∈ s₃, g' y ≠ 0<VAR>s : Set ℝ := s₁ ∩ s₂ ∩ s₃<VAR>hs : s ∈ 𝓝[<] a<GOAL>Tendsto (fun x => f x / g x) (𝓝[<] a) l
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hfa : Tendsto f (𝓝[<] a) (𝓝 0)<VAR>hga : Tendsto g (𝓝[<] a) (𝓝 0)<VAR>hdiv : Tendsto (fun x => f' x / g' x) (𝓝[<] a) l<VAR>s₁ : Set ℝ<VAR>hs₁ : s₁ ∈ 𝓝[<] a<VAR>hff' : ∀ y ∈ s₁, HasDerivAt f (f' y) y<VAR>s₂ : Set ℝ<VAR>hs₂ : s₂ ∈ 𝓝[<] a<VAR>hgg' : ∀ y ∈ s₂, HasDerivAt g (g' y) y<VAR>s₃ : Set ℝ<VAR>hs₃ : s₃ ∈ 𝓝[<] a<VAR>hg' : ∀ y ∈ s₃, g' y ≠ 0<VAR>s : Set ℝ := s₁ ∩ s₂ ∩ s₃<VAR>hs : ∃ l ∈ Iio a, Ioo l a ⊆ s<GOAL>Tendsto (fun x => f x / g x) (𝓝[<] a) l
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l✝ : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hfa : Tendsto f (𝓝[<] a) (𝓝 0)<VAR>hga : Tendsto g (𝓝[<] a) (𝓝 0)<VAR>hdiv : Tendsto (fun x => f' x / g' x) (𝓝[<] a) l✝<VAR>s₁ : Set ℝ<VAR>hs₁ : s₁ ∈ 𝓝[<] a<VAR>hff' : ∀ y ∈ s₁, HasDerivAt f (f' y) y<VAR>s₂ : Set ℝ<VAR>hs₂ : s₂ ∈ 𝓝[<] a<VAR>hgg' : ∀ y ∈ s₂, HasDerivAt g (g' y) y<VAR>s₃ : Set ℝ<VAR>hs₃ : s₃ ∈ 𝓝[<] a<VAR>hg' : ∀ y ∈ s₃, g' y ≠ 0<VAR>s : Set ℝ := s₁ ∩ s₂ ∩ s₃<VAR>l : ℝ<VAR>hal : l ∈ Iio a<VAR>hl : Ioo l a ⊆ s<GOAL>Tendsto (fun x => f x / g x) (𝓝[<] a) l✝
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝² : Category.{v₂, u₂} D<VAR>G : C ⥤ D<VAR>X : C<VAR>inst✝¹ : HasInitial C<VAR>inst✝ : PreservesColimit (Functor.empty C) G<VAR>F : Discrete PEmpty.{1} ⥤ D<GOAL>HasColimit F
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝² : Category.{v₂, u₂} D<VAR>G : C ⥤ D<VAR>X : C<VAR>inst✝¹ : HasInitial C<VAR>inst✝ : PreservesColimit (Functor.empty C) G<VAR>F : Discrete PEmpty.{1} ⥤ D<VAR>this : HasColimit (Functor.empty D)<GOAL>HasColimit F
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedSemifield α<VAR>a b c d e : α<VAR>m n : ℤ<VAR>ha : 1 < a<GOAL>a⁻¹ < 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>l l' : List α<VAR>a : α<GOAL>l.toFinset = l'.toFinset ↔ l.dedup ~ l'.dedup
<VAR>x✝ y x : ℝ<GOAL>rexp |x| ≤ rexp x + rexp (-x)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁵ : CommSemiring R<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>S : Type u_3<VAR>inst✝² : CommMonoid S<VAR>inst✝¹ : DistribMulAction S M<VAR>inst✝ : SMulCommClass S R M<VAR>h : torsion' R M S = ⊤<VAR>x : M<GOAL>∃ a, a • x = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁵ : CommSemiring R<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>S : Type u_3<VAR>inst✝² : CommMonoid S<VAR>inst✝¹ : DistribMulAction S M<VAR>inst✝ : SMulCommClass S R M<VAR>h : torsion' R M S = ⊤<VAR>x : M<GOAL>x ∈ ⊤
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<VAR>h : Dense s<GOAL>Dense sᶜᶜ
<VAR>α : Type u_1<VAR>inst✝¹ : SemilatticeSup α<VAR>ι : Type u_2<VAR>π : ι → Type u_3<VAR>inst✝ : (i : ι) → SemilatticeSup (π i)<VAR>f : ℕ → (i : ι) → π i<VAR>n : ℕ<VAR>i : ι<GOAL>(partialSups f) n i = (partialSups fun x => f x i) n
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝ : CommSemiring R<VAR>P : Ideal R<VAR>hPunique : ∀ (y : Ideal R), (fun P => P ≠ ⊥ ∧ P.IsPrime) y → y = P<VAR>hPnonzero : P ≠ ⊥<VAR>hPnot_top : P ≠ ⊤<VAR>mem_or_mem'✝ : ∀ {x y : R}, x * y ∈ P → x ∈ P ∨ y ∈ P<GOAL>∃! I, I.IsMaximal
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝ : CommSemiring R<VAR>P : Ideal R<VAR>hPunique : ∀ (y : Ideal R), (fun P => P ≠ ⊥ ∧ P.IsPrime) y → y = P<VAR>hPnonzero : P ≠ ⊥<VAR>hPnot_top : P ≠ ⊤<VAR>mem_or_mem'✝ : ∀ {x y : R}, x * y ∈ P → x ∈ P ∨ y ∈ P<GOAL>∀ (b : Ideal R), P < b → b = ⊤
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝ : CommSemiring R<VAR>P : Ideal R<VAR>hPunique : ∀ (y : Ideal R), (fun P => P ≠ ⊥ ∧ P.IsPrime) y → y = P<VAR>hPnonzero : P ≠ ⊥<VAR>hPnot_top : P ≠ ⊤<VAR>mem_or_mem'✝ : ∀ {x y : R}, x * y ∈ P → x ∈ P ∨ y ∈ P<VAR>M : Ideal R<VAR>hM : (fun I => I.IsMaximal) M<GOAL>M ≠ ⊥
<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✝⁶ : LinearOrderedField 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>s : AffineSubspace R P<VAR>x y : P<VAR>hx : x ∈ s<VAR>hy : y ∉ s<GOAL>s.SOppSide y ((pointReflection R x) y)
<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✝⁶ : LinearOrderedField 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>s : AffineSubspace R P<VAR>x y : P<VAR>hx : x ∈ s<VAR>hy : y ∉ s<VAR>h : x = y<GOAL>y ∈ s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : α → β → Prop<VAR>a : α<VAR>cb : Computation β<VAR>x✝ : ∃ b, b ∈ cb ∧ R a b<VAR>b : β<VAR>mb : b ∈ cb<VAR>ab : R a b<VAR>a' : α<VAR>ma' : a' ∈ pure a<GOAL>∃ b, b ∈ cb ∧ R a' b
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : α → β → Prop<VAR>a : α<VAR>cb : Computation β<VAR>x✝ : ∃ b, b ∈ cb ∧ R a b<VAR>b : β<VAR>mb : b ∈ cb<VAR>ab : R a b<VAR>a' : α<VAR>ma' : a' ∈ pure a<GOAL>∃ b, b ∈ cb ∧ R a b
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : α → β → Prop<VAR>a : α<VAR>cb : Computation β<VAR>x✝ : ∃ b, b ∈ cb ∧ R a b<VAR>b : β<VAR>mb : b ∈ cb<VAR>ab : R a b<VAR>b' : β<VAR>mb' : b' ∈ cb<GOAL>R a b'
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : α → β → Prop<VAR>a : α<VAR>cb : Computation β<VAR>x✝ : ∃ b, b ∈ cb ∧ R a b<VAR>b : β<VAR>mb : b ∈ cb<VAR>ab : R a b<VAR>b' : β<VAR>mb' : b' ∈ cb<GOAL>R a b
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_4, u_1} C<VAR>inst✝³ : Category.{u_3, u_2} D<VAR>inst✝² : Preadditive C<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>X Y Z : C<VAR>f : L.obj X ⟶ L.obj Y<VAR>φ : W.LeftFraction X Y<VAR>hφ : f = φ.map L ⋯<GOAL>neg' W f = φ.neg.map L ⋯
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_4, u_1} C<VAR>inst✝³ : Category.{u_3, u_2} D<VAR>inst✝² : Preadditive C<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>X Y Z : C<VAR>φ φ₀ : W.LeftFraction X Y<VAR>hφ : φ₀.map L ⋯ = φ.map L ⋯<VAR>hφ₀ : neg' W (φ₀.map L ⋯) = φ₀.neg.map L ⋯<GOAL>neg' W (φ₀.map L ⋯) = φ.neg.map L ⋯
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_4, u_1} C<VAR>inst✝³ : Category.{u_3, u_2} D<VAR>inst✝² : Preadditive C<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>X Y Z : C<VAR>φ φ₀ : W.LeftFraction X Y<VAR>hφ : LeftFractionRel φ₀ φ<VAR>hφ₀ : neg' W (φ₀.map L ⋯) = φ₀.neg.map L ⋯<GOAL>neg' W (φ₀.map L ⋯) = φ.neg.map L ⋯
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_4, u_1} C<VAR>inst✝³ : Category.{u_3, u_2} D<VAR>inst✝² : Preadditive C<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>X Y Z : C<VAR>φ φ₀ : W.LeftFraction X Y<VAR>hφ₀ : neg' W (φ₀.map L ⋯) = φ₀.neg.map L ⋯<VAR>Y' : C<VAR>t₁ : φ₀.Y' ⟶ Y'<VAR>t₂ : φ.Y' ⟶ Y'<VAR>hst : φ₀.s ≫ t₁ = φ.s ≫ t₂<VAR>hft : φ₀.f ≫ t₁ = φ.f ≫ t₂<VAR>ht : W (φ₀.s ≫ t₁)<GOAL>neg' W (φ₀.map L ⋯) = φ.neg.map L ⋯
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_4, u_1} C<VAR>inst✝³ : Category.{u_3, u_2} D<VAR>inst✝² : Preadditive C<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>X Y Z : C<VAR>φ φ₀ : W.LeftFraction X Y<VAR>hφ₀ : neg' W (φ₀.map L ⋯) = φ₀.neg.map L ⋯<VAR>Y' : C<VAR>t₁ : φ₀.Y' ⟶ Y'<VAR>t₂ : φ.Y' ⟶ Y'<VAR>hst : φ₀.s ≫ t₁ = φ.s ≫ t₂<VAR>hft : φ₀.f ≫ t₁ = φ.f ≫ t₂<VAR>ht : W (φ₀.s ≫ t₁)<VAR>this : IsIso (L.map (φ₀.s ≫ t₁))<GOAL>neg' W (φ₀.map L ⋯) = φ.neg.map L ⋯
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_4, u_1} C<VAR>inst✝³ : Category.{u_3, u_2} D<VAR>inst✝² : Preadditive C<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>X Y Z : C<VAR>φ φ₀ : W.LeftFraction X Y<VAR>hφ₀ : neg' W (φ₀.map L ⋯) = φ₀.neg.map L ⋯<VAR>Y' : C<VAR>t₁ : φ₀.Y' ⟶ Y'<VAR>t₂ : φ.Y' ⟶ Y'<VAR>hst : φ₀.s ≫ t₁ = φ.s ≫ t₂<VAR>hft : φ₀.f ≫ t₁ = φ.f ≫ t₂<VAR>ht : W (φ₀.s ≫ t₁)<VAR>this : IsIso (L.map (φ₀.s ≫ t₁))<GOAL>neg' W (φ₀.map L ⋯) ≫ L.map (φ₀.s ≫ t₁) = φ.neg.map L ⋯ ≫ L.map (φ₀.s ≫ t₁)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_4, u_1} C<VAR>inst✝³ : Category.{u_3, u_2} D<VAR>inst✝² : Preadditive C<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>X Y Z : C<VAR>φ φ₀ : W.LeftFraction X Y<VAR>hφ₀ : neg' W (φ₀.map L ⋯) = φ₀.neg.map L ⋯<VAR>Y' : C<VAR>t₁ : φ₀.Y' ⟶ Y'<VAR>t₂ : φ.Y' ⟶ Y'<VAR>hst : φ₀.s ≫ t₁ = φ.s ≫ t₂<VAR>hft : φ₀.f ≫ t₁ = φ.f ≫ t₂<VAR>ht : W (φ₀.s ≫ t₁)<VAR>this : IsIso (L.map (φ₀.s ≫ t₁))<GOAL>neg' W (φ₀.map L ⋯) ≫ L.map φ₀.s ≫ L.map t₁ = φ.neg.map L ⋯ ≫ L.map (φ₀.s ≫ t₁)
<VAR>n : ℕ<VAR>s : ℂ<VAR>hs : s.re ≠ 0<GOAL>‖↑n ^ s‖ = ↑n ^ s.re
<VAR>K : Type u_1<VAR>inst✝³ : DivisionRing K<VAR>inst✝² : TopologicalSpace K<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : LinearOrderedSemifield β<VAR>a✝ : α<VAR>f : α → β<VAR>a : α<VAR>h1 : IsLocalMin f a<VAR>h2 : ∀ᶠ (z : α) in 𝓝 a, 0 < f z<GOAL>IsLocalMax f⁻¹ a
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : RegularSpace Y<VAR>f : X → Y<VAR>A : Set X<VAR>hA : Dense A<VAR>hf : ∀ (x : X), ∃ y, Tendsto f (𝓝[A] x) (𝓝 y)<GOAL>Continuous (extendFrom A f)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : RegularSpace Y<VAR>f : X → Y<VAR>A : Set X<VAR>hA : Dense A<VAR>hf : ∀ (x : X), ∃ y, Tendsto f (𝓝[A] x) (𝓝 y)<GOAL>ContinuousOn (extendFrom A f) univ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>p✝ : α → Prop<VAR>f : (a : α) → p✝ a → β<VAR>l₁ l₂ : List α<VAR>p : l₁ ~ l₂<VAR>H₁ : ∀ (a : α), a ∈ l₁ → p✝ a<VAR>H₂ : ∀ (a : α), a ∈ l₂ → p✝ a<GOAL>List.pmap f l₁ H₁ ~ List.pmap f l₂ H₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t✝ : Set α<VAR>f : α → β<VAR>s t : Set α<VAR>hs : autoParam s.Finite _auto✝<GOAL>t.ncard ≤ s.ncard + (t \ s).ncard
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t✝ : Set α<VAR>f : α → β<VAR>s t : Set α<VAR>hs : autoParam s.Finite _auto✝<GOAL>t.ncard ≤ (t \ s).ncard + s.ncard
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : InnerProductSpace ℝ V<VAR>inst✝³ : MetricSpace P<VAR>inst✝² : NormedAddTorsor V P<VAR>inst✝¹ : Module.Oriented ℝ V (Fin 2)<VAR>inst✝ : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>p1 p2 p3 : P<VAR>h21 : p2 ≠ p1<VAR>h32 : p3 ≠ p2<VAR>h13 : p1 ≠ p3<GOAL>∡ p1 p2 p3 + ∡ p2 p3 p1 + ∡ p3 p1 p2 = ↑π
<VAR>B : Type u₁<VAR>inst✝² : Bicategory B<VAR>C : Type u₂<VAR>inst✝¹ : Bicategory C<VAR>D : Type u₃<VAR>inst✝ : Bicategory D<VAR>F✝ F : Pseudofunctor B C<VAR>a b : B<VAR>f : a ⟶ b<GOAL>(F.mapId a).hom ▷ F.map f = (F.mapComp (𝟙 a) f).inv ≫ F.map₂ (λ_ f).hom ≫ (λ_ (F.map f)).inv
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>α : Type u_3<VAR>inst✝² : NonUnitalNormedRing E<VAR>inst✝¹ : StarRing E<VAR>inst✝ : CstarRing E<VAR>x : E<GOAL>x⋆ * x ≠ 0 ↔ x ≠ 0
<VAR>a b c d a' : List Γ'<GOAL>update (elim a b c d) main a' = elim a' b c d
<VAR>a b c d a' : List Γ'<VAR>x : K'<GOAL>update (elim a b c d) main a' x = elim a' b c d x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>E : Type u_3<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f✝ g✝ f g : α → E<VAR>hf : Integrable f μ<VAR>hg : Integrable g μ<VAR>hfg : μ.withDensityᵥ f = μ.withDensityᵥ g<GOAL>f =ᶠ[ae μ] g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>E : Type u_3<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f✝ g✝ f g : α → E<VAR>hf : Integrable f μ<VAR>hg : Integrable g μ<VAR>hfg : μ.withDensityᵥ f = μ.withDensityᵥ g<VAR>i : Set α<VAR>hi : MeasurableSet i<VAR>x✝ : μ i < ⊤<GOAL>∫ (x : α) in i, f x ∂μ = ∫ (x : α) in i, g x ∂μ
<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✝⁷ : Ring R<VAR>inst✝⁶ : Invertible 2<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✝ y z : P<VAR>x : V<GOAL>midpoint R (-x) x = 0
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>c c₁ c₂ p₁ p₂ : P<GOAL>c ∈ perpBisector p₁ ((Equiv.pointReflection p₂) p₁) ↔ ⟪c -ᵥ p₂, p₁ -ᵥ p₂⟫_ℝ = 0
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁵ : Ring K<VAR>inst✝⁴ : StrongRankCondition K<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module K V<VAR>inst✝¹ : Module.Free K V<VAR>inst✝ : Module.Finite K V<GOAL>finrank K V ≤ 1 ↔ ∃ v, ∀ (w : V), ∃ c, c • v = w
<VAR>R : Type u<VAR>S✝ : Type v<VAR>A : Type w<VAR>B : Type u₁<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝⁶ : CommSemiring C<VAR>inst✝⁵ : CommSemiring D<VAR>inst✝⁴ : CommSemiring E<VAR>inst✝³ : Algebra C D<VAR>inst✝² : Algebra C E<VAR>inst✝¹ : Algebra D E<VAR>inst✝ : IsScalarTower C D E<VAR>S : Set E<GOAL>Subalgebra.restrictScalars C (adjoin D S) = Subalgebra.restrictScalars C (adjoin (↥(Subalgebra.map (IsScalarTower.toAlgHom C D E) ⊤)) S)
<VAR>R : Type u<VAR>S✝ : Type v<VAR>A : Type w<VAR>B : Type u₁<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝⁶ : CommSemiring C<VAR>inst✝⁵ : CommSemiring D<VAR>inst✝⁴ : CommSemiring E<VAR>inst✝³ : Algebra C D<VAR>inst✝² : Algebra C E<VAR>inst✝¹ : Algebra D E<VAR>inst✝ : IsScalarTower C D E<VAR>S : Set E<GOAL>Set.range ⇑(algebraMap D E) = Set.range ⇑(algebraMap (↥(Subalgebra.map (IsScalarTower.toAlgHom C D E) ⊤)) E)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝ : MeasurableSpace β<VAR>g : α → β<VAR>hg : MeasurableEmbedding g<VAR>f : β → ℝ≥0∞<GOAL>∫⁻ (a : β), f a ∂Measure.map g μ = ∫⁻ (a : α), f (g a) ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝ : MeasurableSpace β<VAR>g : α → β<VAR>hg : MeasurableEmbedding g<VAR>f : β → ℝ≥0∞<GOAL>⨆ g_1, ⨆ (_ : ↑g_1 ≤ fun a => f a), g_1.lintegral (Measure.map g μ) = ⨆ g_1, ⨆ (_ : ↑g_1 ≤ fun a => f (g a)), g_1.lintegral μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝ : MeasurableSpace β<VAR>g : α → β<VAR>hg : MeasurableEmbedding g<VAR>f : β → ℝ≥0∞<VAR>f₀ : β →ₛ ℝ≥0∞<VAR>hf₀ : ↑f₀ ≤ fun a => f a<GOAL>f₀.lintegral (Measure.map g μ) ≤ ⨆ g_1, ⨆ (_ : ↑g_1 ≤ fun a => f (g a)), g_1.lintegral μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝ : MeasurableSpace β<VAR>g : α → β<VAR>hg : MeasurableEmbedding g<VAR>f : β → ℝ≥0∞<VAR>f₀ : α →ₛ ℝ≥0∞<VAR>hf₀ : ↑f₀ ≤ fun a => f (g a)<GOAL>f₀.lintegral μ ≤ ⨆ g_1, ⨆ (_ : ↑g_1 ≤ fun a => f a), g_1.lintegral (Measure.map g μ)
<VAR>α : Type u_1<VAR>M✝ : Matroid α<VAR>I B X : Set α<VAR>M : Matroid α<VAR>h : M✶.RkPos<GOAL>¬M.Base M.E