ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u<VAR>inst✝¹³ : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : NormedSpace 𝕜 E<VAR>F : Type w<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedSpace 𝕜 F<VAR>F' : Type x<VAR>inst✝⁸ : AddCommGroup F'<VAR>inst✝⁷ : Module 𝕜 F'<VAR>inst✝⁶ : TopologicalSpace F'<VAR>inst✝⁵ : TopologicalAddGroup F'<VAR>inst✝⁴ : ContinuousSMul 𝕜 F'<VAR>inst✝³ : CompleteSpace 𝕜<VAR>E' : Type u_1<VAR>inst✝² : NormedAddCommGroup E'<VAR>inst✝¹ : NormedSpace ℝ E'<VAR>inst✝ : FiniteDimensional ℝ E'<GOAL>0 < lipschitzExtensionConstant E'
<VAR>𝕜 : Type u<VAR>inst✝¹³ : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : NormedSpace 𝕜 E<VAR>F : Type w<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedSpace 𝕜 F<VAR>F' : Type x<VAR>inst✝⁸ : AddCommGroup F'<VAR>inst✝⁷ : Module 𝕜 F'<VAR>inst✝⁶ : TopologicalSpace F'<VAR>inst✝⁵ : TopologicalAddGroup F'<VAR>inst✝⁴ : ContinuousSMul 𝕜 F'<VAR>inst✝³ : CompleteSpace 𝕜<VAR>E' : Type u_1<VAR>inst✝² : NormedAddCommGroup E'<VAR>inst✝¹ : NormedSpace ℝ E'<VAR>inst✝ : FiniteDimensional ℝ E'<GOAL>0 < let A := (Basis.ofVectorSpace ℝ E').equivFun.toContinuousLinearEquiv; max (‖↑A.symm‖₊ * ‖↑A‖₊) 1
<VAR>α : Type u<VAR>β : Type v<VAR>a b : α<VAR>inst✝ : CommSemiring α<VAR>I : Ideal α<VAR>m n : ℕ<VAR>ha : a ^ m ∈ I<VAR>h : m ≤ n<GOAL>a ^ n ∈ I
<VAR>α : Type u<VAR>β : Type v<VAR>a b : α<VAR>inst✝ : CommSemiring α<VAR>I : Ideal α<VAR>m n : ℕ<VAR>ha : a ^ m ∈ I<VAR>h : m ≤ n<GOAL>a ^ m * a ^ (n - m) ∈ I
<VAR>Γ : Type u_1<VAR>Γ' : Type u_2<VAR>R : Type u_3<VAR>V : Type u_4<VAR>inst✝⁶ : PartialOrder Γ<VAR>inst✝⁵ : PartialOrder Γ'<VAR>inst✝⁴ : VAdd Γ Γ'<VAR>inst✝³ : IsOrderedCancelVAdd Γ Γ'<VAR>inst✝² : Zero R<VAR>inst✝¹ : AddCommMonoid V<VAR>inst✝ : SMulWithZero R V<VAR>x : HahnSeries Γ R<VAR>y : HahnModule Γ' R V<VAR>a : Γ'<VAR>s : Set Γ<VAR>hs : s.IsPWO<VAR>hxs : x.support ⊆ s<GOAL>((of R).symm (x • y)).coeff a = ∑ ij ∈ VAddAntidiagonal hs ⋯ a, x.coeff ij.1 • ((of R).symm y).coeff ij.2
<VAR>Γ : Type u_1<VAR>Γ' : Type u_2<VAR>R : Type u_3<VAR>V : Type u_4<VAR>inst✝⁶ : PartialOrder Γ<VAR>inst✝⁵ : PartialOrder Γ'<VAR>inst✝⁴ : VAdd Γ Γ'<VAR>inst✝³ : IsOrderedCancelVAdd Γ Γ'<VAR>inst✝² : Zero R<VAR>inst✝¹ : AddCommMonoid V<VAR>inst✝ : SMulWithZero R V<VAR>x : HahnSeries Γ R<VAR>y : HahnModule Γ' R V<VAR>a : Γ'<VAR>s : Set Γ<VAR>hs : s.IsPWO<VAR>hxs : x.support ⊆ s<GOAL>∑ ij ∈ VAddAntidiagonal ⋯ ⋯ a, x.coeff ij.1 • ((of R).symm y).coeff ij.2 = ∑ ij ∈ VAddAntidiagonal hs ⋯ a, x.coeff ij.1 • ((of R).symm y).coeff ij.2
<VAR>Γ : Type u_1<VAR>Γ' : Type u_2<VAR>R : Type u_3<VAR>V : Type u_4<VAR>inst✝⁶ : PartialOrder Γ<VAR>inst✝⁵ : PartialOrder Γ'<VAR>inst✝⁴ : VAdd Γ Γ'<VAR>inst✝³ : IsOrderedCancelVAdd Γ Γ'<VAR>inst✝² : Zero R<VAR>inst✝¹ : AddCommMonoid V<VAR>inst✝ : SMulWithZero R V<VAR>x : HahnSeries Γ R<VAR>y : HahnModule Γ' R V<VAR>a : Γ'<VAR>s : Set Γ<VAR>hs : s.IsPWO<VAR>hxs : x.support ⊆ s<GOAL>∀ x_1 ∈ VAddAntidiagonal hs ⋯ a \ VAddAntidiagonal ⋯ ⋯ a, x.coeff x_1.1 • ((of R).symm y).coeff x_1.2 = 0
<VAR>Γ : Type u_1<VAR>Γ' : Type u_2<VAR>R : Type u_3<VAR>V : Type u_4<VAR>inst✝⁶ : PartialOrder Γ<VAR>inst✝⁵ : PartialOrder Γ'<VAR>inst✝⁴ : VAdd Γ Γ'<VAR>inst✝³ : IsOrderedCancelVAdd Γ Γ'<VAR>inst✝² : Zero R<VAR>inst✝¹ : AddCommMonoid V<VAR>inst✝ : SMulWithZero R V<VAR>x : HahnSeries Γ R<VAR>y : HahnModule Γ' R V<VAR>a : Γ'<VAR>s : Set Γ<VAR>hs : s.IsPWO<VAR>hxs : x.support ⊆ s<VAR>b : Γ × Γ'<VAR>hb : b ∈ VAddAntidiagonal hs ⋯ a \ VAddAntidiagonal ⋯ ⋯ a<GOAL>x.coeff b.1 • ((of R).symm y).coeff b.2 = 0
<VAR>Γ : Type u_1<VAR>Γ' : Type u_2<VAR>R : Type u_3<VAR>V : Type u_4<VAR>inst✝⁶ : PartialOrder Γ<VAR>inst✝⁵ : PartialOrder Γ'<VAR>inst✝⁴ : VAdd Γ Γ'<VAR>inst✝³ : IsOrderedCancelVAdd Γ Γ'<VAR>inst✝² : Zero R<VAR>inst✝¹ : AddCommMonoid V<VAR>inst✝ : SMulWithZero R V<VAR>x : HahnSeries Γ R<VAR>y : HahnModule Γ' R V<VAR>a : Γ'<VAR>s : Set Γ<VAR>hs : s.IsPWO<VAR>hxs : x.support ⊆ s<VAR>b : Γ × Γ'<VAR>hb : (b.1 ∈ s ∧ ((of R).symm y).coeff b.2 ≠ 0 ∧ b.1 +ᵥ b.2 = a) ∧ (((of R).symm y).coeff b.2 ≠ 0 ∧ b.1 +ᵥ b.2 = a → x.coeff b.1 = 0)<GOAL>x.coeff b.1 • ((of R).symm y).coeff b.2 = 0
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>J : Type u₂<VAR>inst✝ : Category.{v₂, u₂} J<VAR>F : J ⥤ Cᵒᵖ<VAR>c : Cocone F.leftOp<VAR>hc : IsColimit c<VAR>s : Cone F<VAR>j : J<GOAL>((fun s => (hc.desc (coconeLeftOpOfCone s)).op) s ≫ (coneOfCoconeLeftOp c).π.app j).unop = (s.π.app j).unop
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>J : Type u₂<VAR>inst✝ : Category.{v₂, u₂} J<VAR>F : J ⥤ Cᵒᵖ<VAR>c : Cocone F.leftOp<VAR>hc : IsColimit c<VAR>s : Cone F<VAR>m : s.pt ⟶ (coneOfCoconeLeftOp c).pt<VAR>w : ∀ (j : J), m ≫ (coneOfCoconeLeftOp c).π.app j = s.π.app j<GOAL>m = (fun s => (hc.desc (coconeLeftOpOfCone s)).op) s
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>J : Type u₂<VAR>inst✝ : Category.{v₂, u₂} J<VAR>F : J ⥤ Cᵒᵖ<VAR>c : Cocone F.leftOp<VAR>hc : IsColimit c<VAR>s : Cone F<VAR>m : s.pt ⟶ (coneOfCoconeLeftOp c).pt<VAR>w : ∀ (j : J), m ≫ (coneOfCoconeLeftOp c).π.app j = s.π.app j<VAR>j : Jᵒᵖ<GOAL>(c.ι.app j ≫ m.unop).op = (c.ι.app j ≫ ((fun s => (hc.desc (coconeLeftOpOfCone s)).op) s).unop).op
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>inst✝¹ : PreservesColimit (span f f) F<VAR>inst✝ : Epi f<VAR>this : IsColimit (PushoutCocone.mk (F.map (𝟙 Y)) (F.map (𝟙 Y)) ⋯)<GOAL>Epi (F.map f)
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>inst✝¹ : PreservesColimit (span f f) F<VAR>inst✝ : Epi f<VAR>this : IsColimit (PushoutCocone.mk (𝟙 (F.obj Y)) (𝟙 (F.obj Y)) ⋯)<GOAL>Epi (F.map f)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → Preorder (π i)<VAR>x y : (i : ι) → π i<VAR>i : ι<VAR>a b : π i<GOAL>update x i a < x ↔ a < x i
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>x y f' : ℝ<VAR>hfc : ConcaveOn ℝ S f<VAR>hfd : ∀ x ∈ S, DifferentiableAt ℝ f x<GOAL>AntitoneOn (deriv f) S
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b✝ c✝ : α<VAR>n : ℤ<VAR>a b c : α<GOAL>toIocMod hp a (b + c) = toIocMod hp (a - c) b + c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : Finite α<VAR>this : Fintype α<GOAL>Nat.card α ≤ 1 ↔ Subsingleton α
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>J : Type u₂<VAR>inst✝ : Category.{v₂, u₂} J<VAR>F : Jᵒᵖ ⥤ Cᵒᵖ<VAR>c : Cone F.unop<VAR>hc : IsLimit c<VAR>s : Cocone F<VAR>m : (coconeOfConeUnop c).pt ⟶ s.pt<VAR>w : ∀ (j : Jᵒᵖ), (coconeOfConeUnop c).ι.app j ≫ m = s.ι.app j<GOAL>m = (fun s => (hc.lift (coneUnopOfCocone s)).op) s
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>J : Type u₂<VAR>inst✝ : Category.{v₂, u₂} J<VAR>F : Jᵒᵖ ⥤ Cᵒᵖ<VAR>c : Cone F.unop<VAR>hc : IsLimit c<VAR>s : Cocone F<VAR>m : (coconeOfConeUnop c).pt ⟶ s.pt<VAR>w : ∀ (j : Jᵒᵖ), (coconeOfConeUnop c).ι.app j ≫ m = s.ι.app j<VAR>j : J<GOAL>(m.unop ≫ c.π.app j).op = (((fun s => (hc.lift (coneUnopOfCocone s)).op) s).unop ≫ c.π.app j).op
<VAR>p : ℕ<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>H K : Subgroup G<VAR>hH : IsPGroup p ↥H<VAR>hK : IsPGroup p ↥K<VAR>inst✝ : K.Normal<GOAL>IsPGroup p ↥(H ⊔ K)
<VAR>p : ℕ<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>H K : Subgroup G<VAR>hH : IsPGroup p ↥H<VAR>hK : IsPGroup p ↥K<VAR>inst✝ : K.Normal<GOAL>IsPGroup p ↥(Subgroup.comap (QuotientGroup.mk' K) (Subgroup.map (QuotientGroup.mk' K) H))
<VAR>p : ℕ<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>H K : Subgroup G<VAR>hH : IsPGroup p ↥H<VAR>hK : IsPGroup p ↥K<VAR>inst✝ : K.Normal<GOAL>IsPGroup p ↥(QuotientGroup.mk' K).ker
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>δ : Type u_4<VAR>mδ : MeasurableSpace δ<VAR>γ : Type u_5<VAR>mγ : MeasurableSpace γ<VAR>f : β → γ<VAR>g : γ → α<VAR>κ : Kernel α (β × γ)<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>(κ.fst a) s = (κ a) {p | p.1 ∈ s}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>δ : Type u_4<VAR>mδ : MeasurableSpace δ<VAR>γ : Type u_5<VAR>mγ : MeasurableSpace γ<VAR>f : β → γ<VAR>g : γ → α<VAR>κ : Kernel α (β × γ)<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>(κ a) (Prod.fst ⁻¹' s) = (κ a) {p | p.1 ∈ s}
<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 t : α → Prop<VAR>hst : s =ᶠ[ae μ] t<VAR>p : α → Prop<GOAL>(∀ᵐ (x : α) ∂μ.restrict s, p x) → ∀ᵐ (x : α) ∂μ.restrict t, p x
<VAR>n k : ℕ<VAR>h : n ∈ k.smoothNumbers<GOAL>∃ s ∈ k.primesBelow.powerset, ∃ m, n = m ^ 2 * s.prod id
<VAR>n k : ℕ<VAR>h : n ∈ k.smoothNumbers<VAR>l m : ℕ<VAR>H₁ : m ^ 2 * l = n<VAR>H₂ : Squarefree l<GOAL>∃ s ∈ k.primesBelow.powerset, ∃ m, n = m ^ 2 * s.prod id
<VAR>n k : ℕ<VAR>h : n ∈ k.smoothNumbers<VAR>l m : ℕ<VAR>H₁ : m ^ 2 * l = n<VAR>H₂ : Squarefree l<VAR>hl : l ∈ k.smoothNumbers<GOAL>∃ s ∈ k.primesBelow.powerset, ∃ m, n = m ^ 2 * s.prod id
<VAR>n k : ℕ<VAR>h : n ∈ k.smoothNumbers<VAR>l m : ℕ<VAR>H₁ : m ^ 2 * l = n<VAR>H₂ : Squarefree l<VAR>hl : l ∈ k.smoothNumbers<GOAL>l = l.primeFactorsList.toFinset.prod id
<VAR>n k : ℕ<VAR>h : n ∈ k.smoothNumbers<VAR>l m : ℕ<VAR>H₁ : m ^ 2 * l = n<VAR>H₂ : Squarefree l<VAR>hl : l ∈ k.smoothNumbers<GOAL>l = l.primeFactors.prod id
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝³ : (i : ι) → Zero (β i)<VAR>inst✝² : (i : ι) → Zero (β₁ i)<VAR>inst✝¹ : (i : ι) → Zero (β₂ i)<VAR>x y : Π₀ (i : ι), β i<VAR>s : Set ι<VAR>inst✝ : (i : ι) → Decidable (i ∈ s)<VAR>x✝ : ι<GOAL>(x.piecewise y s) x✝ = s.piecewise (⇑x) (⇑y) x✝
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>inst✝ : CompleteLattice α<VAR>f : ι → α<VAR>s : Set α<VAR>hne : s.Nonempty<VAR>hsc : SupClosed s<VAR>t : Finset α<VAR>ht₁ : ↑t ⊆ s<VAR>ht₂ : sSup s = t.sup id<GOAL>sSup s ∈ s
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>inst✝ : CompleteLattice α<VAR>f : ι → α<VAR>s : Set α<VAR>hne : s.Nonempty<VAR>hsc : SupClosed s<VAR>t : Finset α<VAR>ht₁ : ↑t ⊆ s<VAR>ht₂ : sSup s = t.sup id<VAR>h : t = ∅<GOAL>sSup s ∈ s
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>inst✝ : CompleteLattice α<VAR>f : ι → α<VAR>s : Set α<VAR>hne : s.Nonempty<VAR>hsc : SupClosed s<VAR>t : Finset α<VAR>ht₁ : ↑t ⊆ s<VAR>ht₂ : sSup s = t.sup id<VAR>h : t.Nonempty<GOAL>sSup s ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : TopologicalSpace δ<VAR>f : CocompactMap α β<VAR>s : Set β<VAR>hs : IsCompact s<VAR>h's : IsClosed s<GOAL>IsCompact (⇑f ⁻¹' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : TopologicalSpace δ<VAR>f : CocompactMap α β<VAR>s : Set β<VAR>hs : IsCompact s<VAR>h's : IsClosed s<VAR>t : Set α<VAR>ht : IsCompact t<VAR>hts : (⇑f ⁻¹' s)ᶜᶜ ⊆ t<GOAL>IsCompact (⇑f ⁻¹' s)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝⁵ : OrderedRing 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : AddCommGroup G<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>x y : E<GOAL>openSegment 𝕜 x y = ⇑(AffineMap.lineMap x y) '' Ioo 0 1
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝⁵ : OrderedRing 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : AddCommGroup G<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>x y : E<VAR>a✝¹ : 𝕜<VAR>a✝ : a✝¹ ∈ Ioo 0 1<GOAL>(AffineMap.lineMap x y) a✝¹ = (1 - a✝¹) • x + a✝¹ • y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s : Multiset α<GOAL>s ≤ s.dedup ↔ s.Nodup
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝ : OrderedRing α<VAR>l : Filter β<VAR>f g : β → α<VAR>hf : Tendsto f l atBot<VAR>hg : Tendsto g l atTop<GOAL>Tendsto (fun x => f x * g x) l atBot
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝ : OrderedRing α<VAR>l : Filter β<VAR>f g : β → α<VAR>hf : Tendsto f l atBot<VAR>hg : Tendsto g l atTop<VAR>this : Tendsto (fun x => -f x * g x) l atTop<GOAL>Tendsto (fun x => f x * g x) l atBot
<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>ι : Type u_4<VAR>v : ι → E<VAR>hv : Orthonormal 𝕜 v<VAR>l₁ l₂ : ι →₀ 𝕜<GOAL>⟪(Finsupp.total ι E 𝕜 v) l₁, (Finsupp.total ι E 𝕜 v) l₂⟫_𝕜 = l₁.sum fun i y => (starRingEnd 𝕜) y * l₂ i
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>z✝ z : K<GOAL>re z⁻¹ = re z / normSq z
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>γ : Type u_3<VAR>A : Type u_4<VAR>B : Type u_5<VAR>C : Type u_6<VAR>inst✝⁷ : AddCommMonoid A<VAR>inst✝⁶ : AddCommMonoid B<VAR>inst✝⁵ : AddCommMonoid C<VAR>t : ι → A → C<VAR>h0 : ∀ (i : ι), t i 0 = 0<VAR>h1 : ∀ (i : ι) (x y : A), t i (x + y) = t i x + t i y<VAR>s : Finset α<VAR>f✝ : α → ι →₀ A<VAR>i : ι<VAR>g : ι →₀ A<VAR>k : ι → A → γ → B<VAR>x : γ<VAR>β : Type u_7<VAR>M : Type u_8<VAR>M' : Type u_9<VAR>N✝ : Type u_10<VAR>P : Type u_11<VAR>G : Type u_12<VAR>H : Type u_13<VAR>R : Type u_14<VAR>S : Type u_15<VAR>inst✝⁴ : Zero M<VAR>inst✝³ : Zero M'<VAR>inst✝² : CommMonoid N✝<VAR>inst✝¹ : DecidableEq α<VAR>N : Type u_16<VAR>inst✝ : AddCommMonoid N<VAR>f : α →₀ N<VAR>a : α<GOAL>(f.sum fun x v => if a = x then v else 0) = f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : TopologicalSpace α<VAR>f g : β → α<VAR>a a₁ a₂ : α<VAR>hf : (mulSupport f).Finite<GOAL>∏' (b : β), f b = ∏ᶠ (b : β), f b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>ι' : Type u_4<VAR>inst✝¹ : Lattice α<VAR>inst✝ : OrderBot α<VAR>s t : Finset ι<VAR>f✝ : ι → α<VAR>i : ι<VAR>f : Bool → α<GOAL>true ≠ false
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝² : GroupWithZero α<VAR>inst✝¹ : MulAction α β<VAR>inst✝ : Zero γ<VAR>c : α<VAR>hc : c ≠ 0<VAR>f : β → γ<VAR>x : β<GOAL>(x ∈ support fun x => f (c⁻¹ • x)) ↔ x ∈ c • support f
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>G : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace ℝ G<VAR>L : E →L[ℝ] F →L[ℝ] G<VAR>u : ℝ → E<VAR>v : ℝ → F<VAR>u' : ℝ → E<VAR>v' : ℝ → F<VAR>m n : G<VAR>hu : ∀ (x : ℝ), HasDerivAt u (u' x) x<VAR>hv : ∀ (x : ℝ), HasDerivAt v (v' x) x<VAR>huv' : Integrable (fun x => (L (u x)) (v' x)) volume<VAR>hu'v : Integrable (fun x => (L (u' x)) (v x)) volume<VAR>huv : Integrable (fun x => (L (u x)) (v x)) volume<VAR>hG : CompleteSpace G<GOAL>∫ (x : ℝ), (L (u x)) (v' x) = -∫ (x : ℝ), (L (u' x)) (v x)
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>G : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace ℝ G<VAR>L : E →L[ℝ] F →L[ℝ] G<VAR>u : ℝ → E<VAR>v : ℝ → F<VAR>u' : ℝ → E<VAR>v' : ℝ → F<VAR>m n : G<VAR>hu : ∀ (x : ℝ), HasDerivAt u (u' x) x<VAR>hv : ∀ (x : ℝ), HasDerivAt v (v' x) x<VAR>huv' : Integrable (fun x => (L (u x)) (v' x)) volume<VAR>hu'v : Integrable (fun x => (L (u' x)) (v x)) volume<VAR>huv : Integrable (fun x => (L (u x)) (v x)) volume<VAR>hG : CompleteSpace G<VAR>I : Tendsto (fun x => (L (u x)) (v x)) atBot (𝓝 0)<GOAL>∫ (x : ℝ), (L (u x)) (v' x) = -∫ (x : ℝ), (L (u' x)) (v x)
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>G : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace ℝ G<VAR>L : E →L[ℝ] F →L[ℝ] G<VAR>u : ℝ → E<VAR>v : ℝ → F<VAR>u' : ℝ → E<VAR>v' : ℝ → F<VAR>m n : G<VAR>hu : ∀ (x : ℝ), HasDerivAt u (u' x) x<VAR>hv : ∀ (x : ℝ), HasDerivAt v (v' x) x<VAR>huv' : Integrable (fun x => (L (u x)) (v' x)) volume<VAR>hu'v : Integrable (fun x => (L (u' x)) (v x)) volume<VAR>huv : Integrable (fun x => (L (u x)) (v x)) volume<VAR>hG : CompleteSpace G<VAR>I : Tendsto (fun x => (L (u x)) (v x)) atBot (𝓝 0)<VAR>J : Tendsto (fun x => (L (u x)) (v x)) atTop (𝓝 0)<GOAL>∫ (x : ℝ), (L (u x)) (v' x) = -∫ (x : ℝ), (L (u' x)) (v x)
<VAR>x x₁ x₂ x₃ x' y y₁ y₂ y₃ y' : PGame<VAR>hx : x.Numeric<VAR>hy : y.Numeric<VAR>ihxy : IH1 x y<VAR>ihyx : IH1 y x<VAR>i j : x.LeftMoves<VAR>k : y.LeftMoves<VAR>l : (-y).LeftMoves<GOAL>⟦x.mulOption y i k⟧ < -⟦x.mulOption (-y) j l⟧
<VAR>x x₁ x₂ x₃ x' y y₁ y₂ y₃ y' : PGame<VAR>hx : x.Numeric<VAR>hy : y.Numeric<VAR>ihxy : IH1 x y<VAR>ihyx : IH1 y x<VAR>i j : x.LeftMoves<VAR>k : y.LeftMoves<VAR>l : (-y).LeftMoves<VAR>h : x.moveLeft i < x.moveLeft j<GOAL>⟦x.mulOption y i k⟧ < -⟦x.mulOption (-y) j l⟧
<VAR>x x₁ x₂ x₃ x' y y₁ y₂ y₃ y' : PGame<VAR>hx : x.Numeric<VAR>hy : y.Numeric<VAR>ihxy : IH1 x y<VAR>ihyx : IH1 y x<VAR>i j : x.LeftMoves<VAR>k : y.LeftMoves<VAR>l : (-y).LeftMoves<VAR>h : x.moveLeft i ≈ x.moveLeft j<GOAL>⟦x.mulOption y i k⟧ < -⟦x.mulOption (-y) j l⟧
<VAR>x x₁ x₂ x₃ x' y y₁ y₂ y₃ y' : PGame<VAR>hx : x.Numeric<VAR>hy : y.Numeric<VAR>ihxy : IH1 x y<VAR>ihyx : IH1 y x<VAR>i j : x.LeftMoves<VAR>k : y.LeftMoves<VAR>l : (-y).LeftMoves<VAR>h : x.moveLeft j < x.moveLeft i<GOAL>⟦x.mulOption y i k⟧ < -⟦x.mulOption (-y) j l⟧
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : Zero M<VAR>inst✝ : (m : M) → Decidable (m ≠ 0)<VAR>i : ι<VAR>m : M<VAR>a✝ : ι<GOAL>(single i m).toFinsupp a✝ = (Finsupp.single i m) a✝
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>c : CokernelCofork f<VAR>i : IsColimit c<VAR>W : C<VAR>g : W ⟶ X<VAR>hg : Epi g<VAR>h : W ⟶ Y<VAR>hh : h = g ≫ f<VAR>s : CokernelCofork h<GOAL>f ≫ Cofork.π s = 0 ≫ Cofork.π s
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>c : CokernelCofork f<VAR>i : IsColimit c<VAR>W : C<VAR>g : W ⟶ X<VAR>hg : Epi g<VAR>h : W ⟶ Y<VAR>hh : h = g ≫ f<VAR>s : CokernelCofork h<GOAL>h ≫ Cofork.π s = g ≫ 0 ≫ Cofork.π s
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : Semiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>b : ArithmeticFunction M<VAR>x : ℕ<GOAL>(1 • b) x = b x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : Semiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>b : ArithmeticFunction M<VAR>x : ℕ<GOAL>∑ x ∈ x.divisorsAntidiagonal, 1 x.1 • b x.2 = b x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : Semiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>b : ArithmeticFunction M<VAR>x : ℕ<VAR>x0 : ¬x = 0<VAR>h : {(1, x)} ⊆ x.divisorsAntidiagonal<GOAL>∑ x ∈ x.divisorsAntidiagonal, 1 x.1 • b x.2 = b x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : Semiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>b : ArithmeticFunction M<VAR>x : ℕ<VAR>x0 : ¬x = 0<VAR>h : {(1, x)} ⊆ x.divisorsAntidiagonal<GOAL>∑ x ∈ {(1, x)}, 1 x.1 • b x.2 = b x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : Semiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>b : ArithmeticFunction M<VAR>x : ℕ<VAR>x0 : ¬x = 0<VAR>h : {(1, x)} ⊆ x.divisorsAntidiagonal<GOAL>∀ x_1 ∈ x.divisorsAntidiagonal, x_1 ∉ {(1, x)} → 1 x_1.1 • b x_1.2 = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : Semiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>b : ArithmeticFunction M<VAR>x : ℕ<VAR>x0 : ¬x = 0<VAR>h : {(1, x)} ⊆ x.divisorsAntidiagonal<VAR>y : ℕ × ℕ<VAR>ymem : y ∈ x.divisorsAntidiagonal<VAR>ynmem : y ∉ {(1, x)}<GOAL>1 y.1 • b y.2 = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : Semiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>b : ArithmeticFunction M<VAR>x : ℕ<VAR>x0 : ¬x = 0<VAR>h : {(1, x)} ⊆ x.divisorsAntidiagonal<VAR>y : ℕ × ℕ<VAR>ymem : y ∈ x.divisorsAntidiagonal<VAR>ynmem : y ∉ {(1, x)}<VAR>y1ne : y.1 ≠ 1<GOAL>1 y.1 • b y.2 = 0
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<VAR>K₁ K₂ : Compacts G<VAR>eval : (Compacts G → ℝ) → ℝ := fun f => f K₁ + f K₂ - f (K₁ ⊔ K₂)<GOAL>chaar K₀ (K₁ ⊔ K₂) ≤ chaar K₀ K₁ + chaar K₀ K₂
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<VAR>K₁ K₂ : Compacts G<VAR>eval : (Compacts G → ℝ) → ℝ := fun f => f K₁ + f K₂ - f (K₁ ⊔ K₂)<VAR>this : Continuous eval<GOAL>chaar K₀ (K₁ ⊔ K₂) ≤ chaar K₀ K₁ + chaar K₀ K₂
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<VAR>K₁ K₂ : Compacts G<VAR>eval : (Compacts G → ℝ) → ℝ := fun f => f K₁ + f K₂ - f (K₁ ⊔ K₂)<VAR>this : Continuous eval<GOAL>0 ≤ chaar K₀ K₁ + chaar K₀ K₂ - chaar K₀ (K₁ ⊔ K₂)
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<VAR>K₁ K₂ : Compacts G<VAR>eval : (Compacts G → ℝ) → ℝ := fun f => f K₁ + f K₂ - f (K₁ ⊔ K₂)<VAR>this : Continuous eval<GOAL>chaar K₀ ∈ eval ⁻¹' Ici 0
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<VAR>K₁ K₂ : Compacts G<VAR>eval : (Compacts G → ℝ) → ℝ := fun f => f K₁ + f K₂ - f (K₁ ⊔ K₂)<VAR>this : Continuous eval<GOAL>clPrehaar ↑K₀ ⊤ ⊆ eval ⁻¹' Ici 0
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<VAR>K₁ K₂ : Compacts G<VAR>eval : (Compacts G → ℝ) → ℝ := fun f => f K₁ + f K₂ - f (K₁ ⊔ K₂)<VAR>this : Continuous eval<GOAL>closure (prehaar ↑K₀ '' {U | U ⊆ ↑⊤.toOpens ∧ IsOpen U ∧ 1 ∈ U}) ⊆ eval ⁻¹' Ici 0
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<VAR>K₁ K₂ : Compacts G<VAR>eval : (Compacts G → ℝ) → ℝ := fun f => f K₁ + f K₂ - f (K₁ ⊔ K₂)<VAR>this : Continuous eval<GOAL>prehaar ↑K₀ '' {U | U ⊆ ↑⊤.toOpens ∧ IsOpen U ∧ 1 ∈ U} ⊆ eval ⁻¹' Ici 0
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<VAR>K₁ K₂ : Compacts G<VAR>eval : (Compacts G → ℝ) → ℝ := fun f => f K₁ + f K₂ - f (K₁ ⊔ K₂)<VAR>this : Continuous eval<GOAL>IsClosed (eval ⁻¹' Ici 0)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>E' : Type u_5<VAR>M' : Type u_6<VAR>H' : Type u_7<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : TopologicalSpace H<VAR>inst✝⁶ : TopologicalSpace M<VAR>f f' : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>inst✝⁵ : NormedAddCommGroup E'<VAR>inst✝⁴ : NormedSpace 𝕜 E'<VAR>inst✝³ : TopologicalSpace H'<VAR>inst✝² : TopologicalSpace M'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>s t : Set M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : ChartedSpace H' M'<VAR>x : M<GOAL>UniqueDiffOn 𝕜 (extChartAt I x).target
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>E' : Type u_5<VAR>M' : Type u_6<VAR>H' : Type u_7<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : TopologicalSpace H<VAR>inst✝⁶ : TopologicalSpace M<VAR>f f' : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>inst✝⁵ : NormedAddCommGroup E'<VAR>inst✝⁴ : NormedSpace 𝕜 E'<VAR>inst✝³ : TopologicalSpace H'<VAR>inst✝² : TopologicalSpace M'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>s t : Set M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : ChartedSpace H' M'<VAR>x : M<GOAL>UniqueDiffOn 𝕜 (↑I.symm ⁻¹' (chartAt H x).target ∩ range ↑I)
<VAR>α : Type u_1<VAR>inst✝¹ : Preorder α<VAR>inst✝ : LocallyFiniteOrderBot α<VAR>b x : α<GOAL>x ∈ Iio b ↔ x < b