ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝¹⁰ : _root_.RCLike 𝕜<VAR>E : Type u_4<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : InnerProductSpace 𝕜 E<VAR>E' : Type u_5<VAR>inst✝⁷ : NormedAddCommGroup E'<VAR>inst✝⁶ : InnerProductSpace 𝕜 E'<VAR>F : Type u_6<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : InnerProductSpace ℝ F<VAR>F' : Type u_7<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : InnerProductSpace ℝ F'<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<GOAL>ι → ι → True
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m✝ m0 : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>s t : Set α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>f g : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>hg : AEMeasurable g μ<VAR>hfi : ∫⁻ (x : α), f x ∂μ ≠ ⊤<VAR>hfg : μ.withDensity f = μ.withDensity g<GOAL>f =ᶠ[ae μ] g
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m✝ m0 : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>s t : Set α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>f g : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>hg : AEMeasurable g μ<VAR>hfi : ∫⁻ (x : α), f x ∂μ ≠ ⊤<VAR>hfg : μ.withDensity f = μ.withDensity g<GOAL>∫⁻ (x : α), g x ∂μ ≠ ⊤
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m✝ m0 : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>s✝ t : Set α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>f g : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>hg : AEMeasurable g μ<VAR>hfi : ∫⁻ (x : α), f x ∂μ ≠ ⊤<VAR>hfg : μ.withDensity f = μ.withDensity g<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>x✝ : μ s < ⊤<GOAL>∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ
<VAR>A : Type u_1<VAR>A' : Type u_2<VAR>B : Type u_3<VAR>B' : Type u_4<VAR>inst✝³ : Category.{u_6, u_1} A<VAR>inst✝² : Category.{u_5, u_2} A'<VAR>inst✝¹ : Category.{u_8, u_3} B<VAR>inst✝ : Category.{u_7, u_4} B'<VAR>eA : A ≌ A'<VAR>eB : B ≌ B'<VAR>e' : A' ≌ B'<VAR>F : A ⥤ B'<VAR>hF : eA.functor ⋙ e'.functor ≅ F<VAR>G : B ⥤ A<VAR>hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor<VAR>η : G ⋙ F ≅ eB.functor<VAR>ε : eA.functor ≅ F ⋙ e'.inverse<VAR>hε : υ hF = ε<VAR>X : A<GOAL>(equivalence₂ eB hF).unitIso.hom.app X ≫ ((𝟙 (eA.inverse.obj (e'.inverse.obj (eB.functor.obj (eB.inverse.obj (F.obj X))))) ≫ eA.inverse.map (hG.hom.app (eB.inverse.obj (F.obj X)))) ≫ eA.unitIso.inv.app (G.obj (eB.inverse.obj (F.obj X)))) ≫ 𝟙 (G.obj (eB.inverse.obj (F.obj X))) = (equivalenceUnitIso hG ε).hom.app X
<VAR>A : Type u_1<VAR>A' : Type u_2<VAR>B : Type u_3<VAR>B' : Type u_4<VAR>inst✝³ : Category.{u_6, u_1} A<VAR>inst✝² : Category.{u_5, u_2} A'<VAR>inst✝¹ : Category.{u_8, u_3} B<VAR>inst✝ : Category.{u_7, u_4} B'<VAR>eA : A ≌ A'<VAR>eB : B ≌ B'<VAR>e' : A' ≌ B'<VAR>F : A ⥤ B'<VAR>hF : eA.functor ⋙ e'.functor ≅ F<VAR>G : B ⥤ A<VAR>hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor<VAR>η : G ⋙ F ≅ eB.functor<VAR>ε : eA.functor ≅ F ⋙ e'.inverse<VAR>hε : υ hF = ε<VAR>X : A<GOAL>(equivalence₂ eB hF).unitIso.hom.app X ≫ 𝟙 (eA.inverse.obj (e'.inverse.obj (eB.functor.obj (eB.inverse.obj (F.obj X))))) ≫ eA.inverse.map (hG.hom.app (eB.inverse.obj (F.obj X))) ≫ eA.unitIso.inv.app (G.obj (eB.inverse.obj (F.obj X))) = eA.unitIso.hom.app X ≫ eA.inverse.map (ε.hom.app X) ≫ eA.inverse.map (e'.inverse.map (eB.counitIso.inv.app (F.obj X))) ≫ eA.inverse.map (hG.hom.app (eB.inverse.obj (F.obj X))) ≫ eA.unitIso.inv.app (G.obj (eB.inverse.obj (F.obj X)))
<VAR>A : Type u_1<VAR>A' : Type u_2<VAR>B : Type u_3<VAR>B' : Type u_4<VAR>inst✝³ : Category.{u_6, u_1} A<VAR>inst✝² : Category.{u_5, u_2} A'<VAR>inst✝¹ : Category.{u_8, u_3} B<VAR>inst✝ : Category.{u_7, u_4} B'<VAR>eA : A ≌ A'<VAR>eB : B ≌ B'<VAR>e' : A' ≌ B'<VAR>F : A ⥤ B'<VAR>hF : eA.functor ⋙ e'.functor ≅ F<VAR>G : B ⥤ A<VAR>hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor<VAR>η : G ⋙ F ≅ eB.functor<VAR>ε : eA.functor ≅ F ⋙ e'.inverse<VAR>hε : υ hF = ε<VAR>X : A<GOAL>(equivalence₂ eB hF).unitIso.hom.app X ≫ eA.inverse.map (hG.hom.app (eB.inverse.obj (F.obj X))) ≫ eA.unitIso.inv.app (G.obj (eB.inverse.obj (F.obj X))) = eA.unitIso.hom.app X ≫ eA.inverse.map (ε.hom.app X) ≫ eA.inverse.map (e'.inverse.map (eB.counitIso.inv.app (F.obj X))) ≫ eA.inverse.map (hG.hom.app (eB.inverse.obj (F.obj X))) ≫ eA.unitIso.inv.app (G.obj (eB.inverse.obj (F.obj X)))
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Ring S<VAR>f : R[X]<VAR>inst✝ : Algebra R S<VAR>h : IsAdjoinRootMonic S f<VAR>z : S<VAR>i : ℕ<VAR>hi : i < f.natDegree<GOAL>h.coeff z i = (h.basis.repr z) ⟨i, hi⟩
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Ring S<VAR>f : R[X]<VAR>inst✝ : Algebra R S<VAR>h : IsAdjoinRootMonic S f<VAR>z : S<VAR>i : ℕ<VAR>hi : i < f.natDegree<GOAL>{ toFun := Polynomial.coeff, map_add' := ⋯ } (h.modByMonicHom z) i = (h.modByMonicHom z).coeff i
<VAR>I : Type u<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f✝ : I → Type v₁<VAR>g✝ : I → Type v₂<VAR>h : I → Type v₃<VAR>x y : (i : I) → f✝ i<VAR>i : I<VAR>inst✝¹ : One β<VAR>inst✝ : One γ<VAR>f : α → β<VAR>g : β → γ<VAR>hg : Injective g<VAR>hg0 : g 1 = 1<GOAL>g ∘ f = 1 ↔ f = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : SizeOf α<VAR>x : α<VAR>val✝ : Multiset α<VAR>nodup✝ : val✝.Nodup<VAR>hx : x ∈ { val := val✝, nodup := nodup✝ }<GOAL>sizeOf x < 1 + Quot.liftOn val✝ (fun m => m._sizeOf_1) ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : SizeOf α<VAR>x : α<VAR>val✝ : Multiset α<VAR>nodup✝ : val✝.Nodup<VAR>hx : x ∈ { val := val✝, nodup := nodup✝ }<GOAL>sizeOf x < Quot.liftOn val✝ (fun m => m._sizeOf_1) ⋯ + 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : SizeOf α<VAR>x : α<VAR>val✝ : Multiset α<VAR>nodup✝ : val✝.Nodup<VAR>hx : x ∈ { val := val✝, nodup := nodup✝ }<GOAL>sizeOf x < Quot.liftOn val✝ (fun m => m._sizeOf_1) ⋯
<VAR>P : AffineTargetMorphismProperty<VAR>inst✝² : P.toProperty.RespectsIso<VAR>X Y Z : Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>inst✝¹ : IsIso f<VAR>inst✝ : IsAffine Z<GOAL>P (f ≫ g) ↔ P g
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedSemiring α<VAR>inst✝ : FloorSemiring α<VAR>a✝ : α<VAR>n✝ n a : ℕ<GOAL>a ≤ ⌊↑n⌋₊ ↔ a ≤ n
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedSemiring α<VAR>inst✝ : FloorSemiring α<VAR>a✝ : α<VAR>n✝ n a : ℕ<GOAL>0 ≤ ↑n
<VAR>R : Type u<VAR>inst✝¹ : CommSemiring R<VAR>S : Type v<VAR>inst✝ : CommSemiring S<VAR>p q : ℕ<VAR>f : R[X]<VAR>hp : p ≠ 0<VAR>n✝ : ℕ<GOAL>(contract p ((expand R p) f)).coeff n✝ = f.coeff n✝
<VAR>𝕜 : Type u_1<VAR>inst✝⁵ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝² : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : ChartedSpace H M<GOAL>Disjoint (I.interior M) (I.boundary M)
<VAR>𝕜 : Type u_1<VAR>inst✝⁵ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝² : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : ChartedSpace H M<VAR>h : ¬Disjoint (I.interior M) (I.boundary M)<GOAL>False
<VAR>𝕜 : Type u_1<VAR>inst✝⁵ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝² : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : ChartedSpace H M<VAR>h : ¬Disjoint (I.interior M) (I.boundary M)<VAR>x : M<VAR>h1 : x ∈ I.interior M<VAR>h2 : x ∈ I.boundary M<GOAL>False
<VAR>𝕜 : Type u_1<VAR>inst✝⁵ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝² : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : ChartedSpace H M<VAR>h : ¬Disjoint (I.interior M) (I.boundary M)<VAR>x : M<VAR>h1 : x ∈ I.interior M<VAR>h2 : x ∈ I.boundary M<GOAL>↑(extChartAt I x) x ∈ interior (range ↑I) ∧ ↑(extChartAt I x) x ∈ frontier (range ↑I)
<VAR>D : Set ℝ<VAR>hD : Convex ℝ D<VAR>f : ℝ → ℝ<VAR>hf : ContinuousOn f D<VAR>h_anti : StrictAntiOn (deriv f) (interior D)<GOAL>StrictMonoOn (deriv (-f)) (interior D)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedField α<VAR>a b c d : α<VAR>n : ℤ<VAR>h : b ≤ a<VAR>hb : b ≤ 0<GOAL>a / b ≤ 1
<VAR>k : Type u_1<VAR>E : Type u_2<VAR>PE : Type u_3<VAR>inst✝³ : OrderedRing k<VAR>inst✝² : OrderedAddCommGroup E<VAR>inst✝¹ : Module k E<VAR>inst✝ : OrderedSMul k E<VAR>a a' b b' : E<VAR>r r' : k<VAR>hb : b < b'<VAR>hr : 0 < r<GOAL>(lineMap a b) r < (lineMap a b') r
<VAR>k : Type u_1<VAR>E : Type u_2<VAR>PE : Type u_3<VAR>inst✝³ : OrderedRing k<VAR>inst✝² : OrderedAddCommGroup E<VAR>inst✝¹ : Module k E<VAR>inst✝ : OrderedSMul k E<VAR>a a' b b' : E<VAR>r r' : k<VAR>hb : b < b'<VAR>hr : 0 < r<GOAL>(1 - r) • a + r • b < (1 - r) • a + r • b'
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>F F' F'' : Cᵒᵖ ⥤ Type w<VAR>G G' : Subpresheaf F<VAR>U : Cᵒᵖ<VAR>s : F.obj U<VAR>Y₁ Y₂ Z : C<VAR>g₁ : Z ⟶ Y₁<VAR>g₂ : Z ⟶ Y₂<VAR>f₁ : Y₁ ⟶ unop U<VAR>f₂ : Y₂ ⟶ unop U<VAR>h₁ : (G.sieveOfSection s).arrows f₁<VAR>h₂ : (G.sieveOfSection s).arrows f₂<VAR>e : g₁ ≫ f₁ = g₂ ≫ f₂<GOAL>G.toPresheaf.map g₁.op (G.familyOfElementsOfSection s f₁ h₁) = G.toPresheaf.map g₂.op (G.familyOfElementsOfSection s f₂ h₂)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>F F' F'' : Cᵒᵖ ⥤ Type w<VAR>G G' : Subpresheaf F<VAR>U : Cᵒᵖ<VAR>s : F.obj U<VAR>Y₁ Y₂ Z : C<VAR>g₁ : Z ⟶ Y₁<VAR>g₂ : Z ⟶ Y₂<VAR>f₁ : Y₁ ⟶ unop U<VAR>f₂ : Y₂ ⟶ unop U<VAR>h₁ : (G.sieveOfSection s).arrows f₁<VAR>h₂ : (G.sieveOfSection s).arrows f₂<VAR>e : g₁ ≫ f₁ = g₂ ≫ f₂<GOAL>↑(G.toPresheaf.map g₁.op (G.familyOfElementsOfSection s f₁ h₁)) = ↑(G.toPresheaf.map g₂.op (G.familyOfElementsOfSection s f₂ h₂))
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>F F' F'' : Cᵒᵖ ⥤ Type w<VAR>G G' : Subpresheaf F<VAR>U : Cᵒᵖ<VAR>s : F.obj U<VAR>Y₁ Y₂ Z : C<VAR>g₁ : Z ⟶ Y₁<VAR>g₂ : Z ⟶ Y₂<VAR>f₁ : Y₁ ⟶ unop U<VAR>f₂ : Y₂ ⟶ unop U<VAR>h₁ : (G.sieveOfSection s).arrows f₁<VAR>h₂ : (G.sieveOfSection s).arrows f₂<VAR>e : g₁ ≫ f₁ = g₂ ≫ f₂<GOAL>F.map g₁.op (F.map f₁.op s) = F.map g₂.op (F.map f₂.op s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Finset α<VAR>p : Option α → Prop<GOAL>(∀ a ∈ insertNone s, p a) ↔ p none ∧ ∀ a ∈ s, p (some a)
<VAR>R : Type u_1<VAR>inst✝¹ : LinearOrderedSemifield R<VAR>inst✝ : FloorSemiring R<VAR>b : ℕ<VAR>r₁ r₂ : R<VAR>h₀ : 0 < r₁<VAR>h : r₁ ≤ r₂<GOAL>clog b r₁ ≤ clog b r₂
<VAR>R : Type u_1<VAR>inst✝¹ : LinearOrderedSemifield R<VAR>inst✝ : FloorSemiring R<VAR>b : ℕ<VAR>r₁ r₂ : R<VAR>h₀ : 0 < r₁<VAR>h : r₁ ≤ r₂<GOAL>log b r₂⁻¹ ≤ log b r₁⁻¹
<VAR>G : Type u<VAR>inst✝¹ : Monoid G<VAR>inst✝ : Fintype G<GOAL>Finset.univ.lcm orderOf ∣ exponent G
<VAR>G : Type u<VAR>inst✝¹ : Monoid G<VAR>inst✝ : Fintype G<GOAL>∀ b ∈ Finset.univ, orderOf b ∣ exponent G
<VAR>G : Type u<VAR>inst✝¹ : Monoid G<VAR>inst✝ : Fintype G<VAR>g : G<VAR>a✝ : g ∈ Finset.univ<GOAL>orderOf g ∣ exponent G
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>a b : α<VAR>h : Acc r a<GOAL>h.rank = sup fun b => succ ⋯.rank
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>a b : α<VAR>h : Acc r a<GOAL>⋯.rank = sup fun b => succ ⋯.rank
<VAR>E : Type u_1<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace ℂ E<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℂ F<VAR>H : Type u_3<VAR>inst✝⁵ : TopologicalSpace H<VAR>I : ModelWithCorners ℂ E H<VAR>inst✝⁴ : I.Boundaryless<VAR>M : Type u_4<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : CompactSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>f : M → F<VAR>U : Set M<VAR>c : M<VAR>hd : MDifferentiableOn I 𝓘(ℂ, F) f U<VAR>hc : IsPreconnected U<VAR>ho : IsOpen U<VAR>hcU : c ∈ U<VAR>hm : IsMaxOn (norm ∘ f) U c<VAR>V : Set M := {z | z ∈ U ∧ ‖f z‖ = ‖f c‖}<GOAL>EqOn (norm ∘ f) (const M ‖f c‖) U
<VAR>E : Type u_1<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace ℂ E<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℂ F<VAR>H : Type u_3<VAR>inst✝⁵ : TopologicalSpace H<VAR>I : ModelWithCorners ℂ E H<VAR>inst✝⁴ : I.Boundaryless<VAR>M : Type u_4<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : CompactSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>f : M → F<VAR>U : Set M<VAR>c : M<VAR>hd : MDifferentiableOn I 𝓘(ℂ, F) f U<VAR>hc : IsPreconnected U<VAR>ho : IsOpen U<VAR>hcU : c ∈ U<VAR>hm : IsMaxOn (norm ∘ f) U c<VAR>V : Set M := {z | z ∈ U ∧ ‖f z‖ = ‖f c‖}<GOAL>U ⊆ V
<VAR>E : Type u_1<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace ℂ E<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℂ F<VAR>H : Type u_3<VAR>inst✝⁵ : TopologicalSpace H<VAR>I : ModelWithCorners ℂ E H<VAR>inst✝⁴ : I.Boundaryless<VAR>M : Type u_4<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : CompactSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>f : M → F<VAR>U : Set M<VAR>c : M<VAR>hd : MDifferentiableOn I 𝓘(ℂ, F) f U<VAR>hc : IsPreconnected U<VAR>ho : IsOpen U<VAR>hcU : c ∈ U<VAR>hm : IsMaxOn (norm ∘ f) U c<VAR>V : Set M := {z | z ∈ U ∧ ‖f z‖ = ‖f c‖}<VAR>hVo : IsOpen V<VAR>hVne : (U ∩ V).Nonempty<VAR>W : Set M := U ∩ {z | ‖f z‖ = ‖f c‖}ᶜ<GOAL>U ⊆ V
<VAR>E : Type u_1<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace ℂ E<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℂ F<VAR>H : Type u_3<VAR>inst✝⁵ : TopologicalSpace H<VAR>I : ModelWithCorners ℂ E H<VAR>inst✝⁴ : I.Boundaryless<VAR>M : Type u_4<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : CompactSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>f : M → F<VAR>U : Set M<VAR>c : M<VAR>hd : MDifferentiableOn I 𝓘(ℂ, F) f U<VAR>hc : IsPreconnected U<VAR>ho : IsOpen U<VAR>hcU : c ∈ U<VAR>hm : IsMaxOn (norm ∘ f) U c<VAR>V : Set M := {z | z ∈ U ∧ ‖f z‖ = ‖f c‖}<VAR>hVo : IsOpen V<VAR>hVne : (U ∩ V).Nonempty<VAR>W : Set M := U ∩ {z | ‖f z‖ = ‖f c‖}ᶜ<VAR>hWo : IsOpen W<GOAL>U ⊆ V
<VAR>E : Type u_1<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace ℂ E<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℂ F<VAR>H : Type u_3<VAR>inst✝⁵ : TopologicalSpace H<VAR>I : ModelWithCorners ℂ E H<VAR>inst✝⁴ : I.Boundaryless<VAR>M : Type u_4<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : CompactSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>f : M → F<VAR>U : Set M<VAR>c : M<VAR>hd : MDifferentiableOn I 𝓘(ℂ, F) f U<VAR>hc : IsPreconnected U<VAR>ho : IsOpen U<VAR>hcU : c ∈ U<VAR>hm : IsMaxOn (norm ∘ f) U c<VAR>V : Set M := {z | z ∈ U ∧ ‖f z‖ = ‖f c‖}<VAR>hVo : IsOpen V<VAR>hVne : (U ∩ V).Nonempty<VAR>W : Set M := U ∩ {z | ‖f z‖ = ‖f c‖}ᶜ<VAR>hWo : IsOpen W<VAR>hdVW : Disjoint V W<GOAL>U ⊆ V
<VAR>E : Type u_1<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace ℂ E<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℂ F<VAR>H : Type u_3<VAR>inst✝⁵ : TopologicalSpace H<VAR>I : ModelWithCorners ℂ E H<VAR>inst✝⁴ : I.Boundaryless<VAR>M : Type u_4<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : CompactSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>f : M → F<VAR>U : Set M<VAR>c : M<VAR>hd : MDifferentiableOn I 𝓘(ℂ, F) f U<VAR>hc : IsPreconnected U<VAR>ho : IsOpen U<VAR>hcU : c ∈ U<VAR>hm : IsMaxOn (norm ∘ f) U c<VAR>V : Set M := {z | z ∈ U ∧ ‖f z‖ = ‖f c‖}<VAR>hVo : IsOpen V<VAR>hVne : (U ∩ V).Nonempty<VAR>W : Set M := U ∩ {z | ‖f z‖ = ‖f c‖}ᶜ<VAR>hWo : IsOpen W<VAR>hdVW : Disjoint V W<VAR>hUVW : U ⊆ V ∪ W<GOAL>U ⊆ V
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>s✝ t u v s : Set α<GOAL>IsConnected s ↔ ∀ (U : Finset (Set α)), (∀ (u v : Set α), u ∈ U → v ∈ U → (s ∩ (u ∩ v)).Nonempty → u = v) → (∀ u ∈ U, IsOpen u) → s ⊆ ⋃₀ ↑U → ∃ u ∈ U, s ⊆ u
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>s✝ t u v s : Set α<GOAL>(s.Nonempty ∧ ∀ (u v : Set α), IsOpen u → IsOpen v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v) ↔ ∀ (U : Finset (Set α)), (∀ (u v : Set α), u ∈ U → v ∈ U → (s ∩ (u ∩ v)).Nonempty → u = v) → (∀ u ∈ U, IsOpen u) → s ⊆ ⋃₀ ↑U → ∃ u ∈ U, s ⊆ u
<VAR>α : Type u_1<VAR>f : α → α<VAR>n : Nat<VAR>l : List α<VAR>h : n < l.length<GOAL>modifyNth f n l = take n l ++ f l[n] :: drop (n + 1) l
<VAR>α : Type u_1<VAR>f : α → α<VAR>n : Nat<VAR>l : List α<VAR>h : n < l.length<GOAL>take n l ++ modifyHead f (l[n] :: drop (n + 1) l) = take n l ++ f l[n] :: drop (n + 1) l
<VAR>x : Cardinal.{u_1}<VAR>n : ℕ<GOAL>x.toENatAux = ↑n ↔ x = ↑n
<VAR>z w : ℍ<VAR>r R : ℝ<GOAL>dist z w ≤ r ↔ dist ↑z ↑w / (2 * √(z.im * w.im)) ≤ sinh (r / 2)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>f : ι' ≃ ι<VAR>t : (i : ι) → Set (α i)<GOAL>⇑(piCongrLeft α f) ⁻¹' univ.pi t = univ.pi fun i => t (f i)
<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>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f g : ↥(Lp β 1 μ)<GOAL>ENNReal.ofReal ‖f - g‖ = ∫⁻ (x : α), ↑‖↑↑f x - ↑↑g x‖₊ ∂μ
<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>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f g : ↥(Lp β 1 μ)<GOAL>∫⁻ (x : α), edist (↑↑(f - g) x) 0 ∂μ = ∫⁻ (x : α), edist (↑↑f x - ↑↑g x) 0 ∂μ
<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>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f g : ↥(Lp β 1 μ)<GOAL>(fun a => edist (↑↑(f - g) a) 0) =ᶠ[ae μ] fun a => edist (↑↑f a - ↑↑g a) 0
<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>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f g : ↥(Lp β 1 μ)<VAR>a✝ : α<VAR>ha : ↑↑(f - g) a✝ = (↑↑f - ↑↑g) a✝<GOAL>edist (↑↑(f - g) a✝) 0 = edist (↑↑f a✝ - ↑↑g a✝) 0
<VAR>R : Type u1<VAR>inst✝² : CommRing R<VAR>M : Type u2<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q : QuadraticForm R M<VAR>d d' : Module.Dual R M<VAR>r : R<GOAL>(contractRight ((algebraMap R (CliffordAlgebra Q)) r)) d = 0
<VAR>n : ℕ<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝ : AddGroup A<VAR>f✝ f : { f // f ↑n = 0 }<GOAL>Injective ⇑((lift n) f) ↔ ∀ (m : ℤ), ↑f m = 0 → ↑m = 0
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝⁵ : EMetricSpace X<VAR>inst✝⁴ : EMetricSpace Y<VAR>C K r : ℝ≥0<VAR>f : X → Y<VAR>s t : Set X<VAR>E : Type u_4<VAR>inst✝³ : Fintype ι<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : FiniteDimensional ℝ E<VAR>n : ℕ<GOAL>dimH univ = ↑n
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>f : R → ℝ<VAR>c : ℝ<VAR>f_nonneg : 0 ≤ f<VAR>f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y<VAR>x : R<GOAL>x ∈ seminormFromBounded' f ⁻¹' {0} ↔ x ∈ f ⁻¹' {0}
<VAR>R : Type u_1<VAR>inst✝¹² : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : AddCommMonoid M'<VAR>inst✝⁹ : AddCommMonoid M''<VAR>A : Type u_5<VAR>inst✝⁸ : CommSemiring A<VAR>inst✝⁷ : Algebra R A<VAR>inst✝⁶ : Module A M'<VAR>inst✝⁵ : IsLocalization S A<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module R M''<VAR>inst✝¹ : IsScalarTower R A M'<VAR>f : M →ₗ[R] M'<VAR>g : M →ₗ[R] M''<VAR>inst✝ : IsLocalizedModule S f<VAR>m : M'<VAR>a : M<VAR>b : ↥S<VAR>eq1 : b • m = f a<GOAL>∃ u, u • b • ⋯.choose.1 = u • ⋯.choose.2 • a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : Group G<VAR>a✝ b✝ c✝ d : G<VAR>n : ℤ<VAR>a b c : G<GOAL>a / c / (b / c) = a / b
<VAR>a x✝ z x : ℂ<GOAL>(x ∈ range fun x => cexp (↑x * I)) ↔ x ∈ sphere 0 1
<VAR>K✝ : Type u<VAR>K : Type u_1<VAR>inst✝ : Field K<GOAL>(idealX K).valuation RatFunc.X = ↑(Multiplicative.ofAdd (-1))
<VAR>K✝ : Type u<VAR>K : Type u_1<VAR>inst✝ : Field K<GOAL>X ≠ 0
<VAR>K✝ : Type u<VAR>K : Type u_1<VAR>inst✝ : Field K<GOAL>(idealX K).asIdeal = Ideal.span {X}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>inst✝³ : One M<VAR>inst✝² : One N<VAR>s✝ t : Set α<VAR>f g : α → M<VAR>a✝ : α<VAR>U : Set α<VAR>s : Set M<VAR>a : M<VAR>inst✝¹ : Decidable (a ∈ s)<VAR>inst✝ : Decidable (1 ∈ s)<GOAL>(U.mulIndicator fun x => a) ⁻¹' s = (if a ∈ s then U else ∅) ∪ if 1 ∈ s then Uᶜ else ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>inst✝³ : One M<VAR>inst✝² : One N<VAR>s✝ t : Set α<VAR>f g : α → M<VAR>a✝ : α<VAR>U : Set α<VAR>s : Set M<VAR>a : M<VAR>inst✝¹ : Decidable (a ∈ s)<VAR>inst✝ : Decidable (1 ∈ s)<GOAL>U.ite (if a ∈ s then univ else ∅) (if 1 ∈ s then univ else ∅) = (if a ∈ s then U else ∅) ∪ if 1 ∈ s then Uᶜ else ∅
<VAR>R✝ : Type u_1<VAR>inst✝⁶ : Ring R✝<VAR>A : Type u_2<VAR>inst✝⁵ : CommRing A<VAR>M : Type u_3<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R✝ M<VAR>U U₁ U₂ : Submodule R✝ M<VAR>x✝ x₁ x₂ y✝ y₁ y₂ z z₁ z₂ : M<VAR>N : Type u_4<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R✝ N<VAR>V V₁ V₂ : Submodule R✝ N<VAR>R : Type u_5<VAR>inst✝ : CommRing R<VAR>I : Ideal R<VAR>x y : R<VAR>h : x ≡ y [SMOD I]<VAR>f : R[X]<GOAL>Polynomial.eval x f ≡ Polynomial.eval y f [SMOD I]
<VAR>R✝ : Type u_1<VAR>inst✝⁶ : Ring R✝<VAR>A : Type u_2<VAR>inst✝⁵ : CommRing A<VAR>M : Type u_3<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R✝ M<VAR>U U₁ U₂ : Submodule R✝ M<VAR>x✝ x₁ x₂ y✝ y₁ y₂ z z₁ z₂ : M<VAR>N : Type u_4<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R✝ N<VAR>V V₁ V₂ : Submodule R✝ N<VAR>R : Type u_5<VAR>inst✝ : CommRing R<VAR>I : Ideal R<VAR>x y : R<VAR>h : Submodule.Quotient.mk x = Submodule.Quotient.mk y<VAR>f : R[X]<GOAL>Submodule.Quotient.mk (Polynomial.eval x f) = Submodule.Quotient.mk (Polynomial.eval y f)
<VAR>R✝ : Type u_1<VAR>inst✝⁶ : Ring R✝<VAR>A : Type u_2<VAR>inst✝⁵ : CommRing A<VAR>M : Type u_3<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R✝ M<VAR>U U₁ U₂ : Submodule R✝ M<VAR>x✝ x₁ x₂ y✝ y₁ y₂ z z₁ z₂ : M<VAR>N : Type u_4<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R✝ N<VAR>V V₁ V₂ : Submodule R✝ N<VAR>R : Type u_5<VAR>inst✝ : CommRing R<VAR>I : Ideal R<VAR>x y : R<VAR>f : R[X]<VAR>h : (Ideal.Quotient.mk I) x = (Ideal.Quotient.mk I) y<GOAL>(Ideal.Quotient.mk I) (Polynomial.eval x f) = (Ideal.Quotient.mk I) (Polynomial.eval y f)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝ : SemilatticeSup α<VAR>s : Finset β<VAR>H : s.Nonempty<VAR>f : β → α<VAR>a : α<GOAL>s.sup' H f ≤ a ↔ ∀ b ∈ s, f b ≤ a
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝ : SemilatticeSup α<VAR>s : Finset β<VAR>H : s.Nonempty<VAR>f : β → α<VAR>a : α<GOAL>(∀ b ∈ s, (WithBot.some ∘ f) b ≤ ↑a) ↔ ∀ b ∈ s, ↑(f b) ≤ ↑a
<VAR>x x₁ x₂ x₃ x' y y₁ y₂ y₃ y' : PGame<VAR>h₁ : ⟦x₁ * y₂⟧ + ⟦x₂ * y₁⟧ < ⟦x₁ * y₁⟧ + ⟦x₂ * y₂⟧<VAR>h₂ : ⟦x₂ * y₂⟧ + ⟦x₃ * y₁⟧ < ⟦x₂ * y₁⟧ + ⟦x₃ * y₂⟧<GOAL>P3 x₁ x₃ y₁ y₂
<VAR>x x₁ x₂ x₃ x' y y₁ y₂ y₃ y' : PGame<VAR>h₁ : ⟦x₁ * y₂⟧ + ⟦x₂ * y₁⟧ < ⟦x₁ * y₁⟧ + ⟦x₂ * y₂⟧<VAR>h₂ : ⟦x₂ * y₂⟧ + ⟦x₃ * y₁⟧ < ⟦x₂ * y₁⟧ + ⟦x₃ * y₂⟧<GOAL>⟦x₂ * y₁⟧ + ⟦x₂ * y₂⟧ + (⟦x₁ * y₂⟧ + ⟦x₃ * y₁⟧) < ⟦x₂ * y₁⟧ + ⟦x₂ * y₂⟧ + (⟦x₁ * y₁⟧ + ⟦x₃ * y₂⟧)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s t : Finset α<VAR>a b : α<VAR>h : a ∉ s<VAR>p : α → Prop<GOAL>(∀ x ∈ cons a s h, p x) ↔ p a ∧ ∀ x ∈ s, p x
<VAR>C : Type u<VAR>𝒞 : Category.{v, u} C<VAR>inst✝ : MonoidalCategory C<VAR>X₁ X₂ : C<VAR>f : X₁ ⟶ X₂<VAR>Y : C<GOAL>f ⊗ 𝟙 Y = f ▷ Y
<VAR>m n✝ : ℕ<VAR>C : ℕ → Sort u<VAR>H : (b : Bool) → (n : ℕ) → C (bit b n)<VAR>b : Bool<VAR>n : ℕ<GOAL>HEq (H (bit b n).bodd (bit b n).div2) (H b n)
<VAR>α β : Type u<VAR>c : Cardinal.{?u.231592}<VAR>f : α → β<VAR>s : Set α<VAR>t : Set β<VAR>h : t ⊆ f '' s<GOAL>#↑t ≤ #↑{x | x ∈ s ∧ f x ∈ t}