ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>D : Type u'<VAR>inst✝¹ : Category.{v', u'} D<VAR>inst✝ : Preadditive D<VAR>K : CochainComplex C ℤ<VAR>a b p : ℤ<GOAL>p + b + a = p + a + b
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>D : Type u'<VAR>inst✝¹ : Category.{v', u'} D<VAR>inst✝ : Preadditive D<VAR>K : CochainComplex C ℤ<VAR>a b p : ℤ<GOAL>((shiftFunctorComm (CochainComplex C ℤ) a b).hom.app K).f p = (XIsoOfEq K ⋯).hom
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>D : Type u'<VAR>inst✝¹ : Category.{v', u'} D<VAR>inst✝ : Preadditive D<VAR>K : CochainComplex C ℤ<VAR>a b p : ℤ<GOAL>(((CategoryTheory.shiftFunctorAdd' (CochainComplex C ℤ) a b (a + b) ⋯).symm ≪≫ CategoryTheory.shiftFunctorAdd' (CochainComplex C ℤ) b a (a + b) ⋯).hom.app K).f p = (XIsoOfEq K ⋯).hom
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>D : Type u'<VAR>inst✝¹ : Category.{v', u'} D<VAR>inst✝ : Preadditive D<VAR>K : CochainComplex C ℤ<VAR>a b p : ℤ<GOAL>((CategoryTheory.shiftFunctorAdd' (CochainComplex C ℤ) a b (a + b) ⋯).inv.app K).f p ≫ ((CategoryTheory.shiftFunctorAdd' (CochainComplex C ℤ) b a (a + b) ⋯).hom.app K).f p = (XIsoOfEq K ⋯).hom
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>D : Type u'<VAR>inst✝¹ : Category.{v', u'} D<VAR>inst✝ : Preadditive D<VAR>K : CochainComplex C ℤ<VAR>a b p : ℤ<GOAL>(XIsoOfEq K ⋯).hom ≫ (XIsoOfEq K ⋯).hom = (XIsoOfEq K ⋯).hom
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type u_4<VAR>inst✝⁷ : Fintype l<VAR>inst✝⁶ : Fintype m<VAR>inst✝⁵ : Fintype n<VAR>inst✝⁴ : DecidableEq l<VAR>inst✝³ : DecidableEq m<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : CommRing α<VAR>A : Matrix l m α<VAR>B : Matrix l n α<VAR>C : Matrix n m α<VAR>D : Matrix n n α<VAR>inst✝ : Invertible D<GOAL>(reindex (Equiv.sumComm l n) (Equiv.sumComm m n)) (fromBlocks A B C D) = (reindex (Equiv.sumComm l n) (Equiv.sumComm m n)) (fromBlocks 1 (B * ⅟D) 0 1 * fromBlocks (A - B * ⅟D * C) 0 0 D * fromBlocks 1 0 (⅟D * C) 1)
<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>h_meas : ∀ (n : ℕ), AEMeasurable (f n) μ<VAR>h_anti : ∀ᵐ (a : α) ∂μ, Antitone fun i => f i a<VAR>h_fin : ∫⁻ (a : α), f 0 a ∂μ ≠ ⊤<GOAL>∫⁻ (a : α), ⨅ n, f n a ∂μ = ⨅ n, ∫⁻ (a : α), f n a ∂μ
<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>h_meas : ∀ (n : ℕ), AEMeasurable (f n) μ<VAR>h_anti : ∀ᵐ (a : α) ∂μ, Antitone fun i => f i a<VAR>h_fin : ∫⁻ (a : α), f 0 a ∂μ ≠ ⊤<GOAL>∫⁻ (a : α), (⨅ i, f i) a ∂μ = ⨅ n, ∫⁻ (a : α), f n a ∂μ
<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>h_meas : ∀ (n : ℕ), AEMeasurable (f n) μ<VAR>h_anti : ∀ᵐ (a : α) ∂μ, Antitone fun i => f i a<VAR>h_fin : ∫⁻ (a : α), f 0 a ∂μ ≠ ⊤<VAR>p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' => Antitone f'<VAR>hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x<VAR>h_ae_seq_mono : Antitone (aeSeq h_meas p)<GOAL>∫⁻ (a : α), (⨅ i, f i) a ∂μ = ⨅ n, ∫⁻ (a : α), f n a ∂μ
<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>h_meas : ∀ (n : ℕ), AEMeasurable (f n) μ<VAR>h_anti : ∀ᵐ (a : α) ∂μ, Antitone fun i => f i a<VAR>h_fin : ∫⁻ (a : α), f 0 a ∂μ ≠ ⊤<VAR>p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' => Antitone f'<VAR>hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x<VAR>h_ae_seq_mono : Antitone (aeSeq h_meas p)<GOAL>∫⁻ (a : α), (⨅ n, aeSeq h_meas p n) a ∂μ = ⨅ n, ∫⁻ (a : α), f n a ∂μ
<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>h_meas : ∀ (n : ℕ), AEMeasurable (f n) μ<VAR>h_anti : ∀ᵐ (a : α) ∂μ, Antitone fun i => f i a<VAR>h_fin : ∫⁻ (a : α), f 0 a ∂μ ≠ ⊤<VAR>p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' => Antitone f'<VAR>hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x<VAR>h_ae_seq_mono : Antitone (aeSeq h_meas p)<GOAL>∫⁻ (a : α), ⨅ i, aeSeq h_meas p i a ∂μ = ⨅ n, ∫⁻ (a : α), f n a ∂μ
<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>h_meas : ∀ (n : ℕ), AEMeasurable (f n) μ<VAR>h_anti : ∀ᵐ (a : α) ∂μ, Antitone fun i => f i a<VAR>h_fin : ∫⁻ (a : α), f 0 a ∂μ ≠ ⊤<VAR>p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' => Antitone f'<VAR>hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x<VAR>h_ae_seq_mono : Antitone (aeSeq h_meas p)<GOAL>⨅ n, ∫⁻ (a : α), aeSeq h_meas p n a ∂μ = ⨅ n, ∫⁻ (a : α), f n a ∂μ
<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>h_meas : ∀ (n : ℕ), AEMeasurable (f n) μ<VAR>h_anti : ∀ᵐ (a : α) ∂μ, Antitone fun i => f i a<VAR>h_fin : ∫⁻ (a : α), f 0 a ∂μ ≠ ⊤<VAR>p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' => Antitone f'<VAR>hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x<VAR>h_ae_seq_mono : Antitone (aeSeq h_meas p)<GOAL>∫⁻ (a : α), aeSeq h_meas p 0 a ∂μ ≠ ⊤
<VAR>N : ℕ<VAR>inst✝¹ : NeZero N<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>e : AddChar (ZMod N) R<VAR>χ : DirichletCharacter R N<VAR>d : ℕ<VAR>hd : d ∣ N<VAR>he : e.mulShift ↑d = 1<VAR>u : (ZMod N)ˣ<VAR>hu : (ZMod.unitsMap hd) u = 1<GOAL>χ ↑u * gaussSum χ e = gaussSum χ e
<VAR>N : ℕ<VAR>inst✝¹ : NeZero N<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>e : AddChar (ZMod N) R<VAR>χ : DirichletCharacter R N<VAR>d : ℕ<VAR>hd : d ∣ N<VAR>he : e.mulShift ↑d = 1<VAR>u : (ZMod N)ˣ<VAR>hu : (ZMod.unitsMap hd) u = 1<GOAL>e.mulShift ↑u = e
<VAR>N : ℕ<VAR>inst✝¹ : NeZero N<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>e : AddChar (ZMod N) R<VAR>χ : DirichletCharacter R N<VAR>d : ℕ<VAR>hd : d ∣ N<VAR>he : e.mulShift ↑d = 1<VAR>u : (ZMod N)ˣ<VAR>hu : (ZMod.unitsMap hd) u = 1<GOAL>e.mulShift (↑u - 1) = 1
<VAR>N : ℕ<VAR>inst✝¹ : NeZero N<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>e : AddChar (ZMod N) R<VAR>χ : DirichletCharacter R N<VAR>d : ℕ<VAR>hd : d ∣ N<VAR>he : e.mulShift ↑d = 1<VAR>u : (ZMod N)ˣ<VAR>hu : (ZMod.unitsMap hd) u = 1<GOAL>↑d ∣ ↑(↑u).val - 1
<VAR>N : ℕ<VAR>inst✝¹ : NeZero N<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>e : AddChar (ZMod N) R<VAR>χ : DirichletCharacter R N<VAR>d : ℕ<VAR>hd : d ∣ N<VAR>he : e.mulShift ↑d = 1<VAR>u : (ZMod N)ˣ<VAR>hu : ↑(ZMod.castHom hd (ZMod d)) ↑u = 1<GOAL>↑d ∣ ↑(↑u).val - 1
<VAR>N : ℕ<VAR>inst✝¹ : NeZero N<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>e : AddChar (ZMod N) R<VAR>χ : DirichletCharacter R N<VAR>d : ℕ<VAR>hd : d ∣ N<VAR>he : e.mulShift ↑d = 1<VAR>u : (ZMod N)ˣ<VAR>hu : ↑(ZMod.castHom hd (ZMod d)) ↑u = 1<VAR>this : (ZMod.castHom hd (ZMod d)) ↑u = ↑↑(↑u).val<GOAL>↑d ∣ ↑(↑u).val - 1
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : WSeq α<GOAL>(ret s).join ~ʷ s
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁷ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁶ : NormedAddCommGroup E<VAR>inst✝¹⁵ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹⁴ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹³ : TopologicalSpace M<VAR>inst✝¹² : ChartedSpace H M<VAR>inst✝¹¹ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝¹⁰ : NormedAddCommGroup E'<VAR>inst✝⁹ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁷ : TopologicalSpace M'<VAR>inst✝⁶ : ChartedSpace H' M'<VAR>inst✝⁵ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝¹ : TopologicalSpace M''<VAR>inst✝ : ChartedSpace H'' M''<VAR>e : PartialHomeomorph M H<VAR>e' : PartialHomeomorph M' H'<VAR>f f₁ : M → M'<VAR>s s₁ t✝ : Set M<VAR>x✝ : M<VAR>m n : ℕ∞<VAR>t : Set M'<VAR>g : M' → M''<VAR>x : M<VAR>hf : ContMDiffWithinAt I I' n f s x<VAR>st : MapsTo f s t<VAR>hg : ContMDiffWithinAt I' I'' n g t (f x)<GOAL>ContMDiffWithinAt I I'' n (g ∘ f) s x
<VAR>α : Type u_2<VAR>n : ℕ<VAR>β : Type u_1<VAR>xs : Vector α n<VAR>ys : Vector β n<VAR>σ : Type<VAR>s : σ<VAR>f : α → σ × σ → (σ × σ) × β<VAR>h : ∀ (x : α) (s : σ), (f x (s, s)).1.1 = (f x (s, s)).1.2<GOAL>∃ R, R (s, s) s ∧ ∀ {s : σ × σ} {q : σ} (a : α), R s q → R (f a s).1 ((f a (q, q)).1.1, (f a (q, q)).2).1 ∧ (f a s).2 = ((f a (q, q)).1.1, (f a (q, q)).2).2
<VAR>α : Type u_2<VAR>n : ℕ<VAR>β : Type u_1<VAR>xs : Vector α n<VAR>ys : Vector β n<VAR>σ : Type<VAR>s : σ<VAR>f : α → σ × σ → (σ × σ) × β<VAR>h : ∀ (x : α) (s : σ), (f x (s, s)).1.1 = (f x (s, s)).1.2<GOAL>(match (s, s) with | (s₁, s₂) => s₂ = s ∧ s₁ = s) ∧ ∀ {s : σ × σ} {q : σ} (a : α), (match s with | (s₁, s₂) => s₂ = q ∧ s₁ = q) → (match (f a s).1 with | (s₁, s₂) => s₂ = ((f a (q, q)).1.1, (f a (q, q)).2).1 ∧ s₁ = ((f a (q, q)).1.1, (f a (q, q)).2).1) ∧ (f a s).2 = ((f a (q, q)).1.1, (f a (q, q)).2).2
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : Nontrivial R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module.Free R M<VAR>inst✝ : Module.Finite R M<VAR>f : M →ₗ[R] M<VAR>hf : Function.Injective ⇑f<VAR>h : (minpoly R f).coeff 0 = 0<GOAL>False
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : Nontrivial R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module.Free R M<VAR>inst✝ : Module.Finite R M<VAR>f : M →ₗ[R] M<VAR>hf : Function.Injective ⇑f<VAR>h : (minpoly R f).coeff 0 = 0<VAR>P : R[X]<VAR>hP : minpoly R f = X * P<GOAL>False
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : Nontrivial R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module.Free R M<VAR>inst✝ : Module.Finite R M<VAR>f : M →ₗ[R] M<VAR>hf : Function.Injective ⇑f<VAR>h : (minpoly R f).coeff 0 = 0<VAR>P : R[X]<VAR>hP : minpoly R f = X * P<VAR>hdegP : P.degree < (minpoly R f).degree<GOAL>False
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : Nontrivial R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module.Free R M<VAR>inst✝ : Module.Finite R M<VAR>f : M →ₗ[R] M<VAR>hf : Function.Injective ⇑f<VAR>h : (minpoly R f).coeff 0 = 0<VAR>P : R[X]<VAR>hP : minpoly R f = X * P<VAR>hdegP : P.degree < (minpoly R f).degree<VAR>hPmonic : P.Monic<GOAL>False
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : Nontrivial R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module.Free R M<VAR>inst✝ : Module.Finite R M<VAR>f : M →ₗ[R] M<VAR>hf : Function.Injective ⇑f<VAR>h : (minpoly R f).coeff 0 = 0<VAR>P : R[X]<VAR>hP : minpoly R f = X * P<VAR>hdegP : P.degree < (minpoly R f).degree<VAR>hPmonic : P.Monic<VAR>hzero : (aeval f) (minpoly R f) = 0<GOAL>False
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : Nontrivial R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module.Free R M<VAR>inst✝ : Module.Finite R M<VAR>f : M →ₗ[R] M<VAR>hf : Function.Injective ⇑f<VAR>h : (minpoly R f).coeff 0 = 0<VAR>P : R[X]<VAR>hP : minpoly R f = X * P<VAR>hdegP : P.degree < (minpoly R f).degree<VAR>hPmonic : P.Monic<VAR>hzero : ∀ (x : M), ((aeval f) P) x = 0<GOAL>False
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝ : BooleanAlgebra α<VAR>s : Finset ι<VAR>hs : s.Nonempty<VAR>f : ι → α<VAR>a : α<GOAL>(s.inf fun b => a \ f b) = a \ s.sup f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>inst✝ : ConditionallyCompleteLinearOrder α<VAR>s t : Set α<VAR>a b : α<VAR>f : ι → α<GOAL>sSup (⋃ i, Iic (f i)) = ⨆ i, f i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>inst✝ : ConditionallyCompleteLinearOrder α<VAR>s t : Set α<VAR>a b : α<VAR>f : ι → α<GOAL>∀ x ∈ ⋃ i, Iic (f i), ∃ y ∈ range fun i => f i, x ≤ y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>inst✝ : ConditionallyCompleteLinearOrder α<VAR>s t : Set α<VAR>a b : α<VAR>f : ι → α<GOAL>∀ y ∈ range fun i => f i, ∃ x ∈ ⋃ i, Iic (f i), y ≤ x
<VAR>μ : Measure ℝ<VAR>inst✝ : NoAtoms μ<VAR>s : Set ℝ<VAR>p : ℝ → Prop<VAR>h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ, x ∈ s ∩ Ioo a b → p x<VAR>T : ↑s × ↑s → Set ℝ := fun p => Ioo ↑p.1 ↑p.2<VAR>u : Set ℝ := ⋃ i, T i<GOAL>∀ᵐ (x : ℝ) ∂μ, x ∈ s → p x
<VAR>μ : Measure ℝ<VAR>inst✝ : NoAtoms μ<VAR>s : Set ℝ<VAR>p : ℝ → Prop<VAR>h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ, x ∈ s ∩ Ioo a b → p x<VAR>T : ↑s × ↑s → Set ℝ := fun p => Ioo ↑p.1 ↑p.2<VAR>u : Set ℝ := ⋃ i, T i<VAR>hfinite : (s \ u).Finite<GOAL>∀ᵐ (x : ℝ) ∂μ, x ∈ s → p x
<VAR>μ : Measure ℝ<VAR>inst✝ : NoAtoms μ<VAR>s : Set ℝ<VAR>p : ℝ → Prop<VAR>h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ, x ∈ s ∩ Ioo a b → p x<VAR>T : ↑s × ↑s → Set ℝ := fun p => Ioo ↑p.1 ↑p.2<VAR>u : Set ℝ := ⋃ i, T i<VAR>hfinite : (s \ u).Finite<VAR>A : Set (↑s × ↑s)<VAR>A_count : A.Countable<VAR>hA : ⋃ i ∈ A, T i = ⋃ i, T i<GOAL>∀ᵐ (x : ℝ) ∂μ, x ∈ s → p x
<VAR>μ : Measure ℝ<VAR>inst✝ : NoAtoms μ<VAR>s : Set ℝ<VAR>p : ℝ → Prop<VAR>h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ, x ∈ s ∩ Ioo a b → p x<VAR>T : ↑s × ↑s → Set ℝ := fun p => Ioo ↑p.1 ↑p.2<VAR>u : Set ℝ := ⋃ i, T i<VAR>hfinite : (s \ u).Finite<VAR>A : Set (↑s × ↑s)<VAR>A_count : A.Countable<VAR>hA : ⋃ i ∈ A, T i = ⋃ i, T i<VAR>M : ∀ᵐ (x : ℝ) ∂μ, x ∉ s \ u<GOAL>∀ᵐ (x : ℝ) ∂μ, x ∈ s → p x
<VAR>μ : Measure ℝ<VAR>inst✝ : NoAtoms μ<VAR>s : Set ℝ<VAR>p : ℝ → Prop<VAR>h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ, x ∈ s ∩ Ioo a b → p x<VAR>T : ↑s × ↑s → Set ℝ := fun p => Ioo ↑p.1 ↑p.2<VAR>u : Set ℝ := ⋃ i, T i<VAR>hfinite : (s \ u).Finite<VAR>A : Set (↑s × ↑s)<VAR>A_count : A.Countable<VAR>hA : ⋃ i ∈ A, T i = ⋃ i, T i<VAR>M : ∀ᵐ (x : ℝ) ∂μ, x ∉ s \ u<VAR>M' : ∀ᵐ (x : ℝ) ∂μ, ∀ i ∈ A, x ∈ s ∩ T i → p x<GOAL>∀ᵐ (x : ℝ) ∂μ, x ∈ s → p x
<VAR>μ : Measure ℝ<VAR>inst✝ : NoAtoms μ<VAR>s : Set ℝ<VAR>p : ℝ → Prop<VAR>h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ, x ∈ s ∩ Ioo a b → p x<VAR>T : ↑s × ↑s → Set ℝ := fun p => Ioo ↑p.1 ↑p.2<VAR>u : Set ℝ := ⋃ i, T i<VAR>hfinite : (s \ u).Finite<VAR>A : Set (↑s × ↑s)<VAR>A_count : A.Countable<VAR>hA : ⋃ i ∈ A, T i = ⋃ i, T i<VAR>M : ∀ᵐ (x : ℝ) ∂μ, x ∉ s \ u<VAR>M' : ∀ᵐ (x : ℝ) ∂μ, ∀ i ∈ A, x ∈ s ∩ T i → p x<VAR>x : ℝ<VAR>hx : x ∉ s \ u<VAR>h'x : ∀ i ∈ A, x ∈ s ∩ T i → p x<GOAL>x ∈ s → p x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>M₂ : Type u_3<VAR>M₃ : Type u_4<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>f : M →ₗ[R] M₂<VAR>p p' : Submodule R M<GOAL>comap p.subtype (p ⊓ p') ≤ ker (subToSupQuotient p p')
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>M₂ : Type u_3<VAR>M₃ : Type u_4<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>f : M →ₗ[R] M₂<VAR>p p' : Submodule R M<GOAL>comap p.subtype (p ⊓ p') ≤ comap p.subtype ((p ⊔ p') ⊓ p')
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LinearOrder β<VAR>f : α → β<VAR>s : Set α<VAR>a a₁ a₂ b b₁ b₂ c d x : α<GOAL>b ∈ Ι a b ↔ a < b
<VAR>n' : Type u_1<VAR>inst✝² : DecidableEq n'<VAR>inst✝¹ : Fintype n'<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>A : M<VAR>n : ℕ<GOAL>A⁻¹ ^ ↑n = (A ^ ↑n)⁻¹
<VAR>n' : Type u_1<VAR>inst✝² : DecidableEq n'<VAR>inst✝¹ : Fintype n'<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>A : M<VAR>n : ℕ<GOAL>A⁻¹ ^ -[n+1] = (A ^ -[n+1])⁻¹
<VAR>n : ℕ<VAR>A : Type u_1<VAR>R : Type u_2<VAR>inst✝⁴ : AddGroup A<VAR>inst✝³ : Ring R<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝² : Group α<VAR>a : α<VAR>inst✝¹ : MulAction α β<VAR>b : β<VAR>inst✝ : Fintype ↑(orbit (↥(zpowers a)) b)<GOAL>minimalPeriod (fun x => a • x) b = Fintype.card ↑(orbit (↥(zpowers a)) b)
<VAR>p : ℕ<VAR>R✝ : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝ : CommRing R✝<VAR>n : ℕ<VAR>R : Type u_2<VAR>_Rcr : CommRing R<VAR>x : 𝕎 R<GOAL>(x * ↑n).coeff = fun n_1 => (aeval x.coeff) (wittMulN p n n_1)
<VAR>p : ℕ<VAR>R✝ : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝ : CommRing R✝<VAR>n : ℕ<VAR>R : Type u_2<VAR>_Rcr : CommRing R<VAR>x : 𝕎 R<VAR>k : ℕ<GOAL>(x * ↑n).coeff k = (aeval x.coeff) (wittMulN p n k)
<VAR>X : Type u_1<VAR>s : Set X<GOAL>(some '' s)ᶜ = some '' 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>variance f μ = variance 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 ν).toReal = variance g ν
<VAR>R : Type u_1<VAR>inst✝¹⁸ : CommSemiring R<VAR>R' : Type u_2<VAR>inst✝¹⁷ : Monoid R'<VAR>R'' : Type u_3<VAR>inst✝¹⁶ : Semiring R''<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>S : Type u_8<VAR>T : Type u_9<VAR>inst✝¹⁵ : AddCommMonoid M<VAR>inst✝¹⁴ : AddCommMonoid N<VAR>inst✝¹³ : AddCommMonoid P<VAR>inst✝¹² : AddCommMonoid Q<VAR>inst✝¹¹ : AddCommMonoid S<VAR>inst✝¹⁰ : AddCommMonoid T<VAR>inst✝⁹ : Module R M<VAR>inst✝⁸ : Module R N<VAR>inst✝⁷ : Module R P<VAR>inst✝⁶ : Module R Q<VAR>inst✝⁵ : Module R S<VAR>inst✝⁴ : Module R T<VAR>inst✝³ : DistribMulAction R' M<VAR>inst✝² : Module R'' M<VAR>inst✝¹ : SMulCommClass R R' M<VAR>inst✝ : SMulCommClass R R'' M<GOAL>Submodule.map₂ (mk R M N) ⊤ ⊤ = ⊤
<VAR>R : Type u_1<VAR>inst✝¹⁸ : CommSemiring R<VAR>R' : Type u_2<VAR>inst✝¹⁷ : Monoid R'<VAR>R'' : Type u_3<VAR>inst✝¹⁶ : Semiring R''<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>S : Type u_8<VAR>T : Type u_9<VAR>inst✝¹⁵ : AddCommMonoid M<VAR>inst✝¹⁴ : AddCommMonoid N<VAR>inst✝¹³ : AddCommMonoid P<VAR>inst✝¹² : AddCommMonoid Q<VAR>inst✝¹¹ : AddCommMonoid S<VAR>inst✝¹⁰ : AddCommMonoid T<VAR>inst✝⁹ : Module R M<VAR>inst✝⁸ : Module R N<VAR>inst✝⁷ : Module R P<VAR>inst✝⁶ : Module R Q<VAR>inst✝⁵ : Module R S<VAR>inst✝⁴ : Module R T<VAR>inst✝³ : DistribMulAction R' M<VAR>inst✝² : Module R'' M<VAR>inst✝¹ : SMulCommClass R R' M<VAR>inst✝ : SMulCommClass R R'' M<GOAL>Submodule.span R {t | ∃ m n, m ⊗ₜ[R] n = t} ≤ Submodule.span R (Set.image2 (fun m n => ((mk R M N) m) n) ↑⊤ ↑⊤)
<VAR>a : UnitAddCircle<GOAL>Tendsto (fun s => hurwitzZeta a s - 1 / (s - 1) / s.Gammaℝ) (𝓝 1) (𝓝 (hurwitzZeta a 1))
<VAR>a : UnitAddCircle<GOAL>Tendsto (fun s => hurwitzZetaEven a s - 1 / (s - 1) / s.Gammaℝ + hurwitzZetaOdd a s) (𝓝 1) (𝓝 (hurwitzZetaEven a 1 + hurwitzZetaOdd a 1))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f : α → ℝ≥0∞<VAR>hf : ∀ᵐ (x : α) ∂μ, f x < ⊤<GOAL>(fun x => ↑(f x).toNNReal) =ᶠ[ae μ] f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f : α → ℝ≥0∞<VAR>hf : ∀ᵐ (x : α) ∂μ, f x < ⊤<GOAL>∀ (a : α), f a < ⊤ → ↑(f a).toNNReal = f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f : α → ℝ≥0∞<VAR>hf : ∀ᵐ (x : α) ∂μ, f x < ⊤<VAR>x : α<VAR>hx : f x < ⊤<GOAL>↑(f x).toNNReal = f x
<VAR>E : Type u_1<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module ℝ E<VAR>inst✝³ : TopologicalSpace E<VAR>inst✝² : T1Space E<VAR>inst✝¹ : TopologicalAddGroup E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>s✝ t✝ s t : Set E<VAR>hsc : Convex ℝ s<VAR>hs₀ : s ∈ 𝓝 0<VAR>hsb : IsVonNBounded ℝ s<VAR>htc : Convex ℝ t<VAR>ht₀ : t ∈ 𝓝 0<VAR>htb : IsVonNBounded ℝ t<GOAL>⇑(gaugeRescaleHomeomorph s t hsc hs₀ hsb htc ht₀ htb) '' closure s = closure t
<VAR>E : Type u_1<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module ℝ E<VAR>inst✝³ : TopologicalSpace E<VAR>inst✝² : T1Space E<VAR>inst✝¹ : TopologicalAddGroup E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>s✝ t✝ s t : Set E<VAR>hsc : Convex ℝ s<VAR>hs₀ : s ∈ 𝓝 0<VAR>hsb : IsVonNBounded ℝ s<VAR>htc : Convex ℝ t<VAR>ht₀ : t ∈ 𝓝 0<VAR>htb : IsVonNBounded ℝ t<GOAL>closure t ⊆ ⇑(gaugeRescaleHomeomorph s t hsc hs₀ hsb htc ht₀ htb) '' closure s
<VAR>E : Type u_1<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module ℝ E<VAR>inst✝³ : TopologicalSpace E<VAR>inst✝² : T1Space E<VAR>inst✝¹ : TopologicalAddGroup E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>s✝ t✝ s t : Set E<VAR>hsc : Convex ℝ s<VAR>hs₀ : s ∈ 𝓝 0<VAR>hsb : IsVonNBounded ℝ s<VAR>htc : Convex ℝ t<VAR>ht₀ : t ∈ 𝓝 0<VAR>htb : IsVonNBounded ℝ t<GOAL>⇑(gaugeRescaleHomeomorph s t hsc hs₀ hsb htc ht₀ htb).symm '' closure t ⊆ closure s
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝ : MonoidWithZero M₀<VAR>u : M₀ˣ<VAR>a : M₀<VAR>h : a * ↑u = 0<GOAL>a = 0
<VAR>B : Type u<VAR>F : Type v<VAR>E : B → Type w₁<VAR>B' : Type w₂<VAR>f✝ : B' → B<VAR>inst✝¹ : TopologicalSpace B'<VAR>inst✝ : TopologicalSpace (TotalSpace F E)<VAR>f : B' → B<GOAL>Continuous (Pullback.lift f)
<VAR>B : Type u<VAR>F : Type v<VAR>E : B → Type w₁<VAR>B' : Type w₂<VAR>f✝ : B' → B<VAR>inst✝¹ : TopologicalSpace B'<VAR>inst✝ : TopologicalSpace (TotalSpace F E)<VAR>f : B' → B<GOAL>induced TotalSpace.proj inst✝¹ ⊓ induced (Pullback.lift f) inst✝ ≤ induced (Pullback.lift f) inst✝
<VAR>x : ℝ*<VAR>r : ℝ<VAR>hxr : x.IsSt r<VAR>h : ∃ r, x.IsSt r<GOAL>x.st = r
<VAR>x : ℝ*<VAR>r : ℝ<VAR>hxr : x.IsSt r<VAR>h : ∃ r, x.IsSt r<GOAL>Classical.choose h = r
<VAR>t : ℝ<GOAL>Tendsto (fun x => x * log (1 + t / x)) atTop (𝓝 t)
<VAR>t : ℝ<VAR>h₁ : Tendsto (fun h => h⁻¹ * log (1 + t * h)) (𝓝[≠] 0) (𝓝 t)<GOAL>Tendsto (fun x => x * log (1 + t / x)) atTop (𝓝 t)
<VAR>t : ℝ<VAR>h₁ : Tendsto (fun h => h⁻¹ * log (1 + t * h)) (𝓝[≠] 0) (𝓝 t)<VAR>h₂ : Tendsto (fun x => x⁻¹) atTop (𝓝[≠] 0)<GOAL>Tendsto (fun x => x * log (1 + t / x)) atTop (𝓝 t)
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>β : Type u<VAR>g : β → F (α ::: β)<VAR>x : β<GOAL>(TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) (corecF g x)) = (TypeVec.id ::: corec g) <$$> g x
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>β : Type u<VAR>g : β → F (α ::: β)<VAR>x : β<GOAL>(TypeVec.id ⊚ TypeVec.id ::: Quot.mk Mcongr ∘ corecF g) <$$> g x = (TypeVec.id ::: corec g) <$$> g x
<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>b : OrthonormalBasis ι 𝕜 E<VAR>x : E<GOAL>∑ i : ι, b.repr x i • b i = x
<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>b : OrthonormalBasis ι 𝕜 E<VAR>x : E<GOAL>∑ x_1 : ι, (b.toBasis.repr x) x_1 • b.toBasis x_1 = x
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝² : Category.{v₂, u₂} D<VAR>inst✝¹ : HasPullbacks C<VAR>𝒢 : Set C<VAR>inst✝ : Small.{v₁, u₁} ↑𝒢<VAR>h𝒢 : IsDetecting 𝒢<VAR>X : C<VAR>P Q : Subobject X<VAR>h : (fun P => {f | P.Factors f.snd}) P = (fun P => {f | P.Factors f.snd}) Q<GOAL>∀ G ∈ 𝒢, ∀ {f : G ⟶ X}, P.Factors f ↔ Q.Factors f