ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace ℝ G<VAR>x y : E<VAR>s t : Set E<VAR>h : s ∈ 𝓝 x<GOAL>UniqueDiffWithinAt 𝕜 s x
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>inst✝ : IsFilteredOrEmpty C<VAR>h₁ : ∀ (d : D), ∃ c, Nonempty (d ⟶ F.obj c)<VAR>h₂ : ∀ {d : D} {c : C} (s s' : d ⟶ F.obj c), ∃ c' t, s ≫ F.map t = s' ≫ F.map t<GOAL>F.Final
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>inst✝ : IsFilteredOrEmpty C<VAR>h₁ : ∀ (d : D), ∃ c, Nonempty (d ⟶ F.obj c)<VAR>h₂ : ∀ {d : D} {c : C} (s s' : d ⟶ F.obj c), ∃ c' t, s ≫ F.map t = s' ≫ F.map t<GOAL>∀ (d : D), IsFiltered (StructuredArrow d F)
<VAR>ι : Type u_1<VAR>n : ℕ<VAR>s : Finset ι<VAR>a : ι → ZMod n<VAR>hs : 2 * n - 1 ≤ s.card<GOAL>∃ t ⊆ s, t.card = n ∧ ∑ i ∈ t, a i = 0
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>T : Type u_5<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommSemiring S<VAR>inst✝ : CommSemiring T<VAR>f✝ : σ → MvPolynomial τ R<VAR>f : R →+* S<VAR>g : τ → S<VAR>h : σ → MvPolynomial τ R<VAR>φ : MvPolynomial σ R<GOAL>(eval₂Hom f g) ((bind₁ h) φ) = (eval₂Hom f fun i => (eval₂Hom f g) (h i)) φ
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>R : ℝ<VAR>c w : ℂ<VAR>f : ℂ → E<VAR>hf : DiffContOnCl ℂ f (ball c R)<VAR>hw : w ∈ ball c R<GOAL>((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z) = f w
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>R : ℝ<VAR>c w : ℂ<VAR>f : ℂ → E<VAR>hf : DiffContOnCl ℂ f (ball c R)<VAR>hw : w ∈ ball c R<VAR>hR : 0 < R<GOAL>((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z) = f w
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>R : ℝ<VAR>c w : ℂ<VAR>f : ℂ → E<VAR>hf : DiffContOnCl ℂ f (ball c R)<VAR>hw : w ∈ ball c R<VAR>hR : 0 < R<GOAL>ContinuousOn f (closedBall c R)
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>R : ℝ<VAR>c w : ℂ<VAR>f : ℂ → E<VAR>hf : DiffContOnCl ℂ f (ball c R)<VAR>hw : w ∈ ball c R<VAR>hR : 0 < R<GOAL>∀ x ∈ ball c R \ ∅, DifferentiableAt ℂ f x
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>A : Type u_2<VAR>inst✝¹ : AddGroup A<VAR>S : Set G<VAR>inst✝ : Finite ↑S<VAR>x : G<VAR>h : ∀ n ∈ S, x * n * x⁻¹ ∈ S<VAR>this : (a : Prop) → Decidable a<GOAL>x ∈ setNormalizer S
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>A : Type u_2<VAR>inst✝¹ : AddGroup A<VAR>S : Set G<VAR>inst✝ : Finite ↑S<VAR>x : G<VAR>h : ∀ n ∈ S, x * n * x⁻¹ ∈ S<VAR>this : (a : Prop) → Decidable a<VAR>val✝ : Fintype ↑S<GOAL>x ∈ setNormalizer S
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>A : Type u_2<VAR>inst✝¹ : AddGroup A<VAR>S : Set G<VAR>inst✝ : Finite ↑S<VAR>x : G<VAR>h : ∀ n ∈ S, x * n * x⁻¹ ∈ S<VAR>this✝ : (a : Prop) → Decidable a<VAR>val✝ : Fintype ↑S<VAR>this : Fintype ↑((fun n => x * n * x⁻¹) '' S)<GOAL>x ∈ setNormalizer S
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>o : Ordinal.{u}<VAR>f : (a : Ordinal.{u}) → a < o → Ordinal.{u}<VAR>c : Ordinal.{u}<VAR>ho : o.card < c.cof<VAR>hf : ∀ (i : Ordinal.{u}) (hi : i < o), f i hi < c<GOAL>Cardinal.lift.{u, u} o.card < c.cof
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : CommRing R<VAR>p : R[X]<VAR>h : p.leadingCoeff ∈ R⁰<GOAL>p ∈ R[X]⁰
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : CommRing R<VAR>p : R[X]<VAR>h : p.leadingCoeff ∈ R⁰<VAR>x : R[X]<VAR>hx : x * p = 0<GOAL>x.leadingCoeff = 0
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : CommRing R<VAR>p : R[X]<VAR>h : p.leadingCoeff ∈ R⁰<VAR>x : R[X]<VAR>hx : x * p = 0<VAR>hx' : ¬x.leadingCoeff = 0<GOAL>False
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : CommRing R<VAR>p : R[X]<VAR>h : p.leadingCoeff ∈ R⁰<VAR>x : R[X]<VAR>hx : x * p = 0<VAR>hx' : ¬x.leadingCoeff * p.leadingCoeff = 0<GOAL>False
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁸ : MeasurableSpace α<VAR>inst✝⁷ : MeasurableSpace α'<VAR>inst✝⁶ : MeasurableSpace β<VAR>inst✝⁵ : MeasurableSpace β'<VAR>inst✝⁴ : MeasurableSpace γ<VAR>μ μ'✝ : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : SFinite ν<VAR>inst✝¹ : SFinite μ<VAR>μ' : Measure α<VAR>inst✝ : SFinite μ'<GOAL>(μ + μ').prod ν = μ.prod ν + μ'.prod ν
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁸ : MeasurableSpace α<VAR>inst✝⁷ : MeasurableSpace α'<VAR>inst✝⁶ : MeasurableSpace β<VAR>inst✝⁵ : MeasurableSpace β'<VAR>inst✝⁴ : MeasurableSpace γ<VAR>μ μ'✝ : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : SFinite ν<VAR>inst✝¹ : SFinite μ<VAR>μ' : Measure α<VAR>inst✝ : SFinite μ'<GOAL>(sum fun p => (sFiniteSeq μ p.1 + sFiniteSeq μ' p.1).prod (sFiniteSeq ν p.2)) = sum fun n => (sFiniteSeq μ n.1).prod (sFiniteSeq ν n.2) + (sFiniteSeq μ' n.1).prod (sFiniteSeq ν n.2)
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁸ : MeasurableSpace α<VAR>inst✝⁷ : MeasurableSpace α'<VAR>inst✝⁶ : MeasurableSpace β<VAR>inst✝⁵ : MeasurableSpace β'<VAR>inst✝⁴ : MeasurableSpace γ<VAR>μ μ'✝ : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : SFinite ν<VAR>inst✝¹ : SFinite μ<VAR>μ' : Measure α<VAR>inst✝ : SFinite μ'<VAR>i : ℕ × ℕ<GOAL>(sFiniteSeq μ i.1 + sFiniteSeq μ' i.1).prod (sFiniteSeq ν i.2) = (sFiniteSeq μ i.1).prod (sFiniteSeq ν i.2) + (sFiniteSeq μ' i.1).prod (sFiniteSeq ν i.2)
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁸ : MeasurableSpace α<VAR>inst✝⁷ : MeasurableSpace α'<VAR>inst✝⁶ : MeasurableSpace β<VAR>inst✝⁵ : MeasurableSpace β'<VAR>inst✝⁴ : MeasurableSpace γ<VAR>μ μ'✝ : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : SFinite ν<VAR>inst✝¹ : SFinite μ<VAR>μ' : Measure α<VAR>inst✝ : SFinite μ'<VAR>i : ℕ × ℕ<VAR>s : Set α<VAR>t : Set β<VAR>x✝¹ : MeasurableSet s<VAR>x✝ : MeasurableSet t<GOAL>((sFiniteSeq μ i.1).prod (sFiniteSeq ν i.2) + (sFiniteSeq μ' i.1).prod (sFiniteSeq ν i.2)) (s ×ˢ t) = (sFiniteSeq μ i.1 + sFiniteSeq μ' i.1) s * (sFiniteSeq ν i.2) t
<VAR>m n✝ n : ℕ<VAR>inst✝ : NeZero n<VAR>x : ZMod n<GOAL>0 ≤ x.valMinAbs ↔ x.val ≤ n / 2
<VAR>m n✝ n : ℕ<VAR>inst✝ : NeZero n<VAR>x : ZMod n<GOAL>(0 ≤ if x.val ≤ n / 2 then ↑x.val else ↑x.val - ↑n) ↔ x.val ≤ n / 2
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : HeytingAlgebra α<VAR>a✝ a b : α<VAR>h : IsCompl a b<GOAL>a ⇔ b = ⊥
<VAR>x y : ℝ<GOAL>↑(expMapCircle (x + y)) = ↑(expMapCircle x * expMapCircle y)
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s✝ : Set ℝ≥0∞<VAR>α : Type u_4<VAR>ι : Type u_5<VAR>s : Finset α<VAR>f : α → ι → ℝ≥0∞<VAR>hf : ∀ (i j : ι), ∃ k, ∀ (a : α), f a i ≤ f a k ∧ f a j ≤ f a k<GOAL>∑ a ∈ s, ⨆ i, f a i = ⨆ i, ∑ a ∈ s, f a i
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>inst✝³ : Semiring R<VAR>φ : ι → Type u_3<VAR>inst✝² : (i : ι) → AddCommMonoid (φ i)<VAR>inst✝¹ : (i : ι) → Module R (φ i)<VAR>inst✝ : DecidableEq ι<VAR>I J : Set ι<VAR>hd : Disjoint I J<VAR>hu : univ ⊆ I ∪ J<VAR>hI : I.Finite<GOAL>⨆ i ∈ I, range (stdBasis R φ i) = ⨅ i ∈ J, ker (proj i)
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>inst✝³ : Semiring R<VAR>φ : ι → Type u_3<VAR>inst✝² : (i : ι) → AddCommMonoid (φ i)<VAR>inst✝¹ : (i : ι) → Module R (φ i)<VAR>inst✝ : DecidableEq ι<VAR>I J : Set ι<VAR>hd : Disjoint I J<VAR>hu : univ ⊆ I ∪ J<VAR>hI : I.Finite<GOAL>⨅ i ∈ J, ker (proj i) ≤ ⨆ i ∈ I, range (stdBasis R φ i)
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>inst✝³ : Semiring R<VAR>φ : ι → Type u_3<VAR>inst✝² : (i : ι) → AddCommMonoid (φ i)<VAR>inst✝¹ : (i : ι) → Module R (φ i)<VAR>inst✝ : DecidableEq ι<VAR>I J : Set ι<VAR>hd : Disjoint I J<VAR>hu : univ ⊆ I ∪ J<VAR>hI : I.Finite<VAR>this : univ ⊆ ↑hI.toFinset ∪ J<GOAL>⨅ i ∈ J, ker (proj i) ≤ ⨆ i ∈ I, range (stdBasis R φ i)
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>inst✝³ : Semiring R<VAR>φ : ι → Type u_3<VAR>inst✝² : (i : ι) → AddCommMonoid (φ i)<VAR>inst✝¹ : (i : ι) → Module R (φ i)<VAR>inst✝ : DecidableEq ι<VAR>I J : Set ι<VAR>hd : Disjoint I J<VAR>hu : univ ⊆ I ∪ J<VAR>hI : I.Finite<VAR>this : univ ⊆ ↑hI.toFinset ∪ J<VAR>i : ι<GOAL>⨆ (_ : i ∈ hI.toFinset), range (stdBasis R φ i) ≤ ⨆ (_ : i ∈ I), range (stdBasis R φ i)
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>M✝ : Type u_3<VAR>R : Type u_4<VAR>A : Type u_5<VAR>inst✝² : Monoid M✝<VAR>inst✝¹ : AddMonoid A<VAR>inst✝ : NonUnitalNonAssocSemiring R<VAR>M N : AddSubmonoid R<VAR>C : R → Prop<VAR>r : R<VAR>hr : r ∈ M * N<VAR>hm : ∀ m ∈ M, ∀ n ∈ N, C (m * n)<VAR>ha : ∀ (x y : R), C x → C y → C (x + y)<GOAL>0 ∈ { carrier := setOf C, add_mem' := ⋯ }.carrier
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t s : Set α<GOAL>(μ.restrict s) univ = μ s
<VAR>num : Int<VAR>den : Nat<GOAL>num /. ↑den = mkRat num den
<VAR>z : ℂ<VAR>E : Type u_1<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>ζ : ℂ<VAR>n : ℕ<VAR>h : ζ ^ n = 1<VAR>hn : n ≠ 0<GOAL>‖ζ‖₊ ^ n = 1 ^ n
<GOAL>∀ ⦃R S T : Type u_1⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S] [inst_4 : Algebra R T], (algebraMap R T).Finite → includeLeftRingHom.Finite
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>A₂ : Type uA₂<VAR>A₃ : Type uA₃<VAR>A₁' : Type uA₁'<VAR>A₂' : Type uA₂'<VAR>A₃' : Type uA₃'<VAR>inst✝¹² : CommSemiring R<VAR>inst✝¹¹ : Semiring A₁<VAR>inst✝¹⁰ : Semiring A₂<VAR>inst✝⁹ : Semiring A₃<VAR>inst✝⁸ : Semiring A₁'<VAR>inst✝⁷ : Semiring A₂'<VAR>inst✝⁶ : Semiring A₃'<VAR>inst✝⁵ : Algebra R A₁<VAR>inst✝⁴ : Algebra R A₂<VAR>inst✝³ : Algebra R A₃<VAR>inst✝² : Algebra R A₁'<VAR>inst✝¹ : Algebra R A₂'<VAR>inst✝ : Algebra R A₃'<VAR>e✝ e : A₁ ≃ₐ[R] A₂<VAR>e' : A₁' ≃ₐ[R] A₂'<VAR>ψ : A₁ ≃ₐ[R] A₁'<VAR>a✝ : A₁<GOAL>((fun ψ => e.trans (ψ.trans e'.symm)) ((fun ψ => e.symm.trans (ψ.trans e')) ψ)) a✝ = ψ a✝
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>A₂ : Type uA₂<VAR>A₃ : Type uA₃<VAR>A₁' : Type uA₁'<VAR>A₂' : Type uA₂'<VAR>A₃' : Type uA₃'<VAR>inst✝¹² : CommSemiring R<VAR>inst✝¹¹ : Semiring A₁<VAR>inst✝¹⁰ : Semiring A₂<VAR>inst✝⁹ : Semiring A₃<VAR>inst✝⁸ : Semiring A₁'<VAR>inst✝⁷ : Semiring A₂'<VAR>inst✝⁶ : Semiring A₃'<VAR>inst✝⁵ : Algebra R A₁<VAR>inst✝⁴ : Algebra R A₂<VAR>inst✝³ : Algebra R A₃<VAR>inst✝² : Algebra R A₁'<VAR>inst✝¹ : Algebra R A₂'<VAR>inst✝ : Algebra R A₃'<VAR>e✝ e : A₁ ≃ₐ[R] A₂<VAR>e' : A₁' ≃ₐ[R] A₂'<VAR>ψ : A₂ ≃ₐ[R] A₂'<VAR>a✝ : A₂<GOAL>((fun ψ => e.symm.trans (ψ.trans e')) ((fun ψ => e.trans (ψ.trans e'.symm)) ψ)) a✝ = ψ a✝
<VAR>U : Type u_1<VAR>V : Type u_2<VAR>W : Type u_3<VAR>inst✝² : Quiver U<VAR>inst✝¹ : Quiver V<VAR>inst✝ : Quiver W<VAR>h : HasInvolutiveReverse V<VAR>a b : V<VAR>f : a ⟶ b<GOAL>reverse (reverse f) = f
<VAR>R : Type u_1<VAR>p i : ℕ<VAR>hp : Nat.Prime p<GOAL>(σ 0) (p ^ i) = i + 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a b : α<VAR>h : a ≤ b<VAR>x : α<GOAL>projIic b x = ⟨b, ⋯⟩ ↔ b ≤ x
<VAR>C : Type u_1<VAR>inst✝ : Category.{?u.432254, u_1} C<VAR>n m : ℕ<VAR>F G : ComposableArrows C n<VAR>f g : ComposableArrows C 5<VAR>app₀ : f.obj' 0 ⋯ ⟶ g.obj' 0 ⋯<VAR>app₁ : f.obj' 1 ⋯ ⟶ g.obj' 1 ⋯<VAR>app₂ : f.obj' 2 ⋯ ⟶ g.obj' 2 ⋯<VAR>app₃ : f.obj' 3 ⋯ ⟶ g.obj' 3 ⋯<VAR>app₄ : f.obj' 4 ⋯ ⟶ g.obj' 4 ⋯<VAR>app₅ : f.obj' 5 ⋯ ⟶ g.obj' 5 ⋯<VAR>w₀ : f.map' 0 1 ⋯ ⋯ ≫ app₁ = app₀ ≫ g.map' 0 1 ⋯ ⋯<VAR>w₁ : f.map' 1 2 ⋯ ⋯ ≫ app₂ = app₁ ≫ g.map' 1 2 ⋯ ⋯<VAR>w₂ : f.map' 2 3 ⋯ ⋯ ≫ app₃ = app₂ ≫ g.map' 2 3 ⋯ ⋯<VAR>w₃ : f.map' 3 4 ⋯ ⋯ ≫ app₄ = app₃ ≫ g.map' 3 4 ⋯ ⋯<VAR>w₄ : f.map' 4 5 ⋯ ⋯ ≫ app₅ = app₄ ≫ g.map' 4 5 ⋯ ⋯<GOAL>5 < 5 + 1
<VAR>F : Type u_1<VAR>G : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace ℝ G<VAR>X : Type u_3<VAR>Y : Type u_4<VAR>Z : Type u_5<VAR>inst✝ : TopologicalSpace X<VAR>f g : X → Y<VAR>A : Set X<VAR>x : X<VAR>s : Set X<VAR>h : ∀ x ∈ s, (↑f).IsConstant<VAR>hs : IsPreconnected s<VAR>x' : X<VAR>x_in : x ∈ s<VAR>x'_in : x' ∈ s<VAR>i : ↑s → X := fun x => ↑x<GOAL>(f ∘ i) ⟨x, x_in⟩ = (f ∘ i) ⟨x', x'_in⟩
<VAR>F : Type u_1<VAR>G : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace ℝ G<VAR>X : Type u_3<VAR>Y : Type u_4<VAR>Z : Type u_5<VAR>inst✝ : TopologicalSpace X<VAR>f g : X → Y<VAR>A : Set X<VAR>x : X<VAR>s : Set X<VAR>h : ∀ x ∈ s, (↑f).IsConstant<VAR>hs : IsPreconnected s<VAR>x' : X<VAR>x_in : x ∈ s<VAR>x'_in : x' ∈ s<VAR>i : ↑s → X := fun x => ↑x<VAR>this : PreconnectedSpace ↑s<GOAL>(f ∘ i) ⟨x, x_in⟩ = (f ∘ i) ⟨x', x'_in⟩
<VAR>X : Type u_1<VAR>α : Type u_2<VAR>ι : Sort u_3<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : BaireSpace X<VAR>s t : Set X<VAR>hs : IsGδ s<VAR>ht : IsGδ t<VAR>hsc : Dense s<VAR>htc : Dense t<GOAL>Dense (s ∩ t)
<VAR>X : Type u_1<VAR>α : Type u_2<VAR>ι : Sort u_3<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : BaireSpace X<VAR>s t : Set X<VAR>hs : IsGδ s<VAR>ht : IsGδ t<VAR>hsc : Dense s<VAR>htc : Dense t<GOAL>Dense (⋂ b, bif b then s else t)
<VAR>I : Type u<VAR>inst✝⁴ : LinearOrder I<VAR>inst✝³ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>J K L : I → Prop<VAR>inst✝² : (i : I) → Decidable (J i)<VAR>inst✝¹ : (i : I) → Decidable (K i)<VAR>inst✝ : (i : I) → Decidable (L i)<VAR>x : I → Bool<VAR>h : ∀ (i : I), x i ≠ false → J i<VAR>i : I<GOAL>Proj J x i = x i
<VAR>I : Type u<VAR>inst✝⁴ : LinearOrder I<VAR>inst✝³ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>J K L : I → Prop<VAR>inst✝² : (i : I) → Decidable (J i)<VAR>inst✝¹ : (i : I) → Decidable (K i)<VAR>inst✝ : (i : I) → Decidable (L i)<VAR>x : I → Bool<VAR>h : ∀ (i : I), x i ≠ false → J i<VAR>i : I<GOAL>¬J i → false = x i
<VAR>I : Type u<VAR>inst✝⁴ : LinearOrder I<VAR>inst✝³ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>J K L : I → Prop<VAR>inst✝² : (i : I) → Decidable (J i)<VAR>inst✝¹ : (i : I) → Decidable (K i)<VAR>inst✝ : (i : I) → Decidable (L i)<VAR>x : I → Bool<VAR>h : ∀ (i : I), x i ≠ false → J i<VAR>i : I<GOAL>false ≠ x i → J i
<VAR>x : ℝ<VAR>hx₀ : 0 ≤ x<VAR>hx : x ≤ π / 2<GOAL>2 / π * x ≤ sin x
<VAR>x : ℝ<VAR>hx₀ : 0 ≤ x<VAR>hx : x ≤ π / 2<GOAL>0 ≤ sin x - 2 / π * x
<VAR>x : ℝ<VAR>hx₀ : 0 ≤ x<VAR>hx : x ≤ π / 2<GOAL>ConcaveOn ℝ (Icc 0 (π / 2)) fun x => sin x - 2 / π * x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>s : Finset β<VAR>t : β → Set α<VAR>hd : (↑s).Pairwise (AEDisjoint μ on t)<VAR>hm : ∀ b ∈ s, NullMeasurableSet (t b) μ<VAR>f : α → ℝ≥0∞<GOAL>∫⁻ (a : α) in ⋃ b ∈ s, t b, f a ∂μ = ∑ b ∈ s, ∫⁻ (a : α) in t b, f a ∂μ
<VAR>R : CommRingCat<VAR>M : Submonoid ↑R<VAR>x : PrimeSpectrum (Localization M)<GOAL>IsIso (PresheafedSpace.Hom.stalkMap (Spec.toPresheafedSpace.map (CommRingCat.ofHom (algebraMap (↑R) (Localization M))).op) x)
<VAR>R : CommRingCat<VAR>M : Submonoid ↑R<VAR>x : PrimeSpectrum (Localization M)<GOAL>IsIso ((stalkIso (↑(unop (op (CommRingCat.of ↑R)))) ((PrimeSpectrum.comap (CommRingCat.ofHom (algebraMap (↑R) (Localization M))).op.unop) x)).hom ≫ Localization.localRingHom ((PrimeSpectrum.comap (CommRingCat.ofHom (algebraMap (↑R) (Localization M))).op.unop) x).asIdeal x.asIdeal (CommRingCat.ofHom (algebraMap (↑R) (Localization M))).op.unop ⋯ ≫ (stalkIso (↑(unop (op (CommRingCat.of (Localization M))))) x).inv)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>a : α<VAR>ha : 0 ≤ a<GOAL>↑⌈a⌉₊ = ↑⌈a⌉
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝⁵ : EMetricSpace X<VAR>inst✝⁴ : EMetricSpace Y<VAR>inst✝³ : MeasurableSpace X<VAR>inst✝² : BorelSpace X<VAR>inst✝¹ : MeasurableSpace Y<VAR>inst✝ : BorelSpace Y<VAR>e : X ≃ᵢ Y<VAR>d : ℝ<GOAL>Measure.map ⇑e μH[d] = μH[d]
<VAR>R : Type u_1<VAR>inst✝¹⁷ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝¹⁶ : AddCommMonoid M<VAR>inst✝¹⁵ : AddCommMonoid M'<VAR>inst✝¹⁴ : AddCommMonoid M''<VAR>A : Type u_5<VAR>inst✝¹³ : CommSemiring A<VAR>inst✝¹² : Algebra R A<VAR>inst✝¹¹ : Module A M'<VAR>inst✝¹⁰ : IsLocalization S A<VAR>inst✝⁹ : Module R M<VAR>inst✝⁸ : Module R M'<VAR>inst✝⁷ : Module R M''<VAR>inst✝⁶ : IsScalarTower R A M'<VAR>f : M →ₗ[R] M'<VAR>g✝ : M →ₗ[R] M''<VAR>M₀ : Type u_6<VAR>M₀' : ?m.1161840<VAR>inst✝⁵ : AddCommGroup M₀<VAR>inst✝⁴ : Module R M₀<VAR>M₁ : Type u_7<VAR>M₁' : ?m.1162365<VAR>inst✝³ : AddCommGroup M₁<VAR>inst✝² : Module R M₁<VAR>M₂ : Type u_8<VAR>M₂' : ?m.1162890<VAR>inst✝¹ : AddCommGroup M₂<VAR>inst✝ : Module R M₂<VAR>g : M₀ →ₗ[R] M₁<VAR>h : M₁ →ₗ[R] M₂<VAR>ex : Exact ⇑g ⇑h<VAR>y : LocalizedModule S M₁<VAR>m : M₁<VAR>s : ↥S<VAR>hy : ((IsLocalizedModule.map S (mkLinearMap S M₁) (mkLinearMap S M₂)) h) (mk m s) = 0<GOAL>mk m s ∈ Set.range ⇑((IsLocalizedModule.map S (mkLinearMap S M₀) (mkLinearMap S M₁)) g)
<VAR>R : Type u_1<VAR>inst✝¹⁷ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝¹⁶ : AddCommMonoid M<VAR>inst✝¹⁵ : AddCommMonoid M'<VAR>inst✝¹⁴ : AddCommMonoid M''<VAR>A : Type u_5<VAR>inst✝¹³ : CommSemiring A<VAR>inst✝¹² : Algebra R A<VAR>inst✝¹¹ : Module A M'<VAR>inst✝¹⁰ : IsLocalization S A<VAR>inst✝⁹ : Module R M<VAR>inst✝⁸ : Module R M'<VAR>inst✝⁷ : Module R M''<VAR>inst✝⁶ : IsScalarTower R A M'<VAR>f : M →ₗ[R] M'<VAR>g✝ : M →ₗ[R] M''<VAR>M₀ : Type u_6<VAR>M₀' : ?m.1161840<VAR>inst✝⁵ : AddCommGroup M₀<VAR>inst✝⁴ : Module R M₀<VAR>M₁ : Type u_7<VAR>M₁' : ?m.1162365<VAR>inst✝³ : AddCommGroup M₁<VAR>inst✝² : Module R M₁<VAR>M₂ : Type u_8<VAR>M₂' : ?m.1162890<VAR>inst✝¹ : AddCommGroup M₂<VAR>inst✝ : Module R M₂<VAR>g : M₀ →ₗ[R] M₁<VAR>h : M₁ →ₗ[R] M₂<VAR>ex : Exact ⇑g ⇑h<VAR>y : LocalizedModule S M₁<VAR>m : M₁<VAR>s : ↥S<VAR>hy : ∃ u, u • h m = u • 0<GOAL>mk m s ∈ Set.range ⇑((IsLocalizedModule.map S (mkLinearMap S M₀) (mkLinearMap S M₁)) g)
<VAR>R : Type u_1<VAR>inst✝¹⁷ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝¹⁶ : AddCommMonoid M<VAR>inst✝¹⁵ : AddCommMonoid M'<VAR>inst✝¹⁴ : AddCommMonoid M''<VAR>A : Type u_5<VAR>inst✝¹³ : CommSemiring A<VAR>inst✝¹² : Algebra R A<VAR>inst✝¹¹ : Module A M'<VAR>inst✝¹⁰ : IsLocalization S A<VAR>inst✝⁹ : Module R M<VAR>inst✝⁸ : Module R M'<VAR>inst✝⁷ : Module R M''<VAR>inst✝⁶ : IsScalarTower R A M'<VAR>f : M →ₗ[R] M'<VAR>g✝ : M →ₗ[R] M''<VAR>M₀ : Type u_6<VAR>M₀' : ?m.1161840<VAR>inst✝⁵ : AddCommGroup M₀<VAR>inst✝⁴ : Module R M₀<VAR>M₁ : Type u_7<VAR>M₁' : ?m.1162365<VAR>inst✝³ : AddCommGroup M₁<VAR>inst✝² : Module R M₁<VAR>M₂ : Type u_8<VAR>M₂' : ?m.1162890<VAR>inst✝¹ : AddCommGroup M₂<VAR>inst✝ : Module R M₂<VAR>g : M₀ →ₗ[R] M₁<VAR>h : M₁ →ₗ[R] M₂<VAR>ex : Exact ⇑g ⇑h<VAR>y : LocalizedModule S M₁<VAR>m : M₁<VAR>s : ↥S<VAR>hy : ∃ u, u • h m = u • 0<VAR>a : R<VAR>aS : a ∈ S<VAR>ha : ⟨a, aS⟩ • h m = ⟨a, aS⟩ • 0<GOAL>mk m s ∈ Set.range ⇑((IsLocalizedModule.map S (mkLinearMap S M₀) (mkLinearMap S M₁)) g)
<VAR>R : Type u_1<VAR>inst✝¹⁷ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝¹⁶ : AddCommMonoid M<VAR>inst✝¹⁵ : AddCommMonoid M'<VAR>inst✝¹⁴ : AddCommMonoid M''<VAR>A : Type u_5<VAR>inst✝¹³ : CommSemiring A<VAR>inst✝¹² : Algebra R A<VAR>inst✝¹¹ : Module A M'<VAR>inst✝¹⁰ : IsLocalization S A<VAR>inst✝⁹ : Module R M<VAR>inst✝⁸ : Module R M'<VAR>inst✝⁷ : Module R M''<VAR>inst✝⁶ : IsScalarTower R A M'<VAR>f : M →ₗ[R] M'<VAR>g✝ : M →ₗ[R] M''<VAR>M₀ : Type u_6<VAR>M₀' : ?m.1161840<VAR>inst✝⁵ : AddCommGroup M₀<VAR>inst✝⁴ : Module R M₀<VAR>M₁ : Type u_7<VAR>M₁' : ?m.1162365<VAR>inst✝³ : AddCommGroup M₁<VAR>inst✝² : Module R M₁<VAR>M₂ : Type u_8<VAR>M₂' : ?m.1162890<VAR>inst✝¹ : AddCommGroup M₂<VAR>inst✝ : Module R M₂<VAR>g : M₀ →ₗ[R] M₁<VAR>h : M₁ →ₗ[R] M₂<VAR>ex : Exact ⇑g ⇑h<VAR>y : LocalizedModule S M₁<VAR>m : M₁<VAR>s : ↥S<VAR>hy : ∃ u, u • h m = u • 0<VAR>a : R<VAR>aS : a ∈ S<VAR>ha : a • m ∈ Set.range ⇑g<GOAL>mk m s ∈ Set.range ⇑((IsLocalizedModule.map S (mkLinearMap S M₀) (mkLinearMap S M₁)) g)
<VAR>R : Type u_1<VAR>inst✝¹⁷ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝¹⁶ : AddCommMonoid M<VAR>inst✝¹⁵ : AddCommMonoid M'<VAR>inst✝¹⁴ : AddCommMonoid M''<VAR>A : Type u_5<VAR>inst✝¹³ : CommSemiring A<VAR>inst✝¹² : Algebra R A<VAR>inst✝¹¹ : Module A M'<VAR>inst✝¹⁰ : IsLocalization S A<VAR>inst✝⁹ : Module R M<VAR>inst✝⁸ : Module R M'<VAR>inst✝⁷ : Module R M''<VAR>inst✝⁶ : IsScalarTower R A M'<VAR>f : M →ₗ[R] M'<VAR>g✝ : M →ₗ[R] M''<VAR>M₀ : Type u_6<VAR>M₀' : ?m.1161840<VAR>inst✝⁵ : AddCommGroup M₀<VAR>inst✝⁴ : Module R M₀<VAR>M₁ : Type u_7<VAR>M₁' : ?m.1162365<VAR>inst✝³ : AddCommGroup M₁<VAR>inst✝² : Module R M₁<VAR>M₂ : Type u_8<VAR>M₂' : ?m.1162890<VAR>inst✝¹ : AddCommGroup M₂<VAR>inst✝ : Module R M₂<VAR>g : M₀ →ₗ[R] M₁<VAR>h : M₁ →ₗ[R] M₂<VAR>ex : Exact ⇑g ⇑h<VAR>y : LocalizedModule S M₁<VAR>m : M₁<VAR>s : ↥S<VAR>hy : ∃ u, u • h m = u • 0<VAR>a : R<VAR>aS : a ∈ S<VAR>x : M₀<VAR>hx : g x = a • m<GOAL>mk m s ∈ Set.range ⇑((IsLocalizedModule.map S (mkLinearMap S M₀) (mkLinearMap S M₁)) g)
<VAR>R : Type u_1<VAR>inst✝¹⁷ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝¹⁶ : AddCommMonoid M<VAR>inst✝¹⁵ : AddCommMonoid M'<VAR>inst✝¹⁴ : AddCommMonoid M''<VAR>A : Type u_5<VAR>inst✝¹³ : CommSemiring A<VAR>inst✝¹² : Algebra R A<VAR>inst✝¹¹ : Module A M'<VAR>inst✝¹⁰ : IsLocalization S A<VAR>inst✝⁹ : Module R M<VAR>inst✝⁸ : Module R M'<VAR>inst✝⁷ : Module R M''<VAR>inst✝⁶ : IsScalarTower R A M'<VAR>f : M →ₗ[R] M'<VAR>g✝ : M →ₗ[R] M''<VAR>M₀ : Type u_6<VAR>M₀' : ?m.1161840<VAR>inst✝⁵ : AddCommGroup M₀<VAR>inst✝⁴ : Module R M₀<VAR>M₁ : Type u_7<VAR>M₁' : ?m.1162365<VAR>inst✝³ : AddCommGroup M₁<VAR>inst✝² : Module R M₁<VAR>M₂ : Type u_8<VAR>M₂' : ?m.1162890<VAR>inst✝¹ : AddCommGroup M₂<VAR>inst✝ : Module R M₂<VAR>g : M₀ →ₗ[R] M₁<VAR>h : M₁ →ₗ[R] M₂<VAR>ex : Exact ⇑g ⇑h<VAR>y : LocalizedModule S M₁<VAR>m : M₁<VAR>s : ↥S<VAR>hy : ∃ u, u • h m = u • 0<VAR>a : R<VAR>aS : a ∈ S<VAR>x : M₀<VAR>hx : g x = a • m<GOAL>((IsLocalizedModule.map S (mkLinearMap S M₀) (mkLinearMap S M₁)) g) (mk x (⟨a, aS⟩ * s)) = mk m s
<VAR>R : Type u_1<VAR>inst✝¹⁷ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝¹⁶ : AddCommMonoid M<VAR>inst✝¹⁵ : AddCommMonoid M'<VAR>inst✝¹⁴ : AddCommMonoid M''<VAR>A : Type u_5<VAR>inst✝¹³ : CommSemiring A<VAR>inst✝¹² : Algebra R A<VAR>inst✝¹¹ : Module A M'<VAR>inst✝¹⁰ : IsLocalization S A<VAR>inst✝⁹ : Module R M<VAR>inst✝⁸ : Module R M'<VAR>inst✝⁷ : Module R M''<VAR>inst✝⁶ : IsScalarTower R A M'<VAR>f : M →ₗ[R] M'<VAR>g✝ : M →ₗ[R] M''<VAR>M₀ : Type u_6<VAR>M₀' : ?m.1161840<VAR>inst✝⁵ : AddCommGroup M₀<VAR>inst✝⁴ : Module R M₀<VAR>M₁ : Type u_7<VAR>M₁' : ?m.1162365<VAR>inst✝³ : AddCommGroup M₁<VAR>inst✝² : Module R M₁<VAR>M₂ : Type u_8<VAR>M₂' : ?m.1162890<VAR>inst✝¹ : AddCommGroup M₂<VAR>inst✝ : Module R M₂<VAR>g : M₀ →ₗ[R] M₁<VAR>h : M₁ →ₗ[R] M₂<VAR>ex : Exact ⇑g ⇑h<VAR>y : LocalizedModule S M₁<VAR>x✝ : y ∈ Set.range ⇑((IsLocalizedModule.map S (mkLinearMap S M₀) (mkLinearMap S M₁)) g)<VAR>x : LocalizedModule S M₀<GOAL>((IsLocalizedModule.map S (mkLinearMap S M₀) (mkLinearMap S M₁)) g) x = y → ((IsLocalizedModule.map S (mkLinearMap S M₁) (mkLinearMap S M₂)) h) y = 0