ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>inst✝² : Semiring R<VAR>f✝ : R[X]<VAR>S : Type u_2<VAR>inst✝¹ : CommSemiring S<VAR>i : R →+* S<VAR>x : S<VAR>inst✝ : Invertible x<VAR>N : ℕ<VAR>f : R[X]<VAR>hf : f.natDegree ≤ N<GOAL>∀ (n : ℕ) (r : R), r ≠ 0 → n ≤ N → (fun f => eval₂ i (⅟x) (reflect N f) * x ^ N = eval₂ i x f) (C r * X ^ n)
<VAR>R : Type u_1<VAR>inst✝² : Semiring R<VAR>f✝ : R[X]<VAR>S : Type u_2<VAR>inst✝¹ : CommSemiring S<VAR>i : R →+* S<VAR>x : S<VAR>inst✝ : Invertible x<VAR>N : ℕ<VAR>f : R[X]<VAR>hf : f.natDegree ≤ N<GOAL>∀ (f g : R[X]), f.natDegree < g.natDegree → g.natDegree ≤ N → (fun f => eval₂ i (⅟x) (reflect N f) * x ^ N = eval₂ i x f) f → (fun f => eval₂ i (⅟x) (reflect N f) * x ^ N = eval₂ i x f) g → (fun f => eval₂ i (⅟x) (reflect N f) * x ^ N = eval₂ i x f) (f + g)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>M : Type u_1<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<VAR>D : Derivation R S M<VAR>x y : S ⊗[R] S<GOAL>D.tensorProductTo (x * y) = (TensorProduct.lmul' R) x • D.tensorProductTo y + (TensorProduct.lmul' R) y • D.tensorProductTo x
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>M : Type u_1<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<VAR>D : Derivation R S M<VAR>x y : S ⊗[R] S<GOAL>D.tensorProductTo (0 * y) = (TensorProduct.lmul' R) 0 • D.tensorProductTo y + (TensorProduct.lmul' R) y • D.tensorProductTo 0
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>M : Type u_1<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<VAR>D : Derivation R S M<VAR>x y : S ⊗[R] S<GOAL>∀ (x y_1 : S), D.tensorProductTo (x ⊗ₜ[R] y_1 * y) = (TensorProduct.lmul' R) (x ⊗ₜ[R] y_1) • D.tensorProductTo y + (TensorProduct.lmul' R) y • D.tensorProductTo (x ⊗ₜ[R] y_1)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>M : Type u_1<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<VAR>D : Derivation R S M<VAR>x y : S ⊗[R] S<GOAL>∀ (x y_1 : S ⊗[R] S), D.tensorProductTo (x * y) = (TensorProduct.lmul' R) x • D.tensorProductTo y + (TensorProduct.lmul' R) y • D.tensorProductTo x → D.tensorProductTo (y_1 * y) = (TensorProduct.lmul' R) y_1 • D.tensorProductTo y + (TensorProduct.lmul' R) y • D.tensorProductTo y_1 → D.tensorProductTo ((x + y_1) * y) = (TensorProduct.lmul' R) (x + y_1) • D.tensorProductTo y + (TensorProduct.lmul' R) y • D.tensorProductTo (x + y_1)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>M : Type u_1<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<VAR>D : Derivation R S M<VAR>x y : S ⊗[R] S<VAR>x₁ x₂ : S<GOAL>D.tensorProductTo (x₁ ⊗ₜ[R] x₂ * y) = (TensorProduct.lmul' R) (x₁ ⊗ₜ[R] x₂) • D.tensorProductTo y + (TensorProduct.lmul' R) y • D.tensorProductTo (x₁ ⊗ₜ[R] x₂)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>M : Type u_1<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<VAR>D : Derivation R S M<VAR>x y : S ⊗[R] S<VAR>x₁ x₂ : S<GOAL>D.tensorProductTo (x₁ ⊗ₜ[R] x₂ * 0) = (TensorProduct.lmul' R) (x₁ ⊗ₜ[R] x₂) • D.tensorProductTo 0 + (TensorProduct.lmul' R) 0 • D.tensorProductTo (x₁ ⊗ₜ[R] x₂)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>M : Type u_1<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<VAR>D : Derivation R S M<VAR>x y : S ⊗[R] S<VAR>x₁ x₂ : S<GOAL>∀ (x y : S), D.tensorProductTo (x₁ ⊗ₜ[R] x₂ * x ⊗ₜ[R] y) = (TensorProduct.lmul' R) (x₁ ⊗ₜ[R] x₂) • D.tensorProductTo (x ⊗ₜ[R] y) + (TensorProduct.lmul' R) (x ⊗ₜ[R] y) • D.tensorProductTo (x₁ ⊗ₜ[R] x₂)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>M : Type u_1<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<VAR>D : Derivation R S M<VAR>x y : S ⊗[R] S<VAR>x₁ x₂ : S<GOAL>∀ (x y : S ⊗[R] S), D.tensorProductTo (x₁ ⊗ₜ[R] x₂ * x) = (TensorProduct.lmul' R) (x₁ ⊗ₜ[R] x₂) • D.tensorProductTo x + (TensorProduct.lmul' R) x • D.tensorProductTo (x₁ ⊗ₜ[R] x₂) → D.tensorProductTo (x₁ ⊗ₜ[R] x₂ * y) = (TensorProduct.lmul' R) (x₁ ⊗ₜ[R] x₂) • D.tensorProductTo y + (TensorProduct.lmul' R) y • D.tensorProductTo (x₁ ⊗ₜ[R] x₂) → D.tensorProductTo (x₁ ⊗ₜ[R] x₂ * (x + y)) = (TensorProduct.lmul' R) (x₁ ⊗ₜ[R] x₂) • D.tensorProductTo (x + y) + (TensorProduct.lmul' R) (x + y) • D.tensorProductTo (x₁ ⊗ₜ[R] x₂)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>M : Type u_1<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<VAR>D : Derivation R S M<VAR>x✝ y✝ : S ⊗[R] S<VAR>x₁ x₂ x y : S<GOAL>D.tensorProductTo (x₁ ⊗ₜ[R] x₂ * x ⊗ₜ[R] y) = (TensorProduct.lmul' R) (x₁ ⊗ₜ[R] x₂) • D.tensorProductTo (x ⊗ₜ[R] y) + (TensorProduct.lmul' R) (x ⊗ₜ[R] y) • D.tensorProductTo (x₁ ⊗ₜ[R] x₂)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>M : Type u_1<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<VAR>D : Derivation R S M<VAR>x✝ y✝ : S ⊗[R] S<VAR>x₁ x₂ x y : S<GOAL>(TensorProduct.lift (↑R ((LinearMap.lsmul S (S →ₗ[R] M)).flip ↑D))) ((x₁ * x) ⊗ₜ[R] (x₂ * y)) = (x₁ * x₂) • (TensorProduct.lift (↑R ((LinearMap.lsmul S (S →ₗ[R] M)).flip ↑D))) (x ⊗ₜ[R] y) + (x * y) • (TensorProduct.lift (↑R ((LinearMap.lsmul S (S →ₗ[R] M)).flip ↑D))) (x₁ ⊗ₜ[R] x₂)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>M : Type u_1<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<VAR>D : Derivation R S M<VAR>x✝ y✝ : S ⊗[R] S<VAR>x₁ x₂ x y : S<GOAL>(x₁ * x) • D (x₂ * y) = (x₁ * x₂) • x • D y + (x * y) • x₁ • D x₂
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>M : Type u_1<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<VAR>D : Derivation R S M<VAR>x✝ y✝ : S ⊗[R] S<VAR>x₁ x₂ x y : S<GOAL>(x₁ * x) • (x₂ • D y + y • D x₂) = (x₁ * x₂) • x • D y + (x * y) • x₁ • D x₂
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddMonoid M<VAR>inst✝ : Nontrivial R<VAR>m : M<VAR>S : Set M<VAR>h : of' R M m ∈ span R ↑(Submonoid.closure (of' R M '' S))<GOAL>m ∈ closure S
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddMonoid M<VAR>inst✝ : Nontrivial R<VAR>m : M<VAR>S : Set M<VAR>h : of' R M m ∈ span R ↑(Submonoid.closure (of' R M '' S))<GOAL>Multiplicative.ofAdd m ∈ Submonoid.closure (⇑Multiplicative.toAdd ⁻¹' S)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddMonoid M<VAR>inst✝ : Nontrivial R<VAR>m : M<VAR>S : Set M<VAR>h : of' R M m ∈ span R ↑(Submonoid.closure (of' R M '' S))<VAR>S' : Submonoid (Multiplicative M) := Submonoid.closure S<GOAL>Multiplicative.ofAdd m ∈ Submonoid.closure (⇑Multiplicative.toAdd ⁻¹' S)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddMonoid M<VAR>inst✝ : Nontrivial R<VAR>m : M<VAR>S : Set M<VAR>h : of' R M m ∈ span R ↑(Submonoid.closure (of' R M '' S))<VAR>S' : Submonoid (Multiplicative M) := Submonoid.closure S<VAR>h' : Submonoid.map (of R M) S' = Submonoid.closure ((fun x => (of R M) x) '' S)<GOAL>Multiplicative.ofAdd m ∈ Submonoid.closure (⇑Multiplicative.toAdd ⁻¹' S)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddMonoid M<VAR>inst✝ : Nontrivial R<VAR>m : M<VAR>S : Set M<VAR>S' : Submonoid (Multiplicative M) := Submonoid.closure S<VAR>h : of' R M m ∈ span R ↑(Submonoid.map (of R M) S')<VAR>h' : Submonoid.map (of R M) S' = Submonoid.closure ((fun x => (of R M) x) '' S)<GOAL>Multiplicative.ofAdd m ∈ Submonoid.closure (⇑Multiplicative.toAdd ⁻¹' S)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<GOAL>(Iio s).card = 2 ^ s.card - 1
<VAR>n : ℕ<VAR>h : n ≠ 0<GOAL>cons n n.properDivisors ⋯ = n.divisors
<VAR>R : Type u<VAR>inst✝ : EuclideanDomain R<VAR>a b c : R<VAR>ha : a ≠ 0<VAR>hcb : c ∣ b<VAR>hc : ¬c = 0<GOAL>a * b / (a * c) = b / c
<VAR>R : Type u<VAR>inst✝ : EuclideanDomain R<VAR>a b c : R<VAR>ha : a ≠ 0<VAR>hcb : c ∣ b<VAR>hc : ¬c = 0<GOAL>a * (c * (a * b / (a * c))) = a * b
<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>a₁ : α<VAR>b₁ b₂ : β a₁<VAR>x✝ : a₁ = a₁ ∧ HEq b₁ b₂<VAR>h₂ : HEq b₁ b₂<GOAL>⟨a₁, b₁⟩ = ⟨a₁, b₂⟩
<VAR>x y : ℝ<GOAL>cos |x| = cos x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>x : M<VAR>f : Dual R M<VAR>y✝ : M<VAR>h : f x = 2<VAR>y : M<GOAL>(preReflection x f) ((preReflection x f) y) = y
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝⁵ : NontriviallyNormedField 𝕜<VAR>inst✝⁴ : SeminormedRing 𝕝<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Module 𝕝 E<VAR>inst✝ : TopologicalSpace E<VAR>p : Seminorm 𝕝 E<VAR>hp : ∀ r > 0, p.closedBall 0 r ∈ 𝓝 0<GOAL>ContinuousAt (⇑p) 0
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝⁵ : NontriviallyNormedField 𝕜<VAR>inst✝⁴ : SeminormedRing 𝕝<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Module 𝕝 E<VAR>inst✝ : TopologicalSpace E<VAR>p : Seminorm 𝕝 E<VAR>hp : ∀ r > 0, ⇑p ⁻¹' Metric.closedBall 0 r ∈ 𝓝 0<GOAL>ContinuousAt (⇑p) 0
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι✝ : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m : MeasurableSpace α✝<VAR>μ✝ μ₁ μ₂ : Measure α✝<VAR>s s₁ s₂ t : Set α✝<VAR>α : Type u_8<VAR>ι : Type u_9<VAR>inst✝³ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝² : Countable ι<VAR>inst✝¹ : Preorder ι<VAR>inst✝ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>f : ι → Set α<VAR>hm : ∀ (i : ι), MeasurableSet (f i)<VAR>hf : ∃ i, μ (f i) ≠ ⊤<GOAL>Tendsto (fun i => μ (⋂ j ∈ {j | j ≤ i}, f j)) atTop (𝓝 (μ (⋂ i, f i)))
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι✝ : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m : MeasurableSpace α✝<VAR>μ✝ μ₁ μ₂ : Measure α✝<VAR>s s₁ s₂ t : Set α✝<VAR>α : Type u_8<VAR>ι : Type u_9<VAR>inst✝³ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝² : Countable ι<VAR>inst✝¹ : Preorder ι<VAR>inst✝ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>f : ι → Set α<VAR>hm : ∀ (i : ι), MeasurableSet (f i)<VAR>hf : ∃ i, μ (f i) ≠ ⊤<GOAL>Tendsto (fun i => μ (⋂ j ∈ {j | j ≤ i}, f j)) atTop (𝓝 (⨅ i, μ (⋂ j, ⋂ (_ : j ≤ i), f j)))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m : MeasurableSpace α<VAR>μ μ₁ μ₂ : Measure α<VAR>s✝ s₁ s₂ t : Set α<VAR>inst✝² : Countable ι<VAR>inst✝¹ : Preorder ι<VAR>inst✝ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>s : ι → Set α<VAR>hs : ∀ (n : ι), MeasurableSet (s n)<VAR>hm : Antitone s<VAR>hf : ∃ i, μ (s i) ≠ ⊤<GOAL>Tendsto (⇑μ ∘ s) atTop (𝓝 (μ (⋂ n, s n)))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m : MeasurableSpace α<VAR>μ μ₁ μ₂ : Measure α<VAR>s✝ s₁ s₂ t : Set α<VAR>inst✝² : Countable ι<VAR>inst✝¹ : Preorder ι<VAR>inst✝ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>s : ι → Set α<VAR>hs : ∀ (n : ι), MeasurableSet (s n)<VAR>hm : Antitone s<VAR>hf : ∃ i, μ (s i) ≠ ⊤<GOAL>Tendsto (⇑μ ∘ s) atTop (𝓝 (⨅ i, μ (s i)))
<VAR>C : Type u<VAR>inst✝⁸ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w₁<VAR>inst✝⁷ : Category.{max v u, w₁} D<VAR>E : Type w₂<VAR>inst✝⁶ : Category.{max v u, w₂} E<VAR>F : D ⥤ E<VAR>inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D<VAR>inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E<VAR>inst✝³ : (X : C) → (W : J.Cover X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (W.index P).multicospan F<VAR>P : Cᵒᵖ ⥤ D<VAR>inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E<VAR>inst✝ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ F<VAR>X : Cᵒᵖ<VAR>W : (J.Cover (unop X))ᵒᵖ<GOAL>F.map (colimit.ι (J.diagram P (unop X)) W) ≫ (NatIso.ofComponents (fun X => (isColimitOfPreserves F (colimit.isColimit (J.diagram P (unop X)))).coconePointUniqueUpToIso (colimit.isColimit (J.diagram P (unop X) ⋙ F)) ≪≫ HasColimit.isoOfNatIso (NatIso.ofComponents (fun W => (isLimitOfPreserves F (limit.isLimit ((unop W).index P).multicospan)).conePointUniqueUpToIso (limit.isLimit (((unop W).index P).multicospan ⋙ F)) ≪≫ HasLimit.isoOfNatIso (Cover.multicospanComp F P (unop W)).symm) ⋯)) ⋯).hom.app X = (NatIso.ofComponents (fun W => (isLimitOfPreserves F (limit.isLimit ((unop W).index P).multicospan)).conePointUniqueUpToIso (limit.isLimit (((unop W).index P).multicospan ⋙ F)) ≪≫ HasLimit.isoOfNatIso (Cover.multicospanComp F P (unop W)).symm) ⋯).hom.app W ≫ colimit.ι (J.diagram (P ⋙ F) (unop X)) W
<VAR>C : Type u<VAR>inst✝⁸ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w₁<VAR>inst✝⁷ : Category.{max v u, w₁} D<VAR>E : Type w₂<VAR>inst✝⁶ : Category.{max v u, w₂} E<VAR>F : D ⥤ E<VAR>inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D<VAR>inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E<VAR>inst✝³ : (X : C) → (W : J.Cover X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (W.index P).multicospan F<VAR>P : Cᵒᵖ ⥤ D<VAR>inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E<VAR>inst✝ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ F<VAR>X : Cᵒᵖ<VAR>W : (J.Cover (unop X))ᵒᵖ<GOAL>(F.map (colimit.ι (J.diagram P (unop X)) W) ≫ ((isColimitOfPreserves F (colimit.isColimit (J.diagram P (unop X)))).coconePointUniqueUpToIso (colimit.isColimit (J.diagram P (unop X) ⋙ F))).hom) ≫ (HasColimit.isoOfNatIso (NatIso.ofComponents (fun W => (isLimitOfPreserves F (limit.isLimit ((unop W).index P).multicospan)).conePointUniqueUpToIso (limit.isLimit (((unop W).index P).multicospan ⋙ F)) ≪≫ HasLimit.isoOfNatIso (Cover.multicospanComp F P (unop W)).symm) ⋯)).hom = (((isLimitOfPreserves F (limit.isLimit ((unop W).index P).multicospan)).conePointUniqueUpToIso (limit.isLimit (((unop W).index P).multicospan ⋙ F))).hom ≫ (HasLimit.isoOfNatIso (Cover.multicospanComp F P (unop W)).symm).hom) ≫ colimit.ι (J.diagram (P ⋙ F) (unop X)) W
<VAR>C : Type u<VAR>inst✝⁸ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w₁<VAR>inst✝⁷ : Category.{max v u, w₁} D<VAR>E : Type w₂<VAR>inst✝⁶ : Category.{max v u, w₂} E<VAR>F : D ⥤ E<VAR>inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D<VAR>inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E<VAR>inst✝³ : (X : C) → (W : J.Cover X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (W.index P).multicospan F<VAR>P : Cᵒᵖ ⥤ D<VAR>inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E<VAR>inst✝ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ F<VAR>X : Cᵒᵖ<VAR>W : (J.Cover (unop X))ᵒᵖ<GOAL>(colimit.cocone (J.diagram P (unop X) ⋙ F)).ι.app W ≫ (HasColimit.isoOfNatIso (NatIso.ofComponents (fun W => (isLimitOfPreserves F (limit.isLimit ((unop W).index P).multicospan)).conePointUniqueUpToIso (limit.isLimit (((unop W).index P).multicospan ⋙ F)) ≪≫ HasLimit.isoOfNatIso (Cover.multicospanComp F P (unop W)).symm) ⋯)).hom = (((isLimitOfPreserves F (limit.isLimit ((unop W).index P).multicospan)).conePointUniqueUpToIso (limit.isLimit (((unop W).index P).multicospan ⋙ F))).hom ≫ (HasLimit.isoOfNatIso (Cover.multicospanComp F P (unop W)).symm).hom) ≫ colimit.ι (J.diagram (P ⋙ F) (unop X)) W
<VAR>n a b : ℕ<GOAL>Prime (a * b) ↔ Prime a ∧ b = 1 ∨ Prime b ∧ a = 1
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>f : X → Y<VAR>f_cont : SeqContinuous f<VAR>K : Set X<VAR>K_cpt : IsSeqCompact K<VAR>ys : ℕ → Y<VAR>xs : ℕ → X<VAR>xs_in_K : ∀ (n : ℕ), xs n ∈ K<VAR>fxs_eq_ys : ∀ (n : ℕ), f (xs n) = ys n<VAR>a : X<VAR>a_in_K : a ∈ K<VAR>phi : ℕ → ℕ<VAR>phi_mono : StrictMono phi<VAR>xs_phi_lim : Tendsto (xs ∘ phi) atTop (𝓝 a)<GOAL>∃ a ∈ f '' K, ∃ φ, StrictMono φ ∧ Tendsto (ys ∘ φ) atTop (𝓝 a)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>f : X → Y<VAR>f_cont : SeqContinuous f<VAR>K : Set X<VAR>K_cpt : IsSeqCompact K<VAR>ys : ℕ → Y<VAR>xs : ℕ → X<VAR>xs_in_K : ∀ (n : ℕ), xs n ∈ K<VAR>fxs_eq_ys : ∀ (n : ℕ), f (xs n) = ys n<VAR>a : X<VAR>a_in_K : a ∈ K<VAR>phi : ℕ → ℕ<VAR>phi_mono : StrictMono phi<VAR>xs_phi_lim : Tendsto (xs ∘ phi) atTop (𝓝 a)<GOAL>Tendsto (ys ∘ phi) atTop (𝓝 (f a))
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>A : Type u_7<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : AddCommGroup N<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R N<VAR>Q✝ : QuadraticMap R M N<VAR>inst✝⁵ : CommSemiring S<VAR>inst✝⁴ : Algebra S R<VAR>inst✝³ : Module S M<VAR>inst✝² : IsScalarTower S R M<VAR>inst✝¹ : Module S N<VAR>inst✝ : IsScalarTower S R N<VAR>ι : Type u_8<VAR>Q : QuadraticMap R M N<VAR>s : Finset ι<VAR>f : ι → M<GOAL>Q (∑ i ∈ s, f i) = ∑ ij ∈ s.sym2, Sym2.lift ⟨fun i j => polar (⇑Q) (f i) (f j), ⋯⟩ ij - ∑ i ∈ s, Q (f i)
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>A : Type u_1<VAR>B : Type u_2<VAR>inst✝² : Category.{u_3, u_1} A<VAR>inst✝¹ : Category.{u_4, u_2} B<VAR>F : A ⥤ B<VAR>G₁ : (Cᵒᵖ ⥤ A) ⥤ Sheaf J A<VAR>adj₁ : G₁ ⊣ sheafToPresheaf J A<VAR>G₂ : (Cᵒᵖ ⥤ B) ⥤ Sheaf J B<VAR>adj₂ : G₂ ⊣ sheafToPresheaf J B<VAR>inst✝ : J.HasSheafCompose F<VAR>P : Cᵒᵖ ⥤ A<VAR>α : G₂.obj (P ⋙ F) ⟶ (sheafCompose J F).obj (G₁.obj P)<VAR>hα : adj₂.unit.app (P ⋙ F) ≫ (sheafToPresheaf J B).map α = whiskerRight (adj₁.unit.app P) F<GOAL>α = (sheafComposeNatTrans J F adj₁ adj₂).app P
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>A : Type u_1<VAR>B : Type u_2<VAR>inst✝² : Category.{u_3, u_1} A<VAR>inst✝¹ : Category.{u_4, u_2} B<VAR>F : A ⥤ B<VAR>G₁ : (Cᵒᵖ ⥤ A) ⥤ Sheaf J A<VAR>adj₁ : G₁ ⊣ sheafToPresheaf J A<VAR>G₂ : (Cᵒᵖ ⥤ B) ⥤ Sheaf J B<VAR>adj₂ : G₂ ⊣ sheafToPresheaf J B<VAR>inst✝ : J.HasSheafCompose F<VAR>P : Cᵒᵖ ⥤ A<VAR>α : G₂.obj (P ⋙ F) ⟶ (sheafCompose J F).obj (G₁.obj P)<VAR>hα : adj₂.unit.app (P ⋙ F) ≫ (sheafToPresheaf J B).map α = whiskerRight (adj₁.unit.app P) F<GOAL>(adj₂.homEquiv (P ⋙ F) ((sheafCompose J F).obj (G₁.obj P))) α = (adj₂.homEquiv (P ⋙ F) ((sheafCompose J F).obj (G₁.obj P))) ((sheafComposeNatTrans J F adj₁ adj₂).app P)
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>A : Type u_1<VAR>B : Type u_2<VAR>inst✝² : Category.{u_3, u_1} A<VAR>inst✝¹ : Category.{u_4, u_2} B<VAR>F : A ⥤ B<VAR>G₁ : (Cᵒᵖ ⥤ A) ⥤ Sheaf J A<VAR>adj₁ : G₁ ⊣ sheafToPresheaf J A<VAR>G₂ : (Cᵒᵖ ⥤ B) ⥤ Sheaf J B<VAR>adj₂ : G₂ ⊣ sheafToPresheaf J B<VAR>inst✝ : J.HasSheafCompose F<VAR>P : Cᵒᵖ ⥤ A<VAR>α : G₂.obj (P ⋙ F) ⟶ (sheafCompose J F).obj (G₁.obj P)<VAR>hα : adj₂.unit.app (P ⋙ F) ≫ (sheafToPresheaf J B).map α = whiskerRight (adj₁.unit.app P) F<GOAL>(adj₂.homEquiv (P ⋙ F) ((sheafCompose J F).obj (G₁.obj P))) α = (adj₂.homEquiv (P ⋙ F) ((sheafCompose J F).obj (G₁.obj P))) ((adj₂.homEquiv (P ⋙ F) ((sheafCompose J F).obj (G₁.obj P))).symm (whiskerRight (adj₁.unit.app P) F))
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>A : Type u_1<VAR>B : Type u_2<VAR>inst✝² : Category.{u_3, u_1} A<VAR>inst✝¹ : Category.{u_4, u_2} B<VAR>F : A ⥤ B<VAR>G₁ : (Cᵒᵖ ⥤ A) ⥤ Sheaf J A<VAR>adj₁ : G₁ ⊣ sheafToPresheaf J A<VAR>G₂ : (Cᵒᵖ ⥤ B) ⥤ Sheaf J B<VAR>adj₂ : G₂ ⊣ sheafToPresheaf J B<VAR>inst✝ : J.HasSheafCompose F<VAR>P : Cᵒᵖ ⥤ A<VAR>α : G₂.obj (P ⋙ F) ⟶ (sheafCompose J F).obj (G₁.obj P)<VAR>hα : adj₂.unit.app (P ⋙ F) ≫ (sheafToPresheaf J B).map α = whiskerRight (adj₁.unit.app P) F<GOAL>(adj₂.homEquiv (P ⋙ F) ((sheafCompose J F).obj (G₁.obj P))) α = whiskerRight (adj₁.unit.app P) F
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>A : Type u_1<VAR>B : Type u_2<VAR>inst✝² : Category.{u_3, u_1} A<VAR>inst✝¹ : Category.{u_4, u_2} B<VAR>F : A ⥤ B<VAR>G₁ : (Cᵒᵖ ⥤ A) ⥤ Sheaf J A<VAR>adj₁ : G₁ ⊣ sheafToPresheaf J A<VAR>G₂ : (Cᵒᵖ ⥤ B) ⥤ Sheaf J B<VAR>adj₂ : G₂ ⊣ sheafToPresheaf J B<VAR>inst✝ : J.HasSheafCompose F<VAR>P : Cᵒᵖ ⥤ A<VAR>α : G₂.obj (P ⋙ F) ⟶ (sheafCompose J F).obj (G₁.obj P)<VAR>hα : adj₂.unit.app (P ⋙ F) ≫ (sheafToPresheaf J B).map α = whiskerRight (adj₁.unit.app P) F<GOAL>(adj₂.homEquiv (P ⋙ F) ((sheafCompose J F).obj (G₁.obj P))) α = adj₂.unit.app (P ⋙ F) ≫ (sheafToPresheaf J B).map α
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : CompleteSpace E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>μ ν : Measure α<VAR>s✝ t : Set α<VAR>f✝ g f : α → ℝ≥0∞<VAR>s : Set α<GOAL>⨍⁻ (x : α) in s, f x ∂μ = (∫⁻ (x : α) in s, f x ∂μ) / μ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l l₁ l₂ l₃ : List α<VAR>a b : α<VAR>m n : ℕ<GOAL>[].dropLast ++ [] = []
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : List α<VAR>s : Set α<GOAL>range (map Subtype.val) = {l | ∀ x ∈ l, x ∈ s}
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Z<VAR>X' : Type u_4<VAR>Y' : Type u_5<VAR>inst✝¹ : TopologicalSpace X'<VAR>inst✝ : TopologicalSpace Y'<VAR>h : X ≃ₜ Y<VAR>x : X<GOAL>map (⇑h) (𝓝[≠] x) = 𝓝[≠] h x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Z<VAR>X' : Type u_4<VAR>Y' : Type u_5<VAR>inst✝¹ : TopologicalSpace X'<VAR>inst✝ : TopologicalSpace Y'<VAR>h : X ≃ₜ Y<VAR>x : X<GOAL>{h x}ᶜ = ⇑h '' {x}ᶜ
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>e : ι ≃ ι'<VAR>p : ι' → P<GOAL>AffineIndependent k (p ∘ ⇑e) ↔ AffineIndependent k p
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>e : ι ≃ ι'<VAR>p : ι' → P<GOAL>AffineIndependent k (p ∘ ⇑e) → AffineIndependent k p
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>e : ι ≃ ι'<VAR>p : ι' → P<VAR>h : AffineIndependent k (p ∘ ⇑e)<VAR>this : p = p ∘ ⇑e ∘ ⇑e.symm.toEmbedding<GOAL>AffineIndependent k (p ∘ ⇑e ∘ ⇑e.symm.toEmbedding)
<GOAL>Tendsto (fun z => z * Gamma z) (𝓝[≠] 0) (𝓝 1)
<GOAL>Tendsto (fun z => z * Gamma z) (𝓝[≠] 0) (𝓝 (Gamma (0 + 1)))
<GOAL>Tendsto (fun x => Gamma (x + 1)) (𝓝 0) (𝓝 (Gamma (0 + 1)))
<VAR>m : ℕ<GOAL>0 + 1 ≠ -↑m
<VAR>m : ℕ<GOAL>¬1 = -↑m
<VAR>m : ℕ<GOAL>-↑m ≤ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n : ℕ<VAR>a a' : α<VAR>i : Fin n<VAR>v : Vector α n<GOAL>v.get i ∈ v.toList
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n : ℕ<VAR>a a' : α<VAR>i : Fin n<VAR>v : Vector α n<GOAL>v.toList.get (Fin.cast ⋯ i) ∈ v.toList