ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Type u_3<VAR>s t u : Finset α<VAR>f : α → β<VAR>n✝ : ℕ<VAR>inst✝ : DecidableEq α<VAR>X Y : Finset α<VAR>n : ℕ<VAR>hXY : n + n < X.card + (Y \ X).card<VAR>h₁ : (X ∩ (Y \ X)).card = 0<VAR>h₂ : (X ∪ Y).card = X.card + (Y \ X).card<VAR>h : n < (Y \ X).card<GOAL>∃ C, n < C.card ∧ (C ⊆ X ∨ C ⊆ Y)
<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✝ : LinearOrder α<VAR>s✝ : Finset α<VAR>H : s✝.Nonempty<VAR>x : α<VAR>s t : Finset α<VAR>h : ∀ x ∈ s, ∀ y ∈ s, x < y → (∀ z ∈ s, z ∉ Set.Ioo x y) → ∃ z ∈ t, x < z ∧ z < y<GOAL>s.card ≤ t.card + 1
<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✝ : LinearOrder α<VAR>s✝ : Finset α<VAR>H : s✝.Nonempty<VAR>x : α<VAR>s t : Finset α<VAR>h : ∀ x ∈ s, ∀ y ∈ s, x < y → ∃ z ∈ t, x < z ∧ z < y<GOAL>s.card ≤ t.card + 1
<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✝ : LinearOrder α<VAR>s✝ : Finset α<VAR>H : s✝.Nonempty<VAR>x : α<VAR>s t : Finset α<VAR>h : ∀ x ∈ s, ∀ y ∈ s, x < y → ∃ z ∈ t, x < z ∧ z < y<VAR>f : α → WithTop α := fun x => (filter (fun y => x < y) t).min<GOAL>s.card ≤ t.card + 1
<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✝ : LinearOrder α<VAR>s✝ : Finset α<VAR>H : s✝.Nonempty<VAR>x : α<VAR>s t : Finset α<VAR>h : ∀ x ∈ s, ∀ y ∈ s, x < y → ∃ z ∈ t, x < z ∧ z < y<VAR>f : α → WithTop α := fun x => (filter (fun y => x < y) t).min<VAR>f_mono : StrictMonoOn f ↑s<GOAL>s.card ≤ t.card + 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>frac : IsFractionRing R₁ K<VAR>inst✝³ : IsDomain R₁<VAR>I✝ J : FractionalIdeal R₁⁰ K<VAR>K' : Type u_5<VAR>inst✝² : Field K'<VAR>inst✝¹ : Algebra R₁ K'<VAR>inst✝ : IsFractionRing R₁ K'<VAR>I : FractionalIdeal R₁⁰ K<VAR>h : K ≃ₐ[R₁] K'<GOAL>map (↑h) (1 / I) = 1 / map (↑h) I
<VAR>α : Type u<VAR>m : ℕ<VAR>a : Fin m → α<VAR>n : ℕ<GOAL>ofFn (Fin.repeat n a) = (replicate n (ofFn a)).join
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>inst✝ : DecidableRel r<VAR>a b : α<VAR>l : List α<VAR>h : Sorted r (a :: b :: l)<GOAL>insertionSort r (a :: b :: l) = a :: b :: l
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>inst✝ : DecidableRel r<VAR>a b : α<VAR>l : List α<VAR>h : Sorted r (a :: b :: l)<GOAL>r a b
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>inst✝ : DecidableRel r<VAR>a b : α<VAR>l : List α<VAR>h : Sorted r (a :: b :: l)<GOAL>Sorted r (b :: l)
<VAR>x y : ℝ<VAR>n : ℕ<GOAL>0 ≤ log (-↑n)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : α → β<VAR>a : α<VAR>l : List α<GOAL>(map f (a :: l)).sublists' = map (map f) (a :: l).sublists'
<VAR>α : Type u<VAR>β : Type v<VAR>e✝ : α ≃ β<VAR>R : Type u_1<VAR>inst✝² : CommSemiring R<VAR>e : α ≃ β<VAR>inst✝¹ : Semiring β<VAR>inst✝ : Algebra R β<VAR>r : R<VAR>semiring✝ : Semiring α := e.semiring<VAR>algebra✝ : Algebra R α := Equiv.algebra R e<GOAL>(algebraMap R α) r = e.symm ((algebraMap R β) r)
<VAR>α : Type u<VAR>β : Type v<VAR>e✝ : α ≃ β<VAR>R : Type u_1<VAR>inst✝² : CommSemiring R<VAR>e : α ≃ β<VAR>inst✝¹ : Semiring β<VAR>inst✝ : Algebra R β<VAR>r : R<VAR>semiring✝ : Semiring α := e.semiring<VAR>algebra✝ : Algebra R α := Equiv.algebra R e<GOAL>r • 1 = e.symm (r • 1)
<VAR>α : Type u<VAR>β : Type v<VAR>e✝ : α ≃ β<VAR>R : Type u_1<VAR>inst✝² : CommSemiring R<VAR>e : α ≃ β<VAR>inst✝¹ : Semiring β<VAR>inst✝ : Algebra R β<VAR>r : R<VAR>semiring✝ : Semiring α := e.semiring<VAR>algebra✝ : Algebra R α := Equiv.algebra R e<GOAL>e.symm (r • e 1) = e.symm (r • 1)
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hdf : ∀ᶠ (x : ℝ) in 𝓝[>] a, DifferentiableAt ℝ f x<VAR>hg' : ∀ᶠ (x : ℝ) in 𝓝[>] a, deriv g x ≠ 0<VAR>hfa : Tendsto f (𝓝[>] a) (𝓝 0)<VAR>hga : Tendsto g (𝓝[>] a) (𝓝 0)<VAR>hdiv : Tendsto (fun x => deriv f x / deriv g x) (𝓝[>] a) l<GOAL>Tendsto (fun x => f x / g x) (𝓝[>] a) l
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hdf : ∀ᶠ (x : ℝ) in 𝓝[>] a, DifferentiableAt ℝ f x<VAR>hg' : ∀ᶠ (x : ℝ) in 𝓝[>] a, deriv g x ≠ 0<VAR>hfa : Tendsto f (𝓝[>] a) (𝓝 0)<VAR>hga : Tendsto g (𝓝[>] a) (𝓝 0)<VAR>hdiv : Tendsto (fun x => deriv f x / deriv g x) (𝓝[>] a) l<VAR>hdg : ∀ᶠ (x : ℝ) in 𝓝[>] a, DifferentiableAt ℝ g x<GOAL>Tendsto (fun x => f x / g x) (𝓝[>] a) l
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hdf : ∀ᶠ (x : ℝ) in 𝓝[>] a, DifferentiableAt ℝ f x<VAR>hg' : ∀ᶠ (x : ℝ) in 𝓝[>] a, deriv g x ≠ 0<VAR>hfa : Tendsto f (𝓝[>] a) (𝓝 0)<VAR>hga : Tendsto g (𝓝[>] a) (𝓝 0)<VAR>hdiv : Tendsto (fun x => deriv f x / deriv g x) (𝓝[>] a) l<VAR>hdg : ∀ᶠ (x : ℝ) in 𝓝[>] a, DifferentiableAt ℝ g x<VAR>hdf' : ∀ᶠ (x : ℝ) in 𝓝[>] a, HasDerivAt f (deriv f x) x<GOAL>Tendsto (fun x => f x / g x) (𝓝[>] a) l
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hdf : ∀ᶠ (x : ℝ) in 𝓝[>] a, DifferentiableAt ℝ f x<VAR>hg' : ∀ᶠ (x : ℝ) in 𝓝[>] a, deriv g x ≠ 0<VAR>hfa : Tendsto f (𝓝[>] a) (𝓝 0)<VAR>hga : Tendsto g (𝓝[>] a) (𝓝 0)<VAR>hdiv : Tendsto (fun x => deriv f x / deriv g x) (𝓝[>] a) l<VAR>hdg : ∀ᶠ (x : ℝ) in 𝓝[>] a, DifferentiableAt ℝ g x<VAR>hdf' : ∀ᶠ (x : ℝ) in 𝓝[>] a, HasDerivAt f (deriv f x) x<VAR>hdg' : ∀ᶠ (x : ℝ) in 𝓝[>] a, HasDerivAt g (deriv g x) x<GOAL>Tendsto (fun x => f x / g x) (𝓝[>] a) l
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>𝒜 : Finset (Finset α)<VAR>s t : Finset α<VAR>a : α<VAR>k r : ℕ<GOAL>t ∈ ∂⁺ 𝒜 ↔ ∃ s ∈ 𝒜, s ⊆ t ∧ t.card = s.card + 1
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>𝒜 : Finset (Finset α)<VAR>s t✝ : Finset α<VAR>a : α<VAR>k r : ℕ<VAR>t : Finset α<VAR>x✝ : t ∈ 𝒜<VAR>hst : t ⊆ t✝<GOAL>(t✝ \ t).card = 1 ↔ t✝.card = t.card + 1
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>𝒜 : Finset (Finset α)<VAR>s t✝ : Finset α<VAR>a : α<VAR>k r : ℕ<VAR>t : Finset α<VAR>x✝ : t ∈ 𝒜<VAR>hst : t ⊆ t✝<GOAL>t.card ≤ t✝.card
<VAR>R : Type u<VAR>S : Type u_1<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : Semiring S<VAR>I : Ideal R[X]<VAR>m n : ℕ<VAR>H : m ≤ n<VAR>r : R<VAR>hr : r ∈ I.leadingCoeffNth m<GOAL>r ∈ I.leadingCoeffNth n
<VAR>R : Type u<VAR>S : Type u_1<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : Semiring S<VAR>I : Ideal R[X]<VAR>m n : ℕ<VAR>H : m ≤ n<VAR>r : R<VAR>hr : ∃ p ∈ I, p.degree ≤ ↑m ∧ p.leadingCoeff = r<GOAL>∃ p ∈ I, p.degree ≤ ↑n ∧ p.leadingCoeff = r
<VAR>R : Type u<VAR>S : Type u_1<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : Semiring S<VAR>I : Ideal R[X]<VAR>m n : ℕ<VAR>H : m ≤ n<VAR>p : R[X]<VAR>hpI : p ∈ I<VAR>hpdeg : p.degree ≤ ↑m<GOAL>∃ p_1 ∈ I, p_1.degree ≤ ↑n ∧ p_1.leadingCoeff = p.leadingCoeff
<VAR>R : Type u<VAR>S : Type u_1<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : Semiring S<VAR>I : Ideal R[X]<VAR>m n : ℕ<VAR>H : m ≤ n<VAR>p : R[X]<VAR>hpI : p ∈ I<VAR>hpdeg : p.degree ≤ ↑m<GOAL>(p * X ^ (n - m)).degree ≤ ↑n
<VAR>R : Type u<VAR>S : Type u_1<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : Semiring S<VAR>I : Ideal R[X]<VAR>m n : ℕ<VAR>H : m ≤ n<VAR>p : R[X]<VAR>hpI : p ∈ I<VAR>hpdeg : p.degree ≤ ↑m<GOAL>p.degree + (X ^ (n - m)).degree ≤ ↑n
<VAR>R : Type u<VAR>S : Type u_1<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : Semiring S<VAR>I : Ideal R[X]<VAR>m n : ℕ<VAR>H : m ≤ n<VAR>p : R[X]<VAR>hpI : p ∈ I<VAR>hpdeg : p.degree ≤ ↑m<GOAL>↑m + ↑(n - m) ≤ ↑n
<VAR>R : Type u<VAR>M : Type v<VAR>N : Type w<VAR>inst✝⁷ : CommSemiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>σ : Type u_1<VAR>inst✝⁴ : DecidableEq σ<VAR>S : Type u_2<VAR>inst✝³ : CommSemiring S<VAR>inst✝² : Algebra R S<VAR>inst✝¹ : CommSemiring N<VAR>inst✝ : Algebra R N<VAR>p : MvPolynomial σ S ⊗[R] N<GOAL>rTensorAlgHom p = rTensor p
<VAR>R : Type u<VAR>M : Type v<VAR>N : Type w<VAR>inst✝⁷ : CommSemiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>σ : Type u_1<VAR>inst✝⁴ : DecidableEq σ<VAR>S : Type u_2<VAR>inst✝³ : CommSemiring S<VAR>inst✝² : Algebra R S<VAR>inst✝¹ : CommSemiring N<VAR>inst✝ : Algebra R N<VAR>p : MvPolynomial σ S ⊗[R] N<GOAL>↑rTensor p = rTensor p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ε : Type u_5<VAR>ι : Type u_6<VAR>f✝ : α →. β<VAR>f : α → β<VAR>s : Set α<VAR>t : Set β<VAR>x : α<GOAL>x ∈ (res f s).core t ↔ x ∈ s → f x ∈ t
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>c : R<VAR>f : RingSeminorm R<VAR>hf1 : f 1 ≤ 1<VAR>hc : f c ≠ 0<VAR>hpm : IsPowMul ⇑f<VAR>x : R<VAR>m n : ℕ<VAR>hmn : m ≤ n<GOAL>f (x * c ^ n) / f c ^ n ≤ f (x * c ^ m) / f c ^ m
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>c : R<VAR>f : RingSeminorm R<VAR>hf1 : f 1 ≤ 1<VAR>hc : f c ≠ 0<VAR>hpm : IsPowMul ⇑f<VAR>x : R<VAR>m n : ℕ<VAR>hmn : m ≤ n<GOAL>f (x * c ^ (m + (n - m))) / f c ^ n ≤ f (x * c ^ m) / f c ^ m
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>c : R<VAR>f : RingSeminorm R<VAR>hf1 : f 1 ≤ 1<VAR>hc : f c ≠ 0<VAR>hpm : IsPowMul ⇑f<VAR>x : R<VAR>m n : ℕ<VAR>hmn : m ≤ n<GOAL>f (x * c ^ m * c ^ (n - m)) / f c ^ n ≤ f (x * c ^ m) / f c ^ m
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>c : R<VAR>f : RingSeminorm R<VAR>hf1 : f 1 ≤ 1<VAR>hc : f c ≠ 0<VAR>hpm : IsPowMul ⇑f<VAR>x : R<VAR>m n : ℕ<VAR>hmn : m ≤ n<VAR>hc_pos : 0 < f c<GOAL>f (x * c ^ m * c ^ (n - m)) / f c ^ n ≤ f (x * c ^ m) / f c ^ m
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>c : R<VAR>f : RingSeminorm R<VAR>hf1 : f 1 ≤ 1<VAR>hc : f c ≠ 0<VAR>hpm : IsPowMul ⇑f<VAR>x : R<VAR>m n : ℕ<VAR>hmn : m ≤ n<VAR>hc_pos : 0 < f c<GOAL>f (x * c ^ m) * f (c ^ (n - m)) / f c ^ n ≤ f (x * c ^ m) / f c ^ m
<VAR>τ : Type u_1<VAR>inst✝³ : AddCommGroup τ<VAR>inst✝² : TopologicalSpace τ<VAR>inst✝¹ : TopologicalAddGroup τ<VAR>α : Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>ϕ : Flow τ α<VAR>s : Set α<VAR>h : ∀ (t : τ), ϕ.toFun t '' s ⊆ s<VAR>t : τ<VAR>x✝ : α<VAR>hx : x✝ ∈ s<GOAL>ϕ.toFun t (ϕ.toFun (-t) x✝) = x✝
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l F : Filter α<VAR>s : Set α<GOAL>F ⊓ 𝓟 s = ⊥ ↔ comap Subtype.val F = ⊥
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>γ' : 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>ν : Type u_13<VAR>inst✝⁷ : DecidableEq α'<VAR>inst✝⁶ : DecidableEq β'<VAR>inst✝⁵ : DecidableEq γ<VAR>inst✝⁴ : DecidableEq γ'<VAR>inst✝³ : DecidableEq δ<VAR>inst✝² : DecidableEq δ'<VAR>inst✝¹ : DecidableEq ε<VAR>inst✝ : DecidableEq ε'<VAR>f f'✝ : α → β → γ<VAR>g✝ g' : α → β → γ → δ<VAR>s s' : Finset α<VAR>t t' : Finset β<VAR>u u' : Finset γ<VAR>a a' : α<VAR>b b' : β<VAR>c : γ<VAR>g : γ → δ<VAR>f' : β' → α' → δ<VAR>g₁ : β → β'<VAR>g₂ : α → α'<VAR>h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' (g₁ b) (g₂ a)<GOAL>image g (image₂ f s t) = image₂ f' (image g₁ t) (image g₂ s)
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>γ' : 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>ν : Type u_13<VAR>inst✝⁷ : DecidableEq α'<VAR>inst✝⁶ : DecidableEq β'<VAR>inst✝⁵ : DecidableEq γ<VAR>inst✝⁴ : DecidableEq γ'<VAR>inst✝³ : DecidableEq δ<VAR>inst✝² : DecidableEq δ'<VAR>inst✝¹ : DecidableEq ε<VAR>inst✝ : DecidableEq ε'<VAR>f f'✝ : α → β → γ<VAR>g✝ g' : α → β → γ → δ<VAR>s s' : Finset α<VAR>t t' : Finset β<VAR>u u' : Finset γ<VAR>a a' : α<VAR>b b' : β<VAR>c : γ<VAR>g : γ → δ<VAR>f' : β' → α' → δ<VAR>g₁ : β → β'<VAR>g₂ : α → α'<VAR>h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' (g₁ b) (g₂ a)<GOAL>image g (image₂ (fun a b => f b a) t s) = image₂ f' (image g₁ t) (image g₂ s)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹⁰ : Semifield R<VAR>inst✝⁹ : StarRing R<VAR>inst✝⁸ : MetricSpace R<VAR>inst✝⁷ : TopologicalSemiring R<VAR>inst✝⁶ : ContinuousStar R<VAR>inst✝⁵ : HasContinuousInv₀ R<VAR>inst✝⁴ : TopologicalSpace A<VAR>inst✝³ : Ring A<VAR>inst✝² : StarRing A<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : ContinuousFunctionalCalculus R p<VAR>f : R → R<VAR>a : A<VAR>hf' : ∀ x ∈ spectrum R a, f x ≠ 0<VAR>hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝<VAR>ha : autoParam (p a) _auto✝<GOAL>cfc (fun x => (f x)⁻¹) a = Ring.inverse (cfc f a)
<VAR>R : Type u<VAR>S✝ : Type v<VAR>F : Type w<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : Semiring S✝<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝⁵ : CommSemiring R₁<VAR>inst✝⁴ : CommSemiring R₂<VAR>inst✝³ : CommRing A<VAR>inst✝² : Algebra R₁ A<VAR>inst✝¹ : Algebra R₂ A<VAR>S : Type v<VAR>inst✝ : CommRing S<VAR>I : Ideal R<VAR>J : Ideal S<VAR>f : R ≃+* S<VAR>hIJ : J = map (↑f) I<GOAL>I ≤ comap (↑f) (map (↑f) I)
<VAR>R : Type u<VAR>S✝ : Type v<VAR>F : Type w<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : Semiring S✝<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝⁵ : CommSemiring R₁<VAR>inst✝⁴ : CommSemiring R₂<VAR>inst✝³ : CommRing A<VAR>inst✝² : Algebra R₁ A<VAR>inst✝¹ : Algebra R₂ A<VAR>S : Type v<VAR>inst✝ : CommRing S<VAR>I : Ideal R<VAR>J : Ideal S<VAR>f : R ≃+* S<VAR>hIJ : J = map (↑f) I<GOAL>map (↑f) I ≤ comap (↑f.symm) I
<VAR>R : Type u<VAR>S✝ : Type v<VAR>F : Type w<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : Semiring S✝<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝⁵ : CommSemiring R₁<VAR>inst✝⁴ : CommSemiring R₂<VAR>inst✝³ : CommRing A<VAR>inst✝² : Algebra R₁ A<VAR>inst✝¹ : Algebra R₂ A<VAR>S : Type v<VAR>inst✝ : CommRing S<VAR>I : Ideal R<VAR>J : Ideal S<VAR>f : R ≃+* S<VAR>hIJ : J = map (↑f) I<VAR>x✝ : R ⧸ I<VAR>r : R<GOAL>(quotientMap I ↑f.symm ⋯) ((↑↑__src✝).toFun (Quot.mk Setoid.r r)) = Quot.mk Setoid.r r
<VAR>R : Type u<VAR>S✝ : Type v<VAR>F : Type w<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : Semiring S✝<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝⁵ : CommSemiring R₁<VAR>inst✝⁴ : CommSemiring R₂<VAR>inst✝³ : CommRing A<VAR>inst✝² : Algebra R₁ A<VAR>inst✝¹ : Algebra R₂ A<VAR>S : Type v<VAR>inst✝ : CommRing S<VAR>I : Ideal R<VAR>J : Ideal S<VAR>f : R ≃+* S<VAR>hIJ : J = map (↑f) I<VAR>x✝ : S ⧸ J<VAR>s : S<GOAL>(↑↑__src✝).toFun ((quotientMap I ↑f.symm ⋯) (Quot.mk Setoid.r s)) = Quot.mk Setoid.r s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g : ι → α<VAR>hF : TendstoUniformlyOnFilter F f p p'<VAR>u : Set (β × β)<VAR>hu : u ∈ 𝓤 β<GOAL>∀ᶠ (m : (ι × ι) × α) in (p ×ˢ p) ×ˢ p', (F m.1.1 m.2, F m.1.2 m.2) ∈ u
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g : ι → α<VAR>hF : TendstoUniformlyOnFilter F f p p'<VAR>u : Set (β × β)<VAR>hu : u ∈ 𝓤 β<VAR>t : Set (β × β)<VAR>ht : t ∈ 𝓤 β<VAR>htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t<VAR>htmem : t ○ t ⊆ u<GOAL>∀ᶠ (m : (ι × ι) × α) in (p ×ˢ p) ×ˢ p', (F m.1.1 m.2, F m.1.2 m.2) ∈ u
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g : ι → α<VAR>hF : TendstoUniformlyOnFilter F f p p'<VAR>u : Set (β × β)<VAR>hu : u ∈ 𝓤 β<VAR>t : Set (β × β)<VAR>ht : t ∈ 𝓤 β<VAR>htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t<VAR>htmem : t ○ t ⊆ u<VAR>this : ∀ᶠ (x : (ι × ι) × α × α) in (p ×ˢ p) ×ˢ p' ×ˢ p', (f ((x.1.1, x.2.1), x.1.2, x.2.2).1.2, F ((x.1.1, x.2.1), x.1.2, x.2.2).1.1 ((x.1.1, x.2.1), x.1.2, x.2.2).1.2) ∈ t ∧ (f ((x.1.1, x.2.1), x.1.2, x.2.2).2.2, F ((x.1.1, x.2.1), x.1.2, x.2.2).2.1 ((x.1.1, x.2.1), x.1.2, x.2.2).2.2) ∈ t<GOAL>∀ᶠ (m : (ι × ι) × α) in (p ×ˢ p) ×ˢ p', (F m.1.1 m.2, F m.1.2 m.2) ∈ u
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g : ι → α<VAR>hF : TendstoUniformlyOnFilter F f p p'<VAR>u : Set (β × β)<VAR>hu : u ∈ 𝓤 β<VAR>t : Set (β × β)<VAR>ht : t ∈ 𝓤 β<VAR>htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t<VAR>htmem : t ○ t ⊆ u<VAR>this : ∀ᶠ (x : (ι × ι) × α × α) in (p ×ˢ p) ×ˢ p' ×ˢ p', (f ((x.1.1, x.2.1), x.1.2, x.2.2).1.2, F ((x.1.1, x.2.1), x.1.2, x.2.2).1.1 ((x.1.1, x.2.1), x.1.2, x.2.2).1.2) ∈ t ∧ (f ((x.1.1, x.2.1), x.1.2, x.2.2).2.2, F ((x.1.1, x.2.1), x.1.2, x.2.2).2.1 ((x.1.1, x.2.1), x.1.2, x.2.2).2.2) ∈ t<GOAL>∀ (x : (ι × ι) × α), (f (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).1.2, F (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).1.1 (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).1.2) ∈ t ∧ (f (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).2.2, F (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).2.1 (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).2.2) ∈ t → (F x.1.1 x.2, F x.1.2 x.2) ∈ u
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g : ι → α<VAR>hF : TendstoUniformlyOnFilter F f p p'<VAR>u : Set (β × β)<VAR>hu : u ∈ 𝓤 β<VAR>t : Set (β × β)<VAR>ht : t ∈ 𝓤 β<VAR>htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t<VAR>htmem : t ○ t ⊆ u<VAR>this : ∀ᶠ (x : (ι × ι) × α × α) in (p ×ˢ p) ×ˢ p' ×ˢ p', (f ((x.1.1, x.2.1), x.1.2, x.2.2).1.2, F ((x.1.1, x.2.1), x.1.2, x.2.2).1.1 ((x.1.1, x.2.1), x.1.2, x.2.2).1.2) ∈ t ∧ (f ((x.1.1, x.2.1), x.1.2, x.2.2).2.2, F ((x.1.1, x.2.1), x.1.2, x.2.2).2.1 ((x.1.1, x.2.1), x.1.2, x.2.2).2.2) ∈ t<GOAL>∀ (a b : ι) (b_1 : α), (f b_1, F a b_1) ∈ t → (f b_1, F b b_1) ∈ t → (F a b_1, F b b_1) ∈ u
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x✝ : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g : ι → α<VAR>hF : TendstoUniformlyOnFilter F f p p'<VAR>u : Set (β × β)<VAR>hu : u ∈ 𝓤 β<VAR>t : Set (β × β)<VAR>ht : t ∈ 𝓤 β<VAR>htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t<VAR>htmem : t ○ t ⊆ u<VAR>this : ∀ᶠ (x : (ι × ι) × α × α) in (p ×ˢ p) ×ˢ p' ×ˢ p', (f ((x.1.1, x.2.1), x.1.2, x.2.2).1.2, F ((x.1.1, x.2.1), x.1.2, x.2.2).1.1 ((x.1.1, x.2.1), x.1.2, x.2.2).1.2) ∈ t ∧ (f ((x.1.1, x.2.1), x.1.2, x.2.2).2.2, F ((x.1.1, x.2.1), x.1.2, x.2.2).2.1 ((x.1.1, x.2.1), x.1.2, x.2.2).2.2) ∈ t<VAR>n1 n2 : ι<VAR>x : α<VAR>hl : (f x, F n1 x) ∈ t<VAR>hr : (f x, F n2 x) ∈ t<GOAL>(F n1 x, F n2 x) ∈ u
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedRing α<VAR>n : ℕ<VAR>a✝ b✝ c a b : α<GOAL>a ^ 2 = b ^ 2 ↔ |a| = |b|
<VAR>α : Type u_1<VAR>F : Type u_2<VAR>F' : Type u_3<VAR>𝕜 : Type u_4<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>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f g : α → F'<VAR>s : Set α<VAR>hm : m ≤ m0<VAR>hμm this : SigmaFinite (μ.trim hm)<GOAL>μ[0|m] = 0
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>J : GrothendieckTopology C<VAR>R₀ : Cᵒᵖ ⥤ RingCat<VAR>R : Sheaf J RingCat<VAR>α : R₀ ⟶ R.val<VAR>inst✝³ : Presheaf.IsLocallyInjective J α<VAR>inst✝² : Presheaf.IsLocallySurjective J α<VAR>M₀ : PresheafOfModules R₀<VAR>A : Sheaf J AddCommGrp<VAR>φ : M₀.presheaf ⟶ A.val<VAR>inst✝¹ : Presheaf.IsLocallyInjective J φ<VAR>inst✝ : Presheaf.IsLocallySurjective J φ<VAR>X Y : Cᵒᵖ<VAR>π : X ⟶ Y<VAR>r r' : ↑(R.val.obj X)<VAR>m m' : ↑(A.val.obj X)<VAR>S : Sieve (Opposite.unop X) := Presheaf.imageSieve α r ⊓ Presheaf.imageSieve α r' ⊓ Presheaf.imageSieve φ m<GOAL>smul α φ (r + r') m = smul α φ r m + smul α φ r' m
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>J : GrothendieckTopology C<VAR>R₀ : Cᵒᵖ ⥤ RingCat<VAR>R : Sheaf J RingCat<VAR>α : R₀ ⟶ R.val<VAR>inst✝³ : Presheaf.IsLocallyInjective J α<VAR>inst✝² : Presheaf.IsLocallySurjective J α<VAR>M₀ : PresheafOfModules R₀<VAR>A : Sheaf J AddCommGrp<VAR>φ : M₀.presheaf ⟶ A.val<VAR>inst✝¹ : Presheaf.IsLocallyInjective J φ<VAR>inst✝ : Presheaf.IsLocallySurjective J φ<VAR>X Y : Cᵒᵖ<VAR>π : X ⟶ Y<VAR>r r' : ↑(R.val.obj X)<VAR>m m' : ↑(A.val.obj X)<VAR>S : Sieve (Opposite.unop X) := Presheaf.imageSieve α r ⊓ Presheaf.imageSieve α r' ⊓ Presheaf.imageSieve φ m<VAR>hS : S ∈ J.sieves (Opposite.unop X)<GOAL>smul α φ (r + r') m = smul α φ r m + smul α φ r' m
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>J : GrothendieckTopology C<VAR>R₀ : Cᵒᵖ ⥤ RingCat<VAR>R : Sheaf J RingCat<VAR>α : R₀ ⟶ R.val<VAR>inst✝³ : Presheaf.IsLocallyInjective J α<VAR>inst✝² : Presheaf.IsLocallySurjective J α<VAR>M₀ : PresheafOfModules R₀<VAR>A : Sheaf J AddCommGrp<VAR>φ : M₀.presheaf ⟶ A.val<VAR>inst✝¹ : Presheaf.IsLocallyInjective J φ<VAR>inst✝ : Presheaf.IsLocallySurjective J φ<VAR>X Y : Cᵒᵖ<VAR>π : X ⟶ Y<VAR>r r' : ↑(R.val.obj X)<VAR>m m' : ↑(A.val.obj X)<VAR>S : Sieve (Opposite.unop X) := Presheaf.imageSieve α r ⊓ Presheaf.imageSieve α r' ⊓ Presheaf.imageSieve φ m<VAR>hS : S ∈ J.sieves (Opposite.unop X)<GOAL>∀ (Y : C) (f : Y ⟶ Opposite.unop X), S.arrows f → (A.val.map f.op) (smul α φ (r + r') m) = (A.val.map f.op) (smul α φ r m + smul α φ r' m)
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>J : GrothendieckTopology C<VAR>R₀ : Cᵒᵖ ⥤ RingCat<VAR>R : Sheaf J RingCat<VAR>α : R₀ ⟶ R.val<VAR>inst✝³ : Presheaf.IsLocallyInjective J α<VAR>inst✝² : Presheaf.IsLocallySurjective J α<VAR>M₀ : PresheafOfModules R₀<VAR>A : Sheaf J AddCommGrp<VAR>φ : M₀.presheaf ⟶ A.val<VAR>inst✝¹ : Presheaf.IsLocallyInjective J φ<VAR>inst✝ : Presheaf.IsLocallySurjective J φ<VAR>X Y✝ : Cᵒᵖ<VAR>π : X ⟶ Y✝<VAR>r r' : ↑(R.val.obj X)<VAR>m m' : ↑(A.val.obj X)<VAR>S : Sieve (Opposite.unop X) := Presheaf.imageSieve α r ⊓ Presheaf.imageSieve α r' ⊓ Presheaf.imageSieve φ m<VAR>hS : S ∈ J.sieves (Opposite.unop X)<VAR>Y : C<VAR>f : Y ⟶ Opposite.unop X<VAR>r₀ : ↑(R₀.obj (Opposite.op Y))<VAR>hr₀ : (α.app (Opposite.op Y)) r₀ = (R.val.map f.op) r<VAR>r₀' : ↑(R₀.obj (Opposite.op Y))<VAR>hr₀' : (α.app (Opposite.op Y)) r₀' = (R.val.map f.op) r'<VAR>m₀ : (forget AddCommGrp).obj (M₀.presheaf.obj (Opposite.op Y))<VAR>hm₀ : (φ.app (Opposite.op Y)) m₀ = (A.val.map f.op) m<GOAL>(A.val.map f.op) (smul α φ (r + r') m) = (A.val.map f.op) (smul α φ r m + smul α φ r' m)
<VAR>K : Type u_1<VAR>F : Type u_2<VAR>R : Type u_3<VAR>inst✝³ : DivisionRing K<VAR>Γ₀ : Type u_4<VAR>Γ'₀ : Type u_5<VAR>Γ''₀ : Type u_6<VAR>inst✝² : LinearOrderedCommMonoidWithZero Γ''₀<VAR>inst✝¹ : Ring R<VAR>inst✝ : LinearOrderedCommGroupWithZero Γ₀<VAR>v✝ : Valuation R Γ₀<VAR>x✝ y z : R<VAR>v : Valuation K Γ₀<VAR>x : K<VAR>h : x ≠ 0<GOAL>v x < 1 ↔ 1 < v 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>x✝ : M<GOAL>x✝ ∈ span R {0} ↔ x✝ ∈ ⊥
<VAR>x y : ℝ<VAR>h : x ≤ 0<GOAL>√x = 0
<VAR>b x : Ordinal.{u_1}<VAR>hx : x ≠ 0<GOAL>b ^ log b x ≤ x
<VAR>x : Ordinal.{u_1}<VAR>hx : x ≠ 0<GOAL>0 ^ log 0 x ≤ x
<VAR>b x : Ordinal.{u_1}<VAR>hx : x ≠ 0<VAR>b0 : b ≠ 0<GOAL>b ^ log b x ≤ x
<VAR>b x : Ordinal.{u_1}<VAR>hx : x ≠ 0<VAR>b0 : b ≠ 0<VAR>hb : 1 < b<GOAL>b ^ log b x ≤ x
<VAR>x : Ordinal.{u_1}<VAR>hx : x ≠ 0<VAR>b0 : 1 ≠ 0<GOAL>1 ^ log 1 x ≤ x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>e : α ≃o β<VAR>l : Filter γ<VAR>u : γ → α<VAR>a : α<GOAL>(∀ᶠ (x : β) in map (fun x => e (u x)) l, (fun x x_1 => x ≤ x_1) x (e a)) ↔ ∀ᶠ (x : α) in map u l, (fun x x_1 => x ≤ x_1) x a
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : ClosedIicTopology α<VAR>inst✝ : TopologicalSpace β<VAR>a b c : α<VAR>f : α → β<GOAL>IsOpen (Ioi a)