ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>Γ : Subgroup SL(2, ℤ)<VAR>k : ℤ<VAR>f : ℍ → ℂ<VAR>A : SL(2, ℤ)<VAR>x : ℂ<VAR>this : (↑↑↑A).det = 1<VAR>x✝ : ℍ<GOAL>Function.const ℍ x (↑A • x✝) * ↑1 ^ (-1) * denom (↑A) x✝ ^ (-0) = Function.const ℍ x x✝
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l : Filter α<VAR>f : Filter (α → β)<VAR>a : α<GOAL>f.seq (pure a) = map (fun g => g a) f
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l : Filter α<VAR>f : Filter (α → β)<VAR>a : α<VAR>s : Set (α → β)<VAR>hs : s ∈ f<GOAL>(fun g => g a) '' s ∈ f.seq (pure a)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l : Filter α<VAR>f : Filter (α → β)<VAR>a : α<VAR>s : Set (α → β)<VAR>hs : s ∈ f<VAR>t : Set α<VAR>ht : t ∈ pure a<GOAL>s.seq t ∈ map (fun g => g a) f
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring S<VAR>inst✝ : Algebra R S<VAR>M N : Submodule R S<VAR>n : ↥N<GOAL>N.lTensorOne' (1 ⊗ₜ[R] n) = n
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁹ : NormedAddCommGroup D<VAR>inst✝⁸ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>i : ℕ<VAR>hf : ContDiffAt 𝕜 n f x₀<VAR>hmn : m + ↑i ≤ n<GOAL>ContDiffAt 𝕜 m (iteratedFDeriv 𝕜 i f) x₀
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁹ : NormedAddCommGroup D<VAR>inst✝⁸ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>i : ℕ<VAR>hf : ContDiffWithinAt 𝕜 n f univ x₀<VAR>hmn : m + ↑i ≤ n<GOAL>ContDiffWithinAt 𝕜 m (iteratedFDerivWithin 𝕜 i f univ) univ x₀
<VAR>x✝ y x : ℝ<GOAL>cosh (arsinh x) = √(1 + x ^ 2)
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → Zero (β i)<VAR>s : Finset ι<VAR>x : (i : ↑↑s) → β ↑i<VAR>i : ι<VAR>f : Π₀ (i : ι), β i<VAR>b : β i<VAR>j✝ j : ι<GOAL>(update i f 0) j = (erase i f) j
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → Zero (β i)<VAR>s : Finset ι<VAR>x : (i : ↑↑s) → β ↑i<VAR>i : ι<VAR>f : Π₀ (i : ι), β i<VAR>b : β i<VAR>j : ι<GOAL>(update i f 0) i = (erase i f) i
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → Zero (β i)<VAR>s : Finset ι<VAR>x : (i : ↑↑s) → β ↑i<VAR>i : ι<VAR>f : Π₀ (i : ι), β i<VAR>b : β i<VAR>j✝ j : ι<VAR>hi : i ≠ j<GOAL>(update i f 0) j = (erase i f) j
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq β<VAR>k : β<VAR>b : α → β<GOAL>image (fun i => b ↑i) univ = (image b univ).erase k
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq β<VAR>k : β<VAR>b : α → β<GOAL>image (fun i => b ↑i) univ ⊆ (image b univ).erase k
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq β<VAR>k : β<VAR>b : α → β<GOAL>(image b univ).erase k ⊆ image (fun i => b ↑i) univ
<VAR>α β : Type u<VAR>a : Cardinal.{u}<VAR>n : ℕ<GOAL>lift.{v, u} a ≤ ↑n ↔ a ≤ ↑n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Finset α<VAR>a b : α<GOAL>s.sym2 = ∅ ↔ s = ∅
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoMetricSpace α<VAR>x y : Completion α<GOAL>dist x y = dist y x
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoMetricSpace α<VAR>x y : Completion α<GOAL>IsClosed {x | dist x.1 x.2 = dist x.2 x.1}
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoMetricSpace α<VAR>x y : Completion α<GOAL>∀ (a b : α), dist (↑α a) (↑α b) = dist (↑α b) (↑α a)
<VAR>α : Type u<VAR>β : Type v<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<VAR>fst✝¹ : Perm { a // p a }<VAR>snd✝¹ : Perm { a // ¬p a }<VAR>fst✝ : Perm { a // p a }<VAR>snd✝ : Perm { a // ¬p a }<VAR>h : (subtypeCongrHom p) (fst✝¹, snd✝¹) = (subtypeCongrHom p) (fst✝, snd✝)<GOAL>(fst✝¹, snd✝¹) = (fst✝, snd✝)
<VAR>α : Type u<VAR>β : Type v<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<VAR>fst✝¹ : Perm { a // p a }<VAR>snd✝¹ : Perm { a // ¬p a }<VAR>fst✝ : Perm { a // p a }<VAR>snd✝ : Perm { a // ¬p a }<VAR>h : (subtypeCongrHom p) (fst✝¹, snd✝¹) = (subtypeCongrHom p) (fst✝, snd✝)<GOAL>fst✝¹ = fst✝ ∧ snd✝¹ = snd✝
<VAR>o : Ordinal.{u_1}<VAR>ho : o ≤ 2<GOAL>Principal (fun x x_1 => x * x_1) o
<VAR>o : Ordinal.{u_1}<VAR>ho✝ : o ≤ 2<VAR>ho : o < 2<GOAL>Principal (fun x x_1 => x * x_1) o
<VAR>ho : 2 ≤ 2<GOAL>Principal (fun x x_1 => x * x_1) 2
<VAR>R : Type u<VAR>S : Type v<VAR>k : Type y<VAR>A : Type z<VAR>a✝ b : R<VAR>n : ℕ<VAR>inst✝¹ : Field R<VAR>p q : R[X]<VAR>K : Type u_1<VAR>inst✝ : Field K<VAR>f : K[X]<VAR>a : K<GOAL>f /ₘ (X - C a) + (X - C a) * derivative (f /ₘ (X - C a)) = derivative f
<VAR>R : Type u<VAR>S : Type v<VAR>k : Type y<VAR>A : Type z<VAR>a✝ b : R<VAR>n : ℕ<VAR>inst✝¹ : Field R<VAR>p q : R[X]<VAR>K : Type u_1<VAR>inst✝ : Field K<VAR>f : K[X]<VAR>a : K<VAR>key : derivative ((X - C a) * (f /ₘ (X - C a))) = derivative (f - f %ₘ (X - C a))<GOAL>f /ₘ (X - C a) + (X - C a) * derivative (f /ₘ (X - C a)) = derivative f
<VAR>R : Type u<VAR>S : Type v<VAR>k : Type y<VAR>A : Type z<VAR>a✝ b : R<VAR>n : ℕ<VAR>inst✝¹ : Field R<VAR>p q : R[X]<VAR>K : Type u_1<VAR>inst✝ : Field K<VAR>f : K[X]<VAR>a : K<VAR>key : derivative ((X - C a) * (f /ₘ (X - C a))) = derivative (f - C (eval a f))<GOAL>f /ₘ (X - C a) + (X - C a) * derivative (f /ₘ (X - C a)) = derivative f
<VAR>R : Type u<VAR>S : Type v<VAR>k : Type y<VAR>A : Type z<VAR>a✝ b : R<VAR>n : ℕ<VAR>inst✝¹ : Field R<VAR>p q : R[X]<VAR>K : Type u_1<VAR>inst✝ : Field K<VAR>f : K[X]<VAR>a : K<VAR>key : (1 - derivative (C a)) * (f /ₘ (X - C a)) + (X - C a) * derivative (f /ₘ (X - C a)) = derivative f - derivative (C (eval a f))<GOAL>f /ₘ (X - C a) + (X - C a) * derivative (f /ₘ (X - C a)) = derivative f
<VAR>R : Type u<VAR>S : Type v<VAR>k : Type y<VAR>A : Type z<VAR>a✝ b : R<VAR>n : ℕ<VAR>inst✝¹ : Field R<VAR>p q : R[X]<VAR>K : Type u_1<VAR>inst✝ : Field K<VAR>f : K[X]<VAR>a : K<VAR>key : f /ₘ (X - C a) + (X - C a) * derivative (f /ₘ (X - C a)) = derivative f - derivative (C (eval a f))<GOAL>f /ₘ (X - C a) + (X - C a) * derivative (f /ₘ (X - C a)) = derivative f
<VAR>R : Type u<VAR>S : Type v<VAR>k : Type y<VAR>A : Type z<VAR>a✝ b : R<VAR>n : ℕ<VAR>inst✝¹ : Field R<VAR>p q : R[X]<VAR>K : Type u_1<VAR>inst✝ : Field K<VAR>f : K[X]<VAR>a : K<VAR>key : f /ₘ (X - C a) + (X - C a) * derivative (f /ₘ (X - C a)) = derivative f<GOAL>f /ₘ (X - C a) + (X - C a) * derivative (f /ₘ (X - C a)) = derivative f
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : Ring α<VAR>inst✝¹ : AddCommGroup β<VAR>inst✝ : Module α β<VAR>a : α<VAR>s : Set α<VAR>t : Set β<GOAL>-s • t = -(s • t)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : Ring α<VAR>inst✝¹ : AddCommGroup β<VAR>inst✝ : Module α β<VAR>a : α<VAR>s : Set α<VAR>t : Set β<GOAL>Neg.neg '' s • t = Neg.neg '' (s • t)
<VAR>ι : Type u_1<VAR>I J J₁ J₂ : Box ι<VAR>π π₁ π₂ : Prepartition I<VAR>x : ι → ℝ<GOAL>π₁.iUnion = ∅ ↔ π₁ = ⊥
<VAR>K : Type u<VAR>inst✝¹ : CommRing K<VAR>inst✝ : IsDomain K<VAR>P : Sort v<VAR>p q : K[X]<VAR>f : K[X] → K[X] → P<VAR>f0 : ∀ (p : K[X]), f p 0 = f 0 1<VAR>H : ∀ {p q a : K[X]}, q ≠ 0 → a ≠ 0 → f (a * p) (a * q) = f p q<GOAL>((algebraMap K[X] (RatFunc K)) p / (algebraMap K[X] (RatFunc K)) q).liftOn' f H = f p q
<VAR>K : Type u<VAR>inst✝¹ : CommRing K<VAR>inst✝ : IsDomain K<VAR>P : Sort v<VAR>p q : K[X]<VAR>f : K[X] → K[X] → P<VAR>f0 : ∀ (p : K[X]), f p 0 = f 0 1<VAR>H : ∀ {p q a : K[X]}, q ≠ 0 → a ≠ 0 → f (a * p) (a * q) = f p q<GOAL>∀ {p q p' q' : K[X]}, q ≠ 0 → q' ≠ 0 → q' * p = q * p' → f p q = f p' q'
<VAR>R : Type u_1<VAR>inst✝⁹ : Ring R<VAR>E : Type u_2<VAR>inst✝⁸ : AddCommGroup E<VAR>inst✝⁷ : Module R E<VAR>F : Type u_3<VAR>inst✝⁶ : AddCommGroup F<VAR>inst✝⁵ : Module R F<VAR>G : Type u_4<VAR>inst✝⁴ : AddCommGroup G<VAR>inst✝³ : Module R G<VAR>M : Type u_5<VAR>inst✝² : Monoid M<VAR>inst✝¹ : DistribMulAction M F<VAR>inst✝ : SMulCommClass R M F<VAR>y : M<VAR>f g : E →ₗ.[R] F<VAR>h : f ≤ g<VAR>x : E × F<VAR>hx : x ∈ f.graph<GOAL>x ∈ g.graph
<VAR>R : Type u_1<VAR>inst✝⁹ : Ring R<VAR>E : Type u_2<VAR>inst✝⁸ : AddCommGroup E<VAR>inst✝⁷ : Module R E<VAR>F : Type u_3<VAR>inst✝⁶ : AddCommGroup F<VAR>inst✝⁵ : Module R F<VAR>G : Type u_4<VAR>inst✝⁴ : AddCommGroup G<VAR>inst✝³ : Module R G<VAR>M : Type u_5<VAR>inst✝² : Monoid M<VAR>inst✝¹ : DistribMulAction M F<VAR>inst✝ : SMulCommClass R M F<VAR>y : M<VAR>f g : E →ₗ.[R] F<VAR>h : f ≤ g<VAR>x : E × F<VAR>hx : ∃ y, ↑y = x.1 ∧ ↑f y = x.2<GOAL>∃ y, ↑y = x.1 ∧ ↑g y = x.2
<VAR>R : Type u_1<VAR>inst✝⁹ : Ring R<VAR>E : Type u_2<VAR>inst✝⁸ : AddCommGroup E<VAR>inst✝⁷ : Module R E<VAR>F : Type u_3<VAR>inst✝⁶ : AddCommGroup F<VAR>inst✝⁵ : Module R F<VAR>G : Type u_4<VAR>inst✝⁴ : AddCommGroup G<VAR>inst✝³ : Module R G<VAR>M : Type u_5<VAR>inst✝² : Monoid M<VAR>inst✝¹ : DistribMulAction M F<VAR>inst✝ : SMulCommClass R M F<VAR>y✝ : M<VAR>f g : E →ₗ.[R] F<VAR>h : f ≤ g<VAR>x : E × F<VAR>y : ↥f.domain<VAR>hx : ↑y = x.1 ∧ ↑f y = x.2<GOAL>∃ y, ↑y = x.1 ∧ ↑g y = x.2
<VAR>R : Type u_1<VAR>inst✝⁹ : Ring R<VAR>E : Type u_2<VAR>inst✝⁸ : AddCommGroup E<VAR>inst✝⁷ : Module R E<VAR>F : Type u_3<VAR>inst✝⁶ : AddCommGroup F<VAR>inst✝⁵ : Module R F<VAR>G : Type u_4<VAR>inst✝⁴ : AddCommGroup G<VAR>inst✝³ : Module R G<VAR>M : Type u_5<VAR>inst✝² : Monoid M<VAR>inst✝¹ : DistribMulAction M F<VAR>inst✝ : SMulCommClass R M F<VAR>y✝ : M<VAR>f g : E →ₗ.[R] F<VAR>h : f ≤ g<VAR>x : E × F<VAR>y : ↥f.domain<VAR>hx : ↑y = x.1 ∧ ↑f y = x.2<GOAL>↑⟨↑y, ⋯⟩ = x.1 ∧ ↑g ⟨↑y, ⋯⟩ = x.2
<VAR>R : Type u_1<VAR>inst✝⁹ : Ring R<VAR>E : Type u_2<VAR>inst✝⁸ : AddCommGroup E<VAR>inst✝⁷ : Module R E<VAR>F : Type u_3<VAR>inst✝⁶ : AddCommGroup F<VAR>inst✝⁵ : Module R F<VAR>G : Type u_4<VAR>inst✝⁴ : AddCommGroup G<VAR>inst✝³ : Module R G<VAR>M : Type u_5<VAR>inst✝² : Monoid M<VAR>inst✝¹ : DistribMulAction M F<VAR>inst✝ : SMulCommClass R M F<VAR>y✝ : M<VAR>f g : E →ₗ.[R] F<VAR>h : f ≤ g<VAR>x : E × F<VAR>y : ↥f.domain<VAR>hx : ↑y = x.1 ∧ ↑f y = x.2<GOAL>↑g ⟨x.1, ⋯⟩ = x.2
<VAR>R : Type u_1<VAR>inst✝⁹ : Ring R<VAR>E : Type u_2<VAR>inst✝⁸ : AddCommGroup E<VAR>inst✝⁷ : Module R E<VAR>F : Type u_3<VAR>inst✝⁶ : AddCommGroup F<VAR>inst✝⁵ : Module R F<VAR>G : Type u_4<VAR>inst✝⁴ : AddCommGroup G<VAR>inst✝³ : Module R G<VAR>M : Type u_5<VAR>inst✝² : Monoid M<VAR>inst✝¹ : DistribMulAction M F<VAR>inst✝ : SMulCommClass R M F<VAR>y✝ : M<VAR>f g : E →ₗ.[R] F<VAR>h : f ≤ g<VAR>x : E × F<VAR>y : ↥f.domain<VAR>hx : ↑y = x.1 ∧ ↑f y = x.2<GOAL>↑g ⟨x.1, ⋯⟩ = ↑f y
<VAR>R : Type u_1<VAR>inst✝⁹ : Ring R<VAR>E : Type u_2<VAR>inst✝⁸ : AddCommGroup E<VAR>inst✝⁷ : Module R E<VAR>F : Type u_3<VAR>inst✝⁶ : AddCommGroup F<VAR>inst✝⁵ : Module R F<VAR>G : Type u_4<VAR>inst✝⁴ : AddCommGroup G<VAR>inst✝³ : Module R G<VAR>M : Type u_5<VAR>inst✝² : Monoid M<VAR>inst✝¹ : DistribMulAction M F<VAR>inst✝ : SMulCommClass R M F<VAR>y✝ : M<VAR>f g : E →ₗ.[R] F<VAR>h : f ≤ g<VAR>x : E × F<VAR>y : ↥f.domain<VAR>hx : ↑y = x.1 ∧ ↑f y = x.2<GOAL>↑y = ↑⟨x.1, ⋯⟩
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X Y Z : Scheme<VAR>𝒰 : X.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g<VAR>s : PullbackCone f g<GOAL>gluedLift 𝒰 f g s ≫ p2 𝒰 f g = s.snd
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X Y Z : Scheme<VAR>𝒰 : X.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g<VAR>s : PullbackCone f g<GOAL>(𝒰.pullbackCover s.fst).fromGlued ≫ gluedLift 𝒰 f g s ≫ p2 𝒰 f g = (𝒰.pullbackCover s.fst).fromGlued ≫ s.snd
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X Y Z : Scheme<VAR>𝒰 : X.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g<VAR>s : PullbackCone f g<GOAL>∀ (b : (𝒰.pullbackCover s.fst).gluedCover.diagram.R), Multicoequalizer.π (𝒰.pullbackCover s.fst).gluedCover.diagram b ≫ (𝒰.pullbackCover s.fst).fromGlued ≫ gluedLift 𝒰 f g s ≫ p2 𝒰 f g = Multicoequalizer.π (𝒰.pullbackCover s.fst).gluedCover.diagram b ≫ (𝒰.pullbackCover s.fst).fromGlued ≫ s.snd
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X Y Z : Scheme<VAR>𝒰 : X.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g<VAR>s : PullbackCone f g<VAR>b : (𝒰.pullbackCover s.fst).gluedCover.diagram.R<GOAL>Multicoequalizer.π (𝒰.pullbackCover s.fst).gluedCover.diagram b ≫ (𝒰.pullbackCover s.fst).fromGlued ≫ gluedLift 𝒰 f g s ≫ p2 𝒰 f g = Multicoequalizer.π (𝒰.pullbackCover s.fst).gluedCover.diagram b ≫ (𝒰.pullbackCover s.fst).fromGlued ≫ s.snd
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X Y Z : Scheme<VAR>𝒰 : X.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g<VAR>s : PullbackCone f g<VAR>b : (𝒰.pullbackCover s.fst).gluedCover.diagram.R<GOAL>((𝒰.pullbackCover s.fst).map b ≫ (𝒰.pullbackCover s.fst).glueMorphisms (fun i => ((pullbackSymmetry s.fst (𝒰.map i)).hom ≫ pullback.map (𝒰.map i) s.fst (𝒰.map i ≫ f) g (𝟙 (𝒰.obj i)) s.snd f ⋯ ⋯) ≫ (gluing 𝒰 f g).ι i) ⋯) ≫ p2 𝒰 f g = (𝒰.pullbackCover s.fst).map b ≫ s.snd
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X Y Z : Scheme<VAR>𝒰 : X.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g<VAR>s : PullbackCone f g<VAR>b : (𝒰.pullbackCover s.fst).gluedCover.diagram.R<GOAL>(((pullbackSymmetry s.fst (𝒰.map b)).hom ≫ pullback.map (𝒰.map b) s.fst (𝒰.map b ≫ f) g (𝟙 (𝒰.obj b)) s.snd f ⋯ ⋯) ≫ (gluing 𝒰 f g).ι b) ≫ p2 𝒰 f g = (𝒰.pullbackCover s.fst).map b ≫ s.snd
<VAR>X✝ : Scheme<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>H : IsOpenImmersion f<VAR>inst✝ : IsReduced Y<VAR>U : X.Opens<GOAL>_root_.IsReduced ↑Γ(X, U)
<VAR>X✝ : Scheme<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>H : IsOpenImmersion f<VAR>inst✝ : IsReduced Y<VAR>U : X.Opens<VAR>this : U = f ⁻¹ᵁ f ''ᵁ U<GOAL>_root_.IsReduced ↑Γ(X, U)
<VAR>X✝ : Scheme<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>H : IsOpenImmersion f<VAR>inst✝ : IsReduced Y<VAR>U : X.Opens<VAR>this : U = f ⁻¹ᵁ f ''ᵁ U<GOAL>_root_.IsReduced ↑Γ(X, f ⁻¹ᵁ f ''ᵁ U)
<VAR>s : ℝ<VAR>hs : 1 < s<GOAL>∑' (n : ℕ), 1 / (↑n + 1) ^ s - 1 / (s - 1) = 1 - s * term_tsum s
<VAR>s : ℝ<VAR>hs : 1 < s<GOAL>∑' (n : ℕ), 1 / (↑n + 1) ^ s - 1 / (s - 1) = 1 - s * (1 / (s - 1) - 1 / s * ∑' (n : ℕ), 1 / (↑n + 1) ^ s)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : Monoid M<VAR>S : Set (MonoidAlgebra R M)<VAR>hS : adjoin R S = ⊤<GOAL>adjoin R (⋃ f ∈ S, ⇑(of R M) '' ↑f.support) = ⊤
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : Monoid M<VAR>S : Set (MonoidAlgebra R M)<VAR>hS : adjoin R S = ⊤<GOAL>⊤ ≤ adjoin R (⋃ f ∈ S, ⇑(of R M) '' ↑f.support)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : Monoid M<VAR>S : Set (MonoidAlgebra R M)<VAR>hS : adjoin R S = ⊤<GOAL>S ⊆ ↑(adjoin R (⋃ f ∈ S, ⇑(of R M) '' ↑f.support))
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : Monoid M<VAR>S : Set (MonoidAlgebra R M)<VAR>hS : adjoin R S = ⊤<VAR>f : MonoidAlgebra R M<VAR>hf : f ∈ S<GOAL>f ∈ ↑(adjoin R (⋃ f ∈ S, ⇑(of R M) '' ↑f.support))
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : Monoid M<VAR>S : Set (MonoidAlgebra R M)<VAR>hS : adjoin R S = ⊤<VAR>f : MonoidAlgebra R M<VAR>hf : f ∈ S<VAR>hincl : ⇑(of R M) '' ↑f.support ⊆ ⋃ g ∈ S, ⇑(of R M) '' ↑g.support<GOAL>f ∈ ↑(adjoin R (⋃ f ∈ S, ⇑(of R M) '' ↑f.support))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : LinearOrder α<VAR>inst✝³ : OrderTopology α<VAR>inst✝² : DenselyOrdered α<VAR>a b : α<VAR>s : Set α<VAR>l : Filter β<VAR>f : α → β<VAR>inst✝¹ : SeparableSpace α<VAR>inst✝ : Nontrivial α<GOAL>∃ s, s.Countable ∧ Dense s ∧ (∀ (x : α), IsBot x → x ∉ s) ∧ ∀ (x : α), IsTop x → x ∉ s
<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✝ : Set α<VAR>S T : Set (Set α)<VAR>h_gen : m0 = generateFrom S<VAR>hc : T.Countable<VAR>h_inter : IsPiSystem S<VAR>hU : ⋃₀ T = univ<VAR>htop : ∀ t ∈ T, μ t ≠ ⊤<VAR>ST_eq : ∀ t ∈ T, ∀ s ∈ S, μ (s ∩ t) = ν (s ∩ t)<VAR>T_eq : ∀ t ∈ T, μ t = ν t<VAR>t : Set α<VAR>ht : t ∈ T<VAR>u : Set α<VAR>hu : MeasurableSet u<GOAL>(μ.restrict t) u = (ν.restrict t) u
<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✝ : Set α<VAR>S T : Set (Set α)<VAR>h_gen : m0 = generateFrom S<VAR>hc : T.Countable<VAR>h_inter : IsPiSystem S<VAR>hU : ⋃₀ T = univ<VAR>htop : ∀ t ∈ T, μ t ≠ ⊤<VAR>ST_eq : ∀ t ∈ T, ∀ s ∈ S, μ (s ∩ t) = ν (s ∩ t)<VAR>T_eq : ∀ t ∈ T, μ t = ν t<VAR>t : Set α<VAR>ht : t ∈ T<VAR>u : Set α<VAR>hu : MeasurableSet u<GOAL>μ (u ∩ t) = ν (u ∩ t)
<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✝ : Set α<VAR>S T : Set (Set α)<VAR>h_gen : m0 = generateFrom S<VAR>hc : T.Countable<VAR>h_inter : IsPiSystem S<VAR>hU : ⋃₀ T = univ<VAR>htop : ∀ t ∈ T, μ t ≠ ⊤<VAR>ST_eq : ∀ t ∈ T, ∀ s ∈ S, μ (s ∩ t) = ν (s ∩ t)<VAR>T_eq : ∀ t ∈ T, μ t = ν t<VAR>t : Set α<VAR>ht : t ∈ T<VAR>u : Set α<VAR>hu : MeasurableSet u<GOAL>μ (∅ ∩ t) = ν (∅ ∩ t)
<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✝ : Set α<VAR>S T : Set (Set α)<VAR>h_gen : m0 = generateFrom S<VAR>hc : T.Countable<VAR>h_inter : IsPiSystem S<VAR>hU : ⋃₀ T = univ<VAR>htop : ∀ t ∈ T, μ t ≠ ⊤<VAR>ST_eq : ∀ t ∈ T, ∀ s ∈ S, μ (s ∩ t) = ν (s ∩ t)<VAR>T_eq : ∀ t ∈ T, μ t = ν t<VAR>t : Set α<VAR>ht : t ∈ T<VAR>u : Set α<VAR>hu : MeasurableSet u<GOAL>∀ (t_1 : Set α), MeasurableSet t_1 → μ (t_1 ∩ t) = ν (t_1 ∩ t) → μ (t_1ᶜ ∩ t) = ν (t_1ᶜ ∩ t)
<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✝ : Set α<VAR>S T : Set (Set α)<VAR>h_gen : m0 = generateFrom S<VAR>hc : T.Countable<VAR>h_inter : IsPiSystem S<VAR>hU : ⋃₀ T = univ<VAR>htop : ∀ t ∈ T, μ t ≠ ⊤<VAR>ST_eq : ∀ t ∈ T, ∀ s ∈ S, μ (s ∩ t) = ν (s ∩ t)<VAR>T_eq : ∀ t ∈ T, μ t = ν t<VAR>t : Set α<VAR>ht : t ∈ T<VAR>u : Set α<VAR>hu : MeasurableSet u<GOAL>∀ (f : ℕ → Set α), Pairwise (Disjoint on f) → (∀ (i : ℕ), MeasurableSet (f i)) → (∀ (i : ℕ), μ (f i ∩ t) = ν (f i ∩ t)) → μ ((⋃ i, f i) ∩ t) = ν ((⋃ i, f i) ∩ t)
<VAR>R : Type u<VAR>ι : Type u_1<VAR>inst✝ : CommSemiring R<VAR>I J✝ K L : Ideal R<VAR>J : ι → Ideal R<VAR>s : Finset ι<VAR>hf : ∀ j ∈ s, IsCoprime I (J j)<GOAL>IsCoprime I (⨅ j ∈ s, J j)
<VAR>f g : CircleDeg1Lift<VAR>n : ℕ<GOAL>↑n * ⌊f 0⌋ ≤ ⌊(⇑f)^[n] 0⌋
<VAR>f g : CircleDeg1Lift<VAR>n : ℕ<GOAL>0 + ↑n * ↑⌊f 0⌋ ≤ (⇑f)^[n] 0
<VAR>f g : CircleDeg1Lift<VAR>n : ℕ<GOAL>0 + ↑⌊f 0⌋ ≤ f 0
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁴ : Ring K<VAR>inst✝³ : StrongRankCondition K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : Module.Free K V<VAR>c : Cardinal.{v}<GOAL>c ≤ Module.rank K V ↔ ∃ s, #↑s = c ∧ LinearIndependent (ι := { x // x ∈ s }) K Subtype.val
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁴ : Ring K<VAR>inst✝³ : StrongRankCondition K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : Module.Free K V<VAR>c : Cardinal.{v}<VAR>this : Nontrivial K<GOAL>c ≤ Module.rank K V ↔ ∃ s, #↑s = c ∧ LinearIndependent (ι := { x // x ∈ s }) K Subtype.val
<VAR>θ : Angle<GOAL>(2 • θ).sign = θ.sign ↔ θ = ↑π ∨ |θ.toReal| < π / 2
<VAR>S : Type u_1<VAR>inst✝ : Semiring S<VAR>a b : ℕ<GOAL>↑(a.ascFactorial b) = Polynomial.eval (↑a) (ascPochhammer S b)
<VAR>C : Type u<VAR>A : Type u_1<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : AddCommMonoid A<VAR>inst✝ : HasShift C A<VAR>i j k : A<VAR>h : i + j = k<GOAL>j + i = k
<VAR>C : Type u<VAR>A : Type u_1<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : AddCommMonoid A<VAR>inst✝ : HasShift C A<VAR>i j : A<GOAL>shiftFunctorComm C i j = (shiftFunctorAdd' C i j (i + j) ⋯).symm ≪≫ shiftFunctorAdd' C j i (i + j) ⋯
<VAR>C : Type u<VAR>A : Type u_1<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : AddCommMonoid A<VAR>inst✝ : HasShift C A<VAR>i j : A<GOAL>shiftFunctorComm C i j = (shiftFunctorAdd C i j).symm ≪≫ shiftFunctorAdd' C j i (i + j) ⋯
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>k : Type u_2<VAR>inst✝ : Field k<VAR>φ : K →+* ℂ<VAR>x✝ : K<GOAL>(place (conjugate φ)) x✝ = (place φ) x✝
<VAR>α : Type u<VAR>β : Type v<VAR>φ : Ultrafilter α<VAR>inst✝ : LinearOrder β<VAR>x y : β<GOAL>↑(max x y) = max ↑x ↑y
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X Y Z : Scheme<VAR>𝒰 : X.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g<VAR>i j : 𝒰.J<GOAL>t 𝒰 f g i j ≫ pullback.snd (pullback.fst (𝒰.map j ≫ f) g ≫ 𝒰.map j) (𝒰.map i) = pullback.fst (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map j) ≫ pullback.fst (𝒰.map i ≫ f) g
<VAR>α✝ : Type u<VAR>β✝ : Type v<VAR>γ : Type w<VAR>inst✝⁴ : UniformSpace α✝<VAR>inst✝³ : UniformSpace β✝<VAR>inst✝² : UniformSpace γ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : UniformSpace α<VAR>inst✝ : UniformSpace β<VAR>f : α ≃ β<VAR>h₁ : UniformContinuous ⇑f<VAR>h₂ : UniformContinuous ⇑f.symm<GOAL>comap (Prod.map ⇑f ⇑f) (𝓤 β) ≤ 𝓤 α
<VAR>R : Type u<VAR>S : Type v<VAR>a✝ b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ p q : R[X]<VAR>ι : Type u_1<VAR>a : R<GOAL>(C a + p).natDegree = p.natDegree
<VAR>α : Type u_1<VAR>inst✝⁵ : Mul α<VAR>inst✝⁴ : PartialOrder α<VAR>inst✝³ : DecidableEq α<VAR>inst✝² : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>inst✝¹ : CovariantClass α α (Function.swap HMul.hMul) LT.lt<VAR>inst✝ : LocallyFiniteOrderBot α<VAR>a b : α<GOAL>↑(Iio a * Iic b) ⊆ ↑(Iio (a * b))
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>h : NullMeasurableSet s μ<GOAL>toMeasurable μ s =ᶠ[ae μ] s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>h : NullMeasurableSet s μ<GOAL>?hc.choose =ᶠ[ae μ] s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>h : NullMeasurableSet s μ<GOAL>∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s
<VAR>G : Type u_1<VAR>M : Type u_2<VAR>inst✝ : Monoid M<VAR>a✝ b c : M<VAR>m✝ n✝ : ℕ<VAR>a : M<VAR>m n : ℕ<GOAL>a ^ (m * n) = (a ^ n) ^ m
<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>f : R⟦X⟧<VAR>n : ℕ<GOAL>trunc (n - 1) ((d⁄dX R) f) = Polynomial.derivative (trunc n f)