ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹⁵ : Category.{u_4, u_1} C<VAR>inst✝¹⁴ : Category.{u_3, u_2} D<VAR>L : C ⥤ D<VAR>inst✝¹³ : HasShift C ℤ<VAR>inst✝¹² : Preadditive C<VAR>inst✝¹¹ : HasZeroObject C<VAR>inst✝¹⁰ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝⁹ : Pretriangulated C<VAR>inst✝⁸ : HasShift D ℤ<VAR>inst✝⁷ : L.CommShift ℤ<VAR>W : MorphismProperty C<VAR>inst✝⁶ : L.IsLocalization W<VAR>inst✝⁵ : W.IsCompatibleWithTriangulation<VAR>inst✝⁴ : W.HasLeftCalculusOfFractions<VAR>inst✝³ : Preadditive D<VAR>inst✝² : HasZeroObject D<VAR>inst✝¹ : ∀ (n : ℤ), (shiftFunctor D n).Additive<VAR>inst✝ : L.Additive<VAR>T₁ T₂ : Triangle C<VAR>hT₁ : T₁ ∈ distinguishedTriangles<VAR>hT₂ : T₂ ∈ distinguishedTriangles<VAR>a : L.obj T₁.obj₁ ⟶ L.obj T₂.obj₁<VAR>b : L.obj T₁.obj₂ ⟶ L.obj T₂.obj₂<VAR>fac✝ : L.map T₁.mor₁ ≫ b = a ≫ L.map T₂.mor₁<VAR>α : W.LeftFraction T₁.obj₁ T₂.obj₁<VAR>hα : a = α.map L ⋯<VAR>β : W.LeftFraction α.Y' T₂.obj₂<VAR>hβ : T₂.mor₁ ≫ β.s = α.s ≫ β.f<VAR>γ : W.LeftFraction T₁.obj₂ β.Y'<VAR>hγ : b ≫ L.map β.s = γ.map L ⋯<VAR>this✝¹ : IsIso (L.map β.s)<VAR>this✝ : IsIso (L.map γ.s)<VAR>Z₂ : C<VAR>σ : γ.Y' ⟶ Z₂<VAR>hσ : W σ<VAR>fac : α.f ≫ β.f ≫ γ.s ≫ σ = T₁.mor₁ ≫ γ.f ≫ σ<VAR>Y₃ : C<VAR>g : Z₂ ⟶ Y₃<VAR>h : Y₃ ⟶ (shiftFunctor C 1).obj α.Y'<VAR>T₃ : Triangle C := Triangle.mk (β.f ≫ γ.s ≫ σ) g h<VAR>hT₃ : T₃ ∈ distinguishedTriangles<VAR>hβγσ : W (β.s ≫ γ.s ≫ σ)<VAR>ψ₃ : T₂.obj₃ ⟶ T₃.obj₃<VAR>hψ₃ : W ψ₃<VAR>hψ₁ : T₂.mor₂ ≫ ψ₃ = (β.s ≫ γ.s ≫ σ) ≫ T₃.mor₂<VAR>hψ₂ : T₂.mor₃ ≫ (shiftFunctor C 1).map α.s = ψ₃ ≫ T₃.mor₃<VAR>ψ : T₂ ⟶ T₃ := T₂.homMk T₃ α.s (β.s ≫ γ.s ≫ σ) ψ₃ ⋯ hψ₁ hψ₂<VAR>this : IsIso (L.mapTriangle.map ψ)<GOAL>(L.mapTriangle.map (completeDistinguishedTriangleMorphism T₁ T₃ hT₁ hT₃ α.f (γ.f ≫ σ) ⋯) ≫ inv (L.mapTriangle.map ψ)).hom₂ = b
<VAR>α✝ : Type u_1<VAR>ι : Type u_2<VAR>γ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>tβ : TopologicalSpace β<VAR>inst✝⁹ : T2Space β<VAR>inst✝⁸ : MeasurableSpace β<VAR>inst✝⁷ : MeasurableSpace α<VAR>s : Set γ<VAR>f✝ : γ → β<VAR>inst✝⁶ : MeasurableSpace γ<VAR>inst✝⁵ : Countable ι<VAR>l : Filter ι<VAR>inst✝⁴ : l.IsCountablyGenerated<VAR>inst✝³ : TopologicalSpace γ<VAR>inst✝² : SecondCountableTopology γ<VAR>inst✝¹ : PseudoMetrizableSpace γ<VAR>inst✝ : OpensMeasurableSpace γ<VAR>f : ι → β → γ<VAR>hf : ∀ (i : ι), Measurable (f i)<VAR>g : β → γ<VAR>hg : Measurable g<VAR>this : PseudoMetricSpace γ := pseudoMetrizableSpacePseudoMetric γ<GOAL>MeasurableSet {x | Tendsto (fun n => f n x) l (𝓝 (g x))}
<VAR>α✝ : Type u_1<VAR>ι : Type u_2<VAR>γ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>tβ : TopologicalSpace β<VAR>inst✝⁹ : T2Space β<VAR>inst✝⁸ : MeasurableSpace β<VAR>inst✝⁷ : MeasurableSpace α<VAR>s : Set γ<VAR>f✝ : γ → β<VAR>inst✝⁶ : MeasurableSpace γ<VAR>inst✝⁵ : Countable ι<VAR>l : Filter ι<VAR>inst✝⁴ : l.IsCountablyGenerated<VAR>inst✝³ : TopologicalSpace γ<VAR>inst✝² : SecondCountableTopology γ<VAR>inst✝¹ : PseudoMetrizableSpace γ<VAR>inst✝ : OpensMeasurableSpace γ<VAR>f : ι → β → γ<VAR>hf : ∀ (i : ι), Measurable (f i)<VAR>g : β → γ<VAR>hg : Measurable g<VAR>this : PseudoMetricSpace γ := pseudoMetrizableSpacePseudoMetric γ<GOAL>MeasurableSet {x | Tendsto (fun b => dist (f b x) (g x)) l (𝓝 0)}
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>a b : ℝ<VAR>f g✝ : ℝ → E<VAR>μ : Measure ℝ<VAR>g : ℝ → ℝ<VAR>h : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ‖f t‖ ≤ g t<VAR>hbound : IntervalIntegrable g μ a b<GOAL>‖∫ (t : ℝ) in a..b, f t ∂μ‖ ≤ |∫ (t : ℝ) in a..b, g t ∂μ|
<VAR>X✝ Y : Scheme<VAR>f : X✝ ⟶ Y<VAR>X : Scheme<VAR>U : X.Opens<VAR>hU : IsCompact U.carrier<GOAL>IsQuasiSeparated U.carrier → ∀ (f : ↑Γ(X, U)) (x : ↑Γ(X, X.basicOpen f)), ∃ n y, (X.presheaf.map (homOfLE ⋯).op) y = (X.presheaf.map (homOfLE ⋯).op) f ^ n * x
<VAR>X✝ Y : Scheme<VAR>f : X✝ ⟶ Y<VAR>X : Scheme<VAR>U : X.Opens<VAR>hU : IsCompact U.carrier<GOAL>IsQuasiSeparated ⊥.carrier → ∀ (f : ↑Γ(X, ⊥)) (x : ↑Γ(X, X.basicOpen f)), ∃ n y, (X.presheaf.map (homOfLE ⋯).op) y = (X.presheaf.map (homOfLE ⋯).op) f ^ n * x
<VAR>X✝ Y : Scheme<VAR>f : X✝ ⟶ Y<VAR>X : Scheme<VAR>U : X.Opens<VAR>hU : IsCompact U.carrier<GOAL>∀ (S : X.Opens), IsCompact S.carrier → ∀ (U : ↑X.affineOpens), (IsQuasiSeparated S.carrier → ∀ (f : ↑Γ(X, S)) (x : ↑Γ(X, X.basicOpen f)), ∃ n y, (X.presheaf.map (homOfLE ⋯).op) y = (X.presheaf.map (homOfLE ⋯).op) f ^ n * x) → IsQuasiSeparated (S ⊔ ↑U).carrier → ∀ (f : ↑Γ(X, S ⊔ ↑U)) (x : ↑Γ(X, X.basicOpen f)), ∃ n y, (X.presheaf.map (homOfLE ⋯).op) y = (X.presheaf.map (homOfLE ⋯).op) f ^ n * x
<VAR>G : Type u<VAR>inst✝² : Group G<VAR>N : Subgroup G<VAR>nN : N.Normal<VAR>H : Type v<VAR>inst✝¹ : Group H<VAR>M : Type x<VAR>inst✝ : Monoid M<VAR>φ : G →* H<VAR>ψ : H → G<VAR>hφ : Function.RightInverse ψ ⇑φ<VAR>x : G ⧸ φ.ker<GOAL>(kerLift φ) ((mk ∘ ψ) ((kerLift φ) x)) = (kerLift φ) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>γ₂ : Type u_4<VAR>δ : Type u_5<VAR>ι : Sort y<VAR>s✝ t u : Set α<VAR>inst✝¹⁵ : TopologicalSpace α<VAR>inst✝¹⁴ : MeasurableSpace α<VAR>inst✝¹³ : OpensMeasurableSpace α<VAR>inst✝¹² : TopologicalSpace β<VAR>inst✝¹¹ : MeasurableSpace β<VAR>inst✝¹⁰ : OpensMeasurableSpace β<VAR>inst✝⁹ : TopologicalSpace γ<VAR>inst✝⁸ : MeasurableSpace γ<VAR>inst✝⁷ : BorelSpace γ<VAR>inst✝⁶ : TopologicalSpace γ₂<VAR>inst✝⁵ : MeasurableSpace γ₂<VAR>inst✝⁴ : BorelSpace γ₂<VAR>inst✝³ : MeasurableSpace δ<VAR>α' : Type u_6<VAR>inst✝² : TopologicalSpace α'<VAR>inst✝¹ : MeasurableSpace α'<VAR>f g : α → γ<VAR>s : Set α<VAR>inst✝ : (j : α) → Decidable (j ∈ s)<VAR>hf : ContinuousOn f s<VAR>hg : ContinuousOn g sᶜ<VAR>hs : MeasurableSet s<GOAL>Measurable (s.piecewise f g)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>γ₂ : Type u_4<VAR>δ : Type u_5<VAR>ι : Sort y<VAR>s✝ t✝ u : Set α<VAR>inst✝¹⁵ : TopologicalSpace α<VAR>inst✝¹⁴ : MeasurableSpace α<VAR>inst✝¹³ : OpensMeasurableSpace α<VAR>inst✝¹² : TopologicalSpace β<VAR>inst✝¹¹ : MeasurableSpace β<VAR>inst✝¹⁰ : OpensMeasurableSpace β<VAR>inst✝⁹ : TopologicalSpace γ<VAR>inst✝⁸ : MeasurableSpace γ<VAR>inst✝⁷ : BorelSpace γ<VAR>inst✝⁶ : TopologicalSpace γ₂<VAR>inst✝⁵ : MeasurableSpace γ₂<VAR>inst✝⁴ : BorelSpace γ₂<VAR>inst✝³ : MeasurableSpace δ<VAR>α' : Type u_6<VAR>inst✝² : TopologicalSpace α'<VAR>inst✝¹ : MeasurableSpace α'<VAR>f g : α → γ<VAR>s : Set α<VAR>inst✝ : (j : α) → Decidable (j ∈ s)<VAR>hf : ContinuousOn f s<VAR>hg : ContinuousOn g sᶜ<VAR>hs : MeasurableSet s<VAR>t : Set γ<VAR>ht : IsOpen t<GOAL>MeasurableSet (s.piecewise f g ⁻¹' t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>γ₂ : Type u_4<VAR>δ : Type u_5<VAR>ι : Sort y<VAR>s✝ t✝ u : Set α<VAR>inst✝¹⁵ : TopologicalSpace α<VAR>inst✝¹⁴ : MeasurableSpace α<VAR>inst✝¹³ : OpensMeasurableSpace α<VAR>inst✝¹² : TopologicalSpace β<VAR>inst✝¹¹ : MeasurableSpace β<VAR>inst✝¹⁰ : OpensMeasurableSpace β<VAR>inst✝⁹ : TopologicalSpace γ<VAR>inst✝⁸ : MeasurableSpace γ<VAR>inst✝⁷ : BorelSpace γ<VAR>inst✝⁶ : TopologicalSpace γ₂<VAR>inst✝⁵ : MeasurableSpace γ₂<VAR>inst✝⁴ : BorelSpace γ₂<VAR>inst✝³ : MeasurableSpace δ<VAR>α' : Type u_6<VAR>inst✝² : TopologicalSpace α'<VAR>inst✝¹ : MeasurableSpace α'<VAR>f g : α → γ<VAR>s : Set α<VAR>inst✝ : (j : α) → Decidable (j ∈ s)<VAR>hf : ContinuousOn f s<VAR>hg : ContinuousOn g sᶜ<VAR>hs : MeasurableSet s<VAR>t : Set γ<VAR>ht : IsOpen t<GOAL>MeasurableSet (f ⁻¹' t ∩ s ∪ g ⁻¹' t \ s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>γ₂ : Type u_4<VAR>δ : Type u_5<VAR>ι : Sort y<VAR>s✝ t✝ u : Set α<VAR>inst✝¹⁵ : TopologicalSpace α<VAR>inst✝¹⁴ : MeasurableSpace α<VAR>inst✝¹³ : OpensMeasurableSpace α<VAR>inst✝¹² : TopologicalSpace β<VAR>inst✝¹¹ : MeasurableSpace β<VAR>inst✝¹⁰ : OpensMeasurableSpace β<VAR>inst✝⁹ : TopologicalSpace γ<VAR>inst✝⁸ : MeasurableSpace γ<VAR>inst✝⁷ : BorelSpace γ<VAR>inst✝⁶ : TopologicalSpace γ₂<VAR>inst✝⁵ : MeasurableSpace γ₂<VAR>inst✝⁴ : BorelSpace γ₂<VAR>inst✝³ : MeasurableSpace δ<VAR>α' : Type u_6<VAR>inst✝² : TopologicalSpace α'<VAR>inst✝¹ : MeasurableSpace α'<VAR>f g : α → γ<VAR>s : Set α<VAR>inst✝ : (j : α) → Decidable (j ∈ s)<VAR>hf : ContinuousOn f s<VAR>hg : ContinuousOn g sᶜ<VAR>hs : MeasurableSet s<VAR>t : Set γ<VAR>ht : IsOpen t<GOAL>MeasurableSet (f ⁻¹' t ∩ s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>γ₂ : Type u_4<VAR>δ : Type u_5<VAR>ι : Sort y<VAR>s✝ t✝ u : Set α<VAR>inst✝¹⁵ : TopologicalSpace α<VAR>inst✝¹⁴ : MeasurableSpace α<VAR>inst✝¹³ : OpensMeasurableSpace α<VAR>inst✝¹² : TopologicalSpace β<VAR>inst✝¹¹ : MeasurableSpace β<VAR>inst✝¹⁰ : OpensMeasurableSpace β<VAR>inst✝⁹ : TopologicalSpace γ<VAR>inst✝⁸ : MeasurableSpace γ<VAR>inst✝⁷ : BorelSpace γ<VAR>inst✝⁶ : TopologicalSpace γ₂<VAR>inst✝⁵ : MeasurableSpace γ₂<VAR>inst✝⁴ : BorelSpace γ₂<VAR>inst✝³ : MeasurableSpace δ<VAR>α' : Type u_6<VAR>inst✝² : TopologicalSpace α'<VAR>inst✝¹ : MeasurableSpace α'<VAR>f g : α → γ<VAR>s : Set α<VAR>inst✝ : (j : α) → Decidable (j ∈ s)<VAR>hf : ContinuousOn f s<VAR>hg : ContinuousOn g sᶜ<VAR>hs : MeasurableSet s<VAR>t : Set γ<VAR>ht : IsOpen t<GOAL>MeasurableSet (g ⁻¹' t \ s)
<VAR>n : ℕ<VAR>c : Composition n<VAR>h : 0 < n<GOAL>0 < c.length
<VAR>n : ℕ<VAR>c : Composition n<VAR>h : 0 < n<GOAL>0 < c.blocks.sum
<VAR>n : ℕ<VAR>c : Composition n<VAR>h : 0 < n<GOAL>c.blocks.sum = n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>e : α ≃o β<VAR>a b : β<GOAL>⇑e ⁻¹' Ioc a b = Ioc (e.symm a) (e.symm b)
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>X✝ Y✝ : C<VAR>inst✝¹ : HasTerminal C<VAR>inst✝ : HasBinaryProducts C<VAR>X Y Z : C<GOAL>(α_ X Y Z).hom ≫ prod.snd ≫ prod.snd = prod.snd
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<VAR>U : Set G<VAR>hU : (interior U).Nonempty<VAR>K : Set G<VAR>h1K : IsCompact K<VAR>h2K : (interior K).Nonempty<GOAL>0 < prehaar (↑K₀) U { carrier := K, isCompact' := h1K }
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<VAR>U : Set G<VAR>hU : (interior U).Nonempty<VAR>K : Set G<VAR>h1K : IsCompact K<VAR>h2K : (interior K).Nonempty<GOAL>0 < index (↑{ carrier := K, isCompact' := h1K }) U
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<VAR>U : Set G<VAR>hU : (interior U).Nonempty<VAR>K : Set G<VAR>h1K : IsCompact K<VAR>h2K : (interior K).Nonempty<GOAL>0 < index (↑K₀) U
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : CommMonoid β<VAR>f : Fin 4 → β<GOAL>∏ i : Fin 4, f i = f 0 * f 1 * f 2 * f 3
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : CommMonoid β<VAR>f : Fin 4 → β<GOAL>f (castSucc 0) * f (castSucc 1) * f (castSucc 2) * f (last 3) = f 0 * f 1 * f 2 * f 3
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>inst✝² : LinearOrderedAddCommGroup 𝕜<VAR>inst✝¹ : TopologicalSpace 𝕜<VAR>inst✝ : OrderTopology 𝕜<VAR>p x : 𝕜<GOAL>↑(x + p) = ↑x
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B B' I J D X : Set α<VAR>e f : α<VAR>hX : autoParam (X ⊆ M.E) _auto✝<GOAL>M.Indep X ∨ M.Dep X
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B B' I J D X : Set α<VAR>e f : α<VAR>hX : autoParam (X ⊆ M.E) _auto✝<GOAL>M.Indep X ∨ ¬M.Indep X
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>α : Type u<VAR>x : F α<VAR>x✝ : α<GOAL>x✝ ∈ supp x ↔ x✝ ∈ {u | ∀ (a : (P F).A) (f : (P F).B a → α), abs ⟨a, f⟩ = x → u ∈ f '' univ}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : LinearOrder α<VAR>inst✝⁴ : Mul α<VAR>inst✝³ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>inst✝² : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a₁ a₂ b₁ b₂ : α<VAR>ha : a₁ ≤ a₂<VAR>hb : b₁ ≤ b₂<GOAL>a₁ * b₁ < a₂ * b₂ ↔ a₁ < a₂ ∨ b₁ < b₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : LinearOrder α<VAR>inst✝⁴ : Mul α<VAR>inst✝³ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>inst✝² : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a₁ a₂ b₁ b₂ : α<VAR>ha : a₁ ≤ a₂<VAR>hb : b₁ ≤ b₂<VAR>h : a₁ < a₂ ∨ b₁ < b₂<GOAL>a₁ * b₁ < a₂ * b₂
<VAR>R : Type u<VAR>K : Type u'<VAR>M : Type v<VAR>V : Type v'<VAR>M₂ : Type w<VAR>V₂ : Type w'<VAR>M₃ : Type y<VAR>V₃ : Type y'<VAR>M₄ : Type z<VAR>ι : Type x<VAR>M₅ : Type u_1<VAR>M₆ : Type u_2<VAR>S : Type u_3<VAR>inst✝¹⁵ : Semiring R<VAR>inst✝¹⁴ : Semiring S<VAR>inst✝¹³ : AddCommMonoid M<VAR>inst✝¹² : AddCommMonoid M₂<VAR>inst✝¹¹ : AddCommMonoid M₃<VAR>inst✝¹⁰ : AddCommMonoid M₄<VAR>inst✝⁹ : AddCommMonoid M₅<VAR>inst✝⁸ : AddCommMonoid M₆<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R M₂<VAR>inst✝⁵ : Module R M₃<VAR>inst✝⁴ : Module R M₄<VAR>inst✝³ : Module R M₅<VAR>inst✝² : Module R M₆<VAR>f✝ : M →ₗ[R] M₂<VAR>inst✝¹ : Module S M₃<VAR>inst✝ : SMulCommClass R S M₃<VAR>f : (M →ₗ[R] M₃) × (M₂ →ₗ[R] M₃)<GOAL>(fun f => (f ∘ₗ inl R M M₂, f ∘ₗ inr R M M₂)) ({ toFun := fun f => f.1.coprod f.2, map_add' := ⋯, map_smul' := ⋯ }.toFun f) = f
<VAR>R : Type u<VAR>K : Type u'<VAR>M : Type v<VAR>V : Type v'<VAR>M₂ : Type w<VAR>V₂ : Type w'<VAR>M₃ : Type y<VAR>V₃ : Type y'<VAR>M₄ : Type z<VAR>ι : Type x<VAR>M₅ : Type u_1<VAR>M₆ : Type u_2<VAR>S : Type u_3<VAR>inst✝¹⁵ : Semiring R<VAR>inst✝¹⁴ : Semiring S<VAR>inst✝¹³ : AddCommMonoid M<VAR>inst✝¹² : AddCommMonoid M₂<VAR>inst✝¹¹ : AddCommMonoid M₃<VAR>inst✝¹⁰ : AddCommMonoid M₄<VAR>inst✝⁹ : AddCommMonoid M₅<VAR>inst✝⁸ : AddCommMonoid M₆<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R M₂<VAR>inst✝⁵ : Module R M₃<VAR>inst✝⁴ : Module R M₄<VAR>inst✝³ : Module R M₅<VAR>inst✝² : Module R M₆<VAR>f✝ : M →ₗ[R] M₂<VAR>inst✝¹ : Module S M₃<VAR>inst✝ : SMulCommClass R S M₃<VAR>f : M × M₂ →ₗ[R] M₃<GOAL>{ toFun := fun f => f.1.coprod f.2, map_add' := ⋯, map_smul' := ⋯ }.toFun ((fun f => (f ∘ₗ inl R M M₂, f ∘ₗ inr R M M₂)) f) = f
<VAR>R : Type u<VAR>K : Type u'<VAR>M : Type v<VAR>V : Type v'<VAR>M₂ : Type w<VAR>V₂ : Type w'<VAR>M₃ : Type y<VAR>V₃ : Type y'<VAR>M₄ : Type z<VAR>ι : Type x<VAR>M₅ : Type u_1<VAR>M₆ : Type u_2<VAR>S : Type u_3<VAR>inst✝¹⁵ : Semiring R<VAR>inst✝¹⁴ : Semiring S<VAR>inst✝¹³ : AddCommMonoid M<VAR>inst✝¹² : AddCommMonoid M₂<VAR>inst✝¹¹ : AddCommMonoid M₃<VAR>inst✝¹⁰ : AddCommMonoid M₄<VAR>inst✝⁹ : AddCommMonoid M₅<VAR>inst✝⁸ : AddCommMonoid M₆<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R M₂<VAR>inst✝⁵ : Module R M₃<VAR>inst✝⁴ : Module R M₄<VAR>inst✝³ : Module R M₅<VAR>inst✝² : Module R M₆<VAR>f : M →ₗ[R] M₂<VAR>inst✝¹ : Module S M₃<VAR>inst✝ : SMulCommClass R S M₃<VAR>a b : (M →ₗ[R] M₃) × (M₂ →ₗ[R] M₃)<VAR>x✝ : M × M₂<GOAL>((fun f => f.1.coprod f.2) (a + b)) x✝ = ((fun f => f.1.coprod f.2) a + (fun f => f.1.coprod f.2) b) x✝
<VAR>R : Type u<VAR>K : Type u'<VAR>M : Type v<VAR>V : Type v'<VAR>M₂ : Type w<VAR>V₂ : Type w'<VAR>M₃ : Type y<VAR>V₃ : Type y'<VAR>M₄ : Type z<VAR>ι : Type x<VAR>M₅ : Type u_1<VAR>M₆ : Type u_2<VAR>S : Type u_3<VAR>inst✝¹⁵ : Semiring R<VAR>inst✝¹⁴ : Semiring S<VAR>inst✝¹³ : AddCommMonoid M<VAR>inst✝¹² : AddCommMonoid M₂<VAR>inst✝¹¹ : AddCommMonoid M₃<VAR>inst✝¹⁰ : AddCommMonoid M₄<VAR>inst✝⁹ : AddCommMonoid M₅<VAR>inst✝⁸ : AddCommMonoid M₆<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R M₂<VAR>inst✝⁵ : Module R M₃<VAR>inst✝⁴ : Module R M₄<VAR>inst✝³ : Module R M₅<VAR>inst✝² : Module R M₆<VAR>f : M →ₗ[R] M₂<VAR>inst✝¹ : Module S M₃<VAR>inst✝ : SMulCommClass R S M₃<VAR>r : S<VAR>a : (M →ₗ[R] M₃) × (M₂ →ₗ[R] M₃)<VAR>x✝ : M × M₂<GOAL>((r • a.1).coprod (r • a.2)) x✝ = (r • a.1.coprod a.2) x✝
<VAR>K : Type u_1<VAR>inst✝² : Field K<VAR>inst✝¹ : NumberField K<VAR>inst✝ : DecidableEq (K →+* ℂ)<GOAL>0 ≤ NumberField.house.c K
<VAR>K : Type u_1<VAR>inst✝² : Field K<VAR>inst✝¹ : NumberField K<VAR>inst✝ : DecidableEq (K →+* ℂ)<GOAL>0 ≤ ↑(finrank ℚ K) ∧ 0 ≤ ‖(basisMatrix K)ᵀ⁻¹‖ ∨ ↑(finrank ℚ K) ≤ 0 ∧ ‖(basisMatrix K)ᵀ⁻¹‖ ≤ 0
<VAR>K : Type u_1<VAR>inst✝² : Field K<VAR>inst✝¹ : NumberField K<VAR>inst✝ : DecidableEq (K →+* ℂ)<GOAL>0 ≤ ↑(finrank ℚ K) ∧ 0 ≤ ‖(basisMatrix K)ᵀ⁻¹‖
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>inst✝² : SMulCommClass ℝ 𝕜 E<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace E<VAR>f : ↥(Lp E 1 μ)<GOAL>integralCLM (-f) = -integralCLM f
<VAR>R : Type uR<VAR>inst✝⁵ : Semiring R<VAR>S : Type uS<VAR>inst✝⁴ : CommSemiring S<VAR>T : Type uT<VAR>A : Type uA<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra S A<VAR>r✝ : R → R → Prop<VAR>inst✝¹ : Semiring T<VAR>B : Type uR<VAR>inst✝ : CommRing B<VAR>r : B → B → Prop<VAR>x : B<GOAL>(ringQuotToIdealQuotient r) ((mkRingHom r) x) = (Ideal.Quotient.mk (Ideal.ofRel r)) x
<VAR>R : Type uR<VAR>inst✝⁵ : Semiring R<VAR>S : Type uS<VAR>inst✝⁴ : CommSemiring S<VAR>T : Type uT<VAR>A : Type uA<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra S A<VAR>r✝ : R → R → Prop<VAR>inst✝¹ : Semiring T<VAR>B : Type uR<VAR>inst✝ : CommRing B<VAR>r : B → B → Prop<VAR>x : B<GOAL>({ toFun := fun f => { toFun := fun x => Quot.lift ⇑↑f ⋯ x.toQuot, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }, invFun := fun F => ⟨F.comp { toFun := fun x => { toQuot := Quot.mk (Rel r) x }, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }, ⋯⟩, left_inv := ⋯, right_inv := ⋯ } ⟨Ideal.Quotient.mk (Ideal.ofRel r), ⋯⟩) ({ toFun := fun x => { toQuot := Quot.mk (Rel r) x }, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } x) = (Ideal.Quotient.mk (Ideal.ofRel r)) x
<VAR>G✝ : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>G : Type u_6<VAR>inst✝¹ : Group G<VAR>inst✝ : Fintype G<VAR>S : Set G<VAR>a : G<VAR>ha : a ∈ S<GOAL>1 ∈ S ^ card G
<VAR>G✝ : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>G : Type u_6<VAR>inst✝¹ : Group G<VAR>inst✝ : Fintype G<VAR>S : Set G<VAR>a : G<VAR>ha : a ∈ S<GOAL>?m.411653 ^ card G ∈ S ^ card G
<VAR>G✝ : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>G : Type u_6<VAR>inst✝¹ : Group G<VAR>inst✝ : Fintype G<VAR>S : Set G<VAR>a : G<VAR>ha : a ∈ S<GOAL>G
<VAR>G✝ : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>G : Type u_6<VAR>inst✝¹ : Group G<VAR>inst✝ : Fintype G<VAR>S : Set G<VAR>hS : S.Nonempty<VAR>one_mem : 1 ∈ S ^ card G<GOAL>S ^ card G * S ^ card G = S ^ card G
<VAR>a b : ℤ<GOAL>Associated a b ↔ a.natAbs = b.natAbs
<VAR>a b : ℤ<GOAL>Associated a.natAbs b.natAbs ↔ a.natAbs = b.natAbs
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>L : Filter ι<VAR>inst✝³ : MeasurableSpace Ω<VAR>inst✝² : TopologicalSpace Ω<VAR>inst✝¹ : OpensMeasurableSpace Ω<VAR>inst✝ : HasOuterApproxClosed Ω<VAR>μ : ProbabilityMeasure Ω<VAR>μs : ι → ProbabilityMeasure Ω<VAR>μs_lim : Tendsto μs L (𝓝 μ)<VAR>F : Set Ω<VAR>F_closed : IsClosed F<GOAL>limsup (fun i => ↑(μs i) F) L ≤ ↑μ F
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝³ : CommGroup α<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalGroup α<VAR>f g : β → α<VAR>a✝ a₁ a₂ : α<VAR>hf : HasProd f a₁<VAR>b : β<VAR>inst✝ : DecidableEq β<VAR>a : α<GOAL>HasProd (Function.update f b a) (a / f b * a₁)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝³ : CommGroup α<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalGroup α<VAR>f g : β → α<VAR>a✝ a₁ a₂ : α<VAR>hf : HasProd f a₁<VAR>b : β<VAR>inst✝ : DecidableEq β<VAR>a : α<VAR>b' : β<GOAL>Function.update f b a b' = (if b' = b then a / f b else 1) * f b'
<VAR>ι : Type u<VAR>s : Finset ι<VAR>p : ℝ<VAR>a b : ℝ≥0<VAR>hp1 : 1 ≤ p<GOAL>(a ^ p + b ^ p) ^ (1 / p) ≤ a + b
<VAR>ι : Type u<VAR>s : Finset ι<VAR>p : ℝ<VAR>a b : ℝ≥0<VAR>hp1 : 1 ≤ p<GOAL>(a ^ p + b ^ p) ^ p⁻¹ ≤ a + b
<VAR>ι : Type u<VAR>s : Finset ι<VAR>p : ℝ<VAR>a b : ℝ≥0<VAR>hp1 : 1 ≤ p<GOAL>a ^ p + b ^ p ≤ (a + b) ^ p⁻¹⁻¹
<VAR>ι : Type u<VAR>s : Finset ι<VAR>p : ℝ<VAR>a b : ℝ≥0<VAR>hp1 : 1 ≤ p<GOAL>a ^ p + b ^ p ≤ (a + b) ^ p
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>x y : E<GOAL>re ⟪x, y⟫_𝕜 = re ⟪y, x⟫_𝕜
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : CommRing A<VAR>inst✝⁷ : Field K<VAR>R₁ : Type u_4<VAR>inst✝⁶ : CommRing R₁<VAR>inst✝⁵ : IsDomain R₁<VAR>inst✝⁴ : Algebra R₁ K<VAR>inst✝³ : IsFractionRing R₁ K<VAR>I J : FractionalIdeal R₁⁰ K<VAR>K' : Type u_5<VAR>inst✝² : Field K'<VAR>inst✝¹ : Algebra R₁ K'<VAR>inst✝ : IsFractionRing R₁ K'<VAR>x : R₁<VAR>hx : x ≠ 0<GOAL>↑(Ideal.span {x}) * (↑(Ideal.span {x}))⁻¹ = 1
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ p q : R[X]<VAR>ι : Type u_1<VAR>hf : p.Monic<VAR>hfd : p.natDegree = 0<GOAL>p = 1
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ p q : R[X]<VAR>ι : Type u_1<VAR>hf : p.coeff 0 = 1<VAR>hfd : p.natDegree = 0<GOAL>p = 1
<VAR>ι : Type u<VAR>inst✝ : Infinite ι<VAR>c : ι → Cardinal.{v}<VAR>h₁ : ∀ (i : ι), 2 ≤ c i<VAR>h₂ : ∀ (i : ι), lift.{u, v} (c i) ≤ lift.{v, u} #ι<GOAL>prod c = 2 ^ lift.{v, u} #ι
<VAR>ι : Type u<VAR>inst✝ : Infinite ι<VAR>c : ι → Cardinal.{v}<VAR>h₁ : ∀ (i : ι), 2 ≤ c i<VAR>h₂ : ∀ (i : ι), lift.{u, v} (c i) ≤ lift.{v, u} #ι<GOAL>(prod fun i => lift.{u, v} (c i)) = lift.{v, u} (2 ^ #ι)
<VAR>ι : Type u<VAR>inst✝ : Infinite ι<VAR>c : ι → Cardinal.{v}<VAR>h₁ : ∀ (i : ι), 2 ≤ c i<VAR>h₂ : ∀ (i : ι), lift.{u, v} (c i) ≤ lift.{v, u} #ι<GOAL>(prod fun i => lift.{u, v} (c i)) ≤ lift.{v, u} (2 ^ #ι)
<VAR>ι : Type u<VAR>inst✝ : Infinite ι<VAR>c : ι → Cardinal.{v}<VAR>h₁ : ∀ (i : ι), 2 ≤ c i<VAR>h₂ : ∀ (i : ι), lift.{u, v} (c i) ≤ lift.{v, u} #ι<GOAL>lift.{v, u} (2 ^ #ι) ≤ prod fun i => lift.{u, v} (c i)
<VAR>Γ✝ : Type u_1<VAR>Γ' : Type u_2<VAR>R : Type u_3<VAR>V : Type u_4<VAR>inst✝² : OrderedCancelAddCommMonoid Γ✝<VAR>Γ : Type u_5<VAR>inst✝¹ : LinearOrderedCancelAddCommMonoid Γ<VAR>inst✝ : NonUnitalNonAssocSemiring R<VAR>x y : HahnSeries Γ R<GOAL>(x * y).coeff (x.order + y.order) = x.leadingCoeff * y.leadingCoeff
<VAR>Γ✝ : Type u_1<VAR>Γ' : Type u_2<VAR>R : Type u_3<VAR>V : Type u_4<VAR>inst✝² : OrderedCancelAddCommMonoid Γ✝<VAR>Γ : Type u_5<VAR>inst✝¹ : LinearOrderedCancelAddCommMonoid Γ<VAR>inst✝ : NonUnitalNonAssocSemiring R<VAR>x y : HahnSeries Γ R<GOAL>((HahnModule.of R).symm (x • (HahnModule.of R) y)).coeff (x.order + y.order) = x.leadingCoeff * y.leadingCoeff
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹ : Category.{?u.25278, u_1} C<VAR>inst✝ : Category.{?u.25282, u_2} D<VAR>F G : C ⥤ Cat<VAR>α : F ⟶ G<VAR>X : Grothendieck F<GOAL>{ obj := fun X => { base := X.base, fiber := (α.app X.base).obj X.fiber }, map := fun {X Y} f => { base := f.base, fiber := (eqToHom ⋯).app X.fiber ≫ (α.app Y.base).map f.fiber } }.map (𝟙 X) = 𝟙 ({ obj := fun X => { base := X.base, fiber := (α.app X.base).obj X.fiber }, map := fun {X Y} f => { base := f.base, fiber := (eqToHom ⋯).app X.fiber ≫ (α.app Y.base).map f.fiber } }.obj X)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹ : Category.{?u.25278, u_1} C<VAR>inst✝ : Category.{?u.25282, u_2} D<VAR>F G : C ⥤ Cat<VAR>α : F ⟶ G<VAR>X : Grothendieck F<GOAL>{ base := (𝟙 X).base, fiber := (eqToHom ⋯).app X.fiber ≫ eqToHom ⋯ } = 𝟙 { base := X.base, fiber := (α.app X.base).obj X.fiber }
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹ : Category.{?u.25278, u_1} C<VAR>inst✝ : Category.{?u.25282, u_2} D<VAR>F G : C ⥤ Cat<VAR>α : F ⟶ G<VAR>X : Grothendieck F<GOAL>(eqToHom ⋯).app X.fiber ≫ eqToHom ⋯ = eqToHom ⋯
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹ : Category.{?u.25278, u_1} C<VAR>inst✝ : Category.{?u.25282, u_2} D<VAR>F G : C ⥤ Cat<VAR>α : F ⟶ G<VAR>X Y Z : Grothendieck F<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>(eqToHom ⋯).app X.fiber ≫ (α.app Z.base).map (eqToHom ⋯ ≫ (F.map g.base).map f.fiber ≫ g.fiber) = eqToHom ⋯ ≫ (G.map { base := g.base, fiber := (eqToHom ⋯).app Y.fiber ≫ (α.app Z.base).map g.fiber }.base).map { base := f.base, fiber := (eqToHom ⋯).app X.fiber ≫ (α.app Y.base).map f.fiber }.fiber ≫ { base := g.base, fiber := (eqToHom ⋯).app Y.fiber ≫ (α.app Z.base).map g.fiber }.fiber