ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>Ω✝ : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω✝<VAR>κ✝ : Kernel α Ω✝<VAR>μ✝ : Measure α<VAR>Ω : Type u_4<VAR>m : ι → MeasurableSpace Ω<VAR>m' m0 : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μ : Measure α<VAR>inst✝ : IsMarkovKernel κ<VAR>h_indep : ∀ (i : ι), Indep (m i) m' κ μ<VAR>h_le : ∀ (i : ι), m i ≤ m0<VAR>h_le' : m' ≤ m0<VAR>hm : Directed (fun x x_1 => x ≤ x_1) m<VAR>p : ι → Set (Set Ω) := fun n => {t | MeasurableSet t}<VAR>hp : ∀ (n : ι), IsPiSystem (p n)<VAR>h_gen_n : ∀ (n : ι), m n = generateFrom (p n)<VAR>hp_supr_pi : IsPiSystem (⋃ n, p n)<VAR>p' : Set (Set Ω) := {t | MeasurableSet t}<VAR>hp'_pi : IsPiSystem p'<VAR>h_gen' : m' = generateFrom p'<VAR>h_pi_system_indep : IndepSets (⋃ n, p n) p' κ μ<GOAL>⨆ i, m i = generateFrom (⋃ n, p n)
<VAR>S : Type u_1<VAR>inst✝³ : CommRing S<VAR>inst✝² : IsDomain S<VAR>inst✝¹ : IsDedekindDomain S<VAR>inst✝ : Module.Free ℤ S<VAR>I J : Ideal S<VAR>b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S<GOAL>cardQuot (I * J) = cardQuot I * cardQuot J
<VAR>S : Type u_1<VAR>inst✝³ : CommRing S<VAR>inst✝² : IsDomain S<VAR>inst✝¹ : IsDedekindDomain S<VAR>inst✝ : Module.Free ℤ S<VAR>I J : Ideal S<VAR>b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S<VAR>this : Infinite S<GOAL>cardQuot (I * J) = cardQuot I * cardQuot J
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module ℝ E<VAR>s t : Set E<VAR>x✝ : E<VAR>a : ℝ<VAR>p : Seminorm ℝ E<VAR>x : E<GOAL>gauge (p.ball 0 1) x = p x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module ℝ E<VAR>s t : Set E<VAR>x✝ : E<VAR>a : ℝ<VAR>p : Seminorm ℝ E<VAR>x : E<VAR>hp : {r | 0 < r ∧ x ∈ r • p.ball 0 1} = ∅<GOAL>gauge (p.ball 0 1) x = p x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module ℝ E<VAR>s t : Set E<VAR>x✝ : E<VAR>a : ℝ<VAR>p : Seminorm ℝ E<VAR>x : E<VAR>hp : {r | 0 < r ∧ x ∈ r • p.ball 0 1}.Nonempty<GOAL>gauge (p.ball 0 1) x = p x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module ℝ E<VAR>s t : Set E<VAR>x✝ : E<VAR>a : ℝ<VAR>p : Seminorm ℝ E<VAR>x : E<VAR>hp : {r | 0 < r ∧ x ∈ r • p.ball 0 1}.Nonempty<VAR>r : ℝ<GOAL>r ∈ {r | 0 < r ∧ x ∈ r • p.ball 0 1} → p x ≤ r
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module ℝ E<VAR>s t : Set E<VAR>x✝ : E<VAR>a : ℝ<VAR>p : Seminorm ℝ E<VAR>x : E<VAR>hp : {r | 0 < r ∧ x ∈ r • p.ball 0 1}.Nonempty<VAR>r : ℝ<VAR>hr : r ∈ lowerBounds {r | 0 < r ∧ x ∈ r • p.ball 0 1}<VAR>ε : ℝ<VAR>hε : 0 < ε<GOAL>r ≤ p x + ε
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_2, u_1} C<VAR>inst✝² : HasZeroMorphisms C<VAR>K L : ChainComplex C ℕ<VAR>φ : K ⟶ L<VAR>inst✝¹ : HomologicalComplex.HasHomology K 0<VAR>inst✝ : HomologicalComplex.HasHomology L 0<GOAL>K.isoHomologyι₀.inv ≫ HomologicalComplex.homologyMap φ 0 = HomologicalComplex.opcyclesMap φ 0 ≫ L.isoHomologyι₀.inv
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>N : Type u_3<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>f : ℕ → M<VAR>h : ∀ (n : ℕ), f n ≡ f (n + 1) [SMOD I ^ n • ⊤]<GOAL>IsAdicCauchy I M f
<VAR>𝕜 : Type u_1<VAR>inst✝³ : RCLike 𝕜<VAR>ι : Type u_2<VAR>inst✝² : Fintype ι<VAR>E : ι → Type u_3<VAR>f : (i : ι) → E i → 𝕜<VAR>inst✝¹ : (i : ι) → MeasureSpace (E i)<VAR>inst✝ : ∀ (i : ι), SigmaFinite volume<VAR>e : Fin (card ι) ≃ ι := (equivFin ι).symm<GOAL>∫ (x : (i : ι) → E i), ∏ i : ι, f i (x i) = ∏ i : ι, ∫ (x : E i), f i x
<VAR>𝕜 : Type u_1<VAR>inst✝³ : RCLike 𝕜<VAR>ι : Type u_2<VAR>inst✝² : Fintype ι<VAR>E : ι → Type u_3<VAR>f : (i : ι) → E i → 𝕜<VAR>inst✝¹ : (i : ι) → MeasureSpace (E i)<VAR>inst✝ : ∀ (i : ι), SigmaFinite volume<VAR>e : Fin (card ι) ≃ ι := (equivFin ι).symm<GOAL>∫ (x : (b : Fin (card ι)) → E (e b)), ∏ i : ι, f i ((MeasurableEquiv.piCongrLeft E e) x i) = ∏ i : ι, ∫ (x : E i), f i x
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Ring R<VAR>inst✝¹ : Module R M<VAR>S : Submodule R M<VAR>inst✝ : S.IsPrincipal<VAR>x : M<GOAL>x ∈ S ↔ ∃ s, x = s • generator S
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : Monoid α<VAR>a : Associates α<GOAL>Associates.mk (Quot.out a) = a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹¹ : RCLike 𝕜<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedSpace 𝕜 F<VAR>inst✝⁸ : NormedAddCommGroup F'<VAR>inst✝⁷ : NormedSpace 𝕜 F'<VAR>inst✝⁶ : NormedSpace ℝ F'<VAR>inst✝⁵ : CompleteSpace F'<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedAddCommGroup G'<VAR>inst✝² : NormedSpace ℝ G'<VAR>inst✝¹ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>f✝ g : α → F'<VAR>s : Set α<VAR>f : ↥(Lp F' 1 μ)<VAR>hs : MeasurableSet s<VAR>S : ℕ → Set α := spanningSets (μ.trim hm)<GOAL>∫ (x : α) in s, ↑↑((condexpL1CLM F' hm μ) f) x ∂μ = ∫ (x : α) in s, ↑↑f x ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹¹ : RCLike 𝕜<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedSpace 𝕜 F<VAR>inst✝⁸ : NormedAddCommGroup F'<VAR>inst✝⁷ : NormedSpace 𝕜 F'<VAR>inst✝⁶ : NormedSpace ℝ F'<VAR>inst✝⁵ : CompleteSpace F'<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedAddCommGroup G'<VAR>inst✝² : NormedSpace ℝ G'<VAR>inst✝¹ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>f✝ g : α → F'<VAR>s : Set α<VAR>f : ↥(Lp F' 1 μ)<VAR>hs : MeasurableSet s<VAR>S : ℕ → Set α := spanningSets (μ.trim hm)<VAR>hS_meas : ∀ (i : ℕ), MeasurableSet (S i)<GOAL>∫ (x : α) in s, ↑↑((condexpL1CLM F' hm μ) f) x ∂μ = ∫ (x : α) in s, ↑↑f x ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹¹ : RCLike 𝕜<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedSpace 𝕜 F<VAR>inst✝⁸ : NormedAddCommGroup F'<VAR>inst✝⁷ : NormedSpace 𝕜 F'<VAR>inst✝⁶ : NormedSpace ℝ F'<VAR>inst✝⁵ : CompleteSpace F'<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedAddCommGroup G'<VAR>inst✝² : NormedSpace ℝ G'<VAR>inst✝¹ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>f✝ g : α → F'<VAR>s : Set α<VAR>f : ↥(Lp F' 1 μ)<VAR>hs : MeasurableSet s<VAR>S : ℕ → Set α := spanningSets (μ.trim hm)<VAR>hS_meas : ∀ (i : ℕ), MeasurableSet (S i)<VAR>hS_meas0 : ∀ (i : ℕ), MeasurableSet (S i)<GOAL>∫ (x : α) in s, ↑↑((condexpL1CLM F' hm μ) f) x ∂μ = ∫ (x : α) in s, ↑↑f x ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹¹ : RCLike 𝕜<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedSpace 𝕜 F<VAR>inst✝⁸ : NormedAddCommGroup F'<VAR>inst✝⁷ : NormedSpace 𝕜 F'<VAR>inst✝⁶ : NormedSpace ℝ F'<VAR>inst✝⁵ : CompleteSpace F'<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedAddCommGroup G'<VAR>inst✝² : NormedSpace ℝ G'<VAR>inst✝¹ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>f✝ g : α → F'<VAR>s : Set α<VAR>f : ↥(Lp F' 1 μ)<VAR>hs : MeasurableSet s<VAR>S : ℕ → Set α := spanningSets (μ.trim hm)<VAR>hS_meas : ∀ (i : ℕ), MeasurableSet (S i)<VAR>hS_meas0 : ∀ (i : ℕ), MeasurableSet (S i)<VAR>hs_eq : s = ⋃ i, S i ∩ s<GOAL>∫ (x : α) in s, ↑↑((condexpL1CLM F' hm μ) f) x ∂μ = ∫ (x : α) in s, ↑↑f x ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹¹ : RCLike 𝕜<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedSpace 𝕜 F<VAR>inst✝⁸ : NormedAddCommGroup F'<VAR>inst✝⁷ : NormedSpace 𝕜 F'<VAR>inst✝⁶ : NormedSpace ℝ F'<VAR>inst✝⁵ : CompleteSpace F'<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedAddCommGroup G'<VAR>inst✝² : NormedSpace ℝ G'<VAR>inst✝¹ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>f✝ g : α → F'<VAR>s : Set α<VAR>f : ↥(Lp F' 1 μ)<VAR>hs : MeasurableSet s<VAR>S : ℕ → Set α := spanningSets (μ.trim hm)<VAR>hS_meas : ∀ (i : ℕ), MeasurableSet (S i)<VAR>hS_meas0 : ∀ (i : ℕ), MeasurableSet (S i)<VAR>hs_eq : s = ⋃ i, S i ∩ s<VAR>hS_finite : ∀ (i : ℕ), μ (S i ∩ s) < ⊤<GOAL>∫ (x : α) in s, ↑↑((condexpL1CLM F' hm μ) f) x ∂μ = ∫ (x : α) in s, ↑↑f x ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹¹ : RCLike 𝕜<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedSpace 𝕜 F<VAR>inst✝⁸ : NormedAddCommGroup F'<VAR>inst✝⁷ : NormedSpace 𝕜 F'<VAR>inst✝⁶ : NormedSpace ℝ F'<VAR>inst✝⁵ : CompleteSpace F'<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedAddCommGroup G'<VAR>inst✝² : NormedSpace ℝ G'<VAR>inst✝¹ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>f✝ g : α → F'<VAR>s : Set α<VAR>f : ↥(Lp F' 1 μ)<VAR>hs : MeasurableSet s<VAR>S : ℕ → Set α := spanningSets (μ.trim hm)<VAR>hS_meas : ∀ (i : ℕ), MeasurableSet (S i)<VAR>hS_meas0 : ∀ (i : ℕ), MeasurableSet (S i)<VAR>hs_eq : s = ⋃ i, S i ∩ s<VAR>hS_finite : ∀ (i : ℕ), μ (S i ∩ s) < ⊤<VAR>h_mono : Monotone fun i => S i ∩ s<GOAL>∫ (x : α) in s, ↑↑((condexpL1CLM F' hm μ) f) x ∂μ = ∫ (x : α) in s, ↑↑f x ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹¹ : RCLike 𝕜<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedSpace 𝕜 F<VAR>inst✝⁸ : NormedAddCommGroup F'<VAR>inst✝⁷ : NormedSpace 𝕜 F'<VAR>inst✝⁶ : NormedSpace ℝ F'<VAR>inst✝⁵ : CompleteSpace F'<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedAddCommGroup G'<VAR>inst✝² : NormedSpace ℝ G'<VAR>inst✝¹ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>f✝ g : α → F'<VAR>s : Set α<VAR>f : ↥(Lp F' 1 μ)<VAR>hs : MeasurableSet s<VAR>S : ℕ → Set α := spanningSets (μ.trim hm)<VAR>hS_meas : ∀ (i : ℕ), MeasurableSet (S i)<VAR>hS_meas0 : ∀ (i : ℕ), MeasurableSet (S i)<VAR>hs_eq : s = ⋃ i, S i ∩ s<VAR>hS_finite : ∀ (i : ℕ), μ (S i ∩ s) < ⊤<VAR>h_mono : Monotone fun i => S i ∩ s<VAR>h_eq_forall : (fun i => ∫ (x : α) in S i ∩ s, ↑↑((condexpL1CLM F' hm μ) f) x ∂μ) = fun i => ∫ (x : α) in S i ∩ s, ↑↑f x ∂μ<GOAL>∫ (x : α) in s, ↑↑((condexpL1CLM F' hm μ) f) x ∂μ = ∫ (x : α) in s, ↑↑f x ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹¹ : RCLike 𝕜<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedSpace 𝕜 F<VAR>inst✝⁸ : NormedAddCommGroup F'<VAR>inst✝⁷ : NormedSpace 𝕜 F'<VAR>inst✝⁶ : NormedSpace ℝ F'<VAR>inst✝⁵ : CompleteSpace F'<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedAddCommGroup G'<VAR>inst✝² : NormedSpace ℝ G'<VAR>inst✝¹ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>f✝ g : α → F'<VAR>s : Set α<VAR>f : ↥(Lp F' 1 μ)<VAR>hs : MeasurableSet s<VAR>S : ℕ → Set α := spanningSets (μ.trim hm)<VAR>hS_meas : ∀ (i : ℕ), MeasurableSet (S i)<VAR>hS_meas0 : ∀ (i : ℕ), MeasurableSet (S i)<VAR>hs_eq : s = ⋃ i, S i ∩ s<VAR>hS_finite : ∀ (i : ℕ), μ (S i ∩ s) < ⊤<VAR>h_mono : Monotone fun i => S i ∩ s<VAR>h_eq_forall : (fun i => ∫ (x : α) in S i ∩ s, ↑↑((condexpL1CLM F' hm μ) f) x ∂μ) = fun i => ∫ (x : α) in S i ∩ s, ↑↑f x ∂μ<VAR>h_right : Tendsto (fun i => ∫ (x : α) in S i ∩ s, ↑↑f x ∂μ) atTop (𝓝 (∫ (x : α) in s, ↑↑f x ∂μ))<GOAL>∫ (x : α) in s, ↑↑((condexpL1CLM F' hm μ) f) x ∂μ = ∫ (x : α) in s, ↑↑f x ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹¹ : RCLike 𝕜<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedSpace 𝕜 F<VAR>inst✝⁸ : NormedAddCommGroup F'<VAR>inst✝⁷ : NormedSpace 𝕜 F'<VAR>inst✝⁶ : NormedSpace ℝ F'<VAR>inst✝⁵ : CompleteSpace F'<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedAddCommGroup G'<VAR>inst✝² : NormedSpace ℝ G'<VAR>inst✝¹ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>f✝ g : α → F'<VAR>s : Set α<VAR>f : ↥(Lp F' 1 μ)<VAR>hs : MeasurableSet s<VAR>S : ℕ → Set α := spanningSets (μ.trim hm)<VAR>hS_meas : ∀ (i : ℕ), MeasurableSet (S i)<VAR>hS_meas0 : ∀ (i : ℕ), MeasurableSet (S i)<VAR>hs_eq : s = ⋃ i, S i ∩ s<VAR>hS_finite : ∀ (i : ℕ), μ (S i ∩ s) < ⊤<VAR>h_mono : Monotone fun i => S i ∩ s<VAR>h_eq_forall : (fun i => ∫ (x : α) in S i ∩ s, ↑↑((condexpL1CLM F' hm μ) f) x ∂μ) = fun i => ∫ (x : α) in S i ∩ s, ↑↑f x ∂μ<VAR>h_right : Tendsto (fun i => ∫ (x : α) in S i ∩ s, ↑↑f x ∂μ) atTop (𝓝 (∫ (x : α) in s, ↑↑f x ∂μ))<VAR>h_left : Tendsto (fun i => ∫ (x : α) in S i ∩ s, ↑↑((condexpL1CLM F' hm μ) f) x ∂μ) atTop (𝓝 (∫ (x : α) in s, ↑↑((condexpL1CLM F' hm μ) f) x ∂μ))<GOAL>∫ (x : α) in s, ↑↑((condexpL1CLM F' hm μ) f) x ∂μ = ∫ (x : α) in s, ↑↑f x ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹¹ : RCLike 𝕜<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedSpace 𝕜 F<VAR>inst✝⁸ : NormedAddCommGroup F'<VAR>inst✝⁷ : NormedSpace 𝕜 F'<VAR>inst✝⁶ : NormedSpace ℝ F'<VAR>inst✝⁵ : CompleteSpace F'<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedAddCommGroup G'<VAR>inst✝² : NormedSpace ℝ G'<VAR>inst✝¹ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>f✝ g : α → F'<VAR>s : Set α<VAR>f : ↥(Lp F' 1 μ)<VAR>hs : MeasurableSet s<VAR>S : ℕ → Set α := spanningSets (μ.trim hm)<VAR>hS_meas : ∀ (i : ℕ), MeasurableSet (S i)<VAR>hS_meas0 : ∀ (i : ℕ), MeasurableSet (S i)<VAR>hs_eq : s = ⋃ i, S i ∩ s<VAR>hS_finite : ∀ (i : ℕ), μ (S i ∩ s) < ⊤<VAR>h_mono : Monotone fun i => S i ∩ s<VAR>h_eq_forall : (fun i => ∫ (x : α) in S i ∩ s, ↑↑((condexpL1CLM F' hm μ) f) x ∂μ) = fun i => ∫ (x : α) in S i ∩ s, ↑↑f x ∂μ<VAR>h_right : Tendsto (fun i => ∫ (x : α) in S i ∩ s, ↑↑f x ∂μ) atTop (𝓝 (∫ (x : α) in s, ↑↑f x ∂μ))<VAR>h_left : Tendsto (fun i => ∫ (x : α) in S i ∩ s, ↑↑f x ∂μ) atTop (𝓝 (∫ (x : α) in s, ↑↑((condexpL1CLM F' hm μ) f) x ∂μ))<GOAL>∫ (x : α) in s, ↑↑((condexpL1CLM F' hm μ) f) x ∂μ = ∫ (x : α) in s, ↑↑f x ∂μ
<VAR>α : Type u<VAR>inst✝ : DivisionRing α<VAR>x y : α<VAR>h' : Commute x y<VAR>h : x ≠ y<VAR>n : ℕ<GOAL>∑ i ∈ range n, x ^ i * y ^ (n - 1 - i) = (x ^ n - y ^ n) / (x - y)
<VAR>α : Type u<VAR>inst✝ : DivisionRing α<VAR>x y : α<VAR>h' : Commute x y<VAR>h : x ≠ y<VAR>n : ℕ<VAR>this : x - y ≠ 0<GOAL>∑ i ∈ range n, x ^ i * y ^ (n - 1 - i) = (x ^ n - y ^ n) / (x - y)
<VAR>𝕜 : Type u<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : CompleteSpace 𝕜<VAR>EM : Type u_1<VAR>inst✝⁴ : NormedAddCommGroup EM<VAR>inst✝³ : NormedSpace 𝕜 EM<VAR>HM : Type u_2<VAR>inst✝² : TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>M : Type u<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : ChartedSpace HM M<VAR>x : M<VAR>f : ↑((smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜).presheaf.stalk x)<GOAL>f ∈ nonunits ↑((smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜).presheaf.stalk x) ↔ f ∈ ↑(RingHom.ker (eval IM 𝓘(𝕜, 𝕜) M 𝕜 x))
<VAR>𝕜 : Type u<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : CompleteSpace 𝕜<VAR>EM : Type u_1<VAR>inst✝⁴ : NormedAddCommGroup EM<VAR>inst✝³ : NormedSpace 𝕜 EM<VAR>HM : Type u_2<VAR>inst✝² : TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>M : Type u<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : ChartedSpace HM M<VAR>x : M<VAR>f : ↑((smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜).presheaf.stalk x)<GOAL>IsUnit f ↔ f ∉ ↑(RingHom.ker (eval IM 𝓘(𝕜, 𝕜) M 𝕜 x))
<VAR>e : ℂ → ℂ<VAR>e' : ℂ<VAR>z : ℝ<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f : ℂ → E<VAR>x : ℂ<VAR>f' : E<VAR>h : HasDerivAt f f' x<GOAL>HasFDerivAt f (reCLM.smulRight f' + I • imCLM.smulRight f') x
<VAR>𝕜 : Type u_1<VAR>inst✝¹ : NormedLinearOrderedField 𝕜<VAR>P Q : 𝕜[X]<VAR>inst✝ : OrderTopology 𝕜<GOAL>Tendsto (fun x => eval x P) atTop atTop ↔ 0 < P.degree ∧ 0 ≤ P.leadingCoeff
<VAR>𝕜 : Type u_1<VAR>inst✝¹ : NormedLinearOrderedField 𝕜<VAR>P Q : 𝕜[X]<VAR>inst✝ : OrderTopology 𝕜<VAR>h : Tendsto (fun x => eval x P) atTop atTop<GOAL>0 < P.degree ∧ 0 ≤ P.leadingCoeff
<VAR>𝕜 : Type u_1<VAR>inst✝¹ : NormedLinearOrderedField 𝕜<VAR>P Q : 𝕜[X]<VAR>inst✝ : OrderTopology 𝕜<VAR>h : Tendsto (fun x => eval x P) atTop atTop<VAR>this : Tendsto (fun x => P.leadingCoeff * x ^ P.natDegree) atTop atTop<GOAL>0 < P.degree ∧ 0 ≤ P.leadingCoeff
<VAR>𝕜 : Type u_1<VAR>inst✝¹ : NormedLinearOrderedField 𝕜<VAR>P Q : 𝕜[X]<VAR>inst✝ : OrderTopology 𝕜<VAR>h : Tendsto (fun x => eval x P) atTop atTop<VAR>this : 0 < P.degree ∧ 0 < P.leadingCoeff<GOAL>0 < P.degree ∧ 0 ≤ P.leadingCoeff
<VAR>x : ℂ<GOAL>HasStrictDerivAt cos (-sin x) x
<VAR>x : ℂ<GOAL>HasStrictDerivAt cos (-(cexp (-x * I) - cexp (x * I)) * I * 2⁻¹) x
<VAR>x : ℂ<GOAL>-(cexp (-x * I) - cexp (x * I)) * I * 2⁻¹ = (cexp (id x * I) * (1 * I) + cexp (-id x * I) * (-1 * I)) * 2⁻¹
<VAR>X Y : Scheme<VAR>U : X.Opens<VAR>hU : IsAffineOpen U<VAR>f : ↑Γ(X, U)<VAR>V : X.Opens<VAR>x : ↥V<VAR>h : ↑x ∈ U<VAR>this : IsAffine ↑U<GOAL>∃ f, X.basicOpen f ≤ V ∧ ↑x ∈ X.basicOpen f
<VAR>X Y : Scheme<VAR>U : X.Opens<VAR>hU : IsAffineOpen U<VAR>f : ↑Γ(X, U)<VAR>V : X.Opens<VAR>x : ↥V<VAR>h : ↑x ∈ U<VAR>this : IsAffine ↑U<VAR>r : ↑Γ(↑U, ⊤)<VAR>h₁ : ⟨↑x, h⟩ ∈ ↑((↑U).basicOpen r)<VAR>h₂ : ↑((↑U).basicOpen r) ⊆ ↑((Opens.map (Opens.inclusion U)).obj V)<GOAL>∃ f, X.basicOpen f ≤ V ∧ ↑x ∈ X.basicOpen f
<VAR>X Y : Scheme<VAR>U : X.Opens<VAR>hU : IsAffineOpen U<VAR>f : ↑Γ(X, U)<VAR>V : X.Opens<VAR>x : ↥V<VAR>h : ↑x ∈ U<VAR>this✝ : IsAffine ↑U<VAR>r : ↑Γ(↑U, ⊤)<VAR>h₁ : ⟨↑x, h⟩ ∈ ↑((↑U).basicOpen r)<VAR>h₂ : ↑((↑U).basicOpen r) ⊆ ↑((Opens.map (Opens.inclusion U)).obj V)<VAR>this : U.ι ''ᵁ (↑U).basicOpen r = X.basicOpen ((X.presheaf.map (eqToHom ⋯).op) r)<GOAL>∃ f, X.basicOpen f ≤ V ∧ ↑x ∈ X.basicOpen f
<VAR>X Y : Scheme<VAR>U : X.Opens<VAR>hU : IsAffineOpen U<VAR>f : ↑Γ(X, U)<VAR>V : X.Opens<VAR>x : ↥V<VAR>h : ↑x ∈ U<VAR>this✝ : IsAffine ↑U<VAR>r : ↑Γ(↑U, ⊤)<VAR>h₁ : ⟨↑x, h⟩ ∈ ↑((↑U).basicOpen r)<VAR>h₂ : ↑((↑U).basicOpen r) ⊆ ↑((Opens.map (Opens.inclusion U)).obj V)<VAR>this : U.ι ''ᵁ (↑U).basicOpen r = X.basicOpen ((X.presheaf.map (eqToHom ⋯).op) r)<GOAL>X.basicOpen ((X.presheaf.map (eqToHom ⋯).op) r) ≤ V ∧ ↑x ∈ X.basicOpen ((X.presheaf.map (eqToHom ⋯).op) r)
<VAR>X Y : Scheme<VAR>U : X.Opens<VAR>hU : IsAffineOpen U<VAR>f : ↑Γ(X, U)<VAR>V : X.Opens<VAR>x : ↥V<VAR>h : ↑x ∈ U<VAR>this✝ : IsAffine ↑U<VAR>r : ↑Γ(↑U, ⊤)<VAR>h₁ : ⟨↑x, h⟩ ∈ ↑((↑U).basicOpen r)<VAR>h₂ : ↑((↑U).basicOpen r) ⊆ ↑((Opens.map (Opens.inclusion U)).obj V)<VAR>this : U.ι ''ᵁ (↑U).basicOpen r = X.basicOpen ((X.presheaf.map (eqToHom ⋯).op) r)<GOAL>U.ι ''ᵁ (↑U).basicOpen r ≤ V ∧ ↑x ∈ U.ι ''ᵁ (↑U).basicOpen r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>e : PartialEquiv α β<VAR>e' : PartialEquiv β γ<GOAL>(e.trans e').source = e.source ∩ ↑e ⁻¹' (e.target ∩ e'.source)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G H : SimpleGraph α<VAR>s s₁ s₂ : Set α<VAR>t✝ : Finset α<VAR>a b : α<VAR>m n : ℕ<VAR>hmn : m ≤ n<VAR>hG : G.CliqueFreeOn s m<VAR>t : Finset α<VAR>hts : ↑t ⊆ s<VAR>ht : G.IsNClique n t<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G H : SimpleGraph α<VAR>s s₁ s₂ : Set α<VAR>t✝ : Finset α<VAR>a b : α<VAR>m n : ℕ<VAR>hmn : m ≤ n<VAR>hG : G.CliqueFreeOn s m<VAR>t : Finset α<VAR>hts : ↑t ⊆ s<VAR>ht : G.IsNClique n t<VAR>u : Finset α<VAR>hut : u ⊆ t<VAR>hu : u.card = m<GOAL>False
<VAR>C : Type u_1<VAR>inst✝ : Category.{u_2, u_1} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>h₁ : ∀ (Z : C), Nonempty (X ⟶ Z)<VAR>h₂ : ∀ ⦃Z : C⦄ (i j : X ⟶ Z), Zigzag (mk i) (mk j)<VAR>Z : C<VAR>this✝ : Nonempty (CostructuredArrow (parallelPair f g) Z)<VAR>this : ∀ (x : CostructuredArrow (parallelPair f g) Z), Zigzag x (mk ⋯.some)<GOAL>IsConnected (CostructuredArrow (parallelPair f g) Z)
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝¹ : Category.{v, u} V<VAR>inst✝ : HasZeroMorphisms V<GOAL>(ComplexShape.up ℕ).prev 0 = 0
<VAR>J : Type v'<VAR>inst✝⁸ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝⁷ : Category.{v, u} C<VAR>D : Type u''<VAR>inst✝⁶ : Category.{v'', u''} D<VAR>X Y : C<VAR>F : C ⥤ D<VAR>inst✝⁵ : FinitaryExtensive D<VAR>inst✝⁴ : HasFiniteCoproducts C<VAR>inst✝³ : HasPullbacks C<VAR>inst✝² : PreservesLimitsOfShape WalkingCospan F<VAR>inst✝¹ : PreservesColimitsOfShape (Discrete WalkingPair) F<VAR>inst✝ : F.ReflectsIsomorphisms<VAR>this✝ : ReflectsLimitsOfShape WalkingCospan F<VAR>this : ReflectsColimitsOfShape (Discrete WalkingPair) F<GOAL>FinitaryExtensive C
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>r : ℝ≥0<VAR>hr : r < 1<GOAL>Tendsto (fun a => ↑(r ^ a)) atTop (𝓝 ↑0)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : Type x<VAR>inst✝ : NonAssocRing α<VAR>a b : α<GOAL>(a - 1) * b = a * b - b
<VAR>p : ℝ≥0∞<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>α : ι → Type u_3<VAR>β✝ : ι → Type u_4<VAR>inst✝² : Fact (1 ≤ p)<VAR>inst✝¹ : Fintype ι<VAR>β : ι → Type u_5<VAR>inst✝ : (i : ι) → SeminormedAddCommGroup (β i)<VAR>x : PiLp 2 β<GOAL>‖x‖ = √(∑ x_1 : ι, ‖x x_1‖ ^ 2)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>g : α → ℝ≥0∞<GOAL>∫⁻ (a : α), f a + g a ∂μ = ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), g a ∂μ
<VAR>K : Type u_1<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>v : K<VAR>n : ℕ<VAR>ifp_succ_n : IntFractPair K<VAR>stream_succ_nth_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n<GOAL>(match (IntFractPair.of v, Stream'.Seq.tail ⟨IntFractPair.stream v, ⋯⟩) with | (h, s) => { h := ↑h.b, s := Stream'.Seq.map (fun p => { a := 1, b := ↑p.b }) s }).s.get? n = some { a := 1, b := ↑ifp_succ_n.b }
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>s s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>a : α<VAR>b : β<GOAL>s = s₁ ∧ t = t₁ ∨ (s = ∅ ∨ t = ∅) ∧ (s₁ = ∅ ∨ t₁ = ∅) ↔ s ×ˢ t = s₁ ×ˢ t₁
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>s s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>a : α<VAR>b : β<VAR>h : s ×ˢ t = ∅<GOAL>s = s₁ ∧ t = t₁ ∨ (s = ∅ ∨ t = ∅) ∧ (s₁ = ∅ ∨ t₁ = ∅) ↔ s ×ˢ t = s₁ ×ˢ t₁
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>s s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>a : α<VAR>b : β<VAR>h : (s ×ˢ t).Nonempty<GOAL>s = s₁ ∧ t = t₁ ∨ (s = ∅ ∨ t = ∅) ∧ (s₁ = ∅ ∨ t₁ = ∅) ↔ s ×ˢ t = s₁ ×ˢ t₁
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>s s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>a : α<VAR>b : β<VAR>h : (s ×ˢ t).Nonempty<GOAL>s = s₁ ∧ t = t₁ ∨ (s = ∅ ∨ t = ∅) ∧ (s₁ = ∅ ∨ t₁ = ∅) ↔ s = s₁ ∧ t = t₁
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>s s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>a : α<VAR>b : β<VAR>h : ¬(s = ∅ ∨ t = ∅)<GOAL>s = s₁ ∧ t = t₁ ∨ (s = ∅ ∨ t = ∅) ∧ (s₁ = ∅ ∨ t₁ = ∅) ↔ s = s₁ ∧ t = t₁
<VAR>R✝ : Type u<VAR>R'✝ : Type u'<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>inst✝¹⁸ : Ring R✝<VAR>inst✝¹⁷ : Ring R'✝<VAR>inst✝¹⁶ : AddCommGroup M<VAR>inst✝¹⁵ : AddCommGroup M'<VAR>inst✝¹⁴ : AddCommGroup M₁<VAR>inst✝¹³ : Module R✝ M<VAR>inst✝¹² : Module R✝ M'<VAR>inst✝¹¹ : Module R✝ M₁<VAR>inst✝¹⁰ : Module R'✝ M'<VAR>inst✝⁹ : Module R'✝ M₁<VAR>R : Type w<VAR>S : Type v<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : Ring S<VAR>inst✝⁶ : Algebra R S<VAR>R' : Type w'<VAR>S'✝ : Type v'<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : Ring S'✝<VAR>inst✝³ : Algebra R' S'✝<VAR>S' : Type v<VAR>inst✝² : CommRing R'<VAR>inst✝¹ : Ring S'<VAR>inst✝ : Algebra R' S'<VAR>i : R ≃+* R'<VAR>j : S ≃+* S'<VAR>hc : (algebraMap R' S').comp i.toRingHom = j.toRingHom.comp (algebraMap R S)<GOAL>Module.rank R S = Module.rank R' S'