ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>m : OuterMeasure α<VAR>s s₁ s₂ : Set α<VAR>h : s₁ ∩ s₂ ⊆ ∅<VAR>h₁ : m.IsCaratheodory s₁<VAR>t : Set α<GOAL>m (t ∩ (s₁ ∪ s₂)) = m (t ∩ s₁) + m (t ∩ s₂)
<VAR>X✝ : Scheme<VAR>P : (X : Scheme) → ↑↑X.toPresheafedSpace → Prop<VAR>h₁ : ∀ (R : CommRingCat) (x : ↑↑(Spec R).toPresheafedSpace), P (Spec R) x<VAR>h₂ : ∀ {X Y : Scheme} (f : X ⟶ Y) [inst : IsOpenImmersion f] (x : ↑↑X.toPresheafedSpace), P X x → P Y (f.val.base x)<VAR>X : Scheme<VAR>x : ↑↑X.toPresheafedSpace<GOAL>P X x
<VAR>X✝ : Scheme<VAR>P : (X : Scheme) → ↑↑X.toPresheafedSpace → Prop<VAR>h₁ : ∀ (R : CommRingCat) (x : ↑↑(Spec R).toPresheafedSpace), P (Spec R) x<VAR>h₂ : ∀ {X Y : Scheme} (f : X ⟶ Y) [inst : IsOpenImmersion f] (x : ↑↑X.toPresheafedSpace), P X x → P Y (f.val.base x)<VAR>X : Scheme<VAR>x : ↑↑X.toPresheafedSpace<VAR>y : ↑↑(X.affineCover.obj (X.affineCover.f x)).toPresheafedSpace<VAR>e : (X.affineCover.map (X.affineCover.f x)).val.base y = x<GOAL>P X x
<VAR>x✝¹ y✝¹ z✝¹ w x✝ y✝ z✝ x : ℝ<VAR>hx : 0 ≤ x<VAR>y z : ℝ<GOAL>x ^ y * x ^ z ≤ x ^ (y + z)
<VAR>x✝¹ y✝¹ z✝¹ w x✝ y✝ z✝ x : ℝ<VAR>hx : 0 ≤ x<VAR>y z : ℝ<VAR>H : 0 = x<GOAL>x ^ y * x ^ z ≤ x ^ (y + z)
<VAR>x✝¹ y✝¹ z✝¹ w x✝ y✝ z✝ x : ℝ<VAR>hx : 0 ≤ x<VAR>y z : ℝ<VAR>pos : 0 < x<GOAL>x ^ y * x ^ z ≤ x ^ (y + z)
<VAR>ι : Type u_1<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroMorphisms C<VAR>c : ComplexShape ι<VAR>K L M K' L' : HomologicalComplex C c<VAR>φ : K ⟶ L<VAR>φ' : L ⟶ M<VAR>inst✝² : ∀ (i : ι), K.HasHomology i<VAR>inst✝¹ : ∀ (i : ι), L.HasHomology i<VAR>inst✝ : ∀ (i : ι), M.HasHomology i<VAR>hφ : QuasiIso φ<GOAL>QuasiIso (φ ≫ φ') ↔ QuasiIso φ'
<VAR>R : Type u_1<VAR>inst✝⁴ : CommSemiring R<VAR>M : Type u_2<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>A : Type u_3<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>g : TensorAlgebra R M →ₐ[R] A<GOAL>(lift R) (g.toLinearMap ∘ₗ ι R) = g
<VAR>R : Type u_1<VAR>inst✝⁴ : CommSemiring R<VAR>M : Type u_2<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>A : Type u_3<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>g : TensorAlgebra R M →ₐ[R] A<GOAL>(lift R) ((lift R).symm g) = g
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝² : Mul α<VAR>inst✝¹ : Mul β<VAR>γ : Type u_1<VAR>inst✝ : Mul γ<VAR>f : α → β<VAR>g : β → γ<VAR>hf : IsMulHom f<VAR>hg : IsMulHom g<VAR>x y : α<GOAL>(g ∘ f) (x * y) = (g ∘ f) x * (g ∘ f) y
<VAR>α : Type u_1<VAR>β : α → Type u<VAR>δ : α → Sort v<VAR>inst✝³ : DecidableEq α<VAR>s✝¹ : Finset α<VAR>t : (a : α) → Finset (β a)<VAR>ι✝ : Type u_2<VAR>inst✝² : DecidableEq (ι✝ → α)<VAR>s✝ : Finset α<VAR>f : ι✝ → α<VAR>s : Finset α<VAR>ι : Type u_3<VAR>inst✝¹ : DecidableEq (ι → α)<VAR>inst✝ : Nonempty ι<GOAL>(s.piDiag ι).card = s.card
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X✝ : C<VAR>inst✝ : HasPullbacks C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>g h : Over Y<VAR>k : g ⟶ h<GOAL>(pullback.fst g.hom f ≫ k.left) ≫ h.hom = pullback.snd g.hom f ≫ f
<VAR>𝓕 : Type u_1<VAR>𝕜 : Type u_2<VAR>α : Type u_3<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>E : Type u_6<VAR>F : Type u_7<VAR>G : Type u_8<VAR>inst✝² : SeminormedGroup E<VAR>inst✝¹ : SeminormedGroup F<VAR>inst✝ : SeminormedGroup G<VAR>s : Set E<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<GOAL>b ∈ closedBall a r ↔ ‖b / a‖ ≤ r
<VAR>D : Set ℝ<VAR>hD : Convex ℝ D<VAR>f : ℝ → ℝ<VAR>hf : ContinuousOn f D<VAR>hf' : StrictMonoOn (deriv f) (interior D)<VAR>x y z : ℝ<VAR>hx : x ∈ D<VAR>hz : z ∈ D<VAR>hxy : x < y<VAR>hyz : y < z<GOAL>(f y - f x) / (y - x) < (f z - f y) / (z - y)
<VAR>D : Set ℝ<VAR>hD : Convex ℝ D<VAR>f : ℝ → ℝ<VAR>hf : ContinuousOn f D<VAR>hf' : StrictMonoOn (deriv f) (interior D)<VAR>x y z : ℝ<VAR>hx : x ∈ D<VAR>hz : z ∈ D<VAR>hxy : x < y<VAR>hyz : y < z<VAR>hxzD : Icc x z ⊆ D<GOAL>(f y - f x) / (y - x) < (f z - f y) / (z - y)
<VAR>D : Set ℝ<VAR>hD : Convex ℝ D<VAR>f : ℝ → ℝ<VAR>hf : ContinuousOn f D<VAR>hf' : StrictMonoOn (deriv f) (interior D)<VAR>x y z : ℝ<VAR>hx : x ∈ D<VAR>hz : z ∈ D<VAR>hxy : x < y<VAR>hyz : y < z<VAR>hxzD : Icc x z ⊆ D<VAR>hxyD : Icc x y ⊆ D<GOAL>(f y - f x) / (y - x) < (f z - f y) / (z - y)
<VAR>D : Set ℝ<VAR>hD : Convex ℝ D<VAR>f : ℝ → ℝ<VAR>hf : ContinuousOn f D<VAR>hf' : StrictMonoOn (deriv f) (interior D)<VAR>x y z : ℝ<VAR>hx : x ∈ D<VAR>hz : z ∈ D<VAR>hxy : x < y<VAR>hyz : y < z<VAR>hxzD : Icc x z ⊆ D<VAR>hxyD : Icc x y ⊆ D<VAR>hxyD' : Ioo x y ⊆ interior D<GOAL>(f y - f x) / (y - x) < (f z - f y) / (z - y)
<VAR>D : Set ℝ<VAR>hD : Convex ℝ D<VAR>f : ℝ → ℝ<VAR>hf : ContinuousOn f D<VAR>hf' : StrictMonoOn (deriv f) (interior D)<VAR>x y z : ℝ<VAR>hx : x ∈ D<VAR>hz : z ∈ D<VAR>hxy : x < y<VAR>hyz : y < z<VAR>hxzD : Icc x z ⊆ D<VAR>hxyD : Icc x y ⊆ D<VAR>hxyD' : Ioo x y ⊆ interior D<VAR>hyzD : Icc y z ⊆ D<GOAL>(f y - f x) / (y - x) < (f z - f y) / (z - y)
<VAR>D : Set ℝ<VAR>hD : Convex ℝ D<VAR>f : ℝ → ℝ<VAR>hf : ContinuousOn f D<VAR>hf' : StrictMonoOn (deriv f) (interior D)<VAR>x y z : ℝ<VAR>hx : x ∈ D<VAR>hz : z ∈ D<VAR>hxy : x < y<VAR>hyz : y < z<VAR>hxzD : Icc x z ⊆ D<VAR>hxyD : Icc x y ⊆ D<VAR>hxyD' : Ioo x y ⊆ interior D<VAR>hyzD : Icc y z ⊆ D<VAR>hyzD' : Ioo y z ⊆ interior D<GOAL>(f y - f x) / (y - x) < (f z - f y) / (z - y)
<VAR>D : Set ℝ<VAR>hD : Convex ℝ D<VAR>f : ℝ → ℝ<VAR>hf : ContinuousOn f D<VAR>hf' : StrictMonoOn (deriv f) (interior D)<VAR>x y z : ℝ<VAR>hx : x ∈ D<VAR>hz : z ∈ D<VAR>hxy : x < y<VAR>hyz : y < z<VAR>hxzD : Icc x z ⊆ D<VAR>hxyD : Icc x y ⊆ D<VAR>hxyD' : Ioo x y ⊆ interior D<VAR>hyzD : Icc y z ⊆ D<VAR>hyzD' : Ioo y z ⊆ interior D<VAR>a : ℝ<VAR>ha : (f y - f x) / (y - x) < deriv f a<VAR>hxa : x < a<VAR>hay : a < y<GOAL>(f y - f x) / (y - x) < (f z - f y) / (z - y)
<VAR>D : Set ℝ<VAR>hD : Convex ℝ D<VAR>f : ℝ → ℝ<VAR>hf : ContinuousOn f D<VAR>hf' : StrictMonoOn (deriv f) (interior D)<VAR>x y z : ℝ<VAR>hx : x ∈ D<VAR>hz : z ∈ D<VAR>hxy : x < y<VAR>hyz : y < z<VAR>hxzD : Icc x z ⊆ D<VAR>hxyD : Icc x y ⊆ D<VAR>hxyD' : Ioo x y ⊆ interior D<VAR>hyzD : Icc y z ⊆ D<VAR>hyzD' : Ioo y z ⊆ interior D<VAR>a : ℝ<VAR>ha : (f y - f x) / (y - x) < deriv f a<VAR>hxa : x < a<VAR>hay : a < y<VAR>b : ℝ<VAR>hb : deriv f b < (f z - f y) / (z - y)<VAR>hyb : y < b<VAR>hbz : b < z<GOAL>(f y - f x) / (y - x) < (f z - f y) / (z - y)
<VAR>D : Set ℝ<VAR>hD : Convex ℝ D<VAR>f : ℝ → ℝ<VAR>hf : ContinuousOn f D<VAR>hf' : StrictMonoOn (deriv f) (interior D)<VAR>x y z : ℝ<VAR>hx : x ∈ D<VAR>hz : z ∈ D<VAR>hxy : x < y<VAR>hyz : y < z<VAR>hxzD : Icc x z ⊆ D<VAR>hxyD : Icc x y ⊆ D<VAR>hxyD' : Ioo x y ⊆ interior D<VAR>hyzD : Icc y z ⊆ D<VAR>hyzD' : Ioo y z ⊆ interior D<VAR>a : ℝ<VAR>ha : (f y - f x) / (y - x) < deriv f a<VAR>hxa : x < a<VAR>hay : a < y<VAR>b : ℝ<VAR>hb : deriv f b < (f z - f y) / (z - y)<VAR>hyb : y < b<VAR>hbz : b < z<GOAL>deriv f a < deriv f b
<VAR>α : Type u<VAR>β : Type v<VAR>f fa g : α → α<VAR>x y : α<VAR>fb : β → β<VAR>m n✝ k : ℕ<VAR>e : Perm α<VAR>s : Set α<VAR>h : IsFixedPt (Set.preimage f) s<VAR>n : ℕ<GOAL>IsFixedPt (Set.preimage f^[n]) s
<VAR>α : Type u<VAR>β : Type v<VAR>f fa g : α → α<VAR>x y : α<VAR>fb : β → β<VAR>m n✝ k : ℕ<VAR>e : Perm α<VAR>s : Set α<VAR>h : IsFixedPt (Set.preimage f) s<VAR>n : ℕ<GOAL>IsFixedPt (Set.preimage f)^[n] s
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Abelian C<VAR>P : C<VAR>f g h : Over P<VAR>R : C<VAR>p : R ⟶ f.left<VAR>q : R ⟶ g.left<VAR>ep : Epi p<VAR>Eq : Epi q<VAR>comm : p ≫ f.hom = q ≫ g.hom<VAR>R' : C<VAR>p' : R' ⟶ g.left<VAR>q' : R' ⟶ h.left<VAR>ep' : Epi p'<VAR>eq' : Epi q'<VAR>comm' : p' ≫ g.hom = q' ≫ h.hom<GOAL>PseudoEqual P f h
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Abelian C<VAR>P : C<VAR>f g h : Over P<VAR>R : C<VAR>p : R ⟶ f.left<VAR>q : R ⟶ g.left<VAR>ep : Epi p<VAR>Eq : Epi q<VAR>comm : p ≫ f.hom = q ≫ g.hom<VAR>R' : C<VAR>p' : R' ⟶ g.left<VAR>q' : R' ⟶ h.left<VAR>ep' : Epi p'<VAR>eq' : Epi q'<VAR>comm' : p' ≫ g.hom = q' ≫ h.hom<GOAL>(pullback.fst q p' ≫ p) ≫ f.hom = (pullback.snd q p' ≫ q') ≫ h.hom
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>σ : Type u_1<VAR>x : MvPolynomial σ R<VAR>i : σ<GOAL>((mvPolynomialBasis R σ).repr ((D R (MvPolynomial σ R)) x)) i = (MvPolynomial.pderiv i) x
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : GeneralizedBooleanAlgebra α<GOAL>x \ (x \ y) = x ⊓ y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>r p q : α → α → Prop<VAR>f g : ι → α<VAR>s t u : Set α<VAR>a b : α<GOAL>(s ∪ t).Pairwise r ↔ s.Pairwise r ∧ t.Pairwise r ∧ ∀ a ∈ s, ∀ b ∈ t, a ≠ b → r a b ∧ r b a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>r p q : α → α → Prop<VAR>f g : ι → α<VAR>s t u : Set α<VAR>a b : α<GOAL>(((∀ x ∈ s, ∀ x_2 ∈ s, x ≠ x_2 → r x x_2) ∧ ∀ x ∈ s, ∀ x_2 ∈ t, x ≠ x_2 → r x x_2) ∧ (∀ x ∈ t, ∀ x_2 ∈ s, x ≠ x_2 → r x x_2) ∧ ∀ x ∈ t, ∀ x_2 ∈ t, x ≠ x_2 → r x x_2) ↔ (∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x ≠ y → r x y) ∧ (∀ ⦃x : α⦄, x ∈ t → ∀ ⦃y : α⦄, y ∈ t → x ≠ y → r x y) ∧ (∀ x ∈ s, ∀ x_2 ∈ t, x ≠ x_2 → r x x_2) ∧ ∀ x ∈ s, ∀ x_2 ∈ t, x ≠ x_2 → r x_2 x
<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>X Y : R<GOAL>W'.Nonsingular ![X, Y, 1] ↔ W'.toAffine.Nonsingular X Y
<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>X Y : R<GOAL>Y ^ 2 + W'.toAffine.a₁ * X * Y + W'.toAffine.a₃ * Y - (X ^ 3 + W'.toAffine.a₂ * X ^ 2 + W'.toAffine.a₄ * X + W'.toAffine.a₆) = 0 → W'.a₁ * Y - (3 * X ^ 2 + 2 * W'.a₂ * X + W'.a₄) = 0 → 2 * Y + W'.toAffine.a₁ * X + W'.toAffine.a₃ = 0 → W'.a₁ * X * Y + 3 * W'.a₃ * Y - (2 * W'.a₂ * X ^ 2 + 4 * W'.a₄ * X + 6 * W'.a₆) = 0
<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>X Y : R<VAR>h : Y ^ 2 + W'.toAffine.a₁ * X * Y + W'.toAffine.a₃ * Y - (X ^ 3 + W'.toAffine.a₂ * X ^ 2 + W'.toAffine.a₄ * X + W'.toAffine.a₆) = 0<VAR>hX : W'.a₁ * Y - (3 * X ^ 2 + 2 * W'.a₂ * X + W'.a₄) = 0<VAR>hY : 2 * Y + W'.toAffine.a₁ * X + W'.toAffine.a₃ = 0<GOAL>W'.a₁ * X * Y + 3 * W'.a₃ * Y - (2 * W'.a₂ * X ^ 2 + 4 * W'.a₄ * X + 6 * W'.a₆) = 0
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>K : Type u_3<VAR>inst✝⁴ : NormedLinearOrderedField K<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace K E<VAR>b : Basis ι K E<VAR>inst✝¹ : FloorRing K<VAR>inst✝ : Fintype ι<VAR>m : E<VAR>h : m ∈ span ℤ (Set.range ⇑b)<GOAL>∀ (i : ι), (b.repr ↑(floor b m)) i = (b.repr m) i
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>K : Type u_3<VAR>inst✝⁴ : NormedLinearOrderedField K<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace K E<VAR>b : Basis ι K E<VAR>inst✝¹ : FloorRing K<VAR>inst✝ : Fintype ι<VAR>m : E<VAR>h : m ∈ span ℤ (Set.range ⇑b)<GOAL>∀ (i : ι), ↑⌊(b.repr m) i⌋ = (b.repr m) i
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>K : Type u_3<VAR>inst✝⁴ : NormedLinearOrderedField K<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace K E<VAR>b : Basis ι K E<VAR>inst✝¹ : FloorRing K<VAR>inst✝ : Fintype ι<VAR>m : E<VAR>h : m ∈ span ℤ (Set.range ⇑b)<VAR>i : ι<GOAL>↑⌊(b.repr m) i⌋ = (b.repr m) i
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>K : Type u_3<VAR>inst✝⁴ : NormedLinearOrderedField K<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace K E<VAR>b : Basis ι K E<VAR>inst✝¹ : FloorRing K<VAR>inst✝ : Fintype ι<VAR>m : E<VAR>h : m ∈ span ℤ (Set.range ⇑b)<VAR>i : ι<VAR>z : ℤ<VAR>hz : (algebraMap ℤ K) z = (b.repr m) i<GOAL>↑⌊(b.repr m) i⌋ = (b.repr m) i
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>K : Type u_3<VAR>inst✝⁴ : NormedLinearOrderedField K<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace K E<VAR>b : Basis ι K E<VAR>inst✝¹ : FloorRing K<VAR>inst✝ : Fintype ι<VAR>m : E<VAR>h : m ∈ span ℤ (Set.range ⇑b)<VAR>i : ι<VAR>z : ℤ<VAR>hz : (algebraMap ℤ K) z = (b.repr m) i<GOAL>↑⌊(algebraMap ℤ K) z⌋ = (algebraMap ℤ K) z
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.112486, u_1} C<VAR>inst✝ : Abelian C<VAR>S S₁ S₂ S₃ : SnakeInput C<VAR>f : S₁.Hom S₂<VAR>g : S₂.Hom S₃<GOAL>(f.f₀ ≫ g.f₀) ≫ S₃.v₀₁ = S₁.v₀₁ ≫ f.f₁ ≫ g.f₁
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.112486, u_1} C<VAR>inst✝ : Abelian C<VAR>S S₁ S₂ S₃ : SnakeInput C<VAR>f : S₁.Hom S₂<VAR>g : S₂.Hom S₃<GOAL>(f.f₁ ≫ g.f₁) ≫ S₃.v₁₂ = S₁.v₁₂ ≫ f.f₂ ≫ g.f₂
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.112486, u_1} C<VAR>inst✝ : Abelian C<VAR>S S₁ S₂ S₃ : SnakeInput C<VAR>f : S₁.Hom S₂<VAR>g : S₂.Hom S₃<GOAL>(f.f₂ ≫ g.f₂) ≫ S₃.v₂₃ = S₁.v₂₃ ≫ f.f₃ ≫ g.f₃
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E : Type u_4<VAR>Eₗ : Type u_5<VAR>F : Type u_6<VAR>Fₗ : Type u_7<VAR>G : Type u_8<VAR>Gₗ : Type u_9<VAR>𝓕 : Type u_10<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedAddCommGroup F<VAR>inst✝¹¹ : NormedAddCommGroup G<VAR>inst✝¹⁰ : NormedAddCommGroup Fₗ<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NontriviallyNormedField 𝕜₂<VAR>inst✝⁷ : NontriviallyNormedField 𝕜₃<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedSpace 𝕜₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₁ : 𝕜₂ →+* 𝕜<VAR>inst✝⁴ : RingHomInvPair σ₁₂ σ₂₁<VAR>inst✝³ : RingHomInvPair σ₂₁ σ₁₂<VAR>inst✝² : RingHomIsometric σ₂₁<VAR>inst✝¹ : RingHomIsometric σ₁₂<VAR>inst✝ : Nontrivial E<VAR>e : E ≃SL[σ₁₂] F<GOAL>1 ≤ ‖↑e‖ * ‖↑e.symm‖
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E : Type u_4<VAR>Eₗ : Type u_5<VAR>F : Type u_6<VAR>Fₗ : Type u_7<VAR>G : Type u_8<VAR>Gₗ : Type u_9<VAR>𝓕 : Type u_10<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedAddCommGroup F<VAR>inst✝¹¹ : NormedAddCommGroup G<VAR>inst✝¹⁰ : NormedAddCommGroup Fₗ<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NontriviallyNormedField 𝕜₂<VAR>inst✝⁷ : NontriviallyNormedField 𝕜₃<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedSpace 𝕜₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₁ : 𝕜₂ →+* 𝕜<VAR>inst✝⁴ : RingHomInvPair σ₁₂ σ₂₁<VAR>inst✝³ : RingHomInvPair σ₂₁ σ₁₂<VAR>inst✝² : RingHomIsometric σ₂₁<VAR>inst✝¹ : RingHomIsometric σ₁₂<VAR>inst✝ : Nontrivial E<VAR>e : E ≃SL[σ₁₂] F<GOAL>1 ≤ ‖↑e.symm‖ * ‖↑e‖
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E : Type u_4<VAR>Eₗ : Type u_5<VAR>F : Type u_6<VAR>Fₗ : Type u_7<VAR>G : Type u_8<VAR>Gₗ : Type u_9<VAR>𝓕 : Type u_10<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedAddCommGroup F<VAR>inst✝¹¹ : NormedAddCommGroup G<VAR>inst✝¹⁰ : NormedAddCommGroup Fₗ<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NontriviallyNormedField 𝕜₂<VAR>inst✝⁷ : NontriviallyNormedField 𝕜₃<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedSpace 𝕜₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₁ : 𝕜₂ →+* 𝕜<VAR>inst✝⁴ : RingHomInvPair σ₁₂ σ₂₁<VAR>inst✝³ : RingHomInvPair σ₂₁ σ₁₂<VAR>inst✝² : RingHomIsometric σ₂₁<VAR>inst✝¹ : RingHomIsometric σ₁₂<VAR>inst✝ : Nontrivial E<VAR>e : E ≃SL[σ₁₂] F<GOAL>1 = ‖(↑e.symm).comp ↑e‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>l✝ m : Language α<VAR>a b x✝ : List α<VAR>l : Language α<VAR>x : List α<GOAL>x ∈ l∗ ↔ x ∈ {x | ∃ S, x = S.join ∧ ∀ y ∈ S, y ∈ l ∧ y ≠ []}
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁷ : NormedAddCommGroup D<VAR>inst✝⁶ : NormedSpace 𝕜 D<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>s✝ s₁ t u : Set E<VAR>f : E → F →L[𝕜] G<VAR>c : F<VAR>s : Set E<VAR>x : E<VAR>N : ℕ∞<VAR>n : ℕ<VAR>hf : ContDiffOn 𝕜 N f s<VAR>hs : UniqueDiffOn 𝕜 s<VAR>hx : x ∈ s<VAR>hn : ↑n ≤ N<VAR>g : (F →L[𝕜] G) →L[𝕜] G := (ContinuousLinearMap.apply 𝕜 G) c<GOAL>‖iteratedFDerivWithin 𝕜 n (fun y => (f y) c) s x‖ ≤ ‖c‖ * ‖iteratedFDerivWithin 𝕜 n f s x‖
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁷ : NormedAddCommGroup D<VAR>inst✝⁶ : NormedSpace 𝕜 D<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>s✝ s₁ t u : Set E<VAR>f : E → F →L[𝕜] G<VAR>c : F<VAR>s : Set E<VAR>x : E<VAR>N : ℕ∞<VAR>n : ℕ<VAR>hf : ContDiffOn 𝕜 N f s<VAR>hs : UniqueDiffOn 𝕜 s<VAR>hx : x ∈ s<VAR>hn : ↑n ≤ N<VAR>g : (F →L[𝕜] G) →L[𝕜] G := (ContinuousLinearMap.apply 𝕜 G) c<VAR>h : ‖g.compContinuousMultilinearMap (iteratedFDerivWithin 𝕜 n f s x)‖ ≤ ‖g‖ * ‖iteratedFDerivWithin 𝕜 n f s x‖<GOAL>‖iteratedFDerivWithin 𝕜 n (fun y => (f y) c) s x‖ ≤ ‖c‖ * ‖iteratedFDerivWithin 𝕜 n f s x‖
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁷ : NormedAddCommGroup D<VAR>inst✝⁶ : NormedSpace 𝕜 D<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>s✝ s₁ t u : Set E<VAR>f : E → F →L[𝕜] G<VAR>c : F<VAR>s : Set E<VAR>x : E<VAR>N : ℕ∞<VAR>n : ℕ<VAR>hf : ContDiffOn 𝕜 N f s<VAR>hs : UniqueDiffOn 𝕜 s<VAR>hx : x ∈ s<VAR>hn : ↑n ≤ N<VAR>g : (F →L[𝕜] G) →L[𝕜] G := (ContinuousLinearMap.apply 𝕜 G) c<VAR>h : ‖iteratedFDerivWithin 𝕜 n (⇑g ∘ f) s x‖ ≤ ‖g‖ * ‖iteratedFDerivWithin 𝕜 n f s x‖<GOAL>‖iteratedFDerivWithin 𝕜 n (fun y => (f y) c) s x‖ ≤ ‖c‖ * ‖iteratedFDerivWithin 𝕜 n f s x‖
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁷ : NormedAddCommGroup D<VAR>inst✝⁶ : NormedSpace 𝕜 D<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>s✝ s₁ t u : Set E<VAR>f : E → F →L[𝕜] G<VAR>c : F<VAR>s : Set E<VAR>x : E<VAR>N : ℕ∞<VAR>n : ℕ<VAR>hf : ContDiffOn 𝕜 N f s<VAR>hs : UniqueDiffOn 𝕜 s<VAR>hx : x ∈ s<VAR>hn : ↑n ≤ N<VAR>g : (F →L[𝕜] G) →L[𝕜] G := (ContinuousLinearMap.apply 𝕜 G) c<VAR>h : ‖iteratedFDerivWithin 𝕜 n (⇑g ∘ f) s x‖ ≤ ‖g‖ * ‖iteratedFDerivWithin 𝕜 n f s x‖<GOAL>‖g‖ ≤ ‖c‖
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁷ : NormedAddCommGroup D<VAR>inst✝⁶ : NormedSpace 𝕜 D<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>s✝ s₁ t u : Set E<VAR>f✝ : E → F →L[𝕜] G<VAR>c : F<VAR>s : Set E<VAR>x : E<VAR>N : ℕ∞<VAR>n : ℕ<VAR>hf : ContDiffOn 𝕜 N f✝ s<VAR>hs : UniqueDiffOn 𝕜 s<VAR>hx : x ∈ s<VAR>hn : ↑n ≤ N<VAR>g : (F →L[𝕜] G) →L[𝕜] G := (ContinuousLinearMap.apply 𝕜 G) c<VAR>h : ‖iteratedFDerivWithin 𝕜 n (⇑g ∘ f✝) s x‖ ≤ ‖g‖ * ‖iteratedFDerivWithin 𝕜 n f✝ s x‖<VAR>f : F →L[𝕜] G<GOAL>‖g f‖ ≤ ‖c‖ * ‖f‖
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁷ : NormedAddCommGroup D<VAR>inst✝⁶ : NormedSpace 𝕜 D<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>s✝ s₁ t u : Set E<VAR>f✝ : E → F →L[𝕜] G<VAR>c : F<VAR>s : Set E<VAR>x : E<VAR>N : ℕ∞<VAR>n : ℕ<VAR>hf : ContDiffOn 𝕜 N f✝ s<VAR>hs : UniqueDiffOn 𝕜 s<VAR>hx : x ∈ s<VAR>hn : ↑n ≤ N<VAR>g : (F →L[𝕜] G) →L[𝕜] G := (ContinuousLinearMap.apply 𝕜 G) c<VAR>h : ‖iteratedFDerivWithin 𝕜 n (⇑g ∘ f✝) s x‖ ≤ ‖g‖ * ‖iteratedFDerivWithin 𝕜 n f✝ s x‖<VAR>f : F →L[𝕜] G<GOAL>‖f c‖ ≤ ‖f‖ * ‖c‖
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>x y : α<VAR>s t : Set α<VAR>Φ : α → β<GOAL>infEdist x s ≤ edist x y + infEdist y s
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>x y : α<VAR>s t : Set α<VAR>Φ : α → β<GOAL>infEdist x s ≤ infEdist y s + edist x y
<VAR>a b : ℝ<GOAL>(polynomialFunctions (Set.Icc a b)).topologicalClosure = ⊤
<VAR>a b : ℝ<VAR>h : a < b<GOAL>(polynomialFunctions (Set.Icc a b)).topologicalClosure = ⊤
<VAR>a b : ℝ<VAR>h : b ≤ a<GOAL>(polynomialFunctions (Set.Icc a b)).topologicalClosure = ⊤
<VAR>α : Type u_1<VAR>inst✝⁴ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝³ : PseudoEMetricSpace E<VAR>V : Type u_3<VAR>inst✝² : NormedAddCommGroup V<VAR>inst✝¹ : NormedSpace ℝ V<VAR>inst✝ : FiniteDimensional ℝ V<VAR>f : ℝ → ℝ<VAR>s : Set ℝ<VAR>h : LocallyBoundedVariationOn f s<GOAL>∀ᵐ (x : ℝ), x ∈ s → DifferentiableWithinAt ℝ f s x
<VAR>α : Type u_1<VAR>inst✝⁴ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝³ : PseudoEMetricSpace E<VAR>V : Type u_3<VAR>inst✝² : NormedAddCommGroup V<VAR>inst✝¹ : NormedSpace ℝ V<VAR>inst✝ : FiniteDimensional ℝ V<VAR>s : Set ℝ<VAR>p q : ℝ → ℝ<VAR>hp : MonotoneOn p s<VAR>hq : MonotoneOn q s<VAR>h : LocallyBoundedVariationOn (p - q) s<GOAL>∀ᵐ (x : ℝ), x ∈ s → DifferentiableWithinAt ℝ (p - q) s x
<VAR>α : Type u_1<VAR>inst✝⁴ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝³ : PseudoEMetricSpace E<VAR>V : Type u_3<VAR>inst✝² : NormedAddCommGroup V<VAR>inst✝¹ : NormedSpace ℝ V<VAR>inst✝ : FiniteDimensional ℝ V<VAR>s : Set ℝ<VAR>p q : ℝ → ℝ<VAR>hp : MonotoneOn p s<VAR>hq : MonotoneOn q s<VAR>h : LocallyBoundedVariationOn (p - q) s<VAR>x : ℝ<VAR>hxp : x ∈ s → DifferentiableWithinAt ℝ p s x<VAR>hxq : x ∈ s → DifferentiableWithinAt ℝ q s x<VAR>xs : x ∈ s<GOAL>DifferentiableWithinAt ℝ (p - q) s x
<VAR>α : Type u_1<VAR>p q : α → Bool<VAR>l₁ l₂ : List α<GOAL>countP p (l₁ ++ l₂) = countP p l₁ + countP p l₂
<VAR>α : Type u_1<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : UniqueFactorizationMonoid α<VAR>inst✝ : DecidableEq α<VAR>x : α<VAR>hx : x ≠ 0<GOAL>∏ p ∈ (factors x).toFinset, p ^ count p (factors x) = (∑ a ∈ (factors x).toFinset, count a (factors x) • {a}).prod
<VAR>α : Type u_1<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : UniqueFactorizationMonoid α<VAR>inst✝ : DecidableEq α<VAR>x : α<VAR>hx : x ≠ 0<GOAL>(∑ a ∈ (factors x).toFinset, count a (factors x) • {a}).prod = (factors x).prod
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x✝ y z : α<VAR>δ ε✝ ε₁ ε₂ : ℝ<VAR>s✝ s : Set α<VAR>hs : Dense s<VAR>x : α<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>this : (ball x ε).Nonempty<GOAL>∃ y ∈ s, dist x y < ε
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : NormalizedGCDMonoid α<VAR>s s₁ s₂ : Finset β<VAR>f : β → α<VAR>inst✝ : DecidableEq β<GOAL>(∅ ∪ s₂).gcd f = GCDMonoid.gcd (∅.gcd f) (s₂.gcd f)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : NormalizedGCDMonoid α<VAR>s✝ s₁ s₂ : Finset β<VAR>f : β → α<VAR>inst✝ : DecidableEq β<VAR>a : β<VAR>s : Finset β<VAR>x✝ : a ∉ s<VAR>ih : (s ∪ s₂).gcd f = GCDMonoid.gcd (s.gcd f) (s₂.gcd f)<GOAL>(insert a s ∪ s₂).gcd f = GCDMonoid.gcd ((insert a s).gcd f) (s₂.gcd f)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>inst✝¹ : Finite ι<VAR>inst✝ : Finite ι'<VAR>C : (i : ι) → Set (Set (α i))<VAR>s : (i : ι) → ℕ → Set (α i)<VAR>h1s : ∀ (i : ι) (n : ℕ), s i n ∈ C i<VAR>h2s : ∀ (i : ι), ⋃ n, s i n = univ<GOAL>IsCountablySpanning (univ.pi '' univ.pi C)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>inst✝¹ : Finite ι<VAR>inst✝ : Finite ι'<VAR>C : (i : ι) → Set (Set (α i))<VAR>s : (i : ι) → ℕ → Set (α i)<VAR>h1s : ∀ (i : ι) (n : ℕ), s i n ∈ C i<VAR>h2s : ∀ (i : ι), ⋃ n, s i n = univ<VAR>val✝ : Encodable (ι → ℕ)<GOAL>IsCountablySpanning (univ.pi '' univ.pi C)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>inst✝¹ : Finite ι<VAR>inst✝ : Finite ι'<VAR>C : (i : ι) → Set (Set (α i))<VAR>s : (i : ι) → ℕ → Set (α i)<VAR>h1s : ∀ (i : ι) (n : ℕ), s i n ∈ C i<VAR>h2s : ∀ (i : ι), ⋃ n, s i n = univ<VAR>val✝ : Encodable (ι → ℕ)<VAR>e : ℕ → ι → ℕ := fun n => (decode n).iget<GOAL>IsCountablySpanning (univ.pi '' univ.pi C)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>inst✝¹ : Finite ι<VAR>inst✝ : Finite ι'<VAR>C : (i : ι) → Set (Set (α i))<VAR>s : (i : ι) → ℕ → Set (α i)<VAR>h1s : ∀ (i : ι) (n : ℕ), s i n ∈ C i<VAR>h2s : ∀ (i : ι), ⋃ n, s i n = univ<VAR>val✝ : Encodable (ι → ℕ)<VAR>e : ℕ → ι → ℕ := fun n => (decode n).iget<GOAL>⋃ n, (fun n => univ.pi fun i => s i (e n i)) n = univ
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>x : ℤ<GOAL>house ↑x = ↑|x|
<VAR>R : Type u_1<VAR>inst✝ : NonUnitalNonAssocRing R<VAR>I✝ I J : TwoSidedIdeal R<GOAL>I < J ↔ ↑I ⊂ ↑J