ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>inst✝⁷ : Ring R<VAR>Q : Type v<VAR>inst✝⁶ : AddCommGroup Q<VAR>inst✝⁵ : Module R Q<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R N<VAR>i : M →ₗ[R] N<VAR>f : M →ₗ[R] Q<VAR>inst✝ : Fact (Function.Injective ⇑i)<VAR>h : Baer R Q<VAR>y : N<VAR>r r' : R<VAR>eq1 : r • y = r' • y<GOAL>(extendIdealTo i f h y) (r - r') = 0
<VAR>R : Type u<VAR>inst✝⁷ : Ring R<VAR>Q : Type v<VAR>inst✝⁶ : AddCommGroup Q<VAR>inst✝⁵ : Module R Q<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R N<VAR>i : M →ₗ[R] N<VAR>f : M →ₗ[R] Q<VAR>inst✝ : Fact (Function.Injective ⇑i)<VAR>h : Baer R Q<VAR>y : N<VAR>r r' : R<VAR>eq1 : r • y = r' • y<GOAL>(r - r') • y = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidablePred fun l => l ≠ []<VAR>L : List (List α)<GOAL>(filter (fun l => decide (l ≠ [])) L).join = L.join
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>s : Set α<VAR>hs : TotallyBounded s<VAR>U : Set (α × α)<VAR>hU : U ∈ 𝓤 α<GOAL>∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, {x | (x, y) ∈ U}
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>s : Set α<VAR>hs : TotallyBounded s<VAR>U : Set (α × α)<VAR>hU : U ∈ 𝓤 α<VAR>r : Set (α × α)<VAR>hr : r ∈ 𝓤 α<VAR>rs : ∀ {a b : α}, (a, b) ∈ r → (b, a) ∈ r<VAR>rU : r ○ r ⊆ U<GOAL>∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, {x | (x, y) ∈ U}
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>s : Set α<VAR>hs : TotallyBounded s<VAR>U : Set (α × α)<VAR>hU : U ∈ 𝓤 α<VAR>r : Set (α × α)<VAR>hr : r ∈ 𝓤 α<VAR>rs : ∀ {a b : α}, (a, b) ∈ r → (b, a) ∈ r<VAR>rU : r ○ r ⊆ U<VAR>k : Set α<VAR>fk : k.Finite<VAR>ks : s ⊆ ⋃ y ∈ k, {x | (x, y) ∈ r}<VAR>u : Set α := k ∩ {y | ∃ x ∈ s, (x, y) ∈ r}<GOAL>∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, {x | (x, y) ∈ U}
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>s : Set α<VAR>hs : TotallyBounded s<VAR>U : Set (α × α)<VAR>hU : U ∈ 𝓤 α<VAR>r : Set (α × α)<VAR>hr : r ∈ 𝓤 α<VAR>rs : ∀ {a b : α}, (a, b) ∈ r → (b, a) ∈ r<VAR>rU : r ○ r ⊆ U<VAR>k : Set α<VAR>fk : k.Finite<VAR>ks : s ⊆ ⋃ y ∈ k, {x | (x, y) ∈ r}<VAR>u : Set α := k ∩ {y | ∃ x ∈ s, (x, y) ∈ r}<VAR>f : ↑u → α<VAR>hfs : ∀ (x : ↑u), f x ∈ s<VAR>hfr : ∀ (x : ↑u), (f x, ↑x) ∈ r<GOAL>∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, {x | (x, y) ∈ U}
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : Computation α<VAR>f : α → Computation β<VAR>g : β → Computation γ<GOAL>(s.bind f).bind g = s.bind fun x => (f x).bind g
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : Computation α<VAR>f : α → Computation β<VAR>g : β → Computation γ<GOAL>IsBisimulation fun c₁ c₂ => c₁ = c₂ ∨ ∃ s, c₁ = (s.bind f).bind g ∧ c₂ = s.bind fun x => (f x).bind g
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : Computation α<VAR>f : α → Computation β<VAR>g : β → Computation γ<GOAL>((s.bind f).bind g = s.bind fun x => (f x).bind g) ∨ ∃ s_1, (s.bind f).bind g = (s_1.bind f).bind g ∧ (s.bind fun x => (f x).bind g) = s_1.bind fun x => (f x).bind g
<VAR>p : Prop<VAR>as ps as₁ : List Prop<GOAL>as = as₁.reverseAux ps → (mk as).implies p ps as₁.length → p
<VAR>R : Type u_1<VAR>inst✝⁹ : CommRing R<VAR>S : Type u_2<VAR>inst✝⁸ : CommRing S<VAR>f : R →+* S<VAR>I✝ J : Ideal S<VAR>inst✝⁷ : Algebra R S<VAR>A : Type u_3<VAR>inst✝⁶ : CommRing A<VAR>inst✝⁵ : Algebra R A<VAR>inst✝⁴ : Algebra A S<VAR>inst✝³ : IsScalarTower R A S<VAR>inst✝² : IsIntegralClosure A R S<VAR>inst✝¹ : IsDomain A<VAR>inst✝ : Nontrivial R<VAR>I : Ideal A<GOAL>comap (algebraMap R A) I = ⊥ → I = ⊥
<VAR>R : Type u_1<VAR>inst✝⁹ : CommRing R<VAR>S : Type u_2<VAR>inst✝⁸ : CommRing S<VAR>f : R →+* S<VAR>I✝ J : Ideal S<VAR>inst✝⁷ : Algebra R S<VAR>A : Type u_3<VAR>inst✝⁶ : CommRing A<VAR>inst✝⁵ : Algebra R A<VAR>inst✝⁴ : Algebra A S<VAR>inst✝³ : IsScalarTower R A S<VAR>inst✝² : IsIntegralClosure A R S<VAR>inst✝¹ : IsDomain A<VAR>inst✝ : Nontrivial R<VAR>I : Ideal A<GOAL>¬I = ⊥ → ¬comap (algebraMap R A) I = ⊥
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : TopologicalSpace γ<VAR>U : Opens α<GOAL>U ≠ ⊥ ↔ (↑U).Nonempty
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace ℝ G<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α → ℝ<VAR>r : ℝ≥0<VAR>hfint : Integrable f μ<VAR>hfint' : 0 ≤ ∫ (x : α), f x ∂μ<VAR>hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ ↑r<VAR>hr : ¬r = 0<VAR>hμ this : IsFiniteMeasure μ<GOAL>eLpNorm f 1 μ ≤ 2 * μ univ * ↑r
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace ℝ G<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α → ℝ<VAR>r : ℝ≥0<VAR>hfint : Integrable f μ<VAR>hfint' : ∫ (a : α), ↑(-f a).toNNReal ∂μ ≤ ∫ (a : α), ↑(f a).toNNReal ∂μ<VAR>hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ ↑r<VAR>hr : ¬r = 0<VAR>hμ this : IsFiniteMeasure μ<GOAL>eLpNorm f 1 μ ≤ 2 * μ univ * ↑r
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace ℝ G<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α → ℝ<VAR>r : ℝ≥0<VAR>hfint : Integrable f μ<VAR>hfint' : ∫ (a : α), ↑(-f a).toNNReal ∂μ ≤ ∫ (a : α), ↑(f a).toNNReal ∂μ<VAR>hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ ↑r<VAR>hr : ¬r = 0<VAR>hμ this : IsFiniteMeasure μ<VAR>hposbdd : ∫ (ω : α), max (f ω) 0 ∂μ ≤ (μ univ).toReal • ↑r<GOAL>eLpNorm f 1 μ ≤ 2 * μ univ * ↑r
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace ℝ G<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α → ℝ<VAR>r : ℝ≥0<VAR>hfint : Integrable f μ<VAR>hfint' : ∫ (a : α), ↑(-f a).toNNReal ∂μ ≤ ∫ (a : α), ↑(f a).toNNReal ∂μ<VAR>hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ ↑r<VAR>hr : ¬r = 0<VAR>hμ this : IsFiniteMeasure μ<VAR>hposbdd : ∫ (ω : α), max (f ω) 0 ∂μ ≤ (μ univ).toReal • ↑r<GOAL>(∫ (a : α), ‖f a‖ ^ ENNReal.toReal 1 ∂μ) ^ (ENNReal.toReal 1)⁻¹ ≤ (2 * μ univ * ↑r).toReal
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace ℝ G<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α → ℝ<VAR>r : ℝ≥0<VAR>hfint : Integrable f μ<VAR>hfint' : ∫ (a : α), ↑(-f a).toNNReal ∂μ ≤ ∫ (a : α), ↑(f a).toNNReal ∂μ<VAR>hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ ↑r<VAR>hr : ¬r = 0<VAR>hμ this : IsFiniteMeasure μ<VAR>hposbdd : ∫ (ω : α), max (f ω) 0 ∂μ ≤ (μ univ).toReal • ↑r<GOAL>∫ (a : α), ↑(f a).toNNReal + ↑(-f a).toNNReal ∂μ ≤ (2 * μ univ * ↑r).toReal
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace ℝ G<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α → ℝ<VAR>r : ℝ≥0<VAR>hfint : Integrable f μ<VAR>hfint' : ∫ (a : α), ↑(-f a).toNNReal ∂μ ≤ ∫ (a : α), ↑(f a).toNNReal ∂μ<VAR>hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ ↑r<VAR>hr : ¬r = 0<VAR>hμ this : IsFiniteMeasure μ<VAR>hposbdd : ∫ (ω : α), max (f ω) 0 ∂μ ≤ (μ univ).toReal • ↑r<GOAL>∫ (a : α), ↑(f a).toNNReal ∂μ + ∫ (a : α), ↑(-f a).toNNReal ∂μ ≤ (2 * μ univ * ↑r).toReal
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace ℝ G<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α → ℝ<VAR>r : ℝ≥0<VAR>hfint : Integrable f μ<VAR>hfint' : ∫ (a : α), ↑(-f a).toNNReal ∂μ ≤ ∫ (a : α), ↑(f a).toNNReal ∂μ<VAR>hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ ↑r<VAR>hr : ¬r = 0<VAR>hμ this : IsFiniteMeasure μ<VAR>hposbdd : ∫ (ω : α), max (f ω) 0 ∂μ ≤ (μ univ).toReal • ↑r<GOAL>Integrable (fun a => ↑(-f a).toNNReal) μ
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>a✝ b c d a : α<GOAL>|a| = max a 0 + max (-a) 0
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : T1Space X<VAR>s : Set X<VAR>x : X<GOAL>𝓝 x ≤ 𝓝ˢ s ↔ x ∈ s
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b✝ c : α<VAR>n : ℤ<VAR>a : α<VAR>b : α ⧸ AddSubgroup.zmultiples p<GOAL>(fun x => ↑↑x) ((fun b => ⟨⋯.lift b, ⋯⟩) b) = b
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b c : α<VAR>n : ℤ<VAR>a z✝ : α<GOAL>(fun x => ↑↑x) ((fun b => ⟨⋯.lift b, ⋯⟩) ↑z✝) = ↑z✝
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b c : α<VAR>n : ℤ<VAR>a z✝ : α<GOAL>↑(toIocMod hp a z✝) = ↑z✝
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b c : α<VAR>n : ℤ<VAR>a z✝ : α<GOAL>-toIocDiv hp a z✝ • p ∈ AddSubgroup.zmultiples p
<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>inst✝ : Fintype ι<VAR>b : Basis ι R M<VAR>c : ι → R<GOAL>⇑(b.repr (∑ i : ι, c i • b i)) = c
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>n✝ m : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>x : R<VAR>k n : ℕ<GOAL>(C x * X ^ k).coeff n = if n = k then x else 0
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>n✝ m : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>x : R<VAR>k n : ℕ<GOAL>(if k = n then x else 0) = if n = k then x else 0
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>n✝ m : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>x : R<VAR>k n : ℕ<GOAL>(k = n) = (n = k)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a b a₁ b₁ a₂ b₂ : α<VAR>h : a₁ < b₁<GOAL>Ico a₁ b₁ ⊆ Ico a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f✝ f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s✝ t : Set E<VAR>L L₁ L₂ : Filter E<VAR>iso : E ≃L[𝕜] F<VAR>f : F → G<VAR>s : Set F<GOAL>DifferentiableOn 𝕜 (f ∘ ⇑iso) (⇑iso ⁻¹' s) ↔ DifferentiableOn 𝕜 f s
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f✝ f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s✝ t : Set E<VAR>L L₁ L₂ : Filter E<VAR>iso : E ≃L[𝕜] F<VAR>f : F → G<VAR>s : Set F<VAR>H : DifferentiableOn 𝕜 (f ∘ ⇑iso) (⇑iso ⁻¹' s)<VAR>y : F<VAR>hy : y ∈ s<GOAL>DifferentiableWithinAt 𝕜 f s y
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f✝ f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s✝ t : Set E<VAR>L L₁ L₂ : Filter E<VAR>iso : E ≃L[𝕜] F<VAR>f : F → G<VAR>s : Set F<VAR>H : DifferentiableOn 𝕜 (f ∘ ⇑iso) (⇑iso ⁻¹' s)<VAR>y : F<VAR>hy : y ∈ s<GOAL>DifferentiableWithinAt 𝕜 (f ∘ ⇑iso) (⇑iso ⁻¹' s) (iso.symm y)
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f✝ f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s✝ t : Set E<VAR>L L₁ L₂ : Filter E<VAR>iso : E ≃L[𝕜] F<VAR>f : F → G<VAR>s : Set F<VAR>H : DifferentiableOn 𝕜 (f ∘ ⇑iso) (⇑iso ⁻¹' s)<VAR>y : F<VAR>hy : y ∈ s<GOAL>iso.symm y ∈ ⇑iso ⁻¹' s
<VAR>R : Type u<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝¹ : Semiring R<VAR>p q r : R[X]<VAR>inst✝ : Nontrivial R<VAR>i j : ℕ<GOAL>(monomial i) 1 = (monomial j) 1 ↔ i = j
<VAR>R : Type u<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝¹ : Semiring R<VAR>p q r : R[X]<VAR>inst✝ : Nontrivial R<VAR>i j : ℕ<GOAL>Finsupp.single i 1 = Finsupp.single j 1 ↔ i = j
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>ι' : Type u_4<VAR>inst✝ : CompleteLattice α<VAR>s : Set α<VAR>hs : SetIndependent s<VAR>t : ι → α<VAR>ht✝ ht : Independent t<VAR>h_ne_bot : ∀ (i : ι), t i ≠ ⊥<GOAL>Injective t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>ι' : Type u_4<VAR>inst✝ : CompleteLattice α<VAR>s : Set α<VAR>hs : SetIndependent s<VAR>t : ι → α<VAR>ht✝ ht : Independent t<VAR>h_ne_bot : ∀ (i : ι), t i ≠ ⊥<GOAL>univ = {i | t i ≠ ⊥}
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_3, u_1} C<VAR>inst✝³ : Category.{?u.87228, u_2} D<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : Preadditive D<VAR>F G : CochainComplex C ℤ<VAR>φ : F ⟶ G<VAR>inst✝ : HasHomotopyCofiber φ<VAR>i j k : ℤ<VAR>hij : i + -1 = j<VAR>hik : k + -1 = i<GOAL>homotopyCofiber.inlX φ i j ⋯ ≫ homotopyCofiber.d φ j i = φ.f i ≫ homotopyCofiber.inrX φ i - F.d i k ≫ homotopyCofiber.inlX φ k i ⋯
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_3, u_1} C<VAR>inst✝³ : Category.{?u.87228, u_2} D<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : Preadditive D<VAR>F G : CochainComplex C ℤ<VAR>φ : F ⟶ G<VAR>inst✝ : HasHomotopyCofiber φ<VAR>i j k : ℤ<VAR>hij : i + -1 = j<VAR>hik : k + -1 = i<GOAL>-F.d i k ≫ homotopyCofiber.inlX φ k i ⋯ + φ.f i ≫ homotopyCofiber.inrX φ i = φ.f i ≫ homotopyCofiber.inrX φ i - F.d i k ≫ homotopyCofiber.inlX φ k i ⋯
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : ModuleCat R<VAR>X : ModuleCat R<VAR>Y : ModuleCat R<VAR>Z : ModuleCat R<GOAL>whiskerRight (associator W X Y).hom Z ≫ (associator W (tensorObj X Y) Z).hom ≫ whiskerLeft W (associator X Y Z).hom = (associator (tensorObj W X) Y Z).hom ≫ (associator W X (tensorObj Y Z)).hom
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁷ : OrderedSemiring 𝕜<VAR>inst✝⁶ : AddCommMonoid E<VAR>inst✝⁵ : AddCommMonoid F<VAR>inst✝⁴ : OrderedAddCommMonoid α<VAR>inst✝³ : OrderedAddCommMonoid β<VAR>inst✝² : SMul 𝕜 E<VAR>inst✝¹ : Module 𝕜 β<VAR>inst✝ : OrderedSMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>hf : ConvexOn 𝕜 s f<VAR>x : E<VAR>r : β<VAR>hx : (x, r).1 ∈ s<VAR>hr : f (x, r).1 ≤ (x, r).2<VAR>y : E<VAR>t : β<VAR>hy : (y, t).1 ∈ s<VAR>ht : f (y, t).1 ≤ (y, t).2<VAR>a b : 𝕜<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>hab : a + b = 1<GOAL>a • (x, r) + b • (y, t) ∈ {p | p.1 ∈ s ∧ f p.1 ≤ p.2}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁷ : OrderedSemiring 𝕜<VAR>inst✝⁶ : AddCommMonoid E<VAR>inst✝⁵ : AddCommMonoid F<VAR>inst✝⁴ : OrderedAddCommMonoid α<VAR>inst✝³ : OrderedAddCommMonoid β<VAR>inst✝² : SMul 𝕜 E<VAR>inst✝¹ : Module 𝕜 β<VAR>inst✝ : OrderedSMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>hf : ConvexOn 𝕜 s f<VAR>x : E<VAR>r : β<VAR>hx : (x, r).1 ∈ s<VAR>hr : f (x, r).1 ≤ (x, r).2<VAR>y : E<VAR>t : β<VAR>hy : (y, t).1 ∈ s<VAR>ht : f (y, t).1 ≤ (y, t).2<VAR>a b : 𝕜<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>hab : a + b = 1<GOAL>f (a • (x, r) + b • (y, t)).1 ≤ (a • (x, r) + b • (y, t)).2
<VAR>k✝ : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R : Type u_2<VAR>k : Type u_3<VAR>A : Type u_4<VAR>inst✝³ : CommSemiring k<VAR>inst✝² : Semiring A<VAR>inst✝¹ : Algebra k A<VAR>inst✝ : AddMonoid G<VAR>x✝ : A[G]<GOAL>(mapDomainAlgHom k A (AddMonoidHom.id G)) x✝ = (AlgHom.id k A[G]) x✝
<VAR>α : Type u<VAR>β : Type v<VAR>r✝ : α → α → Prop<VAR>s✝ : β → β → Prop<VAR>r : α → α → Prop<VAR>s : Set α<GOAL>¬Unbounded r s ↔ Bounded r s
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>x : RatFunc K<GOAL>(algebraMap K[X] (RatFunc K)) x.num / (algebraMap K[X] (RatFunc K)) x.denom = x
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>p q : K[X]<VAR>hq : q ≠ 0<GOAL>(algebraMap K[X] (RatFunc K)) ((algebraMap K[X] (RatFunc K)) p / (algebraMap K[X] (RatFunc K)) q).num / (algebraMap K[X] (RatFunc K)) ((algebraMap K[X] (RatFunc K)) p / (algebraMap K[X] (RatFunc K)) q).denom = (algebraMap K[X] (RatFunc K)) p / (algebraMap K[X] (RatFunc K)) q
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>p q : K[X]<VAR>hq : q ≠ 0<VAR>q_div_ne_zero : q / gcd p q ≠ 0<GOAL>(algebraMap K[X] (RatFunc K)) ((algebraMap K[X] (RatFunc K)) p / (algebraMap K[X] (RatFunc K)) q).num / (algebraMap K[X] (RatFunc K)) ((algebraMap K[X] (RatFunc K)) p / (algebraMap K[X] (RatFunc K)) q).denom = (algebraMap K[X] (RatFunc K)) p / (algebraMap K[X] (RatFunc K)) q
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>p q : K[X]<VAR>hq : q ≠ 0<VAR>q_div_ne_zero : q / gcd p q ≠ 0<GOAL>gcd p q ∣ q
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>p q : K[X]<VAR>hq : q ≠ 0<VAR>q_div_ne_zero : q / gcd p q ≠ 0<GOAL>gcd p q ∣ p
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>p q : K[X]<VAR>hq : q ≠ 0<VAR>q_div_ne_zero : q / gcd p q ≠ 0<GOAL>(algebraMap K[X] (RatFunc K)) (q / gcd p q) ≠ 0
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>p q : K[X]<VAR>hq : q ≠ 0<VAR>q_div_ne_zero : q / gcd p q ≠ 0<GOAL>(algebraMap K[X] (RatFunc K)) q ≠ 0
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>p q : K[X]<VAR>hq : q ≠ 0<VAR>q_div_ne_zero : q / gcd p q ≠ 0<GOAL>(algebraMap K[X] (RatFunc K)) (C (q / gcd p q).leadingCoeff⁻¹) ≠ 0
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>δ' : Type u_2<VAR>inst✝⁴ : UniformSpace α<VAR>inst✝³ : UniformSpace β<VAR>inst✝² : UniformSpace γ<VAR>inst✝¹ : UniformSpace δ<VAR>inst✝ : UniformSpace δ'<VAR>f : α × β → γ<GOAL>UniformContinuous₂ (curry f) ↔ UniformContinuous f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝ : Zero M<VAR>a : α<VAR>m : M<VAR>f : α →₀ M<GOAL>(a, m) ∈ f.graph ↔ f a = m ∧ m ≠ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝ : Zero M<VAR>a : α<VAR>m : M<VAR>f : α →₀ M<GOAL>(∃ a_1, f a_1 ≠ 0 ∧ { toFun := fun a => (a, f a), inj' := ⋯ } a_1 = (a, m)) ↔ f a = m ∧ m ≠ 0
<VAR>𝕜 : Type u<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>F : Type w<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>F' : Type x<VAR>inst✝⁶ : AddCommGroup F'<VAR>inst✝⁵ : Module 𝕜 F'<VAR>inst✝⁴ : TopologicalSpace F'<VAR>inst✝³ : TopologicalAddGroup F'<VAR>inst✝² : ContinuousSMul 𝕜 F'<VAR>inst✝¹ : CompleteSpace 𝕜<VAR>inst✝ : FiniteDimensional 𝕜 E<GOAL>IsOpen {L | Injective ⇑L}
<VAR>𝕜 : Type u<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>F : Type w<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>F' : Type x<VAR>inst✝⁶ : AddCommGroup F'<VAR>inst✝⁵ : Module 𝕜 F'<VAR>inst✝⁴ : TopologicalSpace F'<VAR>inst✝³ : TopologicalAddGroup F'<VAR>inst✝² : ContinuousSMul 𝕜 F'<VAR>inst✝¹ : CompleteSpace 𝕜<VAR>inst✝ : FiniteDimensional 𝕜 E<GOAL>∀ x ∈ {L | Injective ⇑L}, ∀ᶠ (y : E →L[𝕜] F) in 𝓝 x, y ∈ {L | Injective ⇑L}
<VAR>𝕜 : Type u<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>F : Type w<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>F' : Type x<VAR>inst✝⁶ : AddCommGroup F'<VAR>inst✝⁵ : Module 𝕜 F'<VAR>inst✝⁴ : TopologicalSpace F'<VAR>inst✝³ : TopologicalAddGroup F'<VAR>inst✝² : ContinuousSMul 𝕜 F'<VAR>inst✝¹ : CompleteSpace 𝕜<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>φ₀ : E →L[𝕜] F<VAR>hφ₀ : φ₀ ∈ {L | Injective ⇑L}<GOAL>∀ᶠ (y : E →L[𝕜] F) in 𝓝 φ₀, y ∈ {L | Injective ⇑L}
<VAR>𝕜 : Type u<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>F : Type w<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>F' : Type x<VAR>inst✝⁶ : AddCommGroup F'<VAR>inst✝⁵ : Module 𝕜 F'<VAR>inst✝⁴ : TopologicalSpace F'<VAR>inst✝³ : TopologicalAddGroup F'<VAR>inst✝² : ContinuousSMul 𝕜 F'<VAR>inst✝¹ : CompleteSpace 𝕜<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>φ₀ : E →L[𝕜] F<VAR>hφ₀ : φ₀ ∈ {L | Injective ⇑L}<VAR>K : ℝ≥0<VAR>K_pos : K > 0<VAR>H : AntilipschitzWith K ⇑↑φ₀<GOAL>∀ᶠ (y : E →L[𝕜] F) in 𝓝 φ₀, y ∈ {L | Injective ⇑L}
<VAR>𝕜 : Type u<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>F : Type w<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>F' : Type x<VAR>inst✝⁶ : AddCommGroup F'<VAR>inst✝⁵ : Module 𝕜 F'<VAR>inst✝⁴ : TopologicalSpace F'<VAR>inst✝³ : TopologicalAddGroup F'<VAR>inst✝² : ContinuousSMul 𝕜 F'<VAR>inst✝¹ : CompleteSpace 𝕜<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>φ₀ : E →L[𝕜] F<VAR>hφ₀ : φ₀ ∈ {L | Injective ⇑L}<VAR>K : ℝ≥0<VAR>K_pos : K > 0<VAR>H : AntilipschitzWith K ⇑↑φ₀<VAR>this : ∀ᶠ (φ : E →L[𝕜] F) in 𝓝 φ₀, ‖φ - φ₀‖₊ < K⁻¹<GOAL>∀ᶠ (y : E →L[𝕜] F) in 𝓝 φ₀, y ∈ {L | Injective ⇑L}
<VAR>𝕜 : Type u<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>F : Type w<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>F' : Type x<VAR>inst✝⁶ : AddCommGroup F'<VAR>inst✝⁵ : Module 𝕜 F'<VAR>inst✝⁴ : TopologicalSpace F'<VAR>inst✝³ : TopologicalAddGroup F'<VAR>inst✝² : ContinuousSMul 𝕜 F'<VAR>inst✝¹ : CompleteSpace 𝕜<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>φ₀ : E →L[𝕜] F<VAR>hφ₀ : φ₀ ∈ {L | Injective ⇑L}<VAR>K : ℝ≥0<VAR>K_pos : K > 0<VAR>H : AntilipschitzWith K ⇑↑φ₀<VAR>this : ∀ᶠ (φ : E →L[𝕜] F) in 𝓝 φ₀, ‖φ - φ₀‖₊ < K⁻¹<VAR>φ : E →L[𝕜] F<VAR>hφ : ‖φ - φ₀‖₊ < K⁻¹<GOAL>Injective ⇑φ