ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>α : Type u_7<VAR>inst✝⁸ : LinearOrderedField R<VAR>inst✝⁷ : LinearOrderedField R'<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : AddCommGroup F<VAR>inst✝⁴ : LinearOrderedAddCommGroup α<VAR>inst✝³ : Module R E<VAR>inst✝² : Module R F<VAR>inst✝¹ : Module R α<VAR>inst✝ : OrderedSMul R α<VAR>s✝ : Set E<VAR>i j : ι<VAR>c : R<VAR>t✝ : Finset ι<VAR>w : ι → R<VAR>z : ι → E<VAR>s : Finset ι<VAR>t : Finset ι'<VAR>ws : ι → R<VAR>zs : ι → E<VAR>wt : ι' → R<VAR>zt : ι' → E<VAR>hws : ∑ i ∈ s, ws i = 1<VAR>hwt : ∑ i ∈ t, wt i = 1<VAR>a b : R<VAR>hab : a + b = 1<GOAL>∑ x ∈ s.disjSum t, Sum.elim (fun x => a • ws x • zs x) (fun x => b • wt x • zt x) x = ∑ i ∈ s.disjSum t, Sum.elim (fun i => a * ws i) (fun j => b * wt j) i • Sum.elim zs zt i
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>α : Type u_7<VAR>inst✝⁸ : LinearOrderedField R<VAR>inst✝⁷ : LinearOrderedField R'<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : AddCommGroup F<VAR>inst✝⁴ : LinearOrderedAddCommGroup α<VAR>inst✝³ : Module R E<VAR>inst✝² : Module R F<VAR>inst✝¹ : Module R α<VAR>inst✝ : OrderedSMul R α<VAR>s✝ : Set E<VAR>i j : ι<VAR>c : R<VAR>t✝ : Finset ι<VAR>w : ι → R<VAR>z : ι → E<VAR>s : Finset ι<VAR>t : Finset ι'<VAR>ws : ι → R<VAR>zs : ι → E<VAR>wt : ι' → R<VAR>zt : ι' → E<VAR>hws : ∑ i ∈ s, ws i = 1<VAR>hwt : ∑ i ∈ t, wt i = 1<VAR>a b : R<VAR>hab : a + b = 1<GOAL>∑ i ∈ s.disjSum t, Sum.elim (fun i => a * ws i) (fun j => b * wt j) i = 1
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>r : R<VAR>k : ℕ<GOAL>((monomial k) r).content = normalize r
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>l₁ l₂ : List α<VAR>s : l₁ ~ l₂<GOAL>List.filter p l₁ ~ List.filter p l₂
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>l₁ l₂ : List α<VAR>s : l₁ ~ l₂<GOAL>List.filterMap (Option.guard fun x => p x = true) l₁ ~ List.filterMap (Option.guard fun x => p x = true) l₂
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝ : LinearOrder ι<VAR>u : ι → Ω → β<VAR>τ : Ω → ι<VAR>i : ι<VAR>ω : Ω<VAR>h : i ≤ τ ω<GOAL>stoppedProcess u τ i ω = u i ω
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>inst✝⁵ : HasColimits C<VAR>X Y Z : TopCat<VAR>inst✝⁴ : ConcreteCategory C<VAR>inst✝³ : PreservesFilteredColimits (forget C)<VAR>inst✝² : HasLimits C<VAR>inst✝¹ : PreservesLimits (forget C)<VAR>inst✝ : (forget C).ReflectsIsomorphisms<VAR>F : Sheaf C X<VAR>U : Opens ↑X<VAR>s t : (forget C).obj (F.val.obj (op U))<VAR>h : ∀ (x : ↥U), (F.presheaf.germ x) s = (F.presheaf.germ x) t<GOAL>s = t
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>inst✝⁵ : HasColimits C<VAR>X Y Z : TopCat<VAR>inst✝⁴ : ConcreteCategory C<VAR>inst✝³ : PreservesFilteredColimits (forget C)<VAR>inst✝² : HasLimits C<VAR>inst✝¹ : PreservesLimits (forget C)<VAR>inst✝ : (forget C).ReflectsIsomorphisms<VAR>F : Sheaf C X<VAR>U : Opens ↑X<VAR>s t : (forget C).obj (F.val.obj (op U))<VAR>h : ∀ (x : ↥U), (F.presheaf.germ x) s = (F.presheaf.germ x) t<VAR>V : ↥U → Opens ↑X<VAR>m : ∀ (x : ↥U), ↑x ∈ V x<VAR>i₁ i₂ : (x : ↥U) → V x ⟶ U<VAR>heq : ∀ (x : ↥U), (F.presheaf.map (i₁ x).op) s = (F.presheaf.map (i₂ x).op) t<GOAL>s = t
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>inst✝⁵ : HasColimits C<VAR>X Y Z : TopCat<VAR>inst✝⁴ : ConcreteCategory C<VAR>inst✝³ : PreservesFilteredColimits (forget C)<VAR>inst✝² : HasLimits C<VAR>inst✝¹ : PreservesLimits (forget C)<VAR>inst✝ : (forget C).ReflectsIsomorphisms<VAR>F : Sheaf C X<VAR>U : Opens ↑X<VAR>s t : (forget C).obj (F.val.obj (op U))<VAR>h : ∀ (x : ↥U), (F.presheaf.germ x) s = (F.presheaf.germ x) t<VAR>V : ↥U → Opens ↑X<VAR>m : ∀ (x : ↥U), ↑x ∈ V x<VAR>i₁ i₂ : (x : ↥U) → V x ⟶ U<VAR>heq : ∀ (x : ↥U), (F.presheaf.map (i₁ x).op) s = (F.presheaf.map (i₂ x).op) t<GOAL>U ≤ iSup V
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>inst✝⁵ : HasColimits C<VAR>X Y Z : TopCat<VAR>inst✝⁴ : ConcreteCategory C<VAR>inst✝³ : PreservesFilteredColimits (forget C)<VAR>inst✝² : HasLimits C<VAR>inst✝¹ : PreservesLimits (forget C)<VAR>inst✝ : (forget C).ReflectsIsomorphisms<VAR>F : Sheaf C X<VAR>U : Opens ↑X<VAR>s t : (forget C).obj (F.val.obj (op U))<VAR>h : ∀ (x : ↥U), (F.presheaf.germ x) s = (F.presheaf.germ x) t<VAR>V : ↥U → Opens ↑X<VAR>m : ∀ (x : ↥U), ↑x ∈ V x<VAR>i₁ i₂ : (x : ↥U) → V x ⟶ U<VAR>heq : ∀ (x : ↥U), (F.presheaf.map (i₁ x).op) s = (F.presheaf.map (i₂ x).op) t<GOAL>∀ (i : ↥U), (F.val.map (i₁ i).op) s = (F.val.map (i₁ i).op) t
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α✝ : Type u_3<VAR>β✝ : Type u_4<VAR>γ : Type u_5<VAR>s✝ s₁ s₂ : Finset α✝<VAR>a : α✝<VAR>f✝ g✝ : α✝ → β✝<VAR>inst✝³ : CommMonoid β✝<VAR>α : Type u_6<VAR>inst✝² : CommMonoid α<VAR>β : Type u_7<VAR>inst✝¹ : Fintype β<VAR>s : Set β<VAR>inst✝ : DecidablePred fun x => x ∈ s<VAR>f : β → α<VAR>g : ↑s → α<VAR>w : ∀ (x : β) (h : x ∈ s), f x = g ⟨x, h⟩<VAR>w' : ∀ x ∉ s, f x = 1<GOAL>univ.prod f = univ.prod g
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α✝ : Type u_3<VAR>β✝ : Type u_4<VAR>γ : Type u_5<VAR>s✝ s₁ s₂ : Finset α✝<VAR>a : α✝<VAR>f✝ g✝ : α✝ → β✝<VAR>inst✝³ : CommMonoid β✝<VAR>α : Type u_6<VAR>inst✝² : CommMonoid α<VAR>β : Type u_7<VAR>inst✝¹ : Fintype β<VAR>s : Set β<VAR>inst✝ : DecidablePred fun x => x ∈ s<VAR>f : β → α<VAR>g : ↑s → α<VAR>w : ∀ (x : β) (h : x ∈ s), f x = g ⟨x, h⟩<VAR>w' : ∀ x ∉ s, f x = 1<GOAL>∏ x ∈ s.toFinset, f x = univ.prod g
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α✝ : Type u_3<VAR>β✝ : Type u_4<VAR>γ : Type u_5<VAR>s✝ s₁ s₂ : Finset α✝<VAR>a : α✝<VAR>f✝ g✝ : α✝ → β✝<VAR>inst✝³ : CommMonoid β✝<VAR>α : Type u_6<VAR>inst✝² : CommMonoid α<VAR>β : Type u_7<VAR>inst✝¹ : Fintype β<VAR>s : Set β<VAR>inst✝ : DecidablePred fun x => x ∈ s<VAR>f : β → α<VAR>g : ↑s → α<VAR>w : ∀ (x : β) (h : x ∈ s), f x = g ⟨x, h⟩<VAR>w' : ∀ x ∉ s, f x = 1<GOAL>∀ x ∈ univ, x ∉ s.toFinset → f x = 1
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>𝓕 : Type u_3<VAR>inst✝³ : SeminormedAddGroup E<VAR>inst✝² : SeminormedAddCommGroup F<VAR>inst✝¹ : FunLike 𝓕 E F<VAR>inst✝ : ZeroAtInftyContinuousMapClass 𝓕 E F<VAR>f : 𝓕<VAR>ε : ℝ<VAR>hε : 0 < ε<GOAL>∃ r, ∀ (x : E), r < ‖x‖ → ‖f x‖ < ε
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>𝓕 : Type u_3<VAR>inst✝³ : SeminormedAddGroup E<VAR>inst✝² : SeminormedAddCommGroup F<VAR>inst✝¹ : FunLike 𝓕 E F<VAR>inst✝ : ZeroAtInftyContinuousMapClass 𝓕 E F<VAR>f : 𝓕<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>h : Tendsto (⇑f) (cocompact E) (𝓝 0)<GOAL>∃ r, ∀ (x : E), r < ‖x‖ → ‖f x‖ < ε
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>𝓕 : Type u_3<VAR>inst✝³ : SeminormedAddGroup E<VAR>inst✝² : SeminormedAddCommGroup F<VAR>inst✝¹ : FunLike 𝓕 E F<VAR>inst✝ : ZeroAtInftyContinuousMapClass 𝓕 E F<VAR>f : 𝓕<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>h : ∀ s ∈ 𝓝 0, (fun x => ‖f x‖) ⁻¹' s ∈ cocompact E<GOAL>∃ r, ∀ (x : E), r < ‖x‖ → ‖f x‖ < ε
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>𝓕 : Type u_3<VAR>inst✝³ : SeminormedAddGroup E<VAR>inst✝² : SeminormedAddCommGroup F<VAR>inst✝¹ : FunLike 𝓕 E F<VAR>inst✝ : ZeroAtInftyContinuousMapClass 𝓕 E F<VAR>f : 𝓕<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>h : (fun x => ‖f x‖) ⁻¹' Metric.ball 0 ε ∈ cocompact E<GOAL>∃ r, ∀ (x : E), r < ‖x‖ → ‖f x‖ < ε
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>𝓕 : Type u_3<VAR>inst✝³ : SeminormedAddGroup E<VAR>inst✝² : SeminormedAddCommGroup F<VAR>inst✝¹ : FunLike 𝓕 E F<VAR>inst✝ : ZeroAtInftyContinuousMapClass 𝓕 E F<VAR>f : 𝓕<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>h : (fun x => ‖f x‖) ⁻¹' Metric.ball 0 ε ∈ cocompact E<VAR>r : ℝ<VAR>hr : (Metric.closedBall 0 r)ᶜ ⊆ (fun x => ‖f x‖) ⁻¹' Metric.ball 0 ε<GOAL>∃ r, ∀ (x : E), r < ‖x‖ → ‖f x‖ < ε
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>𝓕 : Type u_3<VAR>inst✝³ : SeminormedAddGroup E<VAR>inst✝² : SeminormedAddCommGroup F<VAR>inst✝¹ : FunLike 𝓕 E F<VAR>inst✝ : ZeroAtInftyContinuousMapClass 𝓕 E F<VAR>f : 𝓕<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>h : (fun x => ‖f x‖) ⁻¹' Metric.ball 0 ε ∈ cocompact E<VAR>r : ℝ<VAR>hr : (Metric.closedBall 0 r)ᶜ ⊆ (fun x => ‖f x‖) ⁻¹' Metric.ball 0 ε<GOAL>∀ (x : E), r < ‖x‖ → ‖f x‖ < ε
<VAR>p : ℝ≥0∞<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>α : ι → Type u_3<VAR>β : ι → Type u_4<VAR>inst✝⁷ : Fact (1 ≤ p)<VAR>inst✝⁶ : Fintype ι<VAR>inst✝⁵ : Semiring 𝕜<VAR>inst✝⁴ : (i : ι) → SeminormedAddCommGroup (α i)<VAR>inst✝³ : (i : ι) → SeminormedAddCommGroup (β i)<VAR>inst✝² : (i : ι) → Module 𝕜 (α i)<VAR>inst✝¹ : (i : ι) → Module 𝕜 (β i)<VAR>c : 𝕜<VAR>inst✝ : DecidableEq ι<VAR>i : ι<VAR>b₁ b₂ : β i<GOAL>edist ((WithLp.equiv p ((i : ι) → β i)).symm (Pi.single i b₁)) ((WithLp.equiv p ((i : ι) → β i)).symm (Pi.single i b₂)) = edist b₁ b₂
<VAR>α : Type u<VAR>β : Type u_1<VAR>t✝ : TopologicalSpace α<VAR>B : Set (Set α)<VAR>s t : Set α<VAR>hB : IsTopologicalBasis B<VAR>hs : IsOpen s<VAR>ht : IsOpen t<VAR>h : ∀ U ∈ B, U ⊆ s ↔ U ⊆ t<GOAL>s = t
<VAR>α : Type u<VAR>β : Type u_1<VAR>t✝ : TopologicalSpace α<VAR>B : Set (Set α)<VAR>s t : Set α<VAR>hB : IsTopologicalBasis B<VAR>hs : IsOpen s<VAR>ht : IsOpen t<VAR>h : ∀ U ∈ B, U ⊆ s ↔ U ⊆ t<GOAL>⋃₀ {s_1 | s_1 ∈ B ∧ s_1 ⊆ s} = ⋃₀ {s | s ∈ B ∧ s ⊆ t}
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t✝ : Set α<VAR>s : ι → Set α<VAR>t : Finset ι<VAR>p : α → Prop<GOAL>(∀ᵐ (x : α) ∂μ.restrict (⋃ i ∈ t, s i), p x) ↔ ∀ i ∈ t, ∀ᵐ (x : α) ∂μ.restrict (s i), p x
<VAR>M' : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>φ : M → N<VAR>ψ : N → P<VAR>χ : M → P<VAR>X : Type u_5<VAR>inst✝⁵ : SMul M X<VAR>inst✝⁴ : SMul M' X<VAR>Y : Type u_6<VAR>inst✝³ : SMul N Y<VAR>inst✝² : SMul M' Y<VAR>Z : Type u_7<VAR>inst✝¹ : SMul P Z<VAR>φ' : N → M<VAR>Y₁ : Type u_8<VAR>inst✝ : SMul M Y₁<VAR>f : X →ₑ[φ] Y<VAR>g : Y → X<VAR>k : Function.RightInverse φ' φ<VAR>h₁ : Function.LeftInverse g ⇑f<VAR>h₂ : Function.RightInverse g ⇑f<VAR>m : N<VAR>x : Y<GOAL>g (φ (φ' m) • f (g x)) = g (f (φ' m • g x))
<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 a' : α<VAR>b : M<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Finite α<VAR>x : α<VAR>m : M<VAR>x✝ : α<GOAL>equivFunOnFinite (single x m) x✝ = Pi.single x m x✝
<VAR>R : Type uR<VAR>inst✝⁶ : CommRing R<VAR>A : Type uA<VAR>inst✝⁵ : AddCommGroup A<VAR>A' : Type u_1<VAR>inst✝⁴ : AddCommGroup A'<VAR>B : Type uB<VAR>inst✝³ : AddCommGroup B<VAR>inst✝² : Module R A<VAR>inst✝¹ : Module R A'<VAR>inst✝ : Module R B<VAR>f : A →ₗ[R] A'<VAR>h : Function.Surjective ⇑(dual f)<VAR>a : A<VAR>h0 : f a = 0<VAR>c : CharacterModule A'<GOAL>((dual f) c) a = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_4<VAR>inst✝³ : Primcodable α<VAR>inst✝² : Primcodable β<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Primcodable σ<VAR>n : ℕ<GOAL>Primrec fun a => ↑a.succ
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝³ : AddGroup ι<VAR>inst✝² : Preorder ι<VAR>inst✝¹ : CovariantClass ι ι (Function.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>f : Filtration ι m<VAR>τ : Ω → ι<VAR>hτ : IsStoppingTime f τ<VAR>i : ι<VAR>hi : 0 ≤ i<VAR>j : ι<GOAL>MeasurableSet {ω | (fun ω => τ ω + i) ω ≤ j}
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝³ : AddGroup ι<VAR>inst✝² : Preorder ι<VAR>inst✝¹ : CovariantClass ι ι (Function.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>f : Filtration ι m<VAR>τ : Ω → ι<VAR>hτ : IsStoppingTime f τ<VAR>i : ι<VAR>hi : 0 ≤ i<VAR>j : ι<GOAL>MeasurableSet {ω | τ ω ≤ j - i}
<VAR>α : Type u_1<VAR>b : Bool<VAR>n : Num<GOAL>↑(bit b n) = Nat.bit b ↑n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r r₁ r₂ : α → α → Prop<VAR>s t : Set α<VAR>a✝ b✝ x : α<VAR>ht : IsAntichain r t<VAR>h : minimals r s ⊆ t<VAR>hs : ∀ ⦃a : α⦄, a ∈ t → ∃ b ∈ minimals r s, r a b<VAR>a : α<VAR>ha : a ∈ t<VAR>b : α<VAR>hb : b ∈ minimals r s<VAR>hr : r a b<GOAL>a ∈ minimals r s
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<GOAL>(toFunLinear R A) (1 ⊗ₜ[R] 1) = 1
<VAR>E : Type u_1<VAR>β : Type u_2<VAR>inst✝⁷ : AddCommGroup E<VAR>inst✝⁶ : TopologicalSpace E<VAR>inst✝⁵ : Module ℝ E<VAR>inst✝⁴ : TopologicalAddGroup E<VAR>inst✝³ : ContinuousSMul ℝ E<VAR>inst✝² : OrderedAddCommGroup β<VAR>inst✝¹ : Module ℝ β<VAR>inst✝ : OrderedSMul ℝ β<VAR>s : Set E<VAR>f : E → β<VAR>a : E<VAR>a_in_s : a ∈ s<VAR>h_localmin : IsLocalMinOn f s a<VAR>h_conv : ConvexOn ℝ s f<VAR>x : E<VAR>x_in_s : x ∈ s<VAR>g : ℝ →ᵃ[ℝ] E := AffineMap.lineMap a x<GOAL>x ∈ {x | (fun x => f a ≤ f x) x}
<VAR>E : Type u_1<VAR>β : Type u_2<VAR>inst✝⁷ : AddCommGroup E<VAR>inst✝⁶ : TopologicalSpace E<VAR>inst✝⁵ : Module ℝ E<VAR>inst✝⁴ : TopologicalAddGroup E<VAR>inst✝³ : ContinuousSMul ℝ E<VAR>inst✝² : OrderedAddCommGroup β<VAR>inst✝¹ : Module ℝ β<VAR>inst✝ : OrderedSMul ℝ β<VAR>s : Set E<VAR>f : E → β<VAR>a : E<VAR>a_in_s : a ∈ s<VAR>h_localmin : IsLocalMinOn f s a<VAR>h_conv : ConvexOn ℝ s f<VAR>x : E<VAR>x_in_s : x ∈ s<VAR>g : ℝ →ᵃ[ℝ] E := AffineMap.lineMap a x<VAR>hg0 : g 0 = a<GOAL>x ∈ {x | (fun x => f a ≤ f x) x}
<VAR>E : Type u_1<VAR>β : Type u_2<VAR>inst✝⁷ : AddCommGroup E<VAR>inst✝⁶ : TopologicalSpace E<VAR>inst✝⁵ : Module ℝ E<VAR>inst✝⁴ : TopologicalAddGroup E<VAR>inst✝³ : ContinuousSMul ℝ E<VAR>inst✝² : OrderedAddCommGroup β<VAR>inst✝¹ : Module ℝ β<VAR>inst✝ : OrderedSMul ℝ β<VAR>s : Set E<VAR>f : E → β<VAR>a : E<VAR>a_in_s : a ∈ s<VAR>h_localmin : IsLocalMinOn f s a<VAR>h_conv : ConvexOn ℝ s f<VAR>x : E<VAR>x_in_s : x ∈ s<VAR>g : ℝ →ᵃ[ℝ] E := AffineMap.lineMap a x<VAR>hg0 : g 0 = a<VAR>hg1 : g 1 = x<GOAL>x ∈ {x | (fun x => f a ≤ f x) x}
<VAR>E : Type u_1<VAR>β : Type u_2<VAR>inst✝⁷ : AddCommGroup E<VAR>inst✝⁶ : TopologicalSpace E<VAR>inst✝⁵ : Module ℝ E<VAR>inst✝⁴ : TopologicalAddGroup E<VAR>inst✝³ : ContinuousSMul ℝ E<VAR>inst✝² : OrderedAddCommGroup β<VAR>inst✝¹ : Module ℝ β<VAR>inst✝ : OrderedSMul ℝ β<VAR>s : Set E<VAR>f : E → β<VAR>a : E<VAR>a_in_s : a ∈ s<VAR>h_localmin : IsLocalMinOn f s a<VAR>h_conv : ConvexOn ℝ s f<VAR>x : E<VAR>x_in_s : x ∈ s<VAR>g : ℝ →ᵃ[ℝ] E := AffineMap.lineMap a x<VAR>hg0 : g 0 = a<VAR>hg1 : g 1 = x<VAR>hgc : Continuous ⇑g<GOAL>x ∈ {x | (fun x => f a ≤ f x) x}
<VAR>E : Type u_1<VAR>β : Type u_2<VAR>inst✝⁷ : AddCommGroup E<VAR>inst✝⁶ : TopologicalSpace E<VAR>inst✝⁵ : Module ℝ E<VAR>inst✝⁴ : TopologicalAddGroup E<VAR>inst✝³ : ContinuousSMul ℝ E<VAR>inst✝² : OrderedAddCommGroup β<VAR>inst✝¹ : Module ℝ β<VAR>inst✝ : OrderedSMul ℝ β<VAR>s : Set E<VAR>f : E → β<VAR>a : E<VAR>a_in_s : a ∈ s<VAR>h_localmin : IsLocalMinOn f s a<VAR>h_conv : ConvexOn ℝ s f<VAR>x : E<VAR>x_in_s : x ∈ s<VAR>g : ℝ →ᵃ[ℝ] E := AffineMap.lineMap a x<VAR>hg0 : g 0 = a<VAR>hg1 : g 1 = x<VAR>hgc : Continuous ⇑g<VAR>h_maps : MapsTo (⇑g) (Icc 0 1) s<GOAL>x ∈ {x | (fun x => f a ≤ f x) x}
<VAR>E : Type u_1<VAR>β : Type u_2<VAR>inst✝⁷ : AddCommGroup E<VAR>inst✝⁶ : TopologicalSpace E<VAR>inst✝⁵ : Module ℝ E<VAR>inst✝⁴ : TopologicalAddGroup E<VAR>inst✝³ : ContinuousSMul ℝ E<VAR>inst✝² : OrderedAddCommGroup β<VAR>inst✝¹ : Module ℝ β<VAR>inst✝ : OrderedSMul ℝ β<VAR>s : Set E<VAR>f : E → β<VAR>a : E<VAR>a_in_s : a ∈ s<VAR>h_localmin : IsLocalMinOn f s a<VAR>h_conv : ConvexOn ℝ s f<VAR>x : E<VAR>x_in_s : x ∈ s<VAR>g : ℝ →ᵃ[ℝ] E := AffineMap.lineMap a x<VAR>hg0 : g 0 = a<VAR>hg1 : g 1 = x<VAR>hgc : Continuous ⇑g<VAR>h_maps : MapsTo (⇑g) (Icc 0 1) s<VAR>fg_local_min_on : IsLocalMinOn (f ∘ ⇑g) (Icc 0 1) 0<GOAL>x ∈ {x | (fun x => f a ≤ f x) x}
<VAR>E : Type u_1<VAR>β : Type u_2<VAR>inst✝⁷ : AddCommGroup E<VAR>inst✝⁶ : TopologicalSpace E<VAR>inst✝⁵ : Module ℝ E<VAR>inst✝⁴ : TopologicalAddGroup E<VAR>inst✝³ : ContinuousSMul ℝ E<VAR>inst✝² : OrderedAddCommGroup β<VAR>inst✝¹ : Module ℝ β<VAR>inst✝ : OrderedSMul ℝ β<VAR>s : Set E<VAR>f : E → β<VAR>a : E<VAR>a_in_s : a ∈ s<VAR>h_localmin : IsLocalMinOn f s a<VAR>h_conv : ConvexOn ℝ s f<VAR>x : E<VAR>x_in_s : x ∈ s<VAR>g : ℝ →ᵃ[ℝ] E := AffineMap.lineMap a x<VAR>hg0 : g 0 = a<VAR>hg1 : g 1 = x<VAR>hgc : Continuous ⇑g<VAR>h_maps : MapsTo (⇑g) (Icc 0 1) s<VAR>fg_local_min_on : IsLocalMinOn (f ∘ ⇑g) (Icc 0 1) 0<VAR>fg_min_on : IsMinOn (f ∘ ⇑g) (Icc 0 1) 0<GOAL>x ∈ {x | (fun x => f a ≤ f x) x}
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>n : ℤ<GOAL>U R n = 2 * X * U R (n - 1) - U R (n - 2)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>t : ℝ≥0∞<VAR>t_ne_top : t ≠ ⊤<GOAL>Continuous t.truncateToReal
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>t : ℝ≥0∞<VAR>t_ne_top : t ≠ ⊤<GOAL>∀ (x : ℝ≥0∞), ((fun p => min p.1 p.2) ∘ fun y => (t, y)) x ∈ {a | a ≠ ⊤}
<VAR>M : Type u<VAR>m₁ m₂ : Monoid M<VAR>h_mul : HMul.hMul = HMul.hMul<GOAL>m₁ = m₂
<VAR>M : Type u<VAR>m₁ m₂ : Monoid M<VAR>h_mul : HMul.hMul = HMul.hMul<VAR>this : toMulOneClass = toMulOneClass<GOAL>m₁ = m₂
<VAR>M : Type u<VAR>m₁ m₂ : Monoid M<VAR>h_mul : HMul.hMul = HMul.hMul<VAR>this : toMulOneClass = toMulOneClass<VAR>h₁ : One.one = One.one<VAR>f : M →* M := { toFun := id, map_one' := h₁, map_mul' := ⋯ }<GOAL>m₁ = m₂
<VAR>M : Type u<VAR>m₁ m₂ : Monoid M<VAR>h_mul : HMul.hMul = HMul.hMul<VAR>this✝ : toMulOneClass = toMulOneClass<VAR>h₁ : One.one = One.one<VAR>f : M →* M := { toFun := id, map_one' := h₁, map_mul' := ⋯ }<VAR>this : Monoid.npow = Monoid.npow<GOAL>m₁ = m₂
<VAR>C : Type u_1<VAR>inst✝ : Category.{u_2, u_1} C<VAR>r : HomRel C<VAR>h : Congruence r<VAR>X Y : C<VAR>f f' : X ⟶ Y<GOAL>Quot.mk (CompClosure r) f = Quot.mk (CompClosure r) f' ↔ r f f'
<VAR>C : Type u_1<VAR>inst✝ : Category.{u_2, u_1} C<VAR>r : HomRel C<VAR>h : Congruence r<VAR>X Y : C<VAR>f f' : X ⟶ Y<GOAL>_root_.Equivalence (CompClosure r)
<VAR>R : Type u_1<VAR>inst✝⁵ : Ring R<VAR>C : Type u_2<VAR>inst✝⁴ : Category.{u_3, u_2} C<VAR>inst✝³ : Abelian C<VAR>inst✝² : Linear R C<VAR>inst✝¹ : EnoughProjectives C<VAR>X Y : C<VAR>inst✝ : Projective X<VAR>n : ℕ<GOAL>IsZero (((Ext R C (n + 1)).obj (Opposite.op X)).obj Y)
<VAR>R : Type u_1<VAR>inst✝⁵ : Ring R<VAR>C : Type u_2<VAR>inst✝⁴ : Category.{u_3, u_2} C<VAR>inst✝³ : Abelian C<VAR>inst✝² : Linear R C<VAR>inst✝¹ : EnoughProjectives C<VAR>X Y : C<VAR>inst✝ : Projective X<VAR>n : ℕ<GOAL>IsZero (HomologicalComplex.homology ((ProjectiveResolution.self X).complex.linearYonedaObj R Y) (n + 1))
<VAR>R : Type u_1<VAR>inst✝⁵ : Ring R<VAR>C : Type u_2<VAR>inst✝⁴ : Category.{u_3, u_2} C<VAR>inst✝³ : Abelian C<VAR>inst✝² : Linear R C<VAR>inst✝¹ : EnoughProjectives C<VAR>X Y : C<VAR>inst✝ : Projective X<VAR>n : ℕ<GOAL>(HomologicalComplex.sc ((ProjectiveResolution.self X).complex.linearYonedaObj R Y) (n + 1)).Exact
<VAR>R : Type u_1<VAR>inst✝⁵ : Ring R<VAR>C : Type u_2<VAR>inst✝⁴ : Category.{u_3, u_2} C<VAR>inst✝³ : Abelian C<VAR>inst✝² : Linear R C<VAR>inst✝¹ : EnoughProjectives C<VAR>X Y : C<VAR>inst✝ : Projective X<VAR>n : ℕ<GOAL>IsZero (HomologicalComplex.sc ((ProjectiveResolution.self X).complex.linearYonedaObj R Y) (n + 1)).X₂
<VAR>R : Type u_1<VAR>inst✝⁵ : Ring R<VAR>C : Type u_2<VAR>inst✝⁴ : Category.{u_3, u_2} C<VAR>inst✝³ : Abelian C<VAR>inst✝² : Linear R C<VAR>inst✝¹ : EnoughProjectives C<VAR>X Y : C<VAR>inst✝ : Projective X<VAR>n : ℕ<GOAL>IsZero (ModuleCat.of R (((ChainComplex.single₀ C).obj X).X (n + 1) ⟶ Y))
<VAR>R : Type u_1<VAR>inst✝⁵ : Ring R<VAR>C : Type u_2<VAR>inst✝⁴ : Category.{u_3, u_2} C<VAR>inst✝³ : Abelian C<VAR>inst✝² : Linear R C<VAR>inst✝¹ : EnoughProjectives C<VAR>X Y : C<VAR>inst✝ : Projective X<VAR>n : ℕ<GOAL>𝟙 (ModuleCat.of R (((ChainComplex.single₀ C).obj X).X (n + 1) ⟶ Y)) = 0
<VAR>R : Type u_1<VAR>inst✝⁵ : Ring R<VAR>C : Type u_2<VAR>inst✝⁴ : Category.{u_3, u_2} C<VAR>inst✝³ : Abelian C<VAR>inst✝² : Linear R C<VAR>inst✝¹ : EnoughProjectives C<VAR>X Y : C<VAR>inst✝ : Projective X<VAR>n : ℕ<VAR>x : ((ChainComplex.single₀ C).obj X).X (n + 1) ⟶ Y<GOAL>(𝟙 (ModuleCat.of R (((ChainComplex.single₀ C).obj X).X (n + 1) ⟶ Y))) x = 0 x
<VAR>R : Type u_1<VAR>inst✝⁵ : Ring R<VAR>C : Type u_2<VAR>inst✝⁴ : Category.{u_3, u_2} C<VAR>inst✝³ : Abelian C<VAR>inst✝² : Linear R C<VAR>inst✝¹ : EnoughProjectives C<VAR>X Y : C<VAR>inst✝ : Projective X<VAR>n : ℕ<GOAL>(𝟙 (ModuleCat.of R (((ChainComplex.single₀ C).obj X).X (n + 1) ⟶ Y))) 0 = 0 0
<VAR>M : Type u_1<VAR>inst✝² : CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝¹ : CommMonoid N<VAR>P : Type u_3<VAR>inst✝ : CommMonoid P<VAR>f : S.LocalizationMap N<VAR>g : M →* P<VAR>hg : ∀ (y : ↥S), IsUnit (g ↑y)<VAR>x : M<GOAL>(f.lift hg) (f.toMap x) = g x
<VAR>M : Type u_1<VAR>inst✝² : CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝¹ : CommMonoid N<VAR>P : Type u_3<VAR>inst✝ : CommMonoid P<VAR>f : S.LocalizationMap N<VAR>g : M →* P<VAR>hg : ∀ (y : ↥S), IsUnit (g ↑y)<VAR>x : M<GOAL>g (f.sec (f.toMap x)).1 = g (↑(f.sec (f.toMap x)).2 * x)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : GeneralizedCoheytingAlgebra α<VAR>a b c d : α<GOAL>a ⊓ b ⊔ a ∆ b = a ⊔ b
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : CommSemiring α<VAR>s : Multiset ι<VAR>f g : ι → α<GOAL>(map (fun i => f i + g i) s).prod = (map (fun p => (map f p.1).prod * (map g p.2).prod) s.antidiagonal).sum
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : CommSemiring α<VAR>s : Multiset ι<VAR>f g : ι → α<GOAL>(map (fun i => f i + g i) 0).prod = (map (fun p => (map f p.1).prod * (map g p.2).prod) (antidiagonal 0)).sum
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : CommSemiring α<VAR>s✝ : Multiset ι<VAR>f g : ι → α<VAR>a : ι<VAR>s : Multiset ι<VAR>ih : (map (fun i => f i + g i) s).prod = (map (fun p => (map f p.1).prod * (map g p.2).prod) s.antidiagonal).sum<GOAL>(map (fun i => f i + g i) (a ::ₘ s)).prod = (map (fun p => (map f p.1).prod * (map g p.2).prod) (a ::ₘ s).antidiagonal).sum
<VAR>C✝ : Type u<VAR>𝒞 : Category.{v, u} C✝<VAR>inst✝² : MonoidalCategory C✝<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : MonoidalCategory C<VAR>U V W X Y Z : C<VAR>f : W ⟶ X<VAR>g : Y ⟶ Z<GOAL>(g ⊗ 𝟙 W) ≫ (𝟙 Z ⊗ f) = g ⊗ f
<VAR>C✝ : Type u<VAR>𝒞 : Category.{v, u} C✝<VAR>inst✝² : MonoidalCategory C✝<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : MonoidalCategory C<VAR>U V W X Y Z : C<VAR>f : W ⟶ X<VAR>g : Y ⟶ Z<GOAL>g ≫ 𝟙 Z ⊗ 𝟙 W ≫ f = g ⊗ f
<VAR>α : Type u<VAR>inst✝² : CommGroup α<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c d : α<GOAL>a / d < b / c → a < b ∨ c < d
<VAR>α : Type u<VAR>inst✝² : CommGroup α<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c d : α<GOAL>b ≤ a ∧ d ≤ c → b / c ≤ a / d
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m : MeasurableSpace Ω<VAR>X✝ : Ω → ℝ<VAR>p : ℕ<VAR>μ : Measure Ω<VAR>t : ℝ<VAR>X Y : Ω → ℝ<VAR>h_indep : IndepFun X Y μ<VAR>hX : AEStronglyMeasurable X μ<VAR>hY : AEStronglyMeasurable Y μ<VAR>A : Continuous fun x => rexp (t * x)<GOAL>mgf (X + Y) μ t = mgf X μ t * mgf Y μ t
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m : MeasurableSpace Ω<VAR>X✝ : Ω → ℝ<VAR>p : ℕ<VAR>μ : Measure Ω<VAR>t : ℝ<VAR>X Y : Ω → ℝ<VAR>h_indep : IndepFun X Y μ<VAR>hX : AEStronglyMeasurable X μ<VAR>hY : AEStronglyMeasurable Y μ<VAR>A : Continuous fun x => rexp (t * x)<VAR>h'X : AEStronglyMeasurable (fun ω => rexp (t * X ω)) μ<GOAL>mgf (X + Y) μ t = mgf X μ t * mgf Y μ t
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m : MeasurableSpace Ω<VAR>X✝ : Ω → ℝ<VAR>p : ℕ<VAR>μ : Measure Ω<VAR>t : ℝ<VAR>X Y : Ω → ℝ<VAR>h_indep : IndepFun X Y μ<VAR>hX : AEStronglyMeasurable X μ<VAR>hY : AEStronglyMeasurable Y μ<VAR>A : Continuous fun x => rexp (t * x)<VAR>h'X : AEStronglyMeasurable (fun ω => rexp (t * X ω)) μ<VAR>h'Y : AEStronglyMeasurable (fun ω => rexp (t * Y ω)) μ<GOAL>mgf (X + Y) μ t = mgf X μ t * mgf Y μ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : LinearOrder β<VAR>f : α → β<VAR>𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)<VAR>s t u : Finset α<VAR>a b : α<VAR>r : ℕ<VAR>inst✝ : Fintype α<GOAL>IsInitSeg 𝒜 r ∧ 𝒜.Nonempty ↔ ∃ s, s.card = r ∧ 𝒜 = initSeg s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : LinearOrder β<VAR>f : α → β<VAR>𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)<VAR>s t u : Finset α<VAR>a b : α<VAR>r : ℕ<VAR>inst✝ : Fintype α<GOAL>(∃ s, s.card = r ∧ 𝒜 = initSeg s) → IsInitSeg 𝒜 r ∧ 𝒜.Nonempty