ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace ℝ F<VAR>inst✝⁶ : NormedAddCommGroup F'<VAR>inst✝⁵ : NormedSpace ℝ F'<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝³ : NontriviallyNormedField 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>hT' : DominatedFinMeasAdditive μ T' C'<VAR>hT'' : DominatedFinMeasAdditive μ T'' C''<VAR>h_add : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T'' s = T s + T' s<VAR>f : ↥(Lp E 1 μ)<GOAL>(setToL1 hT'') f = (setToL1 hT) f + (setToL1 hT') f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace ℝ F<VAR>inst✝⁶ : NormedAddCommGroup F'<VAR>inst✝⁵ : NormedSpace ℝ F'<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝³ : NontriviallyNormedField 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>hT' : DominatedFinMeasAdditive μ T' C'<VAR>hT'' : DominatedFinMeasAdditive μ T'' C''<VAR>h_add : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T'' s = T s + T' s<VAR>f : ↥(Lp E 1 μ)<GOAL>setToL1 hT'' = setToL1 hT + setToL1 hT'
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace ℝ F<VAR>inst✝⁶ : NormedAddCommGroup F'<VAR>inst✝⁵ : NormedSpace ℝ F'<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝³ : NontriviallyNormedField 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>hT' : DominatedFinMeasAdditive μ T' C'<VAR>hT'' : DominatedFinMeasAdditive μ T'' C''<VAR>h_add : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T'' s = T s + T' s<VAR>f : ↥(Lp E 1 μ)<GOAL>(setToL1 hT + setToL1 hT').comp (coeToLp α E ℝ) = setToL1SCLM α E μ hT''
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace ℝ F<VAR>inst✝⁶ : NormedAddCommGroup F'<VAR>inst✝⁵ : NormedSpace ℝ F'<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝³ : NontriviallyNormedField 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>hT' : DominatedFinMeasAdditive μ T' C'<VAR>hT'' : DominatedFinMeasAdditive μ T'' C''<VAR>h_add : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T'' s = T s + T' s<VAR>f✝ : ↥(Lp E 1 μ)<VAR>f : ↥(simpleFunc E 1 μ)<GOAL>(setToL1 hT) ↑f + (setToL1 hT') ↑f = (setToL1SCLM α E μ hT'') f
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁵ : CommRing P<VAR>inst✝⁴ : Algebra R P<VAR>loc : IsLocalization S P<VAR>R₁ : Type u_3<VAR>inst✝³ : CommRing R₁<VAR>K : Type u_4<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R₁ K<VAR>inst✝ : IsFractionRing R₁ K<VAR>x✝ : P<GOAL>x✝ ∈ spanSingleton S 1 ↔ x✝ ∈ 1
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁵ : CommRing P<VAR>inst✝⁴ : Algebra R P<VAR>loc : IsLocalization S P<VAR>R₁ : Type u_3<VAR>inst✝³ : CommRing R₁<VAR>K : Type u_4<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R₁ K<VAR>inst✝ : IsFractionRing R₁ K<VAR>x✝ : P<GOAL>∀ (a : R), a • 1 = x✝ ↔ (algebraMap R P) a = x✝
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁵ : CommRing P<VAR>inst✝⁴ : Algebra R P<VAR>loc : IsLocalization S P<VAR>R₁ : Type u_3<VAR>inst✝³ : CommRing R₁<VAR>K : Type u_4<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R₁ K<VAR>inst✝ : IsFractionRing R₁ K<VAR>x✝ : P<VAR>x' : R<GOAL>x' • 1 = x✝ ↔ (algebraMap R P) x' = x✝
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>f : C(AddCircle T, ℂ)<VAR>h : Summable (fourierCoeff ⇑f)<VAR>x : AddCircle T<GOAL>HasSum (fun i => fourierCoeff (⇑f) i • (fourier i) x) (f x)
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℂ → E<GOAL>AnalyticOn ℂ f univ ↔ Differentiable ℂ f
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℂ → E<GOAL>AnalyticOn ℂ f univ ↔ DifferentiableOn ℂ f univ
<VAR>X : Type u_1<VAR>inst✝³ : MeasurableSpace X<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : OpensMeasurableSpace X<VAR>μ✝ : Measure X<VAR>inst✝ : IsFiniteMeasure μ✝<VAR>f : X →ᵇ ℝ≥0<VAR>μ : Measure X<GOAL>(∫⁻ (x : X), ↑(f x) ∂μ).toReal = ∫ (x : X), ↑(f x) ∂μ
<VAR>X : Type u_1<VAR>inst✝³ : MeasurableSpace X<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : OpensMeasurableSpace X<VAR>μ✝ : Measure X<VAR>inst✝ : IsFiniteMeasure μ✝<VAR>f : X →ᵇ ℝ≥0<VAR>μ : Measure X<GOAL>(∫⁻ (x : X), ↑(f x) ∂μ).toReal = (∫⁻ (a : X), ENNReal.ofReal ↑(f a) ∂μ).toReal
<VAR>X : Type u_1<VAR>inst✝³ : MeasurableSpace X<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : OpensMeasurableSpace X<VAR>μ✝ : Measure X<VAR>inst✝ : IsFiniteMeasure μ✝<VAR>f : X →ᵇ ℝ≥0<VAR>μ : Measure X<GOAL>0 ≤ᶠ[ae μ] fun x => ↑(f x)
<VAR>K : Type uK<VAR>V : Type uV<VAR>inst✝³ : CommRing K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : Free K V<GOAL>Function.Surjective (comap (eval K V))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f g : α → β<VAR>c c₁ c₂ x : α<VAR>inst✝¹ : AddZeroClass α<VAR>inst✝ : Neg β<VAR>h : Antiperiodic f c<GOAL>f c = -f 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>p : α → Prop<VAR>inst✝² : DecidablePred p<VAR>x✝ : Monoid R<VAR>inst✝¹ : AddMonoid M<VAR>inst✝ : DistribMulAction R M<VAR>b : R<VAR>v : α →₀ M<GOAL>(fun f => ⇑f) (filter p (b • v)) = (fun f => ⇑f) (b • filter p v)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>p : α → Prop<VAR>inst✝² : DecidablePred p<VAR>x✝ : Monoid R<VAR>inst✝¹ : AddMonoid M<VAR>inst✝ : DistribMulAction R M<VAR>b : R<VAR>v : α →₀ M<GOAL>{x | p x}.indicator (b • ⇑v) = b • {x | p x}.indicator ⇑v
<VAR>M : Type u_1<VAR>X : Type u_2<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : Monoid M<VAR>inst✝ : TopologicalSpace X<GOAL>instTopologicalSpaceUnits = TopologicalSpace.induced val inst✝² ⊓ TopologicalSpace.induced (fun u => ↑u⁻¹) inst✝²
<VAR>M : Type u_1<VAR>X : Type u_2<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : Monoid M<VAR>inst✝ : TopologicalSpace X<GOAL>TopologicalSpace.induced (Prod.fst ∘ ⇑(embedProduct M)) inst✝² ⊓ TopologicalSpace.induced ((unop ∘ Prod.snd) ∘ ⇑(embedProduct M)) inst✝² = TopologicalSpace.induced val inst✝² ⊓ TopologicalSpace.induced (fun u => ↑u⁻¹) inst✝²
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : MulOneClass M<VAR>inst✝² : MulOneClass N<VAR>inst✝¹ : MulOneClass P<VAR>S : Submonoid M<VAR>A : Type u_4<VAR>inst✝ : SetLike A M<VAR>hA : SubmonoidClass A M<VAR>S' : A<GOAL>mrange (inl M N) ⊔ mrange (inr M N) = ⊤
<VAR>α : Type u_1<VAR>n : ℕ<VAR>s : Multiset α<VAR>l : List α<GOAL>powersetCard n ⟦l⟧ ≤ powerset ⟦l⟧
<VAR>α : Type u_1<VAR>n : ℕ<VAR>s : Multiset α<VAR>l : List α<GOAL>List.map ofList (sublistsLen n l) <+~ List.map ofList l.sublists'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : DistribLattice α<VAR>inst✝² : BoundedOrder α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableRel fun x x_1 => x ≤ x_1<VAR>s t : Finset α<VAR>a : α<VAR>ha : a ∉ lowerClosure ↑s ⊓ lowerClosure ↑t<GOAL>a ∉ lowerClosure ↑(s ⊼ t)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝¹ : Semiring R<VAR>p q r : R[X]<VAR>inst✝ : Semiring S<VAR>f : R →+* S<GOAL>map (RingHom.id R) p = p
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>N : Type w₁<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R N<VAR>inst✝¹ : LieRingModule L N<VAR>inst✝ : LieModule R L N<VAR>f : M →ₗ⁅R,L⁆ N<VAR>m✝ : N<GOAL>m✝ ∈ LieSubmodule.map f ⊤ ↔ m✝ ∈ f.range
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Ring S<VAR>inst✝ : Algebra R S<VAR>M N : Submodule R S<VAR>ι : Type u_1<VAR>m : Basis ι R ↥M<VAR>H : LinearMap.ker (mulLeftMap N ⇑m) = ⊥<VAR>this : AddCommGroup (ι →₀ ↥N) := Finsupp.instAddCommGroup<GOAL>M.LinearDisjoint N
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Monoid α<VAR>inst✝² : Monoid β<VAR>inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1<VAR>inst✝ : DecidableRel fun x x_1 => x ∣ x_1<VAR>a b : α<VAR>n : ℕ<GOAL>multiplicity a b = ↑n ↔ a ^ n ∣ b ∧ ¬a ^ (n + 1) ∣ b
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>R : Type u_5<VAR>inst✝³ : Fintype n<VAR>inst✝² : Fintype o<VAR>inst✝¹ : CommRing R<VAR>inst✝ : StrongRankCondition R<VAR>A : Matrix m n R<VAR>B : Matrix n o R<GOAL>(A * B).rank ≤ B.rank
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>R : Type u_5<VAR>inst✝³ : Fintype n<VAR>inst✝² : Fintype o<VAR>inst✝¹ : CommRing R<VAR>inst✝ : StrongRankCondition R<VAR>A : Matrix m n R<VAR>B : Matrix n o R<GOAL>finrank R ↥(LinearMap.range (A.mulVecLin ∘ₗ B.mulVecLin)) ≤ finrank R ↥(LinearMap.range B.mulVecLin)
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>x : M<VAR>p✝ p' : Submodule R M<VAR>inst✝⁴ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>s t : Set M<VAR>p : M → Prop<VAR>h : x ∈ span R s<VAR>zero : p 0<VAR>add : ∀ (x y : M), p x → p y → p (x + y)<VAR>smul_mem : ∀ (r : R), ∀ x ∈ s, p (r • x)<GOAL>p x
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>x : M<VAR>p✝ p' : Submodule R M<VAR>inst✝⁴ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>s t : Set M<VAR>p : M → Prop<VAR>h : x ∈ AddSubmonoid.closure (univ • s)<VAR>zero : p 0<VAR>add : ∀ (x y : M), p x → p y → p (x + y)<VAR>smul_mem : ∀ (r : R), ∀ x ∈ s, p (r • x)<GOAL>p x
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>x : M<VAR>p✝ p' : Submodule R M<VAR>inst✝⁴ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>s t : Set M<VAR>p : M → Prop<VAR>h : x ∈ AddSubmonoid.closure (univ • s)<VAR>zero : p 0<VAR>add : ∀ (x y : M), p x → p y → p (x + y)<VAR>smul_mem : ∀ (r : R), ∀ x ∈ s, p (r • x)<GOAL>∀ x ∈ univ • s, p x
<VAR>R : Type u_1<VAR>X : Type u_2<VAR>inst✝² : PseudoMetricSpace R<VAR>inst✝¹ : Mul R<VAR>inst✝ : BoundedMul R<VAR>f g : X → R<VAR>f_bdd : ∃ C, ∀ (x y : X), dist (f x) (f y) ≤ C<VAR>g_bdd : ∃ C, ∀ (x y : X), dist (g x) (g y) ≤ C<GOAL>∃ C, ∀ (x y : X), dist ((f * g) x) ((f * g) y) ≤ C
<VAR>R : Type u_1<VAR>X : Type u_2<VAR>inst✝² : PseudoMetricSpace R<VAR>inst✝¹ : Mul R<VAR>inst✝ : BoundedMul R<VAR>f g : X → R<VAR>f_bdd : ∃ C, ∀ (x y : X), dist (f x) (f y) ≤ C<VAR>g_bdd : ∃ C, ∀ (x y : X), dist (g x) (g y) ≤ C<VAR>C : ℝ<VAR>hC : ∀ ⦃x : R⦄, x ∈ range f * range g → ∀ ⦃y : R⦄, y ∈ range f * range g → dist x y ≤ C<GOAL>∃ C, ∀ (x y : X), dist ((f * g) x) ((f * g) y) ≤ C
<VAR>R : Type u_1<VAR>X : Type u_2<VAR>inst✝² : PseudoMetricSpace R<VAR>inst✝¹ : Mul R<VAR>inst✝ : BoundedMul R<VAR>f g : X → R<VAR>f_bdd : ∃ C, ∀ (x y : X), dist (f x) (f y) ≤ C<VAR>g_bdd : ∃ C, ∀ (x y : X), dist (g x) (g y) ≤ C<VAR>C : ℝ<VAR>hC : ∀ ⦃x : R⦄, x ∈ range f * range g → ∀ ⦃y : R⦄, y ∈ range f * range g → dist x y ≤ C<GOAL>∀ (x y : X), dist ((f * g) x) ((f * g) y) ≤ C
<VAR>R : Type u_1<VAR>X : Type u_2<VAR>inst✝² : PseudoMetricSpace R<VAR>inst✝¹ : Mul R<VAR>inst✝ : BoundedMul R<VAR>f g : X → R<VAR>f_bdd : ∃ C, ∀ (x y : X), dist (f x) (f y) ≤ C<VAR>g_bdd : ∃ C, ∀ (x y : X), dist (g x) (g y) ≤ C<VAR>C : ℝ<VAR>hC : ∀ ⦃x : R⦄, x ∈ range f * range g → ∀ ⦃y : R⦄, y ∈ range f * range g → dist x y ≤ C<VAR>x y : X<GOAL>dist ((f * g) x) ((f * g) y) ≤ C
<VAR>X✝ Y✝ Z✝ : Stonean<VAR>f✝ : X✝ ⟶ Z✝<VAR>i✝ : Y✝ ⟶ Z✝<VAR>hi✝ : OpenEmbedding ⇑i✝<VAR>X Y Z W : Stonean<VAR>f : X ⟶ Z<VAR>i : Y ⟶ Z<VAR>hi : OpenEmbedding ⇑i<VAR>a : W ⟶ X<VAR>b : W ⟶ Y<VAR>w : a ≫ f = b ≫ i<VAR>z : (forget Stonean).obj W<GOAL>(lift f hi a b w ≫ snd f hi) z = b z
<VAR>X✝ Y✝ Z✝ : Stonean<VAR>f✝ : X✝ ⟶ Z✝<VAR>i✝ : Y✝ ⟶ Z✝<VAR>hi✝ : OpenEmbedding ⇑i✝<VAR>X Y Z W : Stonean<VAR>f : X ⟶ Z<VAR>i : Y ⟶ Z<VAR>hi : OpenEmbedding ⇑i<VAR>a : W ⟶ X<VAR>b : W ⟶ Y<VAR>w : a ≫ f = b ≫ i<VAR>z : (forget Stonean).obj W<VAR>this : (b ≫ i) z = (a ≫ f) z<GOAL>(lift f hi a b w ≫ snd f hi) z = b z
<VAR>X✝ Y✝ Z✝ : Stonean<VAR>f✝ : X✝ ⟶ Z✝<VAR>i✝ : Y✝ ⟶ Z✝<VAR>hi✝ : OpenEmbedding ⇑i✝<VAR>X Y Z W : Stonean<VAR>f : X ⟶ Z<VAR>i : Y ⟶ Z<VAR>hi : OpenEmbedding ⇑i<VAR>a : W ⟶ X<VAR>b : W ⟶ Y<VAR>w : a ≫ f = b ≫ i<VAR>z : (forget Stonean).obj W<VAR>this : (b ≫ i) z = (a ≫ f) z<VAR>h : i (b z) = f (a z)<GOAL>(lift f hi a b w ≫ snd f hi) z = b z
<VAR>X✝ Y✝ Z✝ : Stonean<VAR>f✝ : X✝ ⟶ Z✝<VAR>i✝ : Y✝ ⟶ Z✝<VAR>hi✝ : OpenEmbedding ⇑i✝<VAR>X Y Z W : Stonean<VAR>f : X ⟶ Z<VAR>i : Y ⟶ Z<VAR>hi : OpenEmbedding ⇑i<VAR>a : W ⟶ X<VAR>b : W ⟶ Y<VAR>w : a ≫ f = b ≫ i<VAR>z : (forget Stonean).obj W<VAR>this : (b ≫ i) z = (a ≫ f) z<VAR>h : i (b z) = f (a z)<GOAL>b z = (Homeomorph.ofEmbedding ⇑i ⋯).symm ⟨f (a z), ⋯⟩
<VAR>X✝ Y✝ Z✝ : Stonean<VAR>f✝ : X✝ ⟶ Z✝<VAR>i✝ : Y✝ ⟶ Z✝<VAR>hi✝ : OpenEmbedding ⇑i✝<VAR>X Y Z W : Stonean<VAR>f : X ⟶ Z<VAR>i : Y ⟶ Z<VAR>hi : OpenEmbedding ⇑i<VAR>a : W ⟶ X<VAR>b : W ⟶ Y<VAR>w : a ≫ f = b ≫ i<VAR>z : (forget Stonean).obj W<VAR>this : (b ≫ i) z = (a ≫ f) z<VAR>h : i (b z) = f (a z)<GOAL>(Homeomorph.ofEmbedding ⇑i ⋯) (b z) = (Homeomorph.ofEmbedding ⇑i ⋯) ((Homeomorph.ofEmbedding ⇑i ⋯).symm ⟨f (a z), ⋯⟩)
<VAR>α : Type u_1<VAR>inst✝ : OrderedAddCommGroup α<VAR>a b c : α<GOAL>-Ioo a b = Ioo (-b) (-a)
<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✝ : SupSet α<VAR>f✝ g✝ : ι → α<VAR>f : ι → ι'<VAR>hf : Surjective f<VAR>g : ι' → α<GOAL>(range fun x => g (f x)) = range fun y => g y
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>T : Type u_3<VAR>inst✝³ : CommRing T<VAR>inst✝² : Algebra R T<VAR>inst✝¹ : Algebra S T<VAR>inst✝ : IsScalarTower R S T<VAR>g : S →+* T<VAR>f : R →+* S<GOAL>f.SurjectiveOnStalks ↔ ∀ (I : Ideal S), I.IsMaximal → ∀ (s : S), ∃ x r, ∃ c ∉ I, f r ∉ I ∧ c * f r * s = c * f x
<VAR>n m : ℕ<VAR>h : n = m<GOAL>n.dist m = 0
<VAR>R : Type u<VAR>S : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>x : S<VAR>p : R[X]<VAR>T : Subring R<VAR>hp : ↑p.coeffs ⊆ ↑T<VAR>n : ℕ<GOAL>(map T.subtype (p.toSubring T hp)).coeff n = p.coeff n
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : ConcreteCategory C<VAR>J : Type w<VAR>inst✝ : Category.{r, w} J<VAR>F : J ⥤ C<VAR>D : Cocone F<VAR>i j : J<VAR>x : (forget C).obj (F.obj i)<VAR>y : (forget C).obj (F.obj j)<VAR>E : Cocone (F ⋙ forget C) := (forget C).mapCocone D<VAR>k : J<VAR>f : i ⟶ k<VAR>g : j ⟶ k<VAR>hfg : (F ⋙ forget C).map f x = (F.map g) y<GOAL>(D.ι.app i) x = (D.ι.app j) y
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : ConcreteCategory C<VAR>J : Type w<VAR>inst✝ : Category.{r, w} J<VAR>F : J ⥤ C<VAR>D : Cocone F<VAR>i j : J<VAR>x : (forget C).obj (F.obj i)<VAR>y : (forget C).obj (F.obj j)<VAR>E : Cocone (F ⋙ forget C) := (forget C).mapCocone D<VAR>k : J<VAR>f : i ⟶ k<VAR>g : j ⟶ k<VAR>hfg : (F ⋙ forget C).map f x = (F.map g) y<VAR>h1 : (F ⋙ forget C).map f ≫ E.ι.app k = E.ι.app i := E.ι.naturality f<GOAL>(D.ι.app i) x = (D.ι.app j) y
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : ConcreteCategory C<VAR>J : Type w<VAR>inst✝ : Category.{r, w} J<VAR>F : J ⥤ C<VAR>D : Cocone F<VAR>i j : J<VAR>x : (forget C).obj (F.obj i)<VAR>y : (forget C).obj (F.obj j)<VAR>E : Cocone (F ⋙ forget C) := (forget C).mapCocone D<VAR>k : J<VAR>f : i ⟶ k<VAR>g : j ⟶ k<VAR>hfg : (F ⋙ forget C).map f x = (F.map g) y<VAR>h1 : (F ⋙ forget C).map f ≫ E.ι.app k = E.ι.app i := E.ι.naturality f<VAR>h2 : (F ⋙ forget C).map g ≫ E.ι.app k = E.ι.app j := E.ι.naturality g<GOAL>(D.ι.app i) x = (D.ι.app j) y
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : ConcreteCategory C<VAR>J : Type w<VAR>inst✝ : Category.{r, w} J<VAR>F : J ⥤ C<VAR>D : Cocone F<VAR>i j : J<VAR>x : (forget C).obj (F.obj i)<VAR>y : (forget C).obj (F.obj j)<VAR>E : Cocone (F ⋙ forget C) := (forget C).mapCocone D<VAR>k : J<VAR>f : i ⟶ k<VAR>g : j ⟶ k<VAR>hfg : (F ⋙ forget C).map f x = (F.map g) y<VAR>h1 : (F ⋙ forget C).map f ≫ E.ι.app k = E.ι.app i := E.ι.naturality f<VAR>h2 : (F ⋙ forget C).map g ≫ E.ι.app k = E.ι.app j := E.ι.naturality g<GOAL>E.ι.app i x = E.ι.app j y
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : ConcreteCategory C<VAR>J : Type w<VAR>inst✝ : Category.{r, w} J<VAR>F : J ⥤ C<VAR>D : Cocone F<VAR>i j : J<VAR>x : (forget C).obj (F.obj i)<VAR>y : (forget C).obj (F.obj j)<VAR>E : Cocone (F ⋙ forget C) := (forget C).mapCocone D<VAR>k : J<VAR>f : i ⟶ k<VAR>g : j ⟶ k<VAR>hfg : (F ⋙ forget C).map f x = (F.map g) y<VAR>h1 : (F ⋙ forget C).map f ≫ E.ι.app k = E.ι.app i := E.ι.naturality f<VAR>h2 : (F ⋙ forget C).map g ≫ E.ι.app k = E.ι.app j := E.ι.naturality g<GOAL>E.ι.app k ((F.map g) y) = E.ι.app j y
<VAR>ι : Type u_1<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasZeroMorphisms C<VAR>c : ComplexShape ι<VAR>K L M K' L' : HomologicalComplex C c<VAR>inst✝ : CategoryWithHomology C<VAR>f : K ⟶ L<GOAL>quasiIso C c f ↔ QuasiIso f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : Preorder α<VAR>a a₁ a₂ b b₁ b₂ c x : α<GOAL>Ico a b = ∅ ↔ ¬a < b
<VAR>k : Type u_1<VAR>E : Type u_2<VAR>PE : Type u_3<VAR>inst✝³ : Field k<VAR>inst✝² : AddCommGroup E<VAR>inst✝¹ : Module k E<VAR>inst✝ : AddTorsor E PE<VAR>f : k → PE<VAR>a : k<GOAL>slope f a a = 0
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s✝ s' s : WSeq α<VAR>h : (map ret s).join = s'<GOAL>Computation.LiftRel (LiftRelO (fun x x_1 => x = x_1) fun s1 s2 => (map ret s2).join = s1) (map ret s).join.destruct s.destruct
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s✝ s' s : WSeq α<VAR>h : (map ret s).join = s'<GOAL>∀ {ca cb : Computation (Option (α × WSeq α))}, (∃ s, ca = (map ret s).join.destruct ∧ cb = s.destruct) → LiftRelAux (LiftRelO (fun x x_1 => x = x_1) fun s1 s2 => (map ret s2).join = s1) (fun c1 c2 => ∃ s, c1 = (map ret s).join.destruct ∧ c2 = s.destruct) ca.destruct cb.destruct
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s✝ s' s : WSeq α<VAR>h : (map ret s).join = s'<GOAL>∃ s_1, (map ret s).join.destruct = (map ret s_1).join.destruct ∧ s.destruct = s_1.destruct
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>m n : ℕ<VAR>ι : Type y<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>hf : Injective ⇑f<VAR>p : R[X]<GOAL>(if (map f p).natDegree = 0 then 0 else (map f p).coeff ((map f p).natDegree - 1)) = f (if p.natDegree = 0 then 0 else p.coeff (p.natDegree - 1))
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>m n : ℕ<VAR>ι : Type y<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>hf : Injective ⇑f<VAR>p : R[X]<GOAL>(if p.natDegree = 0 then 0 else (map f p).coeff (p.natDegree - 1)) = f (if p.natDegree = 0 then 0 else p.coeff (p.natDegree - 1))
<VAR>p x : ℝ<GOAL>‖↑x‖ = |x|
<VAR>p x : ℝ<GOAL>{y | ↑y = ↑x} = {x}
<VAR>p x y : ℝ<GOAL>y ∈ {y | ↑y = ↑x} ↔ y ∈ {x}
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>κ : ι → Type u_5<VAR>π : ι → Set (Set Ω)<VAR>m : ι → MeasurableSpace Ω<VAR>x✝ : MeasurableSpace Ω<VAR>μ✝ : Measure Ω<VAR>S : Finset ι<VAR>s✝ : ι → Set Ω<VAR>s t : Set Ω<VAR>μ : Measure Ω<GOAL>IndepSet s t μ ↔ ∀ (t1 t2 : Set Ω), MeasurableSet t1 → MeasurableSet t2 → μ (t1 ∩ t2) = μ t1 * μ t2
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>f : C(AddCircle T, ℂ)<VAR>n : ℤ<GOAL>∀ (x : AddCircle T), (fourier (-n)) x = (fourier (-n)) x
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M₁ : Type u_7<VAR>M₂ : Type u_8<VAR>M₃ : Type u_9<VAR>V : Type u_10<VAR>V₂ : Type u_11<VAR>inst✝¹² : Semiring R<VAR>inst✝¹¹ : Semiring R₂<VAR>inst✝¹⁰ : Semiring R₃<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : AddCommMonoid M₂<VAR>inst✝⁷ : AddCommMonoid M₃<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R →+* R₃<VAR>inst✝⁶ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module R₂ M₂<VAR>inst✝³ : Module R₃ M₃<VAR>σ₂₁ : R₂ →+* R<VAR>τ₁₂ : R →+* R₂<VAR>τ₂₃ : R₂ →+* R₃<VAR>τ₁₃ : R →+* R₃<VAR>inst✝² : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃<VAR>F : Type u_12<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F τ₁₂ M M₂<VAR>f : F<VAR>hf : Injective ⇑f<GOAL>ker f = ⊥
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M₁ : Type u_7<VAR>M₂ : Type u_8<VAR>M₃ : Type u_9<VAR>V : Type u_10<VAR>V₂ : Type u_11<VAR>inst✝¹² : Semiring R<VAR>inst✝¹¹ : Semiring R₂<VAR>inst✝¹⁰ : Semiring R₃<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : AddCommMonoid M₂<VAR>inst✝⁷ : AddCommMonoid M₃<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R →+* R₃<VAR>inst✝⁶ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module R₂ M₂<VAR>inst✝³ : Module R₃ M₃<VAR>σ₂₁ : R₂ →+* R<VAR>τ₁₂ : R →+* R₂<VAR>τ₂₃ : R₂ →+* R₃<VAR>τ₁₃ : R →+* R₃<VAR>inst✝² : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃<VAR>F : Type u_12<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F τ₁₂ M M₂<VAR>f : F<VAR>hf : Injective ⇑f<VAR>this : Disjoint ⊤ (ker f)<GOAL>ker f = ⊥
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : Type u_6<VAR>α : Type u_7<VAR>α' : Type u_8<VAR>β : Type u_9<VAR>β' : Type u_10<VAR>γ : Type u_11<VAR>𝓕 : Type u_12<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>κ₁ : Type u_13<VAR>κ₂ : Type u_14<VAR>p₁ : κ₁ → Prop<VAR>s₁ : κ₁ → Set (β × β)<VAR>p₂ : κ₂ → Prop<VAR>s₂ : κ₂ → Set (α × α)<VAR>F : ι → β → α<VAR>S : Set β<VAR>hβ : (𝓤 β ⊓ 𝓟 (S ×ˢ S)).HasBasis p₁ s₁<VAR>hα : (𝓤 α).HasBasis p₂ s₂<GOAL>UniformEquicontinuousOn F S ↔ ∀ (k₂ : κ₂), p₂ k₂ → ∃ k₁, p₁ k₁ ∧ ∀ (x y : β), (x, y) ∈ s₁ k₁ → ∀ (i : ι), (F i x, F i y) ∈ s₂ k₂