ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>F : Type u_1<VAR>α✝ : Type u_2<VAR>β : Type u_3<VAR>inst✝³ : LinearOrderedRing α✝<VAR>inst✝² : FloorRing α✝<VAR>z : ℤ<VAR>a✝ : α✝<VAR>α : Type u_4<VAR>inst✝¹ : LinearOrderedCommRing α<VAR>inst✝ : FloorRing α<VAR>a b : α<VAR>h : ⌊a⌋ = ⌊b⌋<VAR>this✝² : a < ↑⌊a⌋ + 1<VAR>this✝¹ : b < ↑⌊b⌋ + 1<VAR>this✝ : ↑⌊a⌋ = ↑⌊b⌋<VAR>this : ↑⌊a⌋ ≤ a<GOAL>|a - b| < 1
<VAR>F : Type u_1<VAR>α✝ : Type u_2<VAR>β : Type u_3<VAR>inst✝³ : LinearOrderedRing α✝<VAR>inst✝² : FloorRing α✝<VAR>z : ℤ<VAR>a✝ : α✝<VAR>α : Type u_4<VAR>inst✝¹ : LinearOrderedCommRing α<VAR>inst✝ : FloorRing α<VAR>a b : α<VAR>h : ⌊a⌋ = ⌊b⌋<VAR>this✝³ : a < ↑⌊a⌋ + 1<VAR>this✝² : b < ↑⌊b⌋ + 1<VAR>this✝¹ : ↑⌊a⌋ = ↑⌊b⌋<VAR>this✝ : ↑⌊a⌋ ≤ a<VAR>this : ↑⌊b⌋ ≤ b<GOAL>|a - b| < 1
<VAR>α : Type u_1<VAR>a : α<VAR>l₁ l₂ : List α<VAR>x✝ : a :: l₁ <+~ a :: l₂<VAR>l : List α<VAR>p : l ~ a :: l₁<VAR>s : l <+ a :: l₂<GOAL>l₁ <+~ l₂
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>δ : α → Sort u_2<VAR>m : Multiset α<VAR>a : α<VAR>b : δ a<VAR>f : (a' : α) → a' ∈ m → δ a'<VAR>δ' : α → Sort u_3<VAR>φ : ⦃a' : α⦄ → δ a' → δ' a'<VAR>a' : α<VAR>ha' : a' ∈ a ::ₘ m<GOAL>cons m a (φ b) (fun a' ha' => φ (f a' ha')) a' ha' = φ (cons m a b f a' ha')
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>δ : α → Sort u_2<VAR>m : Multiset α<VAR>a : α<VAR>b : δ a<VAR>f : (a' : α) → a' ∈ m → δ a'<VAR>δ' : α → Sort u_3<VAR>φ : ⦃a' : α⦄ → δ a' → δ' a'<VAR>a' : α<VAR>ha' : a' ∈ a ::ₘ m<GOAL>(fun h => ⋯ ▸ φ b) = fun h => φ (⋯ ▸ b)
<VAR>α : Type u<VAR>β : α → Type v<VAR>l✝ l₁ l₂ : List (Sigma β)<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>l : List (Sigma β)<GOAL>(kerase a l).keys = l.keys.erase a
<VAR>α : Type u<VAR>β : α → Type v<VAR>l✝ l₁ l₂ : List (Sigma β)<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>l : List (Sigma β)<GOAL>map Sigma.fst (eraseP (fun s => decide (a = s.fst)) l) = map Sigma.fst (eraseP (fun x => a == x.fst) l)
<VAR>α : Type u<VAR>β : α → Type v<VAR>l✝ l₁ l₂ : List (Sigma β)<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>l : List (Sigma β)<GOAL>map Sigma.fst (eraseP (fun s => decide (a = s.fst)) l) = map Sigma.fst (eraseP (fun x => decide (a = x.fst)) l)
<VAR>α : Type u<VAR>β : α → Type v<VAR>l✝ l₁ l₂ : List (Sigma β)<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>l : List (Sigma β)<GOAL>(fun s => decide (a = s.fst)) = fun x => decide (a = x.fst)
<VAR>α : Type u<VAR>β : α → Type v<VAR>l✝ l₁ l₂ : List (Sigma β)<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>l : List (Sigma β)<VAR>x✝ : Sigma β<GOAL>decide (a = x✝.fst) = decide (a = x✝.fst)
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>D : Type u_3<VAR>D₁ : Type u_4<VAR>D₂ : Type u_5<VAR>inst✝⁶ : Category.{u_6, u_1} C₁<VAR>inst✝⁵ : Category.{u_8, u_2} C₂<VAR>inst✝⁴ : Category.{?u.22854, u_3} D<VAR>inst✝³ : Category.{u_7, u_4} D₁<VAR>inst✝² : Category.{u_9, u_5} D₂<VAR>L₁ : C₁ ⥤ D₁<VAR>W₁ : MorphismProperty C₁<VAR>inst✝¹ : L₁.IsLocalization W₁<VAR>L₂ : C₂ ⥤ D₂<VAR>W₂ : MorphismProperty C₂<VAR>E : C₁ ≌ C₂<VAR>E' : D₁ ≌ D₂<VAR>inst✝ : CatCommSq E.functor L₁ L₂ E'.functor<VAR>hW₁ : W₁ ≤ W₂.isoClosure.inverseImage E.functor<VAR>hW₂ : W₂.IsInvertedBy L₂<GOAL>L₂.IsLocalization W₂
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>D : Type u_3<VAR>D₁ : Type u_4<VAR>D₂ : Type u_5<VAR>inst✝⁶ : Category.{u_6, u_1} C₁<VAR>inst✝⁵ : Category.{u_8, u_2} C₂<VAR>inst✝⁴ : Category.{?u.22854, u_3} D<VAR>inst✝³ : Category.{u_7, u_4} D₁<VAR>inst✝² : Category.{u_9, u_5} D₂<VAR>L₁ : C₁ ⥤ D₁<VAR>W₁ : MorphismProperty C₁<VAR>inst✝¹ : L₁.IsLocalization W₁<VAR>L₂ : C₂ ⥤ D₂<VAR>W₂ : MorphismProperty C₂<VAR>E : C₁ ≌ C₂<VAR>E' : D₁ ≌ D₂<VAR>inst✝ : CatCommSq E.functor L₁ L₂ E'.functor<VAR>hW₁ : W₁ ≤ W₂.isoClosure.inverseImage E.functor<VAR>hW₂ : W₂.IsInvertedBy L₂<VAR>this : (E.functor ⋙ L₂).IsLocalization W₁<GOAL>L₂.IsLocalization W₂
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : GeneralizedHeytingAlgebra α<VAR>a✝ b✝ c d a b : α<GOAL>(a ⇨ b) ⊓ a = b ⊓ a
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedSemifield α<VAR>a b c d e : α<VAR>m n : ℤ<VAR>hb : 0 < b<GOAL>1 < a / b ↔ b < a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>a b : Ordinal.{u_4}<VAR>h : a - b = 0<GOAL>a ≤ b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>a b : Ordinal.{u_4}<VAR>h : a ≤ b<GOAL>a - b = 0
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>a : ℤ<VAR>ha : ↑a ≠ 0<GOAL>(quadraticChar (ZMod p)) ↑(a ^ 2) = 1
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>a : ℤ<VAR>ha : ↑a ≠ 0<GOAL>(quadraticChar (ZMod p)) (↑a ^ 2) = 1
<VAR>n✝ : ℕ<VAR>α : Type u_1<VAR>n : ℕ<VAR>ns : List ℕ<VAR>IH : ∀ {l : List α}, ns.sum ≤ l.length → map length (l.splitWrtCompositionAux ns) = ns<VAR>l : List α<VAR>h : n + ns.sum ≤ l.length<GOAL>map length (l.splitWrtCompositionAux (n :: ns)) = n :: ns
<VAR>n✝ : ℕ<VAR>α : Type u_1<VAR>n : ℕ<VAR>ns : List ℕ<VAR>IH : ∀ {l : List α}, ns.sum ≤ l.length → map length (l.splitWrtCompositionAux ns) = ns<VAR>l : List α<VAR>h : n + ns.sum ≤ l.length<VAR>this : n ≤ l.length<GOAL>map length (l.splitWrtCompositionAux (n :: ns)) = n :: ns
<VAR>n✝ : ℕ<VAR>α : Type u_1<VAR>n : ℕ<VAR>ns : List ℕ<VAR>IH : ∀ {l : List α}, ns.sum ≤ l.length → map length (l.splitWrtCompositionAux ns) = ns<VAR>l : List α<VAR>h : n + ns.sum ≤ l.length<VAR>this : n ≤ l.length<GOAL>map length (take n l :: (drop n l).splitWrtCompositionAux ns) = n :: ns
<VAR>n✝ : ℕ<VAR>α : Type u_1<VAR>n : ℕ<VAR>ns : List ℕ<VAR>IH : ∀ {l : List α}, ns.sum ≤ l.length → map length (l.splitWrtCompositionAux ns) = ns<VAR>l : List α<VAR>h : n + ns.sum ≤ l.length<VAR>this : n ≤ l.length<GOAL>(take n l).length :: map length ((drop n l).splitWrtCompositionAux ns) = n :: ns
<VAR>n✝ : ℕ<VAR>α : Type u_1<VAR>n : ℕ<VAR>ns : List ℕ<VAR>IH : ∀ {l : List α}, ns.sum ≤ l.length → map length (l.splitWrtCompositionAux ns) = ns<VAR>l : List α<VAR>h : n + ns.sum ≤ l.length<VAR>this : n ≤ l.length<GOAL>n ≤ l.length
<VAR>n✝ : ℕ<VAR>α : Type u_1<VAR>n : ℕ<VAR>ns : List ℕ<VAR>IH : ∀ {l : List α}, ns.sum ≤ l.length → map length (l.splitWrtCompositionAux ns) = ns<VAR>l : List α<VAR>h : n + ns.sum ≤ l.length<VAR>this : n ≤ l.length<GOAL>ns.sum ≤ l.length - n
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_2<VAR>π : ι → Type u_3<VAR>r : α → α → Prop<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : PartialOrder β<VAR>f : α → β<VAR>a₁ a₂ : α<VAR>h_anti : Antitone f<VAR>h_fa : f a₁ = f a₂<VAR>i : α<VAR>h₁ : a₁ ≤ i<VAR>h₂ : i ≤ a₂<GOAL>f i = f a₁
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_2<VAR>π : ι → Type u_3<VAR>r : α → α → Prop<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : PartialOrder β<VAR>f : α → β<VAR>a₁ a₂ : α<VAR>h_anti : Antitone f<VAR>h_fa : f a₁ = f a₂<VAR>i : α<VAR>h₁ : a₁ ≤ i<VAR>h₂ : i ≤ a₂<GOAL>f i ≤ f a₁
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_2<VAR>π : ι → Type u_3<VAR>r : α → α → Prop<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : PartialOrder β<VAR>f : α → β<VAR>a₁ a₂ : α<VAR>h_anti : Antitone f<VAR>h_fa : f a₁ = f a₂<VAR>i : α<VAR>h₁ : a₁ ≤ i<VAR>h₂ : i ≤ a₂<GOAL>f a₁ ≤ f i
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x✝ y✝ x y : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>‖x - y‖ = |‖x‖ - ‖y‖| ↔ angle x y = 0
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x✝ y✝ x y : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>h : ‖x - y‖ = |‖x‖ - ‖y‖|<GOAL>angle x y = 0
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x✝ y✝ x y : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>h : ‖x - y‖ = |‖x‖ - ‖y‖|<GOAL>⟪x, y⟫_ℝ = ‖x‖ * ‖y‖
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x✝ y✝ x y : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>h : ‖x - y‖ = |‖x‖ - ‖y‖|<VAR>h1 : ‖x - y‖ ^ 2 = (‖x‖ - ‖y‖) ^ 2<GOAL>⟪x, y⟫_ℝ = ‖x‖ * ‖y‖
<VAR>d n : PosNum<GOAL>↑n / ↑d = ↑(d.divMod n).1 ∧ ↑n % ↑d = ↑(d.divMod n).2
<VAR>d n : PosNum<GOAL>↑(d.divMod n).2 + ↑d * ↑(d.divMod n).1 = ↑n ∧ ↑(d.divMod n).2 < ↑d
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hdf : DifferentiableOn ℝ f (Ioo a b)<VAR>hg' : ∀ x ∈ Ioo a b, deriv g x ≠ 0<VAR>hfb : Tendsto f (𝓝[<] b) (𝓝 0)<VAR>hgb : Tendsto g (𝓝[<] b) (𝓝 0)<VAR>hdiv : Tendsto (fun x => deriv f x / deriv g x) (𝓝[<] b) l<GOAL>Tendsto (fun x => f x / g x) (𝓝[<] b) l
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hdf✝ : DifferentiableOn ℝ f (Ioo a b)<VAR>hg' : ∀ x ∈ Ioo a b, deriv g x ≠ 0<VAR>hfb : Tendsto f (𝓝[<] b) (𝓝 0)<VAR>hgb : Tendsto g (𝓝[<] b) (𝓝 0)<VAR>hdiv : Tendsto (fun x => deriv f x / deriv g x) (𝓝[<] b) l<VAR>hdf : ∀ x ∈ Ioo a b, DifferentiableAt ℝ f x<GOAL>Tendsto (fun x => f x / g x) (𝓝[<] b) l
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hdf✝ : DifferentiableOn ℝ f (Ioo a b)<VAR>hg' : ∀ x ∈ Ioo a b, deriv g x ≠ 0<VAR>hfb : Tendsto f (𝓝[<] b) (𝓝 0)<VAR>hgb : Tendsto g (𝓝[<] b) (𝓝 0)<VAR>hdiv : Tendsto (fun x => deriv f x / deriv g x) (𝓝[<] b) l<VAR>hdf : ∀ x ∈ Ioo a b, DifferentiableAt ℝ f x<VAR>hdg : ∀ x ∈ Ioo a b, DifferentiableAt ℝ g x<GOAL>Tendsto (fun x => f x / g x) (𝓝[<] b) l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν : Measure α<VAR>s t : SignedMeasure α<VAR>μ : Measure α<VAR>f : α → ℝ<VAR>hf : Measurable f<VAR>hfi : Integrable f μ<VAR>htμ : t ⟂ᵥ μ.toENNRealVectorMeasure<VAR>hadd : s = t + μ.withDensityᵥ f<VAR>htμ' : t ⟂ᵥ μ.toENNRealVectorMeasure<GOAL>s.HaveLebesgueDecomposition μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν : Measure α<VAR>s t : SignedMeasure α<VAR>μ : Measure α<VAR>f : α → ℝ<VAR>hf : Measurable f<VAR>hfi : Integrable f μ<VAR>htμ : t.totalVariation ⟂ₘ μ.toENNRealVectorMeasure.ennrealToMeasure<VAR>hadd : s = t + μ.withDensityᵥ f<VAR>htμ' : t ⟂ᵥ μ.toENNRealVectorMeasure<GOAL>s.HaveLebesgueDecomposition μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν : Measure α<VAR>s t : SignedMeasure α<VAR>μ : Measure α<VAR>f : α → ℝ<VAR>hf : Measurable f<VAR>hfi : Integrable f μ<VAR>hadd : s = t + μ.withDensityᵥ f<VAR>htμ' : t ⟂ᵥ μ.toENNRealVectorMeasure<VAR>htμ : t.totalVariation ⟂ₘ VectorMeasure.equivMeasure.toFun (VectorMeasure.equivMeasure.invFun μ)<GOAL>s.HaveLebesgueDecomposition μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν : Measure α<VAR>s t : SignedMeasure α<VAR>μ : Measure α<VAR>f : α → ℝ<VAR>hf : Measurable f<VAR>hfi : Integrable f μ<VAR>hadd : s = t + μ.withDensityᵥ f<VAR>htμ' : t ⟂ᵥ μ.toENNRealVectorMeasure<VAR>htμ : t.toJordanDecomposition.posPart ⟂ₘ μ ∧ t.toJordanDecomposition.negPart ⟂ₘ μ<GOAL>s.HaveLebesgueDecomposition μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>E : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>κ : Kernel α β<VAR>inst✝⁵ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝⁴ : IsSFiniteKernel η<VAR>a : α<VAR>inst✝³ : NormedSpace ℝ E<VAR>E' : Type u_5<VAR>inst✝² : NormedAddCommGroup E'<VAR>inst✝¹ : CompleteSpace E'<VAR>inst✝ : NormedSpace ℝ E'<VAR>f : β × γ → E<VAR>s : Set β<VAR>t : Set γ<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<VAR>hf : IntegrableOn f (s ×ˢ t) ((κ ⊗ₖ η) a)<GOAL>∫ (z : β × γ) in s ×ˢ t, f z ∂(κ ⊗ₖ η) a = ∫ (x : β) in s, ∫ (y : γ) in t, f (x, y) ∂η (a, x) ∂κ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>E : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>κ : Kernel α β<VAR>inst✝⁵ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝⁴ : IsSFiniteKernel η<VAR>a : α<VAR>inst✝³ : NormedSpace ℝ E<VAR>E' : Type u_5<VAR>inst✝² : NormedAddCommGroup E'<VAR>inst✝¹ : CompleteSpace E'<VAR>inst✝ : NormedSpace ℝ E'<VAR>f : β × γ → E<VAR>s : Set β<VAR>t : Set γ<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<VAR>hf : IntegrableOn f (s ×ˢ t) ((κ ⊗ₖ η) a)<GOAL>∫ (x : β), ∫ (y : γ), f (x, y) ∂(η.restrict ht) (a, x) ∂(κ.restrict hs) a = ∫ (x : β) in s, ∫ (y : γ) in t, f (x, y) ∂η (a, x) ∂κ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>E : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>κ : Kernel α β<VAR>inst✝⁵ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝⁴ : IsSFiniteKernel η<VAR>a : α<VAR>inst✝³ : NormedSpace ℝ E<VAR>E' : Type u_5<VAR>inst✝² : NormedAddCommGroup E'<VAR>inst✝¹ : CompleteSpace E'<VAR>inst✝ : NormedSpace ℝ E'<VAR>f : β × γ → E<VAR>s : Set β<VAR>t : Set γ<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<VAR>hf : IntegrableOn f (s ×ˢ t) ((κ ⊗ₖ η) a)<GOAL>Integrable f ((κ.restrict hs ⊗ₖ η.restrict ht) a)
<VAR>J : Type w<VAR>C✝ : Type u<VAR>inst✝² : Category.{v, u} C✝<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>B : C<VAR>objs : J → C<VAR>arrows : (j : J) → B ⟶ objs j<VAR>inst✝ : HasWidePushout B objs arrows<VAR>X : C<VAR>f : B ⟶ X<VAR>fs : (j : J) → objs j ⟶ X<VAR>w : ∀ (j : J), arrows j ≫ fs j = f<VAR>g : widePushout B objs arrows ⟶ X<VAR>h1 : ∀ (j : J), ι arrows j ≫ g = fs j<VAR>h2 : head arrows ≫ g = f<GOAL>g = desc f fs w
<VAR>J : Type w<VAR>C✝ : Type u<VAR>inst✝² : Category.{v, u} C✝<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>B : C<VAR>objs : J → C<VAR>arrows : (j : J) → B ⟶ objs j<VAR>inst✝ : HasWidePushout B objs arrows<VAR>X : C<VAR>f : B ⟶ X<VAR>fs : (j : J) → objs j ⟶ X<VAR>w : ∀ (j : J), arrows j ≫ fs j = f<VAR>g : widePushout B objs arrows ⟶ X<VAR>h1 : ∀ (j : J), ι arrows j ≫ g = fs j<VAR>h2 : head arrows ≫ g = f<GOAL>∀ (j : WidePushoutShape J), (colimit.cocone (WidePushoutShape.wideSpan B objs arrows)).ι.app j ≫ g = (WidePushoutShape.mkCocone f fs w).ι.app j
<VAR>R' : Type u'<VAR>R✝ : Type u<VAR>A✝ : Type v<VAR>B : Type w<VAR>C : Type w'<VAR>inst✝⁹ : CommSemiring R✝<VAR>inst✝⁸ : Semiring A✝<VAR>inst✝⁷ : Algebra R✝ A✝<VAR>inst✝⁶ : Semiring B<VAR>inst✝⁵ : Algebra R✝ B<VAR>inst✝⁴ : Semiring C<VAR>inst✝³ : Algebra R✝ C<VAR>S✝ : Subalgebra R✝ A✝<VAR>R : Type u<VAR>A : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra R A<VAR>S T : Subalgebra R A<VAR>h : S.toSubring = T.toSubring<VAR>x : A<GOAL>x ∈ S ↔ x ∈ T
<VAR>C : Type u₁<VAR>inst✝³ : Category.{u₂, u₁} C<VAR>inst✝² : PreGaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝¹ : FiberFunctor F<VAR>A : C<VAR>inst✝ : IsConnected A<VAR>a : ↑(F.obj A)<GOAL>Nat.card (Aut A) ≤ Nat.card ↑(F.obj A)
<VAR>C : Type u₁<VAR>inst✝³ : Category.{u₂, u₁} C<VAR>inst✝² : PreGaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝¹ : FiberFunctor F<VAR>A : C<VAR>inst✝ : IsConnected A<VAR>a : ↑(F.obj A)<GOAL>Function.Injective ?intro.f
<VAR>C : Type u₁<VAR>inst✝³ : Category.{u₂, u₁} C<VAR>inst✝² : PreGaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝¹ : FiberFunctor F<VAR>A : C<VAR>inst✝ : IsConnected A<VAR>a : ↑(F.obj A)<GOAL>Aut A → ↑(F.obj A)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : LinearOrder α<VAR>inst✝³ : DenselyOrdered α<VAR>inst✝² : OrderTopology α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : RegularSpace β<VAR>f : α → β<VAR>a b : α<VAR>la lb : β<VAR>hab : a ≠ b<VAR>hf : ContinuousOn f (Ioo a b)<VAR>ha : Tendsto f (𝓝[>] a) (𝓝 la)<VAR>hb : Tendsto f (𝓝[<] b) (𝓝 lb)<GOAL>ContinuousOn (extendFrom (Ioo a b) f) (Icc a b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : LinearOrder α<VAR>inst✝³ : DenselyOrdered α<VAR>inst✝² : OrderTopology α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : RegularSpace β<VAR>f : α → β<VAR>a b : α<VAR>la lb : β<VAR>hab : a ≠ b<VAR>hf : ContinuousOn f (Ioo a b)<VAR>ha : Tendsto f (𝓝[>] a) (𝓝 la)<VAR>hb : Tendsto f (𝓝[<] b) (𝓝 lb)<GOAL>Icc a b ⊆ closure (Ioo a b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : LinearOrder α<VAR>inst✝³ : DenselyOrdered α<VAR>inst✝² : OrderTopology α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : RegularSpace β<VAR>f : α → β<VAR>a b : α<VAR>la lb : β<VAR>hab : a ≠ b<VAR>hf : ContinuousOn f (Ioo a b)<VAR>ha : Tendsto f (𝓝[>] a) (𝓝 la)<VAR>hb : Tendsto f (𝓝[<] b) (𝓝 lb)<GOAL>∀ x ∈ Icc a b, ∃ y, Tendsto f (𝓝[Ioo a b] x) (𝓝 y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace α<VAR>s✝ : SignedMeasure α<VAR>μ ν : Measure α<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : IsFiniteMeasure ν<VAR>s : SignedMeasure α<GOAL>∃ i, ∃ (hi₁ : MeasurableSet i) (hi₂ : VectorMeasure.restrict 0 i ≤ VectorMeasure.restrict s i) (hi₃ : VectorMeasure.restrict s iᶜ ≤ VectorMeasure.restrict 0 iᶜ), s.toJordanDecomposition.posPart = s.toMeasureOfZeroLE i hi₁ hi₂ ∧ s.toJordanDecomposition.negPart = s.toMeasureOfLEZero iᶜ ⋯ hi₃
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace α<VAR>s✝ : SignedMeasure α<VAR>μ ν : Measure α<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : IsFiniteMeasure ν<VAR>s : SignedMeasure α<VAR>i : Set α := ⋯.choose<GOAL>∃ i, ∃ (hi₁ : MeasurableSet i) (hi₂ : VectorMeasure.restrict 0 i ≤ VectorMeasure.restrict s i) (hi₃ : VectorMeasure.restrict s iᶜ ≤ VectorMeasure.restrict 0 iᶜ), s.toJordanDecomposition.posPart = s.toMeasureOfZeroLE i hi₁ hi₂ ∧ s.toJordanDecomposition.negPart = s.toMeasureOfLEZero iᶜ ⋯ hi₃
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace α<VAR>s✝ : SignedMeasure α<VAR>μ ν : Measure α<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : IsFiniteMeasure ν<VAR>s : SignedMeasure α<VAR>i : Set α := ⋯.choose<VAR>hi₁ : MeasurableSet ⋯.choose<VAR>hi₂ : VectorMeasure.restrict 0 ⋯.choose ≤ VectorMeasure.restrict s ⋯.choose<VAR>hi₃ : VectorMeasure.restrict s ⋯.chooseᶜ ≤ VectorMeasure.restrict 0 ⋯.chooseᶜ<GOAL>∃ i, ∃ (hi₁ : MeasurableSet i) (hi₂ : VectorMeasure.restrict 0 i ≤ VectorMeasure.restrict s i) (hi₃ : VectorMeasure.restrict s iᶜ ≤ VectorMeasure.restrict 0 iᶜ), s.toJordanDecomposition.posPart = s.toMeasureOfZeroLE i hi₁ hi₂ ∧ s.toJordanDecomposition.negPart = s.toMeasureOfLEZero iᶜ ⋯ hi₃
<VAR>α : Type u_1<VAR>F : Type u_2<VAR>F' : Type u_3<VAR>𝕜 : Type u_4<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : RCLike 𝕜<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace 𝕜 F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f g : α → F'<VAR>s : Set α<VAR>hf : Integrable f μ<VAR>hg : Integrable g μ<VAR>hm : m ≤ m0<VAR>hμm this : SigmaFinite (μ.trim hm)<GOAL>μ[f + g|m] =ᶠ[ae μ] μ[f|m] + μ[g|m]
<VAR>α : Type u_1<VAR>F : Type u_2<VAR>F' : Type u_3<VAR>𝕜 : Type u_4<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : RCLike 𝕜<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace 𝕜 F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f g : α → F'<VAR>s : Set α<VAR>hf : Integrable f μ<VAR>hg : Integrable g μ<VAR>hm : m ≤ m0<VAR>hμm this : SigmaFinite (μ.trim hm)<GOAL>↑↑(condexpL1 hm μ (f + g)) =ᶠ[ae μ] μ[f|m] + μ[g|m]
<VAR>α : Type u_1<VAR>F : Type u_2<VAR>F' : Type u_3<VAR>𝕜 : Type u_4<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : RCLike 𝕜<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace 𝕜 F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f g : α → F'<VAR>s : Set α<VAR>hf : Integrable f μ<VAR>hg : Integrable g μ<VAR>hm : m ≤ m0<VAR>hμm this : SigmaFinite (μ.trim hm)<GOAL>↑↑(condexpL1 hm μ f + condexpL1 hm μ g) =ᶠ[ae μ] μ[f|m] + μ[g|m]
<VAR>m n✝ n : ℕ<VAR>u : (ZMod n)ˣ<GOAL>(↑u)⁻¹ = ↑u⁻¹
<VAR>m n✝ n : ℕ<VAR>u : (ZMod n)ˣ<VAR>this : ↑((↑u).val.gcd n) = ↑1<GOAL>(↑u)⁻¹ = ↑u⁻¹
<VAR>m n✝ n : ℕ<VAR>u : (ZMod n)ˣ<VAR>this : ↑u * (↑u)⁻¹ = 1<GOAL>(↑u)⁻¹ = ↑u⁻¹
<VAR>m n✝ n : ℕ<VAR>u : (ZMod n)ˣ<VAR>this : ↑u * (↑u)⁻¹ = 1<VAR>u' : (ZMod n)ˣ := { val := ↑u, inv := (↑u)⁻¹, val_inv := this, inv_val := ⋯ }<GOAL>(↑u)⁻¹ = ↑u⁻¹
<VAR>m n✝ n : ℕ<VAR>u : (ZMod n)ˣ<VAR>this : ↑u * (↑u)⁻¹ = 1<VAR>u' : (ZMod n)ˣ := { val := ↑u, inv := (↑u)⁻¹, val_inv := this, inv_val := ⋯ }<VAR>h : u = u'<GOAL>(↑u)⁻¹ = ↑u⁻¹
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>I : Ideal R<VAR>S : Type u_3<VAR>inst✝³ : CommSemiring S<VAR>inst✝² : Algebra S R<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower S R M<VAR>i : ℕ<VAR>r : R<VAR>j : ℕ<VAR>m : M<GOAL>(monomial i) r • (single R j) m = (single R (i + j)) (r • m)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>I : Ideal R<VAR>S : Type u_3<VAR>inst✝³ : CommSemiring S<VAR>inst✝² : Algebra S R<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower S R M<VAR>i : ℕ<VAR>r : R<VAR>j : ℕ<VAR>m : M<GOAL>r • (⇑(Finsupp.lmapDomain M R Nat.succ))^[i] ((single R j) m) = (single R (i + j)) (r • m)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝¹ : AddGroup R<VAR>inst✝ : StarAddMonoid R<VAR>x : R<VAR>hx : IsSelfAdjoint x<GOAL>IsSelfAdjoint (-x)
<VAR>Fq F : Type<VAR>inst✝⁴ : Field Fq<VAR>inst✝³ : Field F<VAR>inst✝² : Algebra Fq[X] F<VAR>inst✝¹ : Algebra (RatFunc Fq) F<VAR>inst✝ : IsScalarTower Fq[X] (RatFunc Fq) F<GOAL>Function.Injective ⇑(algebraMap Fq[X] F)
<VAR>Fq F : Type<VAR>inst✝⁴ : Field Fq<VAR>inst✝³ : Field F<VAR>inst✝² : Algebra Fq[X] F<VAR>inst✝¹ : Algebra (RatFunc Fq) F<VAR>inst✝ : IsScalarTower Fq[X] (RatFunc Fq) F<GOAL>Function.Injective ⇑((algebraMap (RatFunc Fq) F).comp (algebraMap Fq[X] (RatFunc Fq)))
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁶ : Category.{u_3, u_1} C<VAR>inst✝⁵ : Category.{u_4, u_2} D<VAR>inst✝⁴ : HasZeroMorphisms C<VAR>inst✝³ : HasZeroMorphisms D<VAR>S S₁ S₂ : ShortComplex C<VAR>h : S.Exact<VAR>F : C ⥤ D<VAR>inst✝² : F.PreservesZeroMorphisms<VAR>inst✝¹ : F.PreservesLeftHomologyOf S<VAR>inst✝ : F.PreservesRightHomologyOf S<GOAL>(S.map F).Exact
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁶ : Category.{u_3, u_1} C<VAR>inst✝⁵ : Category.{u_4, u_2} D<VAR>inst✝⁴ : HasZeroMorphisms C<VAR>inst✝³ : HasZeroMorphisms D<VAR>S S₁ S₂ : ShortComplex C<VAR>h : S.Exact<VAR>F : C ⥤ D<VAR>inst✝² : F.PreservesZeroMorphisms<VAR>inst✝¹ : F.PreservesLeftHomologyOf S<VAR>inst✝ : F.PreservesRightHomologyOf S<VAR>this : S.HasHomology<GOAL>(S.map F).Exact
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>n m : ℕ<VAR>inst✝ : Ring R<VAR>p : R[X]<GOAL>(-p).support.min = p.support.min
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ✝ : Kernel α β<VAR>inst✝ : Countable ι<VAR>κ : ι → ι → Kernel α β<VAR>a : α<VAR>s : Set β<VAR>a✝ : MeasurableSet s<GOAL>((Kernel.sum fun n => Kernel.sum (κ n)) a) s = ((Kernel.sum fun m => Kernel.sum fun n => κ n m) a) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ✝ : Kernel α β<VAR>inst✝ : Countable ι<VAR>κ : ι → ι → Kernel α β<VAR>a : α<VAR>s : Set β<VAR>a✝ : MeasurableSet s<GOAL>(Measure.sum fun n => Measure.sum fun n_1 => (κ n n_1) a) s = (Measure.sum fun n => Measure.sum fun n_1 => (κ n_1 n) a) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>ι' : Type u_4<VAR>inst✝² : DistribLattice α<VAR>inst✝¹ : OrderBot α<VAR>s✝ : Finset ι<VAR>f✝ : ι → α<VAR>inst✝ : DecidableEq ι<VAR>s : Finset ι'<VAR>g : ι' → Finset ι<VAR>f : ι → α<VAR>hs : s.SupIndep fun i => (g i).sup f<VAR>hg : ∀ i' ∈ s, (g i').SupIndep f<GOAL>(s.biUnion g).SupIndep f
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>k : ℕ<VAR>a₁ a₂ : A<VAR>p₁ p₂ : R[X]<GOAL>a₁ * a₂ * (algebraMap R A) ((p₁ * p₂).coeff k) = ∑ x ∈ Finset.antidiagonal k, a₁ * (algebraMap R A) (p₁.coeff x.1) * (a₂ * (algebraMap R A) (p₂.coeff x.2))
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>k : ℕ<VAR>a₁ a₂ : A<VAR>p₁ p₂ : R[X]<GOAL>a₁ * (a₂ * (algebraMap R A) ((p₁ * p₂).coeff k)) = a₁ * (a₂ * ∑ i ∈ Finset.antidiagonal k, (algebraMap R A) (p₂.coeff i.2) * (algebraMap R A) (p₁.coeff i.1))
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>k : ℕ<VAR>a₁ a₂ : A<VAR>p₁ p₂ : R[X]<GOAL>(algebraMap R A) ((p₁ * p₂).coeff k) = ∑ i ∈ Finset.antidiagonal k, (algebraMap R A) (p₂.coeff i.2) * (algebraMap R A) (p₁.coeff i.1)