ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν : Measure α<VAR>s✝ t s : SignedMeasure α<VAR>μ : Measure α<VAR>inst✝ : s.HaveLebesgueDecomposition μ<GOAL>(-s).rnDeriv μ =ᶠ[ae μ] -s.rnDeriv μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν : Measure α<VAR>s✝ t s : SignedMeasure α<VAR>μ : Measure α<VAR>inst✝ : s.HaveLebesgueDecomposition μ<GOAL>μ.withDensityᵥ ((-s).rnDeriv μ) = μ.withDensityᵥ (-s.rnDeriv μ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>s s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>p✝ : Set γ<VAR>f f₁ f₂ f₃ : α → β<VAR>g g₁ g₂ : β → γ<VAR>f' f₁' f₂' : β → α<VAR>g' : γ → β<VAR>a : α<VAR>b✝ : β<VAR>p : β → Prop<VAR>hf : BijOn f s t<VAR>h : ∀ a ∈ s, p (f a)<VAR>b : β<VAR>hb : b ∈ t<GOAL>p b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>s s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>p✝ : Set γ<VAR>f f₁ f₂ f₃ : α → β<VAR>g g₁ g₂ : β → γ<VAR>f' f₁' f₂' : β → α<VAR>g' : γ → β<VAR>a✝ : α<VAR>b : β<VAR>p : β → Prop<VAR>hf : BijOn f s t<VAR>h : ∀ a ∈ s, p (f a)<VAR>a : α<VAR>ha : a ∈ s<VAR>hb : f a ∈ t<GOAL>p (f a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort uι<VAR>s✝ t u : Set α<VAR>m : MeasurableSpace α<VAR>b : β<VAR>s : Set β<VAR>x✝ : MeasurableSet s<GOAL>MeasurableSet s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort uι<VAR>s✝ t u : Set α<VAR>m : MeasurableSpace α<VAR>b : β<VAR>s : Set β<VAR>x✝ : MeasurableSet s<GOAL>MeasurableSet ((fun _a => b) ⁻¹' s)
<VAR>R : Type u<VAR>ι : Type w<VAR>s : Finset ι<VAR>inst✝ : CommSemiring R<VAR>f : ι → R[X]<VAR>t : Multiset R[X]<VAR>n : ℕ<VAR>hl : ∀ p ∈ t, p.natDegree ≤ n<GOAL>t.prod.coeff (Multiset.card t * n) = (Multiset.map (fun p => p.coeff n) t).prod
<VAR>R : Type u<VAR>ι : Type w<VAR>s : Finset ι<VAR>inst✝ : CommSemiring R<VAR>f : ι → R[X]<VAR>t : Multiset R[X]<VAR>n : ℕ<VAR>a✝ : List R[X]<VAR>hl : ∀ p ∈ ⟦a✝⟧, p.natDegree ≤ n<GOAL>(prod ⟦a✝⟧).coeff (Multiset.card ⟦a✝⟧ * n) = (Multiset.map (fun p => p.coeff n) ⟦a✝⟧).prod
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing S<VAR>inst✝⁵ : Algebra R S<VAR>x✝ : S<VAR>L : Type u_3<VAR>inst✝⁴ : CommRing L<VAR>inst✝³ : Algebra S L<VAR>inst✝² : Algebra R L<VAR>inst✝¹ : IsScalarTower R S L<VAR>inst✝ : NoZeroSMulDivisors S L<VAR>x : S<VAR>y : L<GOAL>y ∈ coeSubmodule L (conductor R x) ↔ ∀ (z : S), y * (algebraMap S L) z ∈ adjoin R {(algebraMap S L) x}
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing S<VAR>inst✝⁵ : Algebra R S<VAR>x✝ : S<VAR>L : Type u_3<VAR>inst✝⁴ : CommRing L<VAR>inst✝³ : Algebra S L<VAR>inst✝² : Algebra R L<VAR>inst✝¹ : IsScalarTower R S L<VAR>inst✝ : NoZeroSMulDivisors S L<VAR>x : S<VAR>y : L<VAR>h✝ : Subsingleton L<GOAL>y ∈ coeSubmodule L (conductor R x) ↔ ∀ (z : S), y * (algebraMap S L) z ∈ adjoin R {(algebraMap S L) x}
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing S<VAR>inst✝⁵ : Algebra R S<VAR>x✝ : S<VAR>L : Type u_3<VAR>inst✝⁴ : CommRing L<VAR>inst✝³ : Algebra S L<VAR>inst✝² : Algebra R L<VAR>inst✝¹ : IsScalarTower R S L<VAR>inst✝ : NoZeroSMulDivisors S L<VAR>x : S<VAR>y : L<VAR>h✝ : Nontrivial L<GOAL>y ∈ coeSubmodule L (conductor R x) ↔ ∀ (z : S), y * (algebraMap S L) z ∈ adjoin R {(algebraMap S L) x}
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α✝ : ι → Type u_3<VAR>inst✝⁴ : Fintype ι<VAR>m✝ : (i : ι) → OuterMeasure (α✝ i)<VAR>inst✝³ : (i : ι) → MeasurableSpace (α✝ i)<VAR>μ✝ : (i : ι) → Measure (α✝ i)<VAR>inst✝² : ∀ (i : ι), SigmaFinite (μ✝ i)<VAR>α : Type u_4<VAR>inst✝¹ : Fintype α<VAR>inst✝ : IsEmpty α<VAR>β : α → Type u_5<VAR>m : (a : α) → MeasurableSpace (β a)<VAR>μ : (a : α) → Measure (β a)<VAR>x : optParam ((a : α) → β a) fun a => isEmptyElim a<VAR>this : ∀ (a : α), SigmaFinite (μ a)<GOAL>Measure.pi μ = dirac x
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α✝ : ι → Type u_3<VAR>inst✝⁴ : Fintype ι<VAR>m✝ : (i : ι) → OuterMeasure (α✝ i)<VAR>inst✝³ : (i : ι) → MeasurableSpace (α✝ i)<VAR>μ✝ : (i : ι) → Measure (α✝ i)<VAR>inst✝² : ∀ (i : ι), SigmaFinite (μ✝ i)<VAR>α : Type u_4<VAR>inst✝¹ : Fintype α<VAR>inst✝ : IsEmpty α<VAR>β : α → Type u_5<VAR>m : (a : α) → MeasurableSpace (β a)<VAR>μ : (a : α) → Measure (β a)<VAR>x : optParam ((a : α) → β a) fun a => isEmptyElim a<VAR>this : ∀ (a : α), SigmaFinite (μ a)<VAR>s : (i : α) → Set (β i)<VAR>x✝ : ∀ (i : α), MeasurableSet (s i)<GOAL>(dirac x) (univ.pi s) = ∏ i : α, (μ i) (s i)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α✝ : ι → Type u_3<VAR>inst✝⁴ : Fintype ι<VAR>m✝ : (i : ι) → OuterMeasure (α✝ i)<VAR>inst✝³ : (i : ι) → MeasurableSpace (α✝ i)<VAR>μ✝ : (i : ι) → Measure (α✝ i)<VAR>inst✝² : ∀ (i : ι), SigmaFinite (μ✝ i)<VAR>α : Type u_4<VAR>inst✝¹ : Fintype α<VAR>inst✝ : IsEmpty α<VAR>β : α → Type u_5<VAR>m : (a : α) → MeasurableSpace (β a)<VAR>μ : (a : α) → Measure (β a)<VAR>x : optParam ((a : α) → β a) fun a => isEmptyElim a<VAR>this : ∀ (a : α), SigmaFinite (μ a)<VAR>s : (i : α) → Set (β i)<VAR>x✝ : ∀ (i : α), MeasurableSet (s i)<GOAL>x ∈ univ.pi s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f g : α → β<VAR>c c₁ c₂ x : α<VAR>inst✝¹ : Ring α<VAR>inst✝ : Ring β<VAR>h : Antiperiodic f c<VAR>n : ℤ<GOAL>f (x - ↑n * c) = ↑↑n.negOnePow * f x
<VAR>C : Type u<VAR>𝒞 : Category.{v, u} C<VAR>inst✝¹ : MonoidalCategory C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>inst✝ : IsIso f<VAR>Z : C<GOAL>f ▷ Z ≫ inv f ▷ Z = 𝟙 (X ⊗ Z)
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace ℝ E<VAR>n : ℕ<VAR>_i : Fact (finrank ℝ E = n)<VAR>o : Orientation ℝ E (Fin n)<VAR>v : OrthonormalBasis (Fin n) ℝ E<GOAL>|o.volumeForm ⇑v| = 1
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁵ : DivisionRing K<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : Module K V<VAR>V₂ : Type v'<VAR>inst✝² : AddCommGroup V₂<VAR>inst✝¹ : Module K V₂<VAR>ι : Type u_1<VAR>inst✝ : Unique ι<VAR>h✝ : finrank K V = 1<VAR>v : V<VAR>hv : v ≠ 0<VAR>b : Basis ι K V := basisUnique ι h✝<VAR>h : (b.repr v) default ≠ 0 := mt basisUnique_repr_eq_zero_iff.mp hv<GOAL>∀ (x y : V), (fun w => Finsupp.single default ((b.repr w) default / (b.repr v) default)) (x + y) = (fun w => Finsupp.single default ((b.repr w) default / (b.repr v) default)) x + (fun w => Finsupp.single default ((b.repr w) default / (b.repr v) default)) y
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁵ : DivisionRing K<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : Module K V<VAR>V₂ : Type v'<VAR>inst✝² : AddCommGroup V₂<VAR>inst✝¹ : Module K V₂<VAR>ι : Type u_1<VAR>inst✝ : Unique ι<VAR>h✝ : finrank K V = 1<VAR>v : V<VAR>hv : v ≠ 0<VAR>b : Basis ι K V := basisUnique ι h✝<VAR>h : (b.repr v) default ≠ 0 := mt basisUnique_repr_eq_zero_iff.mp hv<GOAL>∀ (m : K) (x : V), { toFun := fun w => Finsupp.single default ((b.repr w) default / (b.repr v) default), map_add' := ⋯ }.toFun (m • x) = (RingHom.id K) m • { toFun := fun w => Finsupp.single default ((b.repr w) default / (b.repr v) default), map_add' := ⋯ }.toFun x
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁵ : DivisionRing K<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : Module K V<VAR>V₂ : Type v'<VAR>inst✝² : AddCommGroup V₂<VAR>inst✝¹ : Module K V₂<VAR>ι : Type u_1<VAR>inst✝ : Unique ι<VAR>h✝ : finrank K V = 1<VAR>v : V<VAR>hv : v ≠ 0<VAR>b : Basis ι K V := basisUnique ι h✝<VAR>h : (b.repr v) default ≠ 0 := mt basisUnique_repr_eq_zero_iff.mp hv<VAR>w : V<GOAL>(fun f => f default • v) ({ toFun := fun w => Finsupp.single default ((b.repr w) default / (b.repr v) default), map_add' := ⋯, map_smul' := ⋯ }.toFun w) = w
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁵ : DivisionRing K<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : Module K V<VAR>V₂ : Type v'<VAR>inst✝² : AddCommGroup V₂<VAR>inst✝¹ : Module K V₂<VAR>ι : Type u_1<VAR>inst✝ : Unique ι<VAR>h✝ : finrank K V = 1<VAR>v : V<VAR>hv : v ≠ 0<VAR>b : Basis ι K V := basisUnique ι h✝<VAR>h : (b.repr v) default ≠ 0 := mt basisUnique_repr_eq_zero_iff.mp hv<VAR>w : V<GOAL>b.repr ((fun f => f default • v) ({ toFun := fun w => Finsupp.single default ((b.repr w) default / (b.repr v) default), map_add' := ⋯, map_smul' := ⋯ }.toFun w)) = b.repr w
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁵ : DivisionRing K<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : Module K V<VAR>V₂ : Type v'<VAR>inst✝² : AddCommGroup V₂<VAR>inst✝¹ : Module K V₂<VAR>ι : Type u_1<VAR>inst✝ : Unique ι<VAR>h✝ : finrank K V = 1<VAR>v : V<VAR>hv : v ≠ 0<VAR>b : Basis ι K V := basisUnique ι h✝<VAR>h : (b.repr v) default ≠ 0 := mt basisUnique_repr_eq_zero_iff.mp hv<VAR>w : V<GOAL>Equiv.finsuppUnique (b.repr ((fun f => f default • v) ({ toFun := fun w => Finsupp.single default ((b.repr w) default / (b.repr v) default), map_add' := ⋯, map_smul' := ⋯ }.toFun w))) = Equiv.finsuppUnique (b.repr w)
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁵ : DivisionRing K<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : Module K V<VAR>V₂ : Type v'<VAR>inst✝² : AddCommGroup V₂<VAR>inst✝¹ : Module K V₂<VAR>ι : Type u_1<VAR>inst✝ : Unique ι<VAR>h✝ : finrank K V = 1<VAR>v : V<VAR>hv : v ≠ 0<VAR>b : Basis ι K V := basisUnique ι h✝<VAR>h : (b.repr v) default ≠ 0 := mt basisUnique_repr_eq_zero_iff.mp hv<VAR>w : V<GOAL>(RingHom.id K) ((b.repr w) default / (b.repr v) default) * (b.repr v) default = (b.repr w) default
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁵ : DivisionRing K<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : Module K V<VAR>V₂ : Type v'<VAR>inst✝² : AddCommGroup V₂<VAR>inst✝¹ : Module K V₂<VAR>ι : Type u_1<VAR>inst✝ : Unique ι<VAR>h✝ : finrank K V = 1<VAR>v : V<VAR>hv : v ≠ 0<VAR>b : Basis ι K V := basisUnique ι h✝<VAR>h : (b.repr v) default ≠ 0 := mt basisUnique_repr_eq_zero_iff.mp hv<VAR>f : ι →₀ K<GOAL>({ toFun := fun w => Finsupp.single default ((b.repr w) default / (b.repr v) default), map_add' := ⋯, map_smul' := ⋯ }.toFun ((fun f => f default • v) f)) default = f default
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁵ : DivisionRing K<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : Module K V<VAR>V₂ : Type v'<VAR>inst✝² : AddCommGroup V₂<VAR>inst✝¹ : Module K V₂<VAR>ι : Type u_1<VAR>inst✝ : Unique ι<VAR>h✝ : finrank K V = 1<VAR>v : V<VAR>hv : v ≠ 0<VAR>b : Basis ι K V := basisUnique ι h✝<VAR>h : (b.repr v) default ≠ 0 := mt basisUnique_repr_eq_zero_iff.mp hv<VAR>f : ι →₀ K<GOAL>f default * (b.repr v) default / (b.repr v) default = f default
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>R : Type u_5<VAR>inst✝⁵ : MeasurableSpace X<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : MeasurableSpace Y<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedAddCommGroup F<VAR>f g : X → E<VAR>μ : Measure X<VAR>s : Set X<GOAL>LocallyIntegrableOn f univ μ ↔ LocallyIntegrable f μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>R : Type u_5<VAR>inst✝⁵ : MeasurableSpace X<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : MeasurableSpace Y<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedAddCommGroup F<VAR>f g : X → E<VAR>μ : Measure X<VAR>s : Set X<GOAL>(∀ (x : X), IntegrableAtFilter f (𝓝 x) μ) ↔ LocallyIntegrable f μ
<VAR>α : Type u_1<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>h : ENNReal.ofReal a.toReal = a<GOAL>ENNReal.ofReal a.toReal ≠ ⊤
<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>β : Type u_7<VAR>inst✝ : MeasurableSpace β<VAR>b : β<VAR>f : α → β<VAR>s : Set α<VAR>f_mble : NullMeasurable f (μ.restrict s)<VAR>hs : f =ᶠ[ae (μ.restrict sᶜ)] fun x => b<VAR>t : Set β<VAR>t_mble : MeasurableSet t<VAR>ht : b ∉ t<GOAL>μ (f ⁻¹' t) = (μ.restrict s) (f ⁻¹' 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>β : Type u_7<VAR>inst✝ : MeasurableSpace β<VAR>b : β<VAR>f : α → β<VAR>s : Set α<VAR>f_mble : NullMeasurable f (μ.restrict s)<VAR>hs : f =ᶠ[ae (μ.restrict sᶜ)] fun x => b<VAR>t : Set β<VAR>t_mble : MeasurableSet t<VAR>ht : b ∉ t<GOAL>μ (f ⁻¹' t) = μ (f ⁻¹' t ∩ 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>β : Type u_7<VAR>inst✝ : MeasurableSpace β<VAR>b : β<VAR>f : α → β<VAR>s : Set α<VAR>f_mble : NullMeasurable f (μ.restrict s)<VAR>hs : μ ({a | ¬f a = b} ∩ sᶜ) = 0<VAR>t : Set β<VAR>t_mble : MeasurableSet t<VAR>ht : b ∉ t<GOAL>μ (f ⁻¹' t) = μ (f ⁻¹' t ∩ 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>β : Type u_7<VAR>inst✝ : MeasurableSpace β<VAR>b : β<VAR>f : α → β<VAR>s : Set α<VAR>f_mble : NullMeasurable f (μ.restrict s)<VAR>hs : (μ.restrict sᶜ) {a | ¬f a = b} = 0<VAR>t : Set β<VAR>t_mble : MeasurableSet t<VAR>ht : b ∉ t<GOAL>NullMeasurableSet {a | ¬f a = b} (μ.restrict sᶜ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>inst✝ : MeasurableSpace δ<VAR>μ : Measure α<VAR>ν : Measure β<VAR>f✝ : α → γ<VAR>g✝ : β → γ<VAR>f : α → ℝ<VAR>g : β → ℝ<VAR>h : IdentDistrib f g μ ν<GOAL>evariance f μ = evariance g ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>inst✝ : MeasurableSpace δ<VAR>μ : Measure α<VAR>ν : Measure β<VAR>f✝ : α → γ<VAR>g✝ : β → γ<VAR>f : α → ℝ<VAR>g : β → ℝ<VAR>h : IdentDistrib f g μ ν<GOAL>evariance g ν = ∫⁻ (x : β), ↑‖g x - ∫ (x : α), f x ∂μ‖₊ ^ 2 ∂ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>inst✝ : MeasurableSpace δ<VAR>μ : Measure α<VAR>ν : Measure β<VAR>f✝ : α → γ<VAR>g✝ : β → γ<VAR>f : α → ℝ<VAR>g : β → ℝ<VAR>h : IdentDistrib f g μ ν<GOAL>evariance g ν = ∫⁻ (x : β), ↑‖g x - ∫ (x : β), g x ∂ν‖₊ ^ 2 ∂ν
<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>F : Type u_7<VAR>G : Type u_8<VAR>inst✝³ : SeminormedGroup E<VAR>inst✝² : SeminormedGroup F<VAR>inst✝¹ : SeminormedGroup G<VAR>s : Set E<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>inst✝ : FunLike 𝓕 E F<GOAL>comap norm (𝓝 0) = 𝓝 1
<VAR>J : Type w<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroMorphisms C<VAR>D : Type uD<VAR>inst✝² : Category.{uD', uD} D<VAR>inst✝¹ : HasZeroMorphisms D<VAR>P Q X Y : C<VAR>inst✝ : HasBinaryBiproduct X Y<VAR>hY : IsZero Y<GOAL>biprod.fst ≫ biprod.inl = 𝟙 (X ⊞ Y)
<VAR>J : Type w<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroMorphisms C<VAR>D : Type uD<VAR>inst✝² : Category.{uD', uD} D<VAR>inst✝¹ : HasZeroMorphisms D<VAR>P Q X Y : C<VAR>inst✝ : HasBinaryBiproduct X Y<VAR>hY : IsZero Y<GOAL>0 = biprod.snd
<VAR>V : Type u<VAR>G : SimpleGraph V<GOAL>G.IsAcyclic ↔ ∀ ⦃e : Sym2 V⦄, e ∈ G.edgeSet → G.IsBridge e
<VAR>α✝ : Type u_1<VAR>M : Type u_2<VAR>ι : Type u_3<VAR>α : Type u_4<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : MeasurableSpace M<VAR>inst✝ : MeasurableMul₂ M<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>f : ι → α → M<VAR>l✝ : Multiset (α → M)<VAR>l : List (α → M)<VAR>hl : ∀ f ∈ Quot.mk Setoid.r l, AEMeasurable f μ<GOAL>AEMeasurable (prod (Quot.mk Setoid.r l)) μ
<VAR>M✝ : Type u_1<VAR>inst✝⁶ : Monoid M✝<VAR>inst✝⁵ : MeasurableSpace M✝<VAR>M : Type u_2<VAR>inst✝⁴ : CommMonoid M<VAR>inst✝³ : MeasurableSpace M<VAR>inst✝² : MeasurableMul₂ M<VAR>μ ν : Measure M<VAR>inst✝¹ : SFinite μ<VAR>inst✝ : SFinite ν<GOAL>map (fun x => x.1 * x.2) (μ.prod ν) = map (fun x => x.1 * x.2) (ν.prod μ)
<VAR>M✝ : Type u_1<VAR>inst✝⁶ : Monoid M✝<VAR>inst✝⁵ : MeasurableSpace M✝<VAR>M : Type u_2<VAR>inst✝⁴ : CommMonoid M<VAR>inst✝³ : MeasurableSpace M<VAR>inst✝² : MeasurableMul₂ M<VAR>μ ν : Measure M<VAR>inst✝¹ : SFinite μ<VAR>inst✝ : SFinite ν<GOAL>map ((fun x => x.1 * x.2) ∘ Prod.swap) (ν.prod μ) = map (fun x => x.1 * x.2) (ν.prod μ)
<VAR>M✝ : Type u_1<VAR>inst✝⁶ : Monoid M✝<VAR>inst✝⁵ : MeasurableSpace M✝<VAR>M : Type u_2<VAR>inst✝⁴ : CommMonoid M<VAR>inst✝³ : MeasurableSpace M<VAR>inst✝² : MeasurableMul₂ M<VAR>μ ν : Measure M<VAR>inst✝¹ : SFinite μ<VAR>inst✝ : SFinite ν<GOAL>Measurable Prod.swap
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} C<VAR>inst✝⁴ : Preadditive C<VAR>inst✝³ : MonoidalCategory C<VAR>inst✝² : MonoidalPreadditive C<VAR>inst✝¹ : HasFiniteBiproducts C<VAR>J : Type<VAR>inst✝ : Fintype J<VAR>X : C<VAR>f : J → C<VAR>j : J<GOAL>X ◁ biproduct.ι f j ≫ (leftDistributor X f).hom = biproduct.ι (fun j => X ⊗ f j) j
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>I I' : FractionalIdeal R⁰ K<VAR>hI : I ≠ 0<VAR>hI' : I' ≠ 0<GOAL>count K v (I * I') = count K v I + count K v I'
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>I I' : FractionalIdeal R⁰ K<VAR>hI : I ≠ 0<VAR>hI' : I' ≠ 0<VAR>hv : Irreducible (Associates.mk v.asIdeal)<GOAL>count K v (I * I') = count K v I + count K v I'
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>I I' : FractionalIdeal R⁰ K<VAR>hI : I ≠ 0<VAR>hI' : I' ≠ 0<VAR>hv : Irreducible (Associates.mk v.asIdeal)<VAR>a : R<VAR>J : Ideal R<VAR>ha : a ≠ 0<VAR>haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J<GOAL>count K v (I * I') = count K v I + count K v I'
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>I I' : FractionalIdeal R⁰ K<VAR>hI : I ≠ 0<VAR>hI' : I' ≠ 0<VAR>hv : Irreducible (Associates.mk v.asIdeal)<VAR>a : R<VAR>J : Ideal R<VAR>ha : a ≠ 0<VAR>haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J<VAR>ha_ne_zero : Associates.mk (Ideal.span {a}) ≠ 0<GOAL>count K v (I * I') = count K v I + count K v I'
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>I I' : FractionalIdeal R⁰ K<VAR>hI : I ≠ 0<VAR>hI' : I' ≠ 0<VAR>hv : Irreducible (Associates.mk v.asIdeal)<VAR>a : R<VAR>J : Ideal R<VAR>ha : a ≠ 0<VAR>haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J<VAR>ha_ne_zero : Associates.mk (Ideal.span {a}) ≠ 0<VAR>hJ_ne_zero : Associates.mk J ≠ 0<GOAL>count K v (I * I') = count K v I + count K v I'
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>I I' : FractionalIdeal R⁰ K<VAR>hI : I ≠ 0<VAR>hI' : I' ≠ 0<VAR>hv : Irreducible (Associates.mk v.asIdeal)<VAR>a : R<VAR>J : Ideal R<VAR>ha : a ≠ 0<VAR>haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J<VAR>ha_ne_zero : Associates.mk (Ideal.span {a}) ≠ 0<VAR>hJ_ne_zero : Associates.mk J ≠ 0<VAR>a' : R<VAR>J' : Ideal R<VAR>ha' : a' ≠ 0<VAR>haJ' : I' = spanSingleton R⁰ ((algebraMap R K) a')⁻¹ * ↑J'<GOAL>count K v (I * I') = count K v I + count K v I'
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>I I' : FractionalIdeal R⁰ K<VAR>hI : I ≠ 0<VAR>hI' : I' ≠ 0<VAR>hv : Irreducible (Associates.mk v.asIdeal)<VAR>a : R<VAR>J : Ideal R<VAR>ha : a ≠ 0<VAR>haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J<VAR>ha_ne_zero : Associates.mk (Ideal.span {a}) ≠ 0<VAR>hJ_ne_zero : Associates.mk J ≠ 0<VAR>a' : R<VAR>J' : Ideal R<VAR>ha' : a' ≠ 0<VAR>haJ' : I' = spanSingleton R⁰ ((algebraMap R K) a')⁻¹ * ↑J'<VAR>ha'_ne_zero : Associates.mk (Ideal.span {a'}) ≠ 0<GOAL>count K v (I * I') = count K v I + count K v I'
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>I I' : FractionalIdeal R⁰ K<VAR>hI : I ≠ 0<VAR>hI' : I' ≠ 0<VAR>hv : Irreducible (Associates.mk v.asIdeal)<VAR>a : R<VAR>J : Ideal R<VAR>ha : a ≠ 0<VAR>haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J<VAR>ha_ne_zero : Associates.mk (Ideal.span {a}) ≠ 0<VAR>hJ_ne_zero : Associates.mk J ≠ 0<VAR>a' : R<VAR>J' : Ideal R<VAR>ha' : a' ≠ 0<VAR>haJ' : I' = spanSingleton R⁰ ((algebraMap R K) a')⁻¹ * ↑J'<VAR>ha'_ne_zero : Associates.mk (Ideal.span {a'}) ≠ 0<VAR>hJ'_ne_zero : Associates.mk J' ≠ 0<GOAL>count K v (I * I') = count K v I + count K v I'
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>I I' : FractionalIdeal R⁰ K<VAR>hI : I ≠ 0<VAR>hI' : I' ≠ 0<VAR>hv : Irreducible (Associates.mk v.asIdeal)<VAR>a : R<VAR>J : Ideal R<VAR>ha : a ≠ 0<VAR>haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J<VAR>ha_ne_zero : Associates.mk (Ideal.span {a}) ≠ 0<VAR>hJ_ne_zero : Associates.mk J ≠ 0<VAR>a' : R<VAR>J' : Ideal R<VAR>ha' : a' ≠ 0<VAR>haJ' : I' = spanSingleton R⁰ ((algebraMap R K) a')⁻¹ * ↑J'<VAR>ha'_ne_zero : Associates.mk (Ideal.span {a'}) ≠ 0<VAR>hJ'_ne_zero : Associates.mk J' ≠ 0<VAR>h_prod : I * I' = spanSingleton R⁰ ((algebraMap R K) (a * a'))⁻¹ * ↑(J * J')<GOAL>count K v (I * I') = count K v I + count K v I'
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>I I' : FractionalIdeal R⁰ K<VAR>hI : I ≠ 0<VAR>hI' : I' ≠ 0<VAR>hv : Irreducible (Associates.mk v.asIdeal)<VAR>a : R<VAR>J : Ideal R<VAR>ha : a ≠ 0<VAR>haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J<VAR>ha_ne_zero : Associates.mk (Ideal.span {a}) ≠ 0<VAR>hJ_ne_zero : Associates.mk J ≠ 0<VAR>a' : R<VAR>J' : Ideal R<VAR>ha' : a' ≠ 0<VAR>haJ' : I' = spanSingleton R⁰ ((algebraMap R K) a')⁻¹ * ↑J'<VAR>ha'_ne_zero : Associates.mk (Ideal.span {a'}) ≠ 0<VAR>hJ'_ne_zero : Associates.mk J' ≠ 0<VAR>h_prod : I * I' = spanSingleton R⁰ ((algebraMap R K) (a * a'))⁻¹ * ↑(J * J')<GOAL>↑((Associates.mk v.asIdeal).count (Associates.mk J).factors + (Associates.mk v.asIdeal).count (Associates.mk J').factors) - ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors + (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a'})).factors) = ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) - ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors) + (↑((Associates.mk v.asIdeal).count (Associates.mk J').factors) - ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a'})).factors))
<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>h : 0 < b<GOAL>b⁻¹ * a < c ↔ a < b * c
<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>h : 0 < b<GOAL>a / b < c ↔ a < b * c
<VAR>K : Type u_1<VAR>inst✝¹ : DecidableEq K<VAR>Γ : K → Type u_2<VAR>Λ : Type u_3<VAR>σ : Type u_4<VAR>inst✝ : Inhabited Λ<VAR>M : Λ → Stmt₂<VAR>S : Finset Λ<VAR>q : Stmt₂<VAR>ss : Supports M S<GOAL>some q ∈ stmts M S → SupportsStmt S q
<VAR>K : Type u_1<VAR>inst✝¹ : DecidableEq K<VAR>Γ : K → Type u_2<VAR>Λ : Type u_3<VAR>σ : Type u_4<VAR>inst✝ : Inhabited Λ<VAR>M : Λ → Stmt₂<VAR>S : Finset Λ<VAR>q : Stmt₂<VAR>ss : Supports M S<GOAL>∀ x ∈ S, q ∈ stmts₁ (M x) → SupportsStmt S q