ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>inst✝⁷ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>A : Type u'<VAR>inst✝⁶ : Category.{v', u'} A<VAR>inst✝⁵ : ConcreteCategory A<VAR>inst✝⁴ : HasWeakSheafify J A<VAR>inst✝³ : (forget A).ReflectsIsomorphisms<VAR>inst✝² : J.HasSheafCompose (forget A)<VAR>inst✝¹ : ∀ (P : Cᵒᵖ ⥤ A), Presheaf.IsLocallyInjective J (CategoryTheory.toSheafify J P)<VAR>inst✝ : ∀ (P : Cᵒᵖ ⥤ A), Presheaf.IsLocallySurjective J (CategoryTheory.toSheafify J P)<VAR>P Q : Cᵒᵖ ⥤ A<VAR>f : P ⟶ Q<GOAL>J.W f ↔ Presheaf.IsLocallyInjective J f ∧ Presheaf.IsLocallySurjective J f
<VAR>b c : EReal<VAR>hb : 0 ≤ b<VAR>ha : 0 ≤ 0<GOAL>(0 + b) * c = 0 * c + b * c
<VAR>a b c : EReal<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>a_pos : 0 < a<GOAL>(a + b) * c = a * c + b * c
<VAR>a c : EReal<VAR>ha : 0 ≤ a<VAR>a_pos : 0 < a<VAR>hb : 0 ≤ 0<GOAL>(a + 0) * c = a * c + 0 * c
<VAR>a b c : EReal<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>a_pos : 0 < a<VAR>b_pos : 0 < b<GOAL>(a + b) * c = a * c + b * c
<VAR>a b c : EReal<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>a_pos : 0 < a<VAR>b_pos : 0 < b<VAR>c_neg : c < 0<GOAL>(a + b) * c = a * c + b * c
<VAR>a b : EReal<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>a_pos : 0 < a<VAR>b_pos : 0 < b<GOAL>(a + b) * 0 = a * 0 + b * 0
<VAR>a b c : EReal<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>a_pos : 0 < a<VAR>b_pos : 0 < b<VAR>c_pos : 0 < c<GOAL>(a + b) * c = a * c + b * c
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>M : Type u_2<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q : QuadraticForm R M<VAR>p : Submodule R (CliffordAlgebra Q)<VAR>n : ℕ<GOAL>Submodule.comap reverse (p ^ n) = Submodule.comap reverse p ^ n
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>a a₁ a₂ b c : G<VAR>inst✝¹ : Group G<VAR>inst✝ : Group H<VAR>f : G → H<VAR>hf : IsGroupHom f<VAR>s : Set H<VAR>hs : IsNormalSubgroup s<GOAL>1 ∈ f ⁻¹' s
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>a a₁ a₂ b c : G<VAR>inst✝¹ : Group G<VAR>inst✝ : Group H<VAR>f : G → H<VAR>hf : IsGroupHom f<VAR>s : Set H<VAR>hs : IsNormalSubgroup s<GOAL>∀ {a b : G}, a ∈ f ⁻¹' s → b ∈ f ⁻¹' s → a * b ∈ f ⁻¹' s
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>a a₁ a₂ b c : G<VAR>inst✝¹ : Group G<VAR>inst✝ : Group H<VAR>f : G → H<VAR>hf : IsGroupHom f<VAR>s : Set H<VAR>hs : IsNormalSubgroup s<GOAL>∀ {a : G}, a ∈ f ⁻¹' s → a⁻¹ ∈ f ⁻¹' s
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>a a₁ a₂ b c : G<VAR>inst✝¹ : Group G<VAR>inst✝ : Group H<VAR>f : G → H<VAR>hf : IsGroupHom f<VAR>s : Set H<VAR>hs : IsNormalSubgroup s<GOAL>∀ n ∈ f ⁻¹' s, ∀ (g : G), g * n * g⁻¹ ∈ f ⁻¹' s
<VAR>B : Type u₁<VAR>inst✝¹ : Bicategory B<VAR>C : Type u₂<VAR>inst✝ : Bicategory C<VAR>F G H I : OplaxFunctor B C<VAR>η θ : F ⟶ G<VAR>Γ : η ⟶ θ<VAR>ι : G ⟶ H<VAR>a b : B<VAR>f : a ⟶ b<GOAL>F.map f ◁ Γ.app b ▷ ι.app b ≫ (α_ (F.map f) (θ.app b) (ι.app b)).inv ≫ θ.naturality f ▷ ι.app b ≫ (α_ (θ.app a) (G.map f) (ι.app b)).hom ≫ θ.app a ◁ ι.naturality f ≫ (α_ (θ.app a) (ι.app a) (H.map f)).inv = ((α_ (F.map f) (η.app b) (ι.app b)).inv ≫ η.naturality f ▷ ι.app b ≫ (α_ (η.app a) (G.map f) (ι.app b)).hom ≫ η.app a ◁ ι.naturality f ≫ (α_ (η.app a) (ι.app a) (H.map f)).inv) ≫ Γ.app a ▷ ι.app a ▷ H.map f
<VAR>B : Type u₁<VAR>inst✝¹ : Bicategory B<VAR>C : Type u₂<VAR>inst✝ : Bicategory C<VAR>F G H I : OplaxFunctor B C<VAR>η θ : F ⟶ G<VAR>Γ : η ⟶ θ<VAR>ι : G ⟶ H<VAR>a b : B<VAR>f : a ⟶ b<GOAL>F.map f ◁ Γ.app b ▷ ι.app b ≫ (α_ (F.map f) (θ.app b) (ι.app b)).inv ≫ θ.naturality f ▷ ι.app b ≫ (α_ (θ.app a) (G.map f) (ι.app b)).hom ≫ θ.app a ◁ ι.naturality f ≫ (α_ (θ.app a) (ι.app a) (H.map f)).inv = (α_ (F.map f) (η.app b) (ι.app b)).inv ≫ η.naturality f ▷ ι.app b ≫ (α_ (η.app a) (G.map f) (ι.app b)).hom ≫ Γ.app a ▷ (G.map f ≫ ι.app b) ≫ θ.app a ◁ ι.naturality f ≫ (α_ (θ.app a) (ι.app a) (H.map f)).inv
<VAR>K : Type u₁<VAR>inst✝² : Field K<VAR>v : Valuation K ℝ≥0<VAR>O : Type u₂<VAR>inst✝¹ : CommRing O<VAR>inst✝ : Algebra O K<VAR>hv : v.Integers O<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hvp : Fact (v ↑p ≠ 1)<VAR>f : PreTilt K v O hv p<VAR>hf0 : ¬f = 0<GOAL>(val K v O hv p) f = 0 ↔ f = 0
<VAR>K : Type u₁<VAR>inst✝² : Field K<VAR>v : Valuation K ℝ≥0<VAR>O : Type u₂<VAR>inst✝¹ : CommRing O<VAR>inst✝ : Algebra O K<VAR>hv : v.Integers O<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hvp : Fact (v ↑p ≠ 1)<VAR>f : PreTilt K v O hv p<VAR>hf0 : ¬f = 0<VAR>n : ℕ<VAR>hn : (coeff (ModP K v O hv p) p n) f ≠ 0<GOAL>(val K v O hv p) f = 0 ↔ f = 0
<VAR>K : Type u₁<VAR>inst✝² : Field K<VAR>v : Valuation K ℝ≥0<VAR>O : Type u₂<VAR>inst✝¹ : CommRing O<VAR>inst✝ : Algebra O K<VAR>hv : v.Integers O<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hvp : Fact (v ↑p ≠ 1)<VAR>f : PreTilt K v O hv p<VAR>hf0 : ¬f = 0<VAR>n : ℕ<VAR>hn : (coeff (ModP K v O hv p) p n) f ≠ 0<GOAL>valAux K v O hv p f = 0 ↔ f = 0
<VAR>K : Type u₁<VAR>inst✝² : Field K<VAR>v : Valuation K ℝ≥0<VAR>O : Type u₂<VAR>inst✝¹ : CommRing O<VAR>inst✝ : Algebra O K<VAR>hv : v.Integers O<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hvp : Fact (v ↑p ≠ 1)<VAR>f : PreTilt K v O hv p<VAR>hf0 : ¬f = 0<VAR>n : ℕ<VAR>hn : (coeff (ModP K v O hv p) p n) f ≠ 0<VAR>hvf : valAux K v O hv p f = 0<GOAL>(coeff (ModP K v O hv p) p n) f = 0
<VAR>K : Type u₁<VAR>inst✝² : Field K<VAR>v : Valuation K ℝ≥0<VAR>O : Type u₂<VAR>inst✝¹ : CommRing O<VAR>inst✝ : Algebra O K<VAR>hv : v.Integers O<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hvp : Fact (v ↑p ≠ 1)<VAR>f : PreTilt K v O hv p<VAR>hf0 : ¬f = 0<VAR>n : ℕ<VAR>hn : (coeff (ModP K v O hv p) p n) f ≠ 0<VAR>hvf : ModP.preVal K v O hv p ((coeff (ModP K v O hv p) p n) f) ^ p ^ n = 0<GOAL>(coeff (ModP K v O hv p) p n) f = 0
<VAR>K : Type u₁<VAR>inst✝² : Field K<VAR>v : Valuation K ℝ≥0<VAR>O : Type u₂<VAR>inst✝¹ : CommRing O<VAR>inst✝ : Algebra O K<VAR>hv : v.Integers O<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hvp : Fact (v ↑p ≠ 1)<VAR>f : PreTilt K v O hv p<VAR>hf0 : ¬f = 0<VAR>n : ℕ<VAR>hn : (coeff (ModP K v O hv p) p n) f ≠ 0<VAR>hvf : ModP.preVal K v O hv p ((coeff (ModP K v O hv p) p n) f) = 0<GOAL>(coeff (ModP K v O hv p) p n) f = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>o : Ordinal.{u_4}<GOAL>o.pred = o ↔ ∀ (a : Ordinal.{u_4}), o ≠ succ a
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>A : Type z<VAR>a✝ b : R<VAR>n : ℕ<VAR>inst✝ : Semiring R<VAR>a : R<GOAL>derivative (C a * X) = C a
<VAR>C : Type u₁<VAR>inst✝⁶ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝⁵ : Category.{v₂, u₂} D<VAR>inst✝⁴ : HasZeroMorphisms C<VAR>inst✝³ : HasZeroMorphisms D<VAR>F : C ⥤ D<VAR>inst✝² : F.PreservesZeroMorphisms<VAR>X Y : C<VAR>inst✝¹ : HasBinaryBiproduct X Y<VAR>inst✝ : PreservesBinaryBiproduct X Y F<VAR>W : C<VAR>f : X ⟶ W<VAR>g : Y ⟶ W<GOAL>(F.mapBiprod X Y).hom ≫ desc (F.map f) (F.map g) = F.map (desc f g)
<VAR>m : ℕ<VAR>f : ℕ → ℝ := fun k => 1 / (2 * ↑k + 1) * ((1 / (2 * ↑(m + 1) + 1)) ^ 2) ^ k<GOAL>HasSum (fun k => f (k + 1)) (Real.log (stirlingSeq (m + 1)) - Real.log (stirlingSeq (m + 2)))
<VAR>m : ℕ<VAR>f : ℕ → ℝ := fun k => 1 / (2 * ↑k + 1) * ((1 / (2 * ↑(m + 1) + 1)) ^ 2) ^ k<GOAL>HasSum f (Real.log (stirlingSeq (m + 1)) - Real.log (stirlingSeq (m + 2)) + ∑ i ∈ range 1, f i)
<VAR>m : ℕ<VAR>f : ℕ → ℝ := fun k => 1 / (2 * ↑k + 1) * ((1 / (2 * ↑(m + 1) + 1)) ^ 2) ^ k<GOAL>f = fun i => (↑(m + 1) + 1 / 2) * (2 * (1 / (2 * ↑i + 1)) * (1 / (2 * (↑m + 1) + 1)) ^ (2 * i + 1))
<VAR>m : ℕ<VAR>f : ℕ → ℝ := fun k => 1 / (2 * ↑k + 1) * ((1 / (2 * ↑(m + 1) + 1)) ^ 2) ^ k<GOAL>Real.log (stirlingSeq (m + 1)) - Real.log (stirlingSeq (m + 2)) + ∑ i ∈ range 1, f i = (↑(m + 1) + 1 / 2) * Real.log (1 + (↑m + 1)⁻¹)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>H : Type u_5<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<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>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>g : F → G<VAR>f : E → F<VAR>y : F<VAR>x : E<VAR>hg : AnalyticAt 𝕜 g (f x)<VAR>hf : AnalyticAt 𝕜 f x<VAR>hy : f x = y<GOAL>AnalyticAt 𝕜 (g ∘ f) x
<VAR>S : Type u_1<VAR>inst✝ : UnitalShelf S<VAR>x y : S<GOAL>(x ◃ y) ◃ x = x ◃ y
<VAR>S : Type u_1<VAR>inst✝ : UnitalShelf S<VAR>x y : S<VAR>h : (x ◃ y) ◃ x = (x ◃ y) ◃ x ◃ 1<GOAL>(x ◃ y) ◃ x = x ◃ y
<VAR>α : Type u<VAR>β : α → Type v<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>b : β a<VAR>entries✝ : Multiset (Sigma β)<VAR>l : List (Sigma β)<VAR>hl : Multiset.NodupKeys (Quot.mk Setoid.r l)<GOAL>b ∈ lookup a { entries := Quot.mk Setoid.r l, nodupKeys := hl } ↔ ⟨a, b⟩ ∈ { entries := Quot.mk Setoid.r l, nodupKeys := hl }.entries
<VAR>S : Set Ordinal.{u}<VAR>hS : Unbounded (fun x x_1 => x < x_1) S<GOAL>range (enumOrd S) = S
<VAR>S : Set Ordinal.{u}<VAR>hS : Unbounded (fun x x_1 => x < x_1) S<GOAL>(∀ (a : Ordinal.{u}), enumOrd S a ∈ S) ∧ ∀ b ∈ S, ∃ a, enumOrd S a = b
<VAR>ι : Type u<VAR>X : Type v<VAR>inst✝⁴ : TopologicalSpace X<VAR>E : Type u_1<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : SMulWithZero ℝ E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>s✝ : Set X<VAR>f : PartitionOfUnity ι X s✝<VAR>s : Set X<VAR>ρ : PartitionOfUnity ι X s<VAR>x₀✝ x₀ : X<VAR>x✝ : ι<GOAL>x✝ ∈ ↑(ρ.finsupport x₀) ↔ x✝ ∈ support fun i => (ρ i) x₀
<VAR>R : Type u_1<VAR>inst✝² : CommSemiring R<VAR>k : Type u_2<VAR>l : Type u_3<VAR>m : Type u_4<VAR>n : Type u_5<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : Fintype n<VAR>x : R<GOAL>toMatrix' ((algebraMap R (Module.End R (n → R))) x) = (scalar n) x
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>M : Type w<VAR>M' : Type w₁<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : LieRing L<VAR>inst✝¹⁰ : LieAlgebra R L<VAR>inst✝⁹ : LieRing L'<VAR>inst✝⁸ : LieAlgebra R L'<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : LieRingModule L M'<VAR>inst✝ : LieModule R L M'<VAR>f : L →ₗ⁅R⁆ L'<VAR>I : LieIdeal R L<VAR>J : LieIdeal R L'<GOAL>map f I = ⊥ ↔ I ≤ f.ker
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>M : Type w<VAR>M' : Type w₁<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : LieRing L<VAR>inst✝¹⁰ : LieAlgebra R L<VAR>inst✝⁹ : LieRing L'<VAR>inst✝⁸ : LieAlgebra R L'<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : LieRingModule L M'<VAR>inst✝ : LieModule R L M'<VAR>f : L →ₗ⁅R⁆ L'<VAR>I : LieIdeal R L<VAR>J : LieIdeal R L'<GOAL>map f I ≤ ⊥ ↔ I ≤ f.ker
<VAR>B : Type u_1<VAR>B' : Type u_2<VAR>e : B ≃ B'<VAR>W : Type u_3<VAR>H : Type u_4<VAR>inst✝¹ : Group W<VAR>inst✝ : Group H<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>this : cs.simple = ⇑cs.mulEquiv.symm ∘ PresentedGroup.of<GOAL>Subgroup.closure (Set.range cs.simple) = ⊤
<VAR>B : Type u_1<VAR>B' : Type u_2<VAR>e : B ≃ B'<VAR>W : Type u_3<VAR>H : Type u_4<VAR>inst✝¹ : Group W<VAR>inst✝ : Group H<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>this : cs.simple = ⇑cs.mulEquiv.symm ∘ PresentedGroup.of<GOAL>cs.mulEquiv.symm.toMonoidHom.range = ⊤
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝ : (i : ι) → MeasurableSpace (α i)<VAR>s t : Set ((i : ι) → α i)<GOAL>MeasurableSpace.generateFrom (measurableCylinders α) = MeasurableSpace.pi
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝ : (i : ι) → MeasurableSpace (α i)<VAR>s t : Set ((i : ι) → α i)<GOAL>MeasurableSpace.generateFrom (measurableCylinders α) ≤ MeasurableSpace.pi
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝ : (i : ι) → MeasurableSpace (α i)<VAR>s t : Set ((i : ι) → α i)<GOAL>MeasurableSpace.pi ≤ MeasurableSpace.generateFrom (measurableCylinders α)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>e : PartialEquiv α β<VAR>e' : PartialEquiv β γ<VAR>p : β → Prop<GOAL>(∃ y ∈ e.target, p y) ↔ ∃ x ∈ e.source, p (↑e x)
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁵ : Ring K<VAR>inst✝⁴ : StrongRankCondition K<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module K V<VAR>inst✝¹ : Free K V<VAR>inst✝ : Finite K V<GOAL>finrank K V ≤ 1 ↔ ⊤.IsPrincipal
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : L.Structure M<VAR>inst✝³ : L.Structure N<VAR>inst✝² : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>n✝ l : ℕ<VAR>φ✝ ψ : L.BoundedFormula α l<VAR>θ : L.BoundedFormula α l.succ<VAR>v✝ : α → M<VAR>xs✝ : Fin l → M<VAR>inst✝¹ : L[[α]].Structure M<VAR>inst✝ : (L.lhomWithConstants α).IsExpansionOn M<VAR>n : ℕ<VAR>φ : L[[α]].BoundedFormula β n<VAR>v : β → M<VAR>xs : Fin n → M<GOAL>(constantsVarsEquiv φ).Realize (Sum.elim (fun a => ↑(L.con a)) v) xs ↔ φ.Realize v xs
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : L.Structure M<VAR>inst✝³ : L.Structure N<VAR>inst✝² : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>n✝¹ l : ℕ<VAR>φ✝ ψ : L.BoundedFormula α l<VAR>θ : L.BoundedFormula α l.succ<VAR>v✝ : α → M<VAR>xs✝¹ : Fin l → M<VAR>inst✝¹ : L[[α]].Structure M<VAR>inst✝ : (L.lhomWithConstants α).IsExpansionOn M<VAR>n✝ : ℕ<VAR>φ : L[[α]].BoundedFormula β n✝<VAR>v : β → M<VAR>xs✝ : Fin n✝ → M<VAR>n : ℕ<VAR>R : L[[α]].Relations n<VAR>xs : Fin n → M<GOAL>RelMap (((fun x => Equiv.sumEmpty (L.Relations x) ((constantsOn α).Relations x)) n) R) xs = RelMap R xs
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : L.Structure M<VAR>inst✝³ : L.Structure N<VAR>inst✝² : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>n✝¹ l : ℕ<VAR>φ✝ ψ : L.BoundedFormula α l<VAR>θ : L.BoundedFormula α l.succ<VAR>v✝ : α → M<VAR>xs✝¹ : Fin l → M<VAR>inst✝¹ : L[[α]].Structure M<VAR>inst✝ : (L.lhomWithConstants α).IsExpansionOn M<VAR>n✝ : ℕ<VAR>φ : L[[α]].BoundedFormula β n✝<VAR>v : β → M<VAR>xs✝ : Fin n✝ → M<VAR>n : ℕ<VAR>R : L[[α]].Relations n<VAR>xs : Fin n → M<GOAL>RelMap ((L.lhomWithConstants α).onRelation ((Equiv.sumEmpty (L.Relations n) ((constantsOn α).Relations n)) R)) xs = RelMap R xs
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedAddCommGroup E'<VAR>inst✝⁹ : NormedAddCommGroup E''<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g g' : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedSpace 𝕜 E'<VAR>inst✝⁴ : NormedSpace 𝕜 E''<VAR>inst✝³ : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝² : MeasurableSpace G<VAR>μ ν : Measure G<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : AddGroup G<VAR>x✝ : G<GOAL>(f ⋆[L, μ] 0) x✝ = 0 x✝
<VAR>F : Type u → Type w<VAR>G : Type v → Type u<VAR>inst✝³ : Functor F<VAR>inst✝² : Functor G<VAR>inst✝¹ : LawfulFunctor F<VAR>inst✝ : LawfulFunctor G<VAR>α β γ : Type v<VAR>x : F (G α)<GOAL>Comp.map id (mk x) = mk x
<VAR>F : Type u → Type w<VAR>G : Type v → Type u<VAR>inst✝³ : Functor F<VAR>inst✝² : Functor G<VAR>inst✝¹ : LawfulFunctor F<VAR>inst✝ : LawfulFunctor G<VAR>α β γ : Type v<VAR>x : F (G α)<GOAL>mk (mk x) = mk x
<VAR>k : Type u_1<VAR>inst✝² : Field k<VAR>K : Type u_2<VAR>inst✝¹ : Field K<VAR>F : Type u_3<VAR>inst✝ : Field F<VAR>w : InfinitePlace K<GOAL>¬w.IsReal ↔ w.IsComplex
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝¹⁸ : MeasurableSpace α<VAR>inst✝¹⁷ : MeasurableSpace α'<VAR>inst✝¹⁶ : MeasurableSpace β<VAR>inst✝¹⁵ : MeasurableSpace β'<VAR>inst✝¹⁴ : MeasurableSpace γ<VAR>μ✝ μ' : Measure α<VAR>ν✝ ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : SFinite ν✝<VAR>inst✝¹¹ : NormedSpace ℝ E<VAR>inst✝¹⁰ : SFinite μ✝<VAR>E' : Type u_7<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : NormedSpace ℝ E'<VAR>X : Type u_8<VAR>Y : Type u_9<VAR>inst✝⁷ : TopologicalSpace X<VAR>inst✝⁶ : TopologicalSpace Y<VAR>inst✝⁵ : MeasurableSpace X<VAR>inst✝⁴ : MeasurableSpace Y<VAR>inst✝³ : OpensMeasurableSpace X<VAR>inst✝² : OpensMeasurableSpace Y<VAR>f : X → Y → E<VAR>hf : Continuous (uncurry f)<VAR>h'f : HasCompactSupport (uncurry f)<VAR>μ : Measure X<VAR>ν : Measure Y<VAR>inst✝¹ : IsFiniteMeasureOnCompacts μ<VAR>inst✝ : IsFiniteMeasureOnCompacts ν<VAR>U : Set X := Prod.fst '' tsupport (uncurry f)<GOAL>∫ (x : X), ∫ (y : Y), f x y ∂ν ∂μ = ∫ (y : Y), ∫ (x : X), f x y ∂μ ∂ν
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝¹⁸ : MeasurableSpace α<VAR>inst✝¹⁷ : MeasurableSpace α'<VAR>inst✝¹⁶ : MeasurableSpace β<VAR>inst✝¹⁵ : MeasurableSpace β'<VAR>inst✝¹⁴ : MeasurableSpace γ<VAR>μ✝ μ' : Measure α<VAR>ν✝ ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : SFinite ν✝<VAR>inst✝¹¹ : NormedSpace ℝ E<VAR>inst✝¹⁰ : SFinite μ✝<VAR>E' : Type u_7<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : NormedSpace ℝ E'<VAR>X : Type u_8<VAR>Y : Type u_9<VAR>inst✝⁷ : TopologicalSpace X<VAR>inst✝⁶ : TopologicalSpace Y<VAR>inst✝⁵ : MeasurableSpace X<VAR>inst✝⁴ : MeasurableSpace Y<VAR>inst✝³ : OpensMeasurableSpace X<VAR>inst✝² : OpensMeasurableSpace Y<VAR>f : X → Y → E<VAR>hf : Continuous (uncurry f)<VAR>h'f : HasCompactSupport (uncurry f)<VAR>μ : Measure X<VAR>ν : Measure Y<VAR>inst✝¹ : IsFiniteMeasureOnCompacts μ<VAR>inst✝ : IsFiniteMeasureOnCompacts ν<VAR>U : Set X := Prod.fst '' tsupport (uncurry f)<VAR>this : Fact (μ U < ⊤)<GOAL>∫ (x : X), ∫ (y : Y), f x y ∂ν ∂μ = ∫ (y : Y), ∫ (x : X), f x y ∂μ ∂ν
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝¹⁸ : MeasurableSpace α<VAR>inst✝¹⁷ : MeasurableSpace α'<VAR>inst✝¹⁶ : MeasurableSpace β<VAR>inst✝¹⁵ : MeasurableSpace β'<VAR>inst✝¹⁴ : MeasurableSpace γ<VAR>μ✝ μ' : Measure α<VAR>ν✝ ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : SFinite ν✝<VAR>inst✝¹¹ : NormedSpace ℝ E<VAR>inst✝¹⁰ : SFinite μ✝<VAR>E' : Type u_7<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : NormedSpace ℝ E'<VAR>X : Type u_8<VAR>Y : Type u_9<VAR>inst✝⁷ : TopologicalSpace X<VAR>inst✝⁶ : TopologicalSpace Y<VAR>inst✝⁵ : MeasurableSpace X<VAR>inst✝⁴ : MeasurableSpace Y<VAR>inst✝³ : OpensMeasurableSpace X<VAR>inst✝² : OpensMeasurableSpace Y<VAR>f : X → Y → E<VAR>hf : Continuous (uncurry f)<VAR>h'f : HasCompactSupport (uncurry f)<VAR>μ : Measure X<VAR>ν : Measure Y<VAR>inst✝¹ : IsFiniteMeasureOnCompacts μ<VAR>inst✝ : IsFiniteMeasureOnCompacts ν<VAR>U : Set X := Prod.fst '' tsupport (uncurry f)<VAR>this : Fact (μ U < ⊤)<VAR>V : Set Y := Prod.snd '' tsupport (uncurry f)<GOAL>∫ (x : X), ∫ (y : Y), f x y ∂ν ∂μ = ∫ (y : Y), ∫ (x : X), f x y ∂μ ∂ν
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝¹⁸ : MeasurableSpace α<VAR>inst✝¹⁷ : MeasurableSpace α'<VAR>inst✝¹⁶ : MeasurableSpace β<VAR>inst✝¹⁵ : MeasurableSpace β'<VAR>inst✝¹⁴ : MeasurableSpace γ<VAR>μ✝ μ' : Measure α<VAR>ν✝ ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : SFinite ν✝<VAR>inst✝¹¹ : NormedSpace ℝ E<VAR>inst✝¹⁰ : SFinite μ✝<VAR>E' : Type u_7<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : NormedSpace ℝ E'<VAR>X : Type u_8<VAR>Y : Type u_9<VAR>inst✝⁷ : TopologicalSpace X<VAR>inst✝⁶ : TopologicalSpace Y<VAR>inst✝⁵ : MeasurableSpace X<VAR>inst✝⁴ : MeasurableSpace Y<VAR>inst✝³ : OpensMeasurableSpace X<VAR>inst✝² : OpensMeasurableSpace Y<VAR>f : X → Y → E<VAR>hf : Continuous (uncurry f)<VAR>h'f : HasCompactSupport (uncurry f)<VAR>μ : Measure X<VAR>ν : Measure Y<VAR>inst✝¹ : IsFiniteMeasureOnCompacts μ<VAR>inst✝ : IsFiniteMeasureOnCompacts ν<VAR>U : Set X := Prod.fst '' tsupport (uncurry f)<VAR>this✝ : Fact (μ U < ⊤)<VAR>V : Set Y := Prod.snd '' tsupport (uncurry f)<VAR>this : Fact (ν V < ⊤)<GOAL>∫ (x : X), ∫ (y : Y), f x y ∂ν ∂μ = ∫ (y : Y), ∫ (x : X), f x y ∂μ ∂ν
<VAR>α : Type u_1<VAR>p q : α → Bool<VAR>l : List α<GOAL>countP p (filter q l) = countP (fun a => decide (p a = true ∧ q a = true)) l
<VAR>𝕜 : Type u_1<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝¹⁰ : NormedAddCommGroup D<VAR>inst✝⁹ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝² : NormedAddCommGroup X<VAR>inst✝¹ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>inst✝ : Subsingleton F<GOAL>ContDiff 𝕜 n f
<VAR>𝕜 : Type u_1<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝¹⁰ : NormedAddCommGroup D<VAR>inst✝⁹ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝² : NormedAddCommGroup X<VAR>inst✝¹ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>inst✝ : Subsingleton F<GOAL>ContDiff 𝕜 n fun x => 0
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<GOAL>(deriv fun x => 1 + ε x) =ᶠ[atTop] fun z => deriv ε z
<VAR>α✝ β✝ : Type u<VAR>c : Cardinal.{?u.227041}<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>s : Set β<VAR>h : Injective f<GOAL>lift.{v, u} #↑(f ⁻¹' s) ≤ lift.{u, v} #↑s
<VAR>α✝ β✝ : Type u<VAR>c : Cardinal.{?u.227041}<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>s : Set β<VAR>h : Injective f<GOAL>Nonempty (↑(f ⁻¹' s) ↪ ↑s)
<VAR>α✝ β✝ : Type u<VAR>c : Cardinal.{?u.227041}<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>s : Set β<VAR>h : Injective f<GOAL>Injective (Subtype.coind (fun x => f ↑x) ⋯)
<VAR>α✝ β✝ : Type u<VAR>c : Cardinal.{?u.227041}<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>s : Set β<VAR>h : Injective f<GOAL>Injective fun x => f ↑x
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : MonoidalCategory C<VAR>A✝ : Mon_ C<VAR>M✝ : Mod_ A✝<VAR>A B : Mon_ C<VAR>f : A ⟶ B<VAR>M : Mod_ B<GOAL>A.one ▷ M.X ≫ f.hom ▷ M.X ≫ M.act = (λ_ M.X).hom
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : MonoidalCategory C<VAR>A✝ : Mon_ C<VAR>M✝ : Mod_ A✝<VAR>A B : Mon_ C<VAR>f : A ⟶ B<VAR>M : Mod_ B<GOAL>(A.one ≫ f.hom) ▷ M.X ≫ M.act = (λ_ M.X).hom
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : MonoidalCategory C<VAR>A✝ : Mon_ C<VAR>M✝ : Mod_ A✝<VAR>A B : Mon_ C<VAR>f : A ⟶ B<VAR>M : Mod_ B<GOAL>A.mul ▷ M.X ≫ f.hom ▷ M.X ≫ M.act = (α_ A.X A.X M.X).hom ≫ A.X ◁ (f.hom ▷ M.X ≫ M.act) ≫ f.hom ▷ M.X ≫ M.act
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : MonoidalCategory C<VAR>A✝ : Mon_ C<VAR>M✝ : Mod_ A✝<VAR>A B : Mon_ C<VAR>f : A ⟶ B<VAR>M : Mod_ B<GOAL>A.mul ▷ M.X ≫ f.hom ▷ M.X ≫ M.act = (α_ A.X A.X M.X).hom ≫ (f.hom ▷ (A.X ⊗ M.X) ≫ B.X ◁ (f.hom ▷ M.X ≫ M.act)) ≫ M.act
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : MonoidalCategory C<VAR>A✝ : Mon_ C<VAR>M✝ : Mod_ A✝<VAR>A B : Mon_ C<VAR>f : A ⟶ B<VAR>M : Mod_ B<GOAL>A.mul ▷ M.X ≫ f.hom ▷ M.X ≫ M.act = f.hom ▷ A.X ▷ M.X ≫ (α_ B.X A.X M.X).hom ≫ B.X ◁ f.hom ▷ M.X ≫ B.X ◁ M.act ≫ M.act
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : MonoidalCategory C<VAR>A✝ : Mon_ C<VAR>M✝ : Mod_ A✝<VAR>A B : Mon_ C<VAR>f : A ⟶ B<VAR>M : Mod_ B<GOAL>A.mul ▷ M.X ≫ f.hom ▷ M.X ≫ M.act = f.hom ▷ A.X ▷ M.X ≫ (α_ B.X A.X M.X).hom ≫ B.X ◁ f.hom ▷ M.X ≫ (α_ B.X B.X M.X).inv ≫ B.mul ▷ M.X ≫ M.act
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : MonoidalCategory C<VAR>A✝ : Mon_ C<VAR>M✝ : Mod_ A✝<VAR>A B : Mon_ C<VAR>f : A ⟶ B<VAR>M : Mod_ B<GOAL>A.mul ▷ M.X ≫ f.hom ▷ M.X ≫ M.act = f.hom ▷ A.X ▷ M.X ≫ (α_ B.X A.X M.X).hom ≫ (((α_ B.X A.X M.X).inv ≫ (B.X ◁ f.hom) ▷ M.X) ≫ B.mul ▷ M.X) ≫ M.act
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : MonoidalCategory C<VAR>A✝ : Mon_ C<VAR>M✝ : Mod_ A✝<VAR>A B : Mon_ C<VAR>f : A ⟶ B<VAR>M : Mod_ B<GOAL>A.mul ▷ M.X ≫ f.hom ▷ M.X ≫ M.act = f.hom ▷ A.X ▷ M.X ≫ ((B.X ◁ f.hom) ▷ M.X ≫ B.mul ▷ M.X) ≫ M.act