ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>E : Type u_1<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module ℂ E<GOAL>2 * Cardinal.lift.{0, u_1} (Module.rank ℂ E) = Cardinal.lift.{0, u_1} (2 * Module.rank ℂ E)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>inst✝¹ : MetricSpace β<VAR>μ : Measure α<VAR>n : ℕ<VAR>i j : ι<VAR>s : Set α<VAR>ε : ℝ<VAR>f : ι → α → β<VAR>g : α → β<VAR>inst✝ : Preorder ι<VAR>x : α<GOAL>x ∈ notConvergentSeq f g n j ↔ ∃ k ≥ j, 1 / (↑n + 1) < dist (f k x) (g x)
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B B' I J D X : Set α<VAR>e f : α<VAR>hI : M.Indep I<GOAL>I ⊆ M.E
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B✝ B' I J D X : Set α<VAR>e f : α<VAR>hI : M.Indep I<VAR>B : Set α<VAR>hB : M.Base B<VAR>hIB : I ⊆ B<GOAL>I ⊆ M.E
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>R' : Type v<VAR>inst✝¹ : CommMonoid R'<VAR>inst✝ : Finite R<VAR>e : AddChar R R'<VAR>r : R<VAR>hr : ¬IsUnit r<GOAL>¬(e.mulShift r).IsPrimitive
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>R' : Type v<VAR>inst✝¹ : CommMonoid R'<VAR>inst✝ : Finite R<VAR>e : AddChar R R'<VAR>r : R<VAR>hr : ¬IsUnit r<GOAL>∃ x, ∃ (_ : x ≠ 0), ¬(e.mulShift r).mulShift x ≠ 1
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>R' : Type v<VAR>inst✝¹ : CommMonoid R'<VAR>inst✝ : Finite R<VAR>e : AddChar R R'<VAR>r : R<VAR>hr : ∃ x, ∃ (_ : x * r = 0), ¬x = 0<GOAL>∃ x, ∃ (_ : x ≠ 0), ¬(e.mulShift r).mulShift x ≠ 1
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>R' : Type v<VAR>inst✝¹ : CommMonoid R'<VAR>inst✝ : Finite R<VAR>e : AddChar R R'<VAR>r x : R<VAR>h : x * r = 0<VAR>h' : ¬x = 0<GOAL>∃ x, ∃ (_ : x ≠ 0), ¬(e.mulShift r).mulShift x ≠ 1
<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✝³ : OrderedAddCommMonoid α<VAR>inst✝² : SMul 𝕜 α<VAR>inst✝¹ : OrderedAddCommMonoid β<VAR>inst✝ : SMul 𝕜 β<VAR>f : α ≃o β<VAR>hf : ConcaveOn 𝕜 univ ⇑f<GOAL>ConvexOn 𝕜 univ ⇑f.symm
<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✝³ : OrderedAddCommMonoid α<VAR>inst✝² : SMul 𝕜 α<VAR>inst✝¹ : OrderedAddCommMonoid β<VAR>inst✝ : SMul 𝕜 β<VAR>f : α ≃o β<VAR>hf : ConcaveOn 𝕜 univ ⇑f<VAR>x : β<VAR>x✝¹ : x ∈ univ<VAR>y : β<VAR>x✝ : y ∈ univ<VAR>a b : 𝕜<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>hab : a + b = 1<GOAL>f.symm (a • x + b • y) ≤ a • f.symm x + b • f.symm y
<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✝³ : OrderedAddCommMonoid α<VAR>inst✝² : SMul 𝕜 α<VAR>inst✝¹ : OrderedAddCommMonoid β<VAR>inst✝ : SMul 𝕜 β<VAR>f : α ≃o β<VAR>hf : ConcaveOn 𝕜 univ ⇑f<VAR>x : β<VAR>x✝¹ : x ∈ univ<VAR>y : β<VAR>x✝ : y ∈ univ<VAR>a b : 𝕜<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>hab : a + b = 1<VAR>x' : α<VAR>hx'' : x = f x'<GOAL>f.symm (a • x + b • y) ≤ a • f.symm x + b • f.symm y
<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✝³ : OrderedAddCommMonoid α<VAR>inst✝² : SMul 𝕜 α<VAR>inst✝¹ : OrderedAddCommMonoid β<VAR>inst✝ : SMul 𝕜 β<VAR>f : α ≃o β<VAR>hf : ConcaveOn 𝕜 univ ⇑f<VAR>x : β<VAR>x✝¹ : x ∈ univ<VAR>y : β<VAR>x✝ : y ∈ univ<VAR>a b : 𝕜<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>hab : a + b = 1<VAR>x' : α<VAR>hx'' : x = f x'<VAR>y' : α<VAR>hy'' : y = f y'<GOAL>f.symm (a • x + b • y) ≤ a • f.symm x + b • f.symm y
<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✝³ : OrderedAddCommMonoid α<VAR>inst✝² : SMul 𝕜 α<VAR>inst✝¹ : OrderedAddCommMonoid β<VAR>inst✝ : SMul 𝕜 β<VAR>f : α ≃o β<VAR>hf : ConcaveOn 𝕜 univ ⇑f<VAR>x : β<VAR>x✝¹ : x ∈ univ<VAR>y : β<VAR>x✝ : y ∈ univ<VAR>a b : 𝕜<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>hab : a + b = 1<VAR>x' : α<VAR>hx'' : x = f x'<VAR>y' : α<VAR>hy'' : y = f y'<GOAL>f.symm (a • f x' + b • f y') ≤ a • x' + b • y'
<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✝³ : OrderedAddCommMonoid α<VAR>inst✝² : SMul 𝕜 α<VAR>inst✝¹ : OrderedAddCommMonoid β<VAR>inst✝ : SMul 𝕜 β<VAR>f : α ≃o β<VAR>hf : ConcaveOn 𝕜 univ ⇑f<VAR>x : β<VAR>x✝¹ : x ∈ univ<VAR>y : β<VAR>x✝ : y ∈ univ<VAR>a b : 𝕜<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>hab : a + b = 1<VAR>x' : α<VAR>hx'' : x = f x'<VAR>y' : α<VAR>hy'' : y = f y'<GOAL>a • f x' + b • f y' ≤ f (a • x' + b • y')
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>f f₁ : E → F<VAR>f' f₀' f₁' : F<VAR>s t : Set E<VAR>x v : E<VAR>h : HasLineDerivAt 𝕜 f f' x v<GOAL>lineDeriv 𝕜 f x v = f'
<VAR>n : PosNum<VAR>d : ZNum<GOAL>↑(Num.pos n % d.abs) = ↑(pos n) % ↑d
<VAR>n : PosNum<VAR>d : ZNum<GOAL>↑(↑(Num.pos n) % (↑d).natAbs) = ↑↑n % ↑d
<VAR>n : PosNum<VAR>d : ZNum<GOAL>↑d.abs - ↑(n.pred' % d.abs).succ = ↑(neg n) % ↑d
<VAR>n : PosNum<VAR>d : ZNum<GOAL>subNatNat (↑d).natAbs (↑n.pred' % (↑d).natAbs + 1) = -(↑↑n.pred' + 1) % ↑d
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁶ : Category.{?u.42589, u_1} C<VAR>inst✝⁵ : Category.{?u.42593, u_2} D<VAR>inst✝⁴ : HasZeroMorphisms C<VAR>inst✝³ : HasZeroMorphisms D<VAR>S S₁ S₂ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.RightHomologyData<VAR>h₂ : S₂.RightHomologyData<VAR>ψ : RightHomologyMapData φ h₁ h₂<VAR>F : C ⥤ D<VAR>inst✝² : F.PreservesZeroMorphisms<VAR>inst✝¹ : h₁.IsPreservedBy F<VAR>inst✝ : h₂.IsPreservedBy F<GOAL>(h₁.map F).p ≫ F.map ψ.φQ = (F.mapShortComplex.map φ).τ₂ ≫ (h₂.map F).p
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁶ : Category.{?u.42589, u_1} C<VAR>inst✝⁵ : Category.{?u.42593, u_2} D<VAR>inst✝⁴ : HasZeroMorphisms C<VAR>inst✝³ : HasZeroMorphisms D<VAR>S S₁ S₂ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.RightHomologyData<VAR>h₂ : S₂.RightHomologyData<VAR>ψ : RightHomologyMapData φ h₁ h₂<VAR>F : C ⥤ D<VAR>inst✝² : F.PreservesZeroMorphisms<VAR>inst✝¹ : h₁.IsPreservedBy F<VAR>inst✝ : h₂.IsPreservedBy F<GOAL>F.map ψ.φQ ≫ (h₂.map F).g' = (h₁.map F).g' ≫ (F.mapShortComplex.map φ).τ₃
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁶ : Category.{?u.42589, u_1} C<VAR>inst✝⁵ : Category.{?u.42593, u_2} D<VAR>inst✝⁴ : HasZeroMorphisms C<VAR>inst✝³ : HasZeroMorphisms D<VAR>S S₁ S₂ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.RightHomologyData<VAR>h₂ : S₂.RightHomologyData<VAR>ψ : RightHomologyMapData φ h₁ h₂<VAR>F : C ⥤ D<VAR>inst✝² : F.PreservesZeroMorphisms<VAR>inst✝¹ : h₁.IsPreservedBy F<VAR>inst✝ : h₂.IsPreservedBy F<GOAL>F.map ψ.φH ≫ (h₂.map F).ι = (h₁.map F).ι ≫ F.map ψ.φQ
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : HasContDiffBump E<VAR>inst✝⁴ : MeasurableSpace E<VAR>c : E<VAR>f : ContDiffBump c<VAR>x : E<VAR>n : ℕ∞<VAR>μ : Measure E<VAR>inst✝³ : BorelSpace E<VAR>inst✝² : FiniteDimensional ℝ E<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>inst✝ : μ.IsOpenPosMeasure<VAR>ι : Type u_2<VAR>φ : ι → ContDiffBump c<VAR>l : Filter ι<VAR>hφ : Tendsto (fun i => (φ i).rOut) l (𝓝 0)<GOAL>Tendsto (fun i => support fun x => (φ i).normed μ x) l (𝓝 c).smallSets
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : HasContDiffBump E<VAR>inst✝⁴ : MeasurableSpace E<VAR>c : E<VAR>f : ContDiffBump c<VAR>x : E<VAR>n : ℕ∞<VAR>μ : Measure E<VAR>inst✝³ : BorelSpace E<VAR>inst✝² : FiniteDimensional ℝ E<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>inst✝ : μ.IsOpenPosMeasure<VAR>ι : Type u_2<VAR>φ : ι → ContDiffBump c<VAR>l : Filter ι<VAR>hφ : ∀ ε > 0, ∀ᶠ (x : ι) in l, (φ x).rOut < ε<GOAL>Tendsto (fun i => support fun x => (φ i).normed μ x) l (𝓝 c).smallSets
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : HasContDiffBump E<VAR>inst✝⁴ : MeasurableSpace E<VAR>c : E<VAR>f : ContDiffBump c<VAR>x : E<VAR>n : ℕ∞<VAR>μ : Measure E<VAR>inst✝³ : BorelSpace E<VAR>inst✝² : FiniteDimensional ℝ E<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>inst✝ : μ.IsOpenPosMeasure<VAR>ι : Type u_2<VAR>φ : ι → ContDiffBump c<VAR>l : Filter ι<VAR>hφ : ∀ ε > 0, ∀ᶠ (x : ι) in l, (φ x).rOut < ε<GOAL>∀ (i : ℝ), 0 < i → ∀ᶠ (x : ι) in l, (support fun x_1 => (φ x).normed μ x_1) ∈ 𝒫 ball c i
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : HasContDiffBump E<VAR>inst✝⁴ : MeasurableSpace E<VAR>c : E<VAR>f : ContDiffBump c<VAR>x : E<VAR>n : ℕ∞<VAR>μ : Measure E<VAR>inst✝³ : BorelSpace E<VAR>inst✝² : FiniteDimensional ℝ E<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>inst✝ : μ.IsOpenPosMeasure<VAR>ι : Type u_2<VAR>φ : ι → ContDiffBump c<VAR>l : Filter ι<VAR>hφ : ∀ ε > 0, ∀ᶠ (x : ι) in l, (φ x).rOut < ε<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>i : ι<VAR>hi : (φ i).rOut < ε<GOAL>(support fun x => (φ i).normed μ x) ∈ 𝒫 ball c ε
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : HasContDiffBump E<VAR>inst✝⁴ : MeasurableSpace E<VAR>c : E<VAR>f : ContDiffBump c<VAR>x : E<VAR>n : ℕ∞<VAR>μ : Measure E<VAR>inst✝³ : BorelSpace E<VAR>inst✝² : FiniteDimensional ℝ E<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>inst✝ : μ.IsOpenPosMeasure<VAR>ι : Type u_2<VAR>φ : ι → ContDiffBump c<VAR>l : Filter ι<VAR>hφ : ∀ ε > 0, ∀ᶠ (x : ι) in l, (φ x).rOut < ε<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>i : ι<VAR>hi : (φ i).rOut < ε<GOAL>ball c (φ i).rOut ∈ 𝒫 ball c ε
<VAR>R : Type u_1<VAR>inst✝⁹ : Ring R<VAR>E : Type u_2<VAR>inst✝⁸ : AddCommGroup E<VAR>inst✝⁷ : Module R E<VAR>F : Type u_3<VAR>inst✝⁶ : AddCommGroup F<VAR>inst✝⁵ : Module R F<VAR>G : Type u_4<VAR>inst✝⁴ : AddCommGroup G<VAR>inst✝³ : Module R G<VAR>M : Type u_5<VAR>inst✝² : Monoid M<VAR>inst✝¹ : DistribMulAction M F<VAR>inst✝ : SMulCommClass R M F<VAR>y : M<VAR>f : E →ₗ.[R] F<VAR>x_fst : E<VAR>x_snd : F<VAR>h : (x_fst, x_snd) ∈ Submodule.map (LinearMap.id.prodMap (-LinearMap.id)) f.graph<GOAL>(x_fst, x_snd) ∈ (-f).graph
<VAR>R : Type u_1<VAR>inst✝⁹ : Ring R<VAR>E : Type u_2<VAR>inst✝⁸ : AddCommGroup E<VAR>inst✝⁷ : Module R E<VAR>F : Type u_3<VAR>inst✝⁶ : AddCommGroup F<VAR>inst✝⁵ : Module R F<VAR>G : Type u_4<VAR>inst✝⁴ : AddCommGroup G<VAR>inst✝³ : Module R G<VAR>M : Type u_5<VAR>inst✝² : Monoid M<VAR>inst✝¹ : DistribMulAction M F<VAR>inst✝ : SMulCommClass R M F<VAR>y : M<VAR>f : E →ₗ.[R] F<VAR>x_fst : E<VAR>x_snd : F<VAR>h : ∃ y ∈ f.graph, (LinearMap.id.prodMap (-LinearMap.id)) y = (x_fst, x_snd)<GOAL>(x_fst, x_snd) ∈ (-f).graph
<VAR>R : Type u_1<VAR>inst✝⁹ : Ring R<VAR>E : Type u_2<VAR>inst✝⁸ : AddCommGroup E<VAR>inst✝⁷ : Module R E<VAR>F : Type u_3<VAR>inst✝⁶ : AddCommGroup F<VAR>inst✝⁵ : Module R F<VAR>G : Type u_4<VAR>inst✝⁴ : AddCommGroup G<VAR>inst✝³ : Module R G<VAR>M : Type u_5<VAR>inst✝² : Monoid M<VAR>inst✝¹ : DistribMulAction M F<VAR>inst✝ : SMulCommClass R M F<VAR>y : M<VAR>f : E →ₗ.[R] F<VAR>x_fst : E<VAR>x_snd : F<VAR>fst✝ : E<VAR>snd✝ : F<VAR>hx' : (fst✝, snd✝) ∈ f.graph<VAR>h : (LinearMap.id.prodMap (-LinearMap.id)) (fst✝, snd✝) = (x_fst, x_snd)<GOAL>(x_fst, x_snd) ∈ (-f).graph
<VAR>R : Type u_1<VAR>inst✝⁹ : Ring R<VAR>E : Type u_2<VAR>inst✝⁸ : AddCommGroup E<VAR>inst✝⁷ : Module R E<VAR>F : Type u_3<VAR>inst✝⁶ : AddCommGroup F<VAR>inst✝⁵ : Module R F<VAR>G : Type u_4<VAR>inst✝⁴ : AddCommGroup G<VAR>inst✝³ : Module R G<VAR>M : Type u_5<VAR>inst✝² : Monoid M<VAR>inst✝¹ : DistribMulAction M F<VAR>inst✝ : SMulCommClass R M F<VAR>y : M<VAR>f : E →ₗ.[R] F<VAR>x_fst : E<VAR>x_snd : F<VAR>fst✝ : E<VAR>snd✝ : F<VAR>hx' : (fst✝, snd✝) ∈ f.graph<VAR>h : fst✝ = x_fst ∧ -snd✝ = x_snd<GOAL>(x_fst, x_snd) ∈ (-f).graph
<VAR>R : Type u_1<VAR>inst✝⁹ : Ring R<VAR>E : Type u_2<VAR>inst✝⁸ : AddCommGroup E<VAR>inst✝⁷ : Module R E<VAR>F : Type u_3<VAR>inst✝⁶ : AddCommGroup F<VAR>inst✝⁵ : Module R F<VAR>G : Type u_4<VAR>inst✝⁴ : AddCommGroup G<VAR>inst✝³ : Module R G<VAR>M : Type u_5<VAR>inst✝² : Monoid M<VAR>inst✝¹ : DistribMulAction M F<VAR>inst✝ : SMulCommClass R M F<VAR>y : M<VAR>f : E →ₗ.[R] F<VAR>x_fst : E<VAR>x_snd : F<VAR>fst✝ : E<VAR>snd✝ : F<VAR>hx' : ∃ y, ↑y = (fst✝, snd✝).1 ∧ ↑f y = (fst✝, snd✝).2<VAR>h : fst✝ = x_fst ∧ -snd✝ = x_snd<GOAL>∃ y, ↑y = (x_fst, x_snd).1 ∧ ↑(-f) y = (x_fst, x_snd).2
<VAR>R : Type u_1<VAR>inst✝⁹ : Ring R<VAR>E : Type u_2<VAR>inst✝⁸ : AddCommGroup E<VAR>inst✝⁷ : Module R E<VAR>F : Type u_3<VAR>inst✝⁶ : AddCommGroup F<VAR>inst✝⁵ : Module R F<VAR>G : Type u_4<VAR>inst✝⁴ : AddCommGroup G<VAR>inst✝³ : Module R G<VAR>M : Type u_5<VAR>inst✝² : Monoid M<VAR>inst✝¹ : DistribMulAction M F<VAR>inst✝ : SMulCommClass R M F<VAR>y✝ : M<VAR>f : E →ₗ.[R] F<VAR>x_fst : E<VAR>x_snd : F<VAR>fst✝ : E<VAR>snd✝ : F<VAR>h : fst✝ = x_fst ∧ -snd✝ = x_snd<VAR>y : ↥f.domain<VAR>hy : ↑y = (fst✝, snd✝).1<VAR>hx' : ↑f y = (fst✝, snd✝).2<GOAL>∃ y, ↑y = (x_fst, x_snd).1 ∧ ↑(-f) y = (x_fst, x_snd).2
<VAR>R : Type u_1<VAR>inst✝⁹ : Ring R<VAR>E : Type u_2<VAR>inst✝⁸ : AddCommGroup E<VAR>inst✝⁷ : Module R E<VAR>F : Type u_3<VAR>inst✝⁶ : AddCommGroup F<VAR>inst✝⁵ : Module R F<VAR>G : Type u_4<VAR>inst✝⁴ : AddCommGroup G<VAR>inst✝³ : Module R G<VAR>M : Type u_5<VAR>inst✝² : Monoid M<VAR>inst✝¹ : DistribMulAction M F<VAR>inst✝ : SMulCommClass R M F<VAR>y✝ : M<VAR>f : E →ₗ.[R] F<VAR>x_fst : E<VAR>x_snd : F<VAR>fst✝ : E<VAR>snd✝ : F<VAR>h : fst✝ = x_fst ∧ -snd✝ = x_snd<VAR>y : ↥f.domain<VAR>hy : ↑y = (fst✝, snd✝).1<VAR>hx' : ↑f y = (fst✝, snd✝).2<GOAL>↑y = (x_fst, x_snd).1 ∧ ↑(-f) y = (x_fst, x_snd).2
<VAR>R : Type u_1<VAR>inst✝⁹ : Ring R<VAR>E : Type u_2<VAR>inst✝⁸ : AddCommGroup E<VAR>inst✝⁷ : Module R E<VAR>F : Type u_3<VAR>inst✝⁶ : AddCommGroup F<VAR>inst✝⁵ : Module R F<VAR>G : Type u_4<VAR>inst✝⁴ : AddCommGroup G<VAR>inst✝³ : Module R G<VAR>M : Type u_5<VAR>inst✝² : Monoid M<VAR>inst✝¹ : DistribMulAction M F<VAR>inst✝ : SMulCommClass R M F<VAR>y✝ : M<VAR>f : E →ₗ.[R] F<VAR>x_fst : E<VAR>x_snd : F<VAR>fst✝ : E<VAR>snd✝ : F<VAR>h : fst✝ = x_fst ∧ -snd✝ = x_snd<VAR>y : ↥f.domain<VAR>hy : ↑y = (fst✝, snd✝).1<VAR>hx' : ↑f y = (fst✝, snd✝).2<GOAL>↑y = (fst✝, -snd✝).1 ∧ ↑(-f) y = (fst✝, -snd✝).2
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : CommMonoid β<VAR>s t : Multiset α<VAR>a : α<VAR>m : Multiset ι<VAR>f g : ι → α<VAR>p : α → Prop<VAR>p_mul : ∀ (a b : α), p a → p b → p (a * b)<VAR>hs : s ≠ ∅<VAR>p_s : ∀ a ∈ s, p a<GOAL>p s.prod
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : CommMonoid β<VAR>s t : Multiset α<VAR>a : α<VAR>m : Multiset ι<VAR>f g : ι → α<VAR>p : α → Prop<VAR>p_mul : ∀ (a b : α), p a → p b → p (a * b)<VAR>hs : 0 ≠ ∅<VAR>p_s : ∀ a ∈ 0, p a<GOAL>p (prod 0)
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : CommMonoid β<VAR>s✝ t : Multiset α<VAR>a✝ : α<VAR>m : Multiset ι<VAR>f g : ι → α<VAR>p : α → Prop<VAR>p_mul : ∀ (a b : α), p a → p b → p (a * b)<VAR>a : α<VAR>s : Multiset α<VAR>hsa : s ≠ ∅ → (∀ a ∈ s, p a) → p s.prod<VAR>hs : a ::ₘ s ≠ ∅<VAR>p_s : ∀ a_1 ∈ a ::ₘ s, p a_1<GOAL>p (a ::ₘ s).prod
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : CommMonoid β<VAR>s✝ t : Multiset α<VAR>a✝ : α<VAR>m : Multiset ι<VAR>f g : ι → α<VAR>p : α → Prop<VAR>p_mul : ∀ (a b : α), p a → p b → p (a * b)<VAR>a : α<VAR>s : Multiset α<VAR>hsa : s ≠ ∅ → (∀ a ∈ s, p a) → p s.prod<VAR>hs : a ::ₘ s ≠ ∅<VAR>p_s : ∀ a_1 ∈ a ::ₘ s, p a_1<GOAL>p (a * s.prod)
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : CommMonoid β<VAR>s✝ t : Multiset α<VAR>a✝ : α<VAR>m : Multiset ι<VAR>f g : ι → α<VAR>p : α → Prop<VAR>p_mul : ∀ (a b : α), p a → p b → p (a * b)<VAR>a : α<VAR>s : Multiset α<VAR>hsa : s ≠ ∅ → (∀ a ∈ s, p a) → p s.prod<VAR>hs : a ::ₘ s ≠ ∅<VAR>p_s : ∀ a_1 ∈ a ::ₘ s, p a_1<VAR>hs_empty : ¬s = ∅<GOAL>p (a * s.prod)
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : CommMonoid β<VAR>s✝ t : Multiset α<VAR>a✝ : α<VAR>m : Multiset ι<VAR>f g : ι → α<VAR>p : α → Prop<VAR>p_mul : ∀ (a b : α), p a → p b → p (a * b)<VAR>a : α<VAR>s : Multiset α<VAR>hsa : s ≠ ∅ → (∀ a ∈ s, p a) → p s.prod<VAR>hs : a ::ₘ s ≠ ∅<VAR>p_s : ∀ a_1 ∈ a ::ₘ s, p a_1<VAR>hs_empty : ¬s = ∅<VAR>hps : ∀ x ∈ s, p x<GOAL>p (a * s.prod)
<VAR>α✝ : Type u_1<VAR>M✝ : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>R✝ : Type u_5<VAR>S : Type u_6<VAR>inst✝¹⁰ : Semiring R✝<VAR>inst✝⁹ : Semiring S<VAR>inst✝⁸ : AddCommMonoid M✝<VAR>inst✝⁷ : Module R✝ M✝<VAR>inst✝⁶ : AddCommMonoid N<VAR>inst✝⁵ : Module R✝ N<VAR>inst✝⁴ : AddCommMonoid P<VAR>inst✝³ : Module R✝ P<VAR>α : Type u_7<VAR>β : Type u_8<VAR>R : Type u_9<VAR>M : Type u_10<VAR>inst✝² : Semiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>f : α × β →₀ M<VAR>x : α<VAR>y : β<GOAL>(((finsuppProdLEquiv R) f) x) y = f (x, y)
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : FiniteDimensional ℝ E<GOAL>1 < 1 + ⋯.choose / 4
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedRing α<VAR>n : ℕ<VAR>a b c : α<GOAL>|a| ≤ |b| ↔ a * a ≤ b * b
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedRing α<VAR>n : ℕ<VAR>a b c : α<GOAL>|a| ≤ |b| ↔ |a| * |a| ≤ |b| * |b|
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ✝ : Kernel α (β × ℝ)<VAR>ν✝ : Kernel α β<VAR>x✝ : MeasurableSpace β<VAR>f : α × β → StieltjesFunction<VAR>κ : Kernel α (β × ℝ)<VAR>ν : Kernel α β<VAR>hf : IsCondKernelCDF f κ ν<VAR>p : α × β<VAR>x : ℝ<GOAL>((toKernel f hf) p) (Iic x) = ENNReal.ofReal (↑(f p) x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ✝ : Kernel α (β × ℝ)<VAR>ν✝ : Kernel α β<VAR>x✝ : MeasurableSpace β<VAR>f : α × β → StieltjesFunction<VAR>κ : Kernel α (β × ℝ)<VAR>ν : Kernel α β<VAR>hf : IsCondKernelCDF f κ ν<VAR>p : α × β<VAR>x : ℝ<GOAL>ENNReal.ofReal (↑(f p) x - 0) = ENNReal.ofReal (↑(f p) x)
<VAR>J : Type v<VAR>inst✝ : SmallCategory J<VAR>F : J ⥤ Cat<VAR>X✝ Y : limit (F ⋙ objects)<VAR>X : J<GOAL>{ obj := fun j => limit.π (F ⋙ objects) j X✝ ⟶ limit.π (F ⋙ objects) j Y, map := fun {X Y_1} f g => eqToHom ⋯ ≫ (F.map f).map g ≫ eqToHom ⋯ }.map (𝟙 X) = 𝟙 ({ obj := fun j => limit.π (F ⋙ objects) j X✝ ⟶ limit.π (F ⋙ objects) j Y, map := fun {X Y_1} f g => eqToHom ⋯ ≫ (F.map f).map g ≫ eqToHom ⋯ }.obj X)
<VAR>J : Type v<VAR>inst✝ : SmallCategory J<VAR>F : J ⥤ Cat<VAR>X✝ Y : limit (F ⋙ objects)<VAR>X : J<VAR>f : { obj := fun j => limit.π (F ⋙ objects) j X✝ ⟶ limit.π (F ⋙ objects) j Y, map := fun {X Y_1} f g => eqToHom ⋯ ≫ (F.map f).map g ≫ eqToHom ⋯ }.obj X<GOAL>{ obj := fun j => limit.π (F ⋙ objects) j X✝ ⟶ limit.π (F ⋙ objects) j Y, map := fun {X Y_1} f g => eqToHom ⋯ ≫ (F.map f).map g ≫ eqToHom ⋯ }.map (𝟙 X) f = 𝟙 ({ obj := fun j => limit.π (F ⋙ objects) j X✝ ⟶ limit.π (F ⋙ objects) j Y, map := fun {X Y_1} f g => eqToHom ⋯ ≫ (F.map f).map g ≫ eqToHom ⋯ }.obj X) f
<VAR>J : Type v<VAR>inst✝ : SmallCategory J<VAR>F : J ⥤ Cat<VAR>X✝ Y : limit (F ⋙ objects)<VAR>X : J<VAR>f : { obj := fun j => limit.π (F ⋙ objects) j X✝ ⟶ limit.π (F ⋙ objects) j Y, map := fun {X Y_1} f g => eqToHom ⋯ ≫ (F.map f).map g ≫ eqToHom ⋯ }.obj X<VAR>this : Category.{v, v} (objects.obj (F.obj X)) := inferInstance<GOAL>{ obj := fun j => limit.π (F ⋙ objects) j X✝ ⟶ limit.π (F ⋙ objects) j Y, map := fun {X Y_1} f g => eqToHom ⋯ ≫ (F.map f).map g ≫ eqToHom ⋯ }.map (𝟙 X) f = 𝟙 ({ obj := fun j => limit.π (F ⋙ objects) j X✝ ⟶ limit.π (F ⋙ objects) j Y, map := fun {X Y_1} f g => eqToHom ⋯ ≫ (F.map f).map g ≫ eqToHom ⋯ }.obj X) f
<VAR>J : Type v<VAR>inst✝ : SmallCategory J<VAR>F : J ⥤ Cat<VAR>X Y : limit (F ⋙ objects)<VAR>x✝¹ x✝ Z : J<VAR>f : x✝¹ ⟶ x✝<VAR>g : x✝ ⟶ Z<GOAL>{ obj := fun j => limit.π (F ⋙ objects) j X ⟶ limit.π (F ⋙ objects) j Y, map := fun {X_1 Y_1} f g => eqToHom ⋯ ≫ (F.map f).map g ≫ eqToHom ⋯ }.map (f ≫ g) = { obj := fun j => limit.π (F ⋙ objects) j X ⟶ limit.π (F ⋙ objects) j Y, map := fun {X_1 Y_1} f g => eqToHom ⋯ ≫ (F.map f).map g ≫ eqToHom ⋯ }.map f ≫ { obj := fun j => limit.π (F ⋙ objects) j X ⟶ limit.π (F ⋙ objects) j Y, map := fun {X_1 Y_1} f g => eqToHom ⋯ ≫ (F.map f).map g ≫ eqToHom ⋯ }.map g
<VAR>J : Type v<VAR>inst✝ : SmallCategory J<VAR>F : J ⥤ Cat<VAR>X Y : limit (F ⋙ objects)<VAR>x✝¹ x✝ Z : J<VAR>f : x✝¹ ⟶ x✝<VAR>g : x✝ ⟶ Z<VAR>h : { obj := fun j => limit.π (F ⋙ objects) j X ⟶ limit.π (F ⋙ objects) j Y, map := fun {X_1 Y_1} f g => eqToHom ⋯ ≫ (F.map f).map g ≫ eqToHom ⋯ }.obj x✝¹<GOAL>{ obj := fun j => limit.π (F ⋙ objects) j X ⟶ limit.π (F ⋙ objects) j Y, map := fun {X_1 Y_1} f g => eqToHom ⋯ ≫ (F.map f).map g ≫ eqToHom ⋯ }.map (f ≫ g) h = ({ obj := fun j => limit.π (F ⋙ objects) j X ⟶ limit.π (F ⋙ objects) j Y, map := fun {X_1 Y_1} f g => eqToHom ⋯ ≫ (F.map f).map g ≫ eqToHom ⋯ }.map f ≫ { obj := fun j => limit.π (F ⋙ objects) j X ⟶ limit.π (F ⋙ objects) j Y, map := fun {X_1 Y_1} f g => eqToHom ⋯ ≫ (F.map f).map g ≫ eqToHom ⋯ }.map g) h
<VAR>J : Type v<VAR>inst✝ : SmallCategory J<VAR>F : J ⥤ Cat<VAR>X Y : limit (F ⋙ objects)<VAR>x✝¹ x✝ Z : J<VAR>f : x✝¹ ⟶ x✝<VAR>g : x✝ ⟶ Z<VAR>h : { obj := fun j => limit.π (F ⋙ objects) j X ⟶ limit.π (F ⋙ objects) j Y, map := fun {X_1 Y_1} f g => eqToHom ⋯ ≫ (F.map f).map g ≫ eqToHom ⋯ }.obj x✝¹<VAR>this : Category.{v, v} (objects.obj (F.obj Z)) := inferInstance<GOAL>{ obj := fun j => limit.π (F ⋙ objects) j X ⟶ limit.π (F ⋙ objects) j Y, map := fun {X_1 Y_1} f g => eqToHom ⋯ ≫ (F.map f).map g ≫ eqToHom ⋯ }.map (f ≫ g) h = ({ obj := fun j => limit.π (F ⋙ objects) j X ⟶ limit.π (F ⋙ objects) j Y, map := fun {X_1 Y_1} f g => eqToHom ⋯ ≫ (F.map f).map g ≫ eqToHom ⋯ }.map f ≫ { obj := fun j => limit.π (F ⋙ objects) j X ⟶ limit.π (F ⋙ objects) j Y, map := fun {X_1 Y_1} f g => eqToHom ⋯ ≫ (F.map f).map g ≫ eqToHom ⋯ }.map g) h
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : Fintype α<VAR>s t : Finset α<VAR>inst✝ : DecidableEq α<VAR>a a✝ : α<GOAL>a✝ ∈ (insert a s)ᶜ ↔ a✝ ∈ sᶜ.erase a
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>inst✝⁹ : AddCommMonoid ι<VAR>inst✝⁸ : DecidableEq ι<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing A<VAR>inst✝⁵ : Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>inst✝⁴ : GradedAlgebra 𝒜<VAR>x : Submonoid A<VAR>α : Type u_4<VAR>inst✝³ : SMul α R<VAR>inst✝² : SMul α A<VAR>inst✝¹ : IsScalarTower α R A<VAR>inst✝ : IsScalarTower α A A<VAR>n : ℤ<VAR>y : HomogeneousLocalization 𝒜 x<GOAL>(n • y).val = n • y.val
<VAR>R : Type u<VAR>inst✝⁷ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type v<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>T : Type u_1<VAR>inst✝⁴ : CommSemiring T<VAR>inst✝³ : Algebra R T<VAR>inst✝² : IsLocalization S T<VAR>A : Type u_2<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>a : R<VAR>s : ↥S<GOAL>(algebraMap (Localization S) (LocalizedModule S A)) (Localization.mk a s) = mk ((algebraMap R A) a) s
<VAR>R : Type u<VAR>inst✝⁷ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type v<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>T : Type u_1<VAR>inst✝⁴ : CommSemiring T<VAR>inst✝³ : Algebra R T<VAR>inst✝² : IsLocalization S T<VAR>A : Type u_2<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>a : R<VAR>s : ↥S<GOAL>(algebraMap (Localization S) (LocalizedModule S A)) (IsLocalization.mk' (Localization S) a s) = mk ((algebraMap R A) a) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>f : α → β<VAR>s : Set β<VAR>ι : Type u_3<VAR>U : ι → Opens β<VAR>hU : iSup U = ⊤<VAR>h : Continuous f<GOAL>OpenEmbedding f ↔ ∀ (i : ι), OpenEmbedding ((U i).carrier.restrictPreimage f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>f : α → β<VAR>s : Set β<VAR>ι : Type u_3<VAR>U : ι → Opens β<VAR>hU : iSup U = ⊤<VAR>h : Continuous f<GOAL>Embedding f ∧ IsOpen (range f) ↔ ∀ (i : ι), Embedding ((U i).carrier.restrictPreimage f) ∧ IsOpen (range ((U i).carrier.restrictPreimage f))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>f : α → β<VAR>s : Set β<VAR>ι : Type u_3<VAR>U : ι → Opens β<VAR>hU : iSup U = ⊤<VAR>h : Continuous f<GOAL>Embedding f ∧ IsOpen (range f) ↔ (∀ (x : ι), Embedding ((U x).carrier.restrictPreimage f)) ∧ ∀ (x : ι), IsOpen (range ((U x).carrier.restrictPreimage f))