ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>f : ↥(Lp E 1 μ)<GOAL>integral f = ∫ (a : α), ↑↑f a ∂μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>f : ↥(Lp E 1 μ)<GOAL>integralCLM f = setToFun μ (weightedSMul μ) ⋯ ↑↑f
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>X : Type u_3<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph W<VAR>u v✝ v : V<GOAL>induce {v} G = ⊤
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>X : Type u_3<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph W<VAR>u v✝ v : V<GOAL>⊤ ≤ induce {v} G
<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>F : Cᵒᵖ ⥤ Type w<VAR>I : Type u_1<VAR>Y : I → C<VAR>x : FamilyOfElementsOnObjects F Y<VAR>hx : x.IsCompatible<VAR>X Y₁ Y₂ Z : C<VAR>g₁ : Z ⟶ Y₁<VAR>g₂ : Z ⟶ Y₂<VAR>f₁ : Y₁ ⟶ X<VAR>f₂ : Y₂ ⟶ X<VAR>i₁ : I<VAR>φ₁ : Y₁ ⟶ Y i₁<VAR>i₂ : I<VAR>φ₂ : Y₂ ⟶ Y i₂<VAR>a✝ : g₁ ≫ f₁ = g₂ ≫ f₂<GOAL>F.map g₁.op (x.familyOfElements X f₁ ⋯) = F.map g₂.op (x.familyOfElements X f₂ ⋯)
<VAR>α : Type u_1<VAR>inst✝ : OrderedAddCommGroup α<VAR>a b c : α<GOAL>(fun x => x - a) '' Iio b = Iio (b - a)
<VAR>X✝ : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>inst✝² : TopologicalSpace X✝<VAR>X : Type u_5<VAR>inst✝¹ : TopologicalSpace X<VAR>U : Set X<VAR>inst✝ : (x : X) → Decidable (x ∈ U)<VAR>hU : IsClopen U<VAR>x✝ : X<GOAL>x✝ ∈ ⇑(ofIsClopen hU) ⁻¹' {1} ↔ x✝ ∈ Uᶜ
<VAR>α : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>W : Type u_4<VAR>Q : Type u_5<VAR>inst✝⁸ : SeminormedAddCommGroup V<VAR>inst✝⁷ : PseudoMetricSpace P<VAR>inst✝⁶ : NormedAddTorsor V P<VAR>inst✝⁵ : NormedAddCommGroup W<VAR>inst✝⁴ : MetricSpace Q<VAR>inst✝³ : NormedAddTorsor W Q<VAR>𝕜 : Type u_6<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : NormedSpace 𝕜 V<VAR>inst✝ : NormedSpace 𝕜 W<VAR>p₁ p₂ : P<VAR>c : 𝕜<GOAL>dist ((lineMap p₁ p₂) c) p₂ = ‖1 - c‖ * dist p₁ p₂
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝¹⁰ : _root_.RCLike 𝕜<VAR>E : Type u_4<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : InnerProductSpace 𝕜 E<VAR>E' : Type u_5<VAR>inst✝⁷ : NormedAddCommGroup E'<VAR>inst✝⁶ : InnerProductSpace 𝕜 E'<VAR>F : Type u_6<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : InnerProductSpace ℝ F<VAR>F' : Type u_7<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : InnerProductSpace ℝ F'<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>b : OrthonormalBasis ι 𝕜 E<VAR>i : ι<GOAL>b.repr (b i) = EuclideanSpace.single i 1
<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>s t : ℝ<GOAL>IndepFun (fun ω => rexp (s * X ω)) (fun ω => rexp (t * Y ω)) μ
<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>s t : ℝ<VAR>h_meas : ∀ (t : ℝ), Measurable fun x => rexp (t * x)<GOAL>IndepFun (fun ω => rexp (s * X ω)) (fun ω => rexp (t * Y ω)) μ
<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>s t : ℝ<VAR>h_meas : ∀ (t : ℝ), Measurable fun x => rexp (t * x)<GOAL>IndepFun ((fun x => rexp (s * x)) ∘ X) ((fun x => rexp (t * x)) ∘ Y) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<GOAL>s.encard = ⊤ ↔ s.Infinite
<VAR>R : Type u_1<VAR>inst✝³ : NonAssocRing R<VAR>inst✝² : Pow R ℕ<VAR>inst✝¹ : BinomialRing R<VAR>inst✝ : NatPowAssoc R<VAR>r : R<GOAL>choose r 1 = r
<VAR>n : ℕ<GOAL>decodeNat (encodeNat n) = n
<VAR>n : ℕ<GOAL>decodeNat (encodeNat n) = ↑↑n
<VAR>A : Set ℕ<VAR>inst✝¹ : DecidablePred fun x => x ∈ A<VAR>B : Set ℕ<VAR>inst✝ : DecidablePred fun x => x ∈ B<VAR>h : A ⊆ B<VAR>x✝ : { n // 0 < n }<GOAL>filter (fun x => x ∈ A) (Ioc 0 ↑x✝) ⊆ filter (fun x => x ∈ B) (Ioc 0 ↑x✝)
<VAR>ι : Sort uι<VAR>R : Type u<VAR>inst✝² : CommSemiring R<VAR>A : Type v<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>S T : Set A<VAR>M N P Q : Submodule R A<VAR>m n✝ : A<VAR>n : ℕ<GOAL>(Nat.castAddMonoidHom A) n ∈ toAddSubmonoid 1
<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<GOAL>↑(f.extend I) '' (f.source ∩ f'.source) = ((f.extend I).symm ≫ f'.extend I).source
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → α<VAR>m n : ℕ<VAR>x : α<GOAL>f^[m + n] x = f^[m] (f^[n] x)
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → α<VAR>m n : ℕ<VAR>x : α<GOAL>(f^[m] ∘ f^[n]) x = f^[m] (f^[n] x)
<VAR>Ω : Type u_1<VAR>inst✝⁶ : TopologicalSpace Ω<VAR>inst✝⁵ : MeasurableSpace Ω<VAR>inst✝⁴ : OpensMeasurableSpace Ω<VAR>ι : Type u_2<VAR>L : Filter ι<VAR>inst✝³ : L.IsCountablyGenerated<VAR>inst✝² : TopologicalSpace Ω<VAR>inst✝¹ : OpensMeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<VAR>c : ℝ≥0<VAR>E : Set Ω<VAR>E_mble : MeasurableSet E<VAR>fs : ι → Ω →ᵇ ℝ≥0<VAR>fs_bdd : ∀ᶠ (i : ι) in L, ∀ᵐ (ω : Ω) ∂μ, (fs i) ω ≤ c<VAR>fs_lim : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun i => (fs i) ω) L (𝓝 (E.indicator (fun x => 1) ω))<GOAL>Tendsto (fun n => ∫⁻ (ω : Ω), ↑((fs n) ω) ∂μ) L (𝓝 (μ E))
<VAR>Ω : Type u_1<VAR>inst✝⁶ : TopologicalSpace Ω<VAR>inst✝⁵ : MeasurableSpace Ω<VAR>inst✝⁴ : OpensMeasurableSpace Ω<VAR>ι : Type u_2<VAR>L : Filter ι<VAR>inst✝³ : L.IsCountablyGenerated<VAR>inst✝² : TopologicalSpace Ω<VAR>inst✝¹ : OpensMeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<VAR>c : ℝ≥0<VAR>E : Set Ω<VAR>E_mble : MeasurableSet E<VAR>fs : ι → Ω →ᵇ ℝ≥0<VAR>fs_bdd : ∀ᶠ (i : ι) in L, ∀ᵐ (ω : Ω) ∂μ, (fs i) ω ≤ c<VAR>fs_lim : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun i => (fs i) ω) L (𝓝 (E.indicator (fun x => 1) ω))<GOAL>μ E = ∫⁻ (ω : Ω), ↑(E.indicator (fun x => 1) ω) ∂μ
<VAR>Ω : Type u_1<VAR>inst✝⁶ : TopologicalSpace Ω<VAR>inst✝⁵ : MeasurableSpace Ω<VAR>inst✝⁴ : OpensMeasurableSpace Ω<VAR>ι : Type u_2<VAR>L : Filter ι<VAR>inst✝³ : L.IsCountablyGenerated<VAR>inst✝² : TopologicalSpace Ω<VAR>inst✝¹ : OpensMeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<VAR>c : ℝ≥0<VAR>E : Set Ω<VAR>E_mble : MeasurableSet E<VAR>fs : ι → Ω →ᵇ ℝ≥0<VAR>fs_bdd : ∀ᶠ (i : ι) in L, ∀ᵐ (ω : Ω) ∂μ, (fs i) ω ≤ c<VAR>fs_lim : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun i => (fs i) ω) L (𝓝 (E.indicator (fun x => 1) ω))<VAR>aux : ∀ (ω : Ω), E.indicator (fun x => 1) ω = ↑(E.indicator (fun x => 1) ω)<GOAL>μ E = ∫⁻ (ω : Ω), ↑(E.indicator (fun x => 1) ω) ∂μ
<VAR>Ω : Type u_1<VAR>inst✝⁶ : TopologicalSpace Ω<VAR>inst✝⁵ : MeasurableSpace Ω<VAR>inst✝⁴ : OpensMeasurableSpace Ω<VAR>ι : Type u_2<VAR>L : Filter ι<VAR>inst✝³ : L.IsCountablyGenerated<VAR>inst✝² : TopologicalSpace Ω<VAR>inst✝¹ : OpensMeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<VAR>c : ℝ≥0<VAR>E : Set Ω<VAR>E_mble : MeasurableSet E<VAR>fs : ι → Ω →ᵇ ℝ≥0<VAR>fs_bdd : ∀ᶠ (i : ι) in L, ∀ᵐ (ω : Ω) ∂μ, (fs i) ω ≤ c<VAR>fs_lim : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun i => (fs i) ω) L (𝓝 (E.indicator (fun x => 1) ω))<VAR>aux : ∀ (ω : Ω), E.indicator (fun x => 1) ω = ↑(E.indicator (fun x => 1) ω)<GOAL>μ E = ∫⁻ (x : Ω) in E, 1 ∂μ
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>s t : Set (PrimeSpectrum R)<VAR>ht : IsClosed t<VAR>h : vanishingIdeal t ≤ vanishingIdeal s<GOAL>s ⊆ t
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>s t : Set (PrimeSpectrum R)<VAR>ht : IsClosed t<VAR>h : vanishingIdeal t ≤ vanishingIdeal s<GOAL>closure s ⊆ closure t
<VAR>α✝ : Type u_1<VAR>σ : Type u_2<VAR>inst✝⁴ : Primcodable α✝<VAR>inst✝³ : Primcodable σ<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝² : Primcodable α<VAR>inst✝¹ : Primcodable β<VAR>inst✝ : Primcodable γ<VAR>f : α → β<VAR>g : α → γ<VAR>hf : Primrec f<VAR>hg : Primrec g<VAR>n : ℕ<GOAL>(Nat.casesOn (encode (decode n)) 0 fun n => (Nat.pair (encode (Option.map f (decode n))).pred (encode (Option.map g (decode n))).pred).succ) = encode (Option.map (fun a => (f a, g a)) (decode n))
<VAR>α : Type u_1<VAR>r c : ℝ<VAR>l : Filter α<VAR>f g : α → ℝ<VAR>h : IsBigOWith c l f g<VAR>hc : 0 ≤ c<VAR>hr : 0 ≤ r<VAR>hg : 0 ≤ᶠ[l] g<GOAL>∀ᶠ (x : α) in l, ‖f x ^ r‖ ≤ c ^ r * ‖g x ^ r‖
<VAR>α : Type u_1<VAR>r c : ℝ<VAR>l : Filter α<VAR>f g : α → ℝ<VAR>h : IsBigOWith c l f g<VAR>hc : 0 ≤ c<VAR>hr : 0 ≤ r<VAR>hg : 0 ≤ᶠ[l] g<VAR>x : α<VAR>hgx : 0 x ≤ g x<VAR>hx : ‖f x‖ ≤ c * ‖g x‖<GOAL>‖f x ^ r‖ ≤ c ^ r * ‖g x ^ r‖
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>m✝ m : OuterMeasure α<VAR>s : Set α<VAR>h : m.trim s = 0<GOAL>∃ t, s ⊆ t ∧ MeasurableSet t ∧ m t = 0
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>m✝ m : OuterMeasure α<VAR>s : Set α<VAR>h : m.trim s = 0<VAR>t : Set α<VAR>hst : s ⊆ t<VAR>ht : MeasurableSet t<VAR>hm : m t = m.trim s<GOAL>∃ t, s ⊆ t ∧ MeasurableSet t ∧ m t = 0
<VAR>f : ℝ → ℝ<VAR>x✝ : ℝ<VAR>n✝ : ℕ<VAR>x : ℝ<VAR>n : ℕ<GOAL>logGammaSeq (x + 1) n = logGammaSeq x (n + 1) + log x - (x + 1) * (log (↑n + 1) - log ↑n)
<VAR>f : ℝ → ℝ<VAR>x✝ : ℝ<VAR>n✝ : ℕ<VAR>x : ℝ<VAR>n : ℕ<GOAL>(x + 1) * log ↑n + log ↑n ! - ∑ m ∈ Finset.range (n + 1), log (x + 1 + ↑m) = x * log ↑(n + 1) + log ↑((n + 1) * n !) - ∑ m ∈ Finset.range (n + 1 + 1), log (x + ↑m) + log x - (x + 1) * (log (↑n + 1) - log ↑n)
<VAR>f : ℝ → ℝ<VAR>x✝ : ℝ<VAR>n✝ : ℕ<VAR>x : ℝ<VAR>n : ℕ<GOAL>(x + 1) * log ↑n + log ↑n ! - ∑ m ∈ Finset.range (n + 1), log (x + 1 + ↑m) = x * log ↑(n + 1) + log ↑((n + 1) * n !) - (∑ k ∈ Finset.range (n + 1), log (x + ↑(k + 1)) + log x) + log x - (x + 1) * (log (↑n + 1) - log ↑n)
<VAR>f : ℝ → ℝ<VAR>x✝ : ℝ<VAR>n✝ : ℕ<VAR>x : ℝ<VAR>n : ℕ<GOAL>(x + 1) * log ↑n + log ↑n ! - ∑ m ∈ Finset.range (n + 1), log (x + 1 + ↑m) = x * log ↑(n + 1) + (log ↑(n + 1) + log ↑n !) - (∑ k ∈ Finset.range (n + 1), log (x + ↑(k + 1)) + log x) + log x - (x + 1) * (log (↑n + 1) - log ↑n)
<VAR>f : ℝ → ℝ<VAR>x✝ : ℝ<VAR>n✝ : ℕ<VAR>x : ℝ<VAR>n : ℕ<GOAL>↑(n + 1) ≠ 0
<VAR>f : ℝ → ℝ<VAR>x✝ : ℝ<VAR>n✝ : ℕ<VAR>x : ℝ<VAR>n : ℕ<GOAL>↑n ! ≠ 0
<VAR>f : ℝ → ℝ<VAR>x✝ : ℝ<VAR>n✝ : ℕ<VAR>x : ℝ<VAR>n : ℕ<VAR>this : ∑ m ∈ Finset.range (n + 1), log (x + 1 + ↑m) = ∑ k ∈ Finset.range (n + 1), log (x + ↑(k + 1))<GOAL>(x + 1) * log ↑n + log ↑n ! - ∑ m ∈ Finset.range (n + 1), log (x + 1 + ↑m) = x * log ↑(n + 1) + (log ↑(n + 1) + log ↑n !) - (∑ k ∈ Finset.range (n + 1), log (x + ↑(k + 1)) + log x) + log x - (x + 1) * (log (↑n + 1) - log ↑n)
<VAR>f : ℝ → ℝ<VAR>x✝ : ℝ<VAR>n✝ : ℕ<VAR>x : ℝ<VAR>n : ℕ<VAR>this : ∑ m ∈ Finset.range (n + 1), log (x + 1 + ↑m) = ∑ k ∈ Finset.range (n + 1), log (x + ↑(k + 1))<GOAL>(x + 1) * log ↑n + log ↑n ! - ∑ m ∈ Finset.range (n + 1), log (x + 1 + ↑m) = x * log (↑n + 1) + (log (↑n + 1) + log ↑n !) - (∑ m ∈ Finset.range (n + 1), log (x + 1 + ↑m) + log x) + log x - (x + 1) * (log (↑n + 1) - log ↑n)
<VAR>α : Type u_1<VAR>s : Finset α<VAR>f✝ : α → ℕ<VAR>a✝ b : α<VAR>n : ℕ<VAR>a : α<VAR>f : α → ℕ<GOAL>multinomial {a} f = 1
<VAR>α : Type u_1<VAR>s : Finset α<VAR>f✝ : α → ℕ<VAR>a✝ b : α<VAR>n : ℕ<VAR>a : α<VAR>f : α → ℕ<GOAL>(f a + ∑ i ∈ ∅, f i).choose (f a) * multinomial ∅ f = 1
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : Projective R<VAR>P✝ : Fin 3 → R<VAR>u✝ u : Rˣ<VAR>P : Fin 3 → R<VAR>h : W.Equation P<GOAL>W.Equation (u • P)
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : Projective R<VAR>P✝ : Fin 3 → R<VAR>u✝ u : Rˣ<VAR>P : Fin 3 → R<VAR>h : P 1 ^ 2 * P 2 + W.a₁ * P 0 * P 1 * P 2 + W.a₃ * P 1 * P 2 ^ 2 = P 0 ^ 3 + W.a₂ * P 0 ^ 2 * P 2 + W.a₄ * P 0 * P 2 ^ 2 + W.a₆ * P 2 ^ 3<GOAL>(u • P) 1 ^ 2 * (u • P) 2 + W.a₁ * (u • P) 0 * (u • P) 1 * (u • P) 2 + W.a₃ * (u • P) 1 * (u • P) 2 ^ 2 = (u • P) 0 ^ 3 + W.a₂ * (u • P) 0 ^ 2 * (u • P) 2 + W.a₄ * (u • P) 0 * (u • P) 2 ^ 2 + W.a₆ * (u • P) 2 ^ 3
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : Projective R<VAR>P : Fin 3 → R<VAR>u : Rˣ<VAR>this : ∀ (u : Rˣ) {P : Fin 3 → R}, W.Equation P → W.Equation (u • P)<VAR>h : W.Equation (u • P)<GOAL>P = u⁻¹ • u • P
<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>I : Ideal R<VAR>inst✝³ : IsDomain R<VAR>inst✝² : IsIntegrallyClosed R<VAR>inst✝¹ : IsDedekindDomain S<VAR>inst✝ : NoZeroSMulDivisors R S<VAR>hI : I.IsMaximal<VAR>hI' : I ≠ ⊥<VAR>hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤<VAR>hx' : _root_.IsIntegral R x<VAR>J : Ideal S<VAR>hJ : J ∈ normalizedFactors (Ideal.map (algebraMap R S) I)<GOAL>multiplicity J (Ideal.map (algebraMap R S) I) = multiplicity (↑((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx') ⟨J, hJ⟩)) (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s t u : Set α<VAR>μ ν : Measure ℝ<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>h : ∀ (a b : ℚ), μ (Ioo ↑a ↑b) = ν (Ioo ↑a ↑b)<GOAL>∀ s ∈ ⋃ a, ⋃ b, ⋃ (_ : a < b), {Ioo ↑a ↑b}, μ s = ν s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s t u : Set α<VAR>μ ν : Measure ℝ<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>h : ∀ (a b : ℚ), μ (Ioo ↑a ↑b) = ν (Ioo ↑a ↑b)<GOAL>∀ (s : Set ℝ), (∃ i i_1, ∃ (_ : i < i_1), s = Ioo ↑i ↑i_1) → μ s = ν s
<VAR>r x : ℝ<GOAL>HasDerivAt (fun a => -rexp (-(r * a))) (r * rexp (-(r * x))) x
<VAR>r x : ℝ<GOAL>(fun a => -rexp (-(r * a))) = fun y => -1 * rexp (-r * id y)
<VAR>r x : ℝ<GOAL>r * rexp (-(r * x)) = -1 * (rexp (-r * id x) * (-r * 1))
<VAR>α : Type u_1<VAR>inst✝ : TopologicalSpace α<VAR>f : α → Angle<VAR>s : Set α<VAR>hf : ContinuousOn f s<VAR>hs : ∀ z ∈ s, f z ≠ 0 ∧ f z ≠ ↑π<GOAL>ContinuousOn (sign ∘ f) s
<VAR>α : Type u_1<VAR>inst✝ : TopologicalSpace α<VAR>f : α → Angle<VAR>s : Set α<VAR>hf : ContinuousOn f s<VAR>hs : ∀ z ∈ s, f z ≠ 0 ∧ f z ≠ ↑π<VAR>θ : Angle<VAR>hθ : θ ∈ f '' s<GOAL>ContinuousAt sign θ
<VAR>α : Type u_1<VAR>inst✝ : TopologicalSpace α<VAR>f : α → Angle<VAR>s : Set α<VAR>hf : ContinuousOn f s<VAR>hs : ∀ z ∈ s, f z ≠ 0 ∧ f z ≠ ↑π<VAR>z : α<VAR>hz : z ∈ s<GOAL>ContinuousAt sign (f z)
<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>m1 : MeasurableSpace β<VAR>f : α → β<VAR>hf : MeasurableEmbedding f<VAR>μ : Measure β<VAR>s : Set α<GOAL>(Measure.comap f μ) s = (Measure.comap f μ) (f ⁻¹' (f '' 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>m1 : MeasurableSpace β<VAR>f : α → β<VAR>hf : MeasurableEmbedding f<VAR>μ : Measure β<VAR>s : Set α<GOAL>(Measure.map f (Measure.comap f μ)) (f '' s) = μ (f '' s)
<VAR>α : Type u_1<VAR>R : α → α → Prop<VAR>L : List (List α)<GOAL>Pairwise R L.join ↔ (∀ (l : List α), l ∈ L → Pairwise R l) ∧ Pairwise (fun l₁ l₂ => ∀ (x : α), x ∈ l₁ → ∀ (y : α), y ∈ l₂ → R x y) L
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>m✝ : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>c : ℝ≥0∞<VAR>s : Set α<VAR>x : F<GOAL>(weightedSMul (c • μ) s) x = (c.toReal • ⇑(weightedSMul μ s)) x
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>m✝ : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>c : ℝ≥0∞<VAR>s : Set α<VAR>x : F<GOAL>((c • μ) s).toReal • x = c.toReal • (μ s).toReal • x
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>m✝ : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>c : ℝ≥0∞<VAR>s : Set α<VAR>x : F<GOAL>((c • ⇑μ) s).toReal • x = c.toReal • (μ s).toReal • x
<VAR>J : Type w<VAR>C✝ : Type u<VAR>inst✝² : Category.{v, u} C✝<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>B : C<VAR>objs : J → C<VAR>arrows : (j : J) → B ⟶ objs j<VAR>inst✝ : HasWidePushout B objs arrows<VAR>X : C<VAR>f : B ⟶ X<VAR>fs : (j : J) → objs j ⟶ X<VAR>w : ∀ (j : J), arrows j ≫ fs j = f<VAR>g1 g2 : widePushout B objs arrows ⟶ X<VAR>h1 : ∀ (j : J), ι arrows j ≫ g1 = ι arrows j ≫ g2<VAR>h2 : head arrows ≫ g1 = head arrows ≫ g2<GOAL>g1 = g2
<VAR>J : Type w<VAR>C✝ : Type u<VAR>inst✝² : Category.{v, u} C✝<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>B : C<VAR>objs : J → C<VAR>arrows : (j : J) → B ⟶ objs j<VAR>inst✝ : HasWidePushout B objs arrows<VAR>X : C<VAR>f : B ⟶ X<VAR>fs : (j : J) → objs j ⟶ X<VAR>w : ∀ (j : J), arrows j ≫ fs j = f<VAR>g1 g2 : widePushout B objs arrows ⟶ X<VAR>h1 : ∀ (j : J), ι arrows j ≫ g1 = ι arrows j ≫ g2<VAR>h2 : head arrows ≫ g1 = head arrows ≫ g2<GOAL>∀ (j : WidePushoutShape J), colimit.ι (WidePushoutShape.wideSpan B objs arrows) j ≫ g1 = colimit.ι (WidePushoutShape.wideSpan B objs arrows) j ≫ g2
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝ : LinearOrder ι<VAR>f : Filtration ι m<VAR>τ π : Ω → ι<VAR>hτ : IsStoppingTime f τ<VAR>i j : ι<GOAL>MeasurableSet ({ω | τ ω ≤ i} ∩ {ω | τ ω ≤ j})
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝ : LinearOrder ι<VAR>f : Filtration ι m<VAR>τ π : Ω → ι<VAR>hτ : IsStoppingTime f τ<VAR>i j : ι<VAR>this : {ω | τ ω ≤ i} ∩ {ω | τ ω ≤ j} = {ω | τ ω ≤ min i j}<GOAL>MeasurableSet ({ω | τ ω ≤ i} ∩ {ω | τ ω ≤ j})
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝ : LinearOrder ι<VAR>f : Filtration ι m<VAR>τ π : Ω → ι<VAR>hτ : IsStoppingTime f τ<VAR>i j : ι<VAR>this : {ω | τ ω ≤ i} ∩ {ω | τ ω ≤ j} = {ω | τ ω ≤ min i j}<GOAL>MeasurableSet {ω | τ ω ≤ min i j}
<VAR>p : ℕ<GOAL>Nat.rec 1 (fun y IH => IH * (unpair p).1) (unpair p).2 = (unpair p).1 ^ (unpair p).2
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l f : Filter α<VAR>g : α → Filter β<VAR>s✝ s : Set β<GOAL>(s ∈ f.bind fun x => g x ⊓ 𝓟 s✝) ↔ s ∈ f.bind g ⊓ 𝓟 s✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s : Finset α<GOAL>(image Sym2.mk s.diag).card = s.card
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s : Finset α<GOAL>Set.InjOn Sym2.mk ↑s.diag
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s : Finset α<VAR>x₀ x₁ : α<VAR>hx : (x₀, x₁) ∈ ↑s.diag<VAR>x₂✝ : α × α<VAR>a✝ : x₂✝ ∈ ↑s.diag<VAR>h : s(x₀, x₁) = Sym2.mk x₂✝<GOAL>(x₀, x₁) = x₂✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s : Finset α<VAR>x₀ x₁ : α<VAR>hx a✝ : (x₀, x₁) ∈ ↑s.diag<VAR>h : s(x₀, x₁) = s(x₀, x₁)<GOAL>(x₀, x₁) = (x₀, x₁)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s : Finset α<VAR>x₀ x₁ : α<VAR>hx : (x₀, x₁) ∈ ↑s.diag<VAR>a✝ : (x₁, x₀) ∈ ↑s.diag<VAR>h : s(x₀, x₁) = s(x₁, x₀)<GOAL>(x₀, x₁) = (x₁, x₀)
<VAR>α : Type u_1<VAR>inst✝ : NormedLatticeAddCommGroup α<VAR>x y : α<GOAL>‖x ⊓ y‖ ≤ ‖x‖ + ‖y‖
<VAR>α : Type u_1<VAR>inst✝ : NormedLatticeAddCommGroup α<VAR>x y : α<VAR>h : ‖x ⊓ y - 0 ⊓ 0‖ ≤ ‖x - 0‖ + ‖y - 0‖<GOAL>‖x ⊓ y‖ ≤ ‖x‖ + ‖y‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>β₂ : Type u_3<VAR>γ : Type u_4<VAR>ι✝ : Sort u_5<VAR>ι' : Sort u_6<VAR>κ : ι✝ → Sort u_7<VAR>κ' : ι' → Sort u_8<VAR>inst✝ : CompleteLattice α<VAR>f✝ g s✝ t : ι✝ → α<VAR>a b : α<VAR>ι : Type u_9<VAR>s : Set ι<VAR>f : ι → α<VAR>i : ι<VAR>hi : i ∈ s<GOAL>⨅ i ∈ s, f i ≤ f i
<VAR>S : Type u_1<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : IsDomain S<VAR>inst✝³ : Nontrivial S<VAR>inst✝² : IsDedekindDomain S<VAR>inst✝¹ : Module.Free ℤ S<VAR>inst✝ : Module.Finite ℤ S<VAR>x : S<VAR>hx : Prime ((Algebra.norm ℤ) x)<VAR>y : ℤ<GOAL>(Algebra.norm ℤ) x ∣ y ↔ x ∣ ↑y
<VAR>S : Type u_1<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : IsDomain S<VAR>inst✝³ : Nontrivial S<VAR>inst✝² : IsDedekindDomain S<VAR>inst✝¹ : Module.Free ℤ S<VAR>inst✝ : Module.Finite ℤ S<VAR>x : S<VAR>hx : Prime ((Algebra.norm ℤ) x)<VAR>y : ℤ<GOAL>Nat.Prime (absNorm (span {x}))
<VAR>α : Type u<VAR>β : Type u_1<VAR>inst✝³ : CanonicallyOrderedCommSemiring α<VAR>a b c : α<VAR>inst✝² : Sub α<VAR>inst✝¹ : OrderedSub α<VAR>inst✝ : IsTotal α fun x x_1 => x ≤ x_1<VAR>h : AddLECancellable (b * c)<GOAL>(a - b) * c = a * c - b * c
<VAR>α : Type u<VAR>β : Type u_1<VAR>inst✝³ : CanonicallyOrderedCommSemiring α<VAR>a b c : α<VAR>inst✝² : Sub α<VAR>inst✝¹ : OrderedSub α<VAR>inst✝ : IsTotal α fun x x_1 => x ≤ x_1<VAR>h : AddLECancellable (c * b)<GOAL>c * (a - b) = c * a - c * b
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>L : List (List α)<GOAL>L.join.length = (map length L).sum
<VAR>α : Type u<VAR>β : Type v<VAR>r✝ : α → α → Prop<VAR>s : β → β → Prop<VAR>r : α → α → Prop<VAR>inst✝ : IsTrichotomous α r<VAR>a b : α<GOAL>Function.swap r a b ∨ a = b ∨ Function.swap r b a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<GOAL>∀ (l : List α), ContinuousAt length l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<GOAL>∀ (l : List α), Tendsto length (𝓝 l) (pure l.length)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<GOAL>Tendsto length (pure []) (pure [].length)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<GOAL>∀ (l : List α) (a : α), Tendsto length (𝓝 l) (pure l.length) → Tendsto (fun p => (p.1 :: p.2).length) (𝓝 a ×ˢ 𝓝 l) (pure (a :: l).length)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedField α<VAR>a✝ b c d : α<VAR>n : ℤ<VAR>a : α<GOAL>a / 2 - a = -(a / 2)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedField α<VAR>a✝ b c d : α<VAR>n : ℤ<VAR>a : α<GOAL>a / 2 - (a / 2 + a / 2) = -(a / 2)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝ : (i : ι) → MeasurableSpace (α i)<VAR>P : (J : Finset ι) → Measure ((j : { x // x ∈ J }) → α ↑j)<VAR>μ ν : Measure ((i : ι) → α i)<VAR>hμ : IsProjectiveLimit μ P<VAR>hν : IsProjectiveLimit ν P<GOAL>μ univ = ν univ
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>inst✝³ : RCLike 𝕂<VAR>inst✝² : NormedDivisionRing 𝔸<VAR>inst✝¹ : NormedAlgebra 𝕂 𝔸<VAR>inst✝ : CompleteSpace 𝔸<VAR>z : ℤ<VAR>x : 𝔸<GOAL>exp 𝕂 (z • x) = exp 𝕂 x ^ z
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>inst✝³ : RCLike 𝕂<VAR>inst✝² : NormedDivisionRing 𝔸<VAR>inst✝¹ : NormedAlgebra 𝕂 𝔸<VAR>inst✝ : CompleteSpace 𝔸<VAR>x : 𝔸<VAR>n : ℕ<GOAL>exp 𝕂 (↑n • x) = exp 𝕂 x ^ ↑n
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>inst✝³ : RCLike 𝕂<VAR>inst✝² : NormedDivisionRing 𝔸<VAR>inst✝¹ : NormedAlgebra 𝕂 𝔸<VAR>inst✝ : CompleteSpace 𝔸<VAR>x : 𝔸<VAR>n : ℕ<GOAL>exp 𝕂 (-↑n • x) = exp 𝕂 x ^ (-↑n)
<VAR>F : Type u<VAR>K : Type v<VAR>L : Type w<VAR>inst✝² : Field K<VAR>inst✝¹ : Field L<VAR>inst✝ : Field F<VAR>f : K[X]<GOAL>f.removeFactor.natDegree = f.natDegree - 1
<VAR>w x✝ y z p : ℝ<VAR>x : ℝ≥0<VAR>hx_pos : 0 < x<GOAL>0 < x ^ p
<VAR>w x✝ y z p : ℝ<VAR>x : ℝ≥0<VAR>hx_pos : 0 < x<VAR>rpow_pos_of_nonneg : ∀ {p : ℝ}, 0 < p → 0 < x ^ p<GOAL>0 < x ^ p
<VAR>w x✝ y z p : ℝ<VAR>x : ℝ≥0<VAR>hx_pos : 0 < x<VAR>rpow_pos_of_nonneg : ∀ {p : ℝ}, 0 < p → 0 < x ^ p<VAR>hp_pos : 0 < p<GOAL>0 < x ^ p
<VAR>w x✝ y z : ℝ<VAR>x : ℝ≥0<VAR>hx_pos : 0 < x<VAR>rpow_pos_of_nonneg : ∀ {p : ℝ}, 0 < p → 0 < x ^ p<GOAL>0 < x ^ 0
<VAR>w x✝ y z p : ℝ<VAR>x : ℝ≥0<VAR>hx_pos : 0 < x<VAR>rpow_pos_of_nonneg : ∀ {p : ℝ}, 0 < p → 0 < x ^ p<VAR>hp_neg : p < 0<GOAL>0 < x ^ p
<VAR>θ ψ : Angle<GOAL>θ.cos = ψ.cos ↔ θ = ψ ∨ θ = -ψ