ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>x : S ⊗[R] S<VAR>hx : x ∈ ideal R S<VAR>this : x ∈ Submodule.span S (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)<GOAL>∀ (a : S) (x : S ⊗[R] S), (∃ (hx : x ∈ ideal R S), (ideal R S).toCotangent ⟨x, hx⟩ ∈ Submodule.span S (Set.range ⇑(D R S))) → ∃ (hx : a • x ∈ ideal R S), (ideal R S).toCotangent ⟨a • x, hx⟩ ∈ Submodule.span S (Set.range ⇑(D R S))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>e : α ≃o β<VAR>a b : β<GOAL>⇑e ⁻¹' Ico a b = Ico (e.symm a) (e.symm b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>s✝ t s : Set α<VAR>h : (⇑ofDual ⁻¹' s).OrdConnected<GOAL>s.OrdConnected
<VAR>R✝ : Type u<VAR>inst✝¹¹ : CommRing R✝<VAR>W✝ : Affine R✝<VAR>R : Type r<VAR>inst✝¹⁰ : CommRing R<VAR>W : Affine R<VAR>S : Type s<VAR>inst✝⁹ : CommRing S<VAR>inst✝⁸ : Algebra R S<VAR>A : Type u<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : Algebra S A<VAR>inst✝⁴ : IsScalarTower R S A<VAR>B : Type v<VAR>inst✝³ : CommRing B<VAR>inst✝² : Algebra R B<VAR>inst✝¹ : Algebra S B<VAR>inst✝ : IsScalarTower R S B<VAR>f : A →ₐ[S] B<VAR>x₁ x₂ y₁ L : A<GOAL>(baseChange W B).toAffine.negAddY (f x₁) (f x₂) (f y₁) (f L) = f ((baseChange W A).toAffine.negAddY x₁ x₂ y₁ L)
<VAR>R✝ : Type u<VAR>inst✝¹¹ : CommRing R✝<VAR>W✝ : Affine R✝<VAR>R : Type r<VAR>inst✝¹⁰ : CommRing R<VAR>W : Affine R<VAR>S : Type s<VAR>inst✝⁹ : CommRing S<VAR>inst✝⁸ : Algebra R S<VAR>A : Type u<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : Algebra S A<VAR>inst✝⁴ : IsScalarTower R S A<VAR>B : Type v<VAR>inst✝³ : CommRing B<VAR>inst✝² : Algebra R B<VAR>inst✝¹ : Algebra S B<VAR>inst✝ : IsScalarTower R S B<VAR>f : A →ₐ[S] B<VAR>x₁ x₂ y₁ L : A<GOAL>(baseChange W B).toAffine.negAddY (f x₁) (f x₂) (f y₁) (f L) = (baseChange W B).toAffine.negAddY (f.toRingHom x₁) (f.toRingHom x₂) (f.toRingHom y₁) (f.toRingHom L)
<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>t : R<VAR>n : ℕ<GOAL>(X - C t) ^ n ∣ p ↔ X ^ n ∣ p.comp (X + C t)
<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>t : R<VAR>n : ℕ<GOAL>X ^ n = (algEquivAevalXAddC t) ((X - C t) ^ n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>op : β → β → β<VAR>hc : Std.Commutative op<VAR>ha : Std.Associative op<VAR>f : α → β<VAR>b : β<VAR>s : Finset α<VAR>a : α<VAR>g : α → β<VAR>H : ∀ x ∈ s, f x = g x<GOAL>fold op b f s = fold op b g s
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x<VAR>hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x<VAR>hg' : ∀ x ∈ Ioo a b, g' x ≠ 0<VAR>hfa : Tendsto f (𝓝[>] a) (𝓝 0)<VAR>hga : Tendsto g (𝓝[>] a) (𝓝 0)<VAR>hdiv : Tendsto (fun x => f' x / 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>hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x<VAR>hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x<VAR>hg' : ∀ x ∈ Ioo a b, g' x ≠ 0<VAR>hfa : Tendsto f (𝓝[>] a) (𝓝 0)<VAR>hga : Tendsto g (𝓝[>] a) (𝓝 0)<VAR>hdiv : Tendsto (fun x => f' x / g' x) (𝓝[>] a) l<VAR>sub : ∀ x ∈ Ioo a b, Ioo a x ⊆ Ioo a b<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>hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x<VAR>hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x<VAR>hg' : ∀ x ∈ Ioo a b, g' x ≠ 0<VAR>hfa : Tendsto f (𝓝[>] a) (𝓝 0)<VAR>hga : Tendsto g (𝓝[>] a) (𝓝 0)<VAR>hdiv : Tendsto (fun x => f' x / g' x) (𝓝[>] a) l<VAR>sub : ∀ x ∈ Ioo a b, Ioo a x ⊆ Ioo a b<VAR>hg : ∀ x ∈ Ioo a b, g x ≠ 0<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>hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x<VAR>hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x<VAR>hg' : ∀ x ∈ Ioo a b, g' x ≠ 0<VAR>hfa : Tendsto f (𝓝[>] a) (𝓝 0)<VAR>hga : Tendsto g (𝓝[>] a) (𝓝 0)<VAR>hdiv : Tendsto (fun x => f' x / g' x) (𝓝[>] a) l<VAR>sub : ∀ x ∈ Ioo a b, Ioo a x ⊆ Ioo a b<VAR>hg : ∀ x ∈ Ioo a b, g x ≠ 0<VAR>this : ∀ x ∈ Ioo a b, ∃ c ∈ Ioo a x, f x * g' c = g x * f' c<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>hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x<VAR>hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x<VAR>hg' : ∀ x ∈ Ioo a b, g' x ≠ 0<VAR>hfa : Tendsto f (𝓝[>] a) (𝓝 0)<VAR>hga : Tendsto g (𝓝[>] a) (𝓝 0)<VAR>hdiv : Tendsto (fun x => f' x / g' x) (𝓝[>] a) l<VAR>sub : ∀ x ∈ Ioo a b, Ioo a x ⊆ Ioo a b<VAR>hg : ∀ x ∈ Ioo a b, g x ≠ 0<VAR>c : ℝ → ℝ<VAR>hc : ∀ x ∈ Ioo a b, c x ∈ Ioo a x ∧ f x * g' (c x) = g x * f' (c 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>hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x<VAR>hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x<VAR>hg' : ∀ x ∈ Ioo a b, g' x ≠ 0<VAR>hfa : Tendsto f (𝓝[>] a) (𝓝 0)<VAR>hga : Tendsto g (𝓝[>] a) (𝓝 0)<VAR>hdiv : Tendsto (fun x => f' x / g' x) (𝓝[>] a) l<VAR>sub : ∀ x ∈ Ioo a b, Ioo a x ⊆ Ioo a b<VAR>hg : ∀ x ∈ Ioo a b, g x ≠ 0<VAR>c : ℝ → ℝ<VAR>hc : ∀ x ∈ Ioo a b, c x ∈ Ioo a x ∧ f x * g' (c x) = g x * f' (c x)<VAR>this : ∀ x ∈ Ioo a b, ((fun x' => f' x' / g' x') ∘ c) x = f x / 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>hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x<VAR>hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x<VAR>hg' : ∀ x ∈ Ioo a b, g' x ≠ 0<VAR>hfa : Tendsto f (𝓝[>] a) (𝓝 0)<VAR>hga : Tendsto g (𝓝[>] a) (𝓝 0)<VAR>hdiv : Tendsto (fun x => f' x / g' x) (𝓝[>] a) l<VAR>sub : ∀ x ∈ Ioo a b, Ioo a x ⊆ Ioo a b<VAR>hg : ∀ x ∈ Ioo a b, g x ≠ 0<VAR>c : ℝ → ℝ<VAR>hc : ∀ x ∈ Ioo a b, c x ∈ Ioo a x ∧ f x * g' (c x) = g x * f' (c x)<VAR>this : ∀ x ∈ Ioo a b, ((fun x' => f' x' / g' x') ∘ c) x = f x / g x<VAR>cmp : ∀ x ∈ Ioo a b, a < c x ∧ c 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>hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x<VAR>hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x<VAR>hg' : ∀ x ∈ Ioo a b, g' x ≠ 0<VAR>hfa : Tendsto f (𝓝[>] a) (𝓝 0)<VAR>hga : Tendsto g (𝓝[>] a) (𝓝 0)<VAR>hdiv : Tendsto (fun x => f' x / g' x) (𝓝[>] a) l<VAR>sub : ∀ x ∈ Ioo a b, Ioo a x ⊆ Ioo a b<VAR>hg : ∀ x ∈ Ioo a b, g x ≠ 0<VAR>c : ℝ → ℝ<VAR>hc : ∀ x ∈ Ioo a b, c x ∈ Ioo a x ∧ f x * g' (c x) = g x * f' (c x)<VAR>this : ∀ x ∈ Ioo a b, ((fun x' => f' x' / g' x') ∘ c) x = f x / g x<VAR>cmp : ∀ x ∈ Ioo a b, a < c x ∧ c x < x<GOAL>Tendsto (fun x => f x / g x) (𝓝[Ioo a b] a) l
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x<VAR>hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x<VAR>hg' : ∀ x ∈ Ioo a b, g' x ≠ 0<VAR>hfa : Tendsto f (𝓝[>] a) (𝓝 0)<VAR>hga : Tendsto g (𝓝[>] a) (𝓝 0)<VAR>hdiv : Tendsto (fun x => f' x / g' x) (𝓝[>] a) l<VAR>sub : ∀ x ∈ Ioo a b, Ioo a x ⊆ Ioo a b<VAR>hg : ∀ x ∈ Ioo a b, g x ≠ 0<VAR>c : ℝ → ℝ<VAR>hc : ∀ x ∈ Ioo a b, c x ∈ Ioo a x ∧ f x * g' (c x) = g x * f' (c x)<VAR>this : ∀ x ∈ Ioo a b, ((fun x' => f' x' / g' x') ∘ c) x = f x / g x<VAR>cmp : ∀ x ∈ Ioo a b, a < c x ∧ c x < x<GOAL>Tendsto ((fun x' => f' x' / g' x') ∘ c) (𝓝[Ioo a b] a) l
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x<VAR>hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x<VAR>hg' : ∀ x ∈ Ioo a b, g' x ≠ 0<VAR>hfa : Tendsto f (𝓝[>] a) (𝓝 0)<VAR>hga : Tendsto g (𝓝[>] a) (𝓝 0)<VAR>hdiv : Tendsto (fun x => f' x / g' x) (𝓝[>] a) l<VAR>sub : ∀ x ∈ Ioo a b, Ioo a x ⊆ Ioo a b<VAR>hg : ∀ x ∈ Ioo a b, g x ≠ 0<VAR>c : ℝ → ℝ<VAR>hc : ∀ x ∈ Ioo a b, c x ∈ Ioo a x ∧ f x * g' (c x) = g x * f' (c x)<VAR>this : ∀ x ∈ Ioo a b, ((fun x' => f' x' / g' x') ∘ c) x = f x / g x<VAR>cmp : ∀ x ∈ Ioo a b, a < c x ∧ c x < x<GOAL>Tendsto c (𝓝[Ioo a b] a) (𝓝[>] a)
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x<VAR>hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x<VAR>hg' : ∀ x ∈ Ioo a b, g' x ≠ 0<VAR>hfa : Tendsto f (𝓝[>] a) (𝓝 0)<VAR>hga : Tendsto g (𝓝[>] a) (𝓝 0)<VAR>hdiv : Tendsto (fun x => f' x / g' x) (𝓝[>] a) l<VAR>sub : ∀ x ∈ Ioo a b, Ioo a x ⊆ Ioo a b<VAR>hg : ∀ x ∈ Ioo a b, g x ≠ 0<VAR>c : ℝ → ℝ<VAR>hc : ∀ x ∈ Ioo a b, c x ∈ Ioo a x ∧ f x * g' (c x) = g x * f' (c x)<VAR>this : ∀ x ∈ Ioo a b, ((fun x' => f' x' / g' x') ∘ c) x = f x / g x<VAR>cmp : ∀ x ∈ Ioo a b, a < c x ∧ c x < x<GOAL>∀ᶠ (b : ℝ) in 𝓝[Ioo a b] a, a ≤ c b
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x<VAR>hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x<VAR>hg' : ∀ x ∈ Ioo a b, g' x ≠ 0<VAR>hfa : Tendsto f (𝓝[>] a) (𝓝 0)<VAR>hga : Tendsto g (𝓝[>] a) (𝓝 0)<VAR>hdiv : Tendsto (fun x => f' x / g' x) (𝓝[>] a) l<VAR>sub : ∀ x ∈ Ioo a b, Ioo a x ⊆ Ioo a b<VAR>hg : ∀ x ∈ Ioo a b, g x ≠ 0<VAR>c : ℝ → ℝ<VAR>hc : ∀ x ∈ Ioo a b, c x ∈ Ioo a x ∧ f x * g' (c x) = g x * f' (c x)<VAR>this : ∀ x ∈ Ioo a b, ((fun x' => f' x' / g' x') ∘ c) x = f x / g x<VAR>cmp : ∀ x ∈ Ioo a b, a < c x ∧ c x < x<GOAL>∀ᶠ (b : ℝ) in 𝓝[Ioo a b] a, c b ≤ id b
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x<VAR>hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x<VAR>hg' : ∀ x ∈ Ioo a b, g' x ≠ 0<VAR>hfa : Tendsto f (𝓝[>] a) (𝓝 0)<VAR>hga : Tendsto g (𝓝[>] a) (𝓝 0)<VAR>hdiv : Tendsto (fun x => f' x / g' x) (𝓝[>] a) l<VAR>sub : ∀ x ∈ Ioo a b, Ioo a x ⊆ Ioo a b<VAR>hg : ∀ x ∈ Ioo a b, g x ≠ 0<VAR>c : ℝ → ℝ<VAR>hc : ∀ x ∈ Ioo a b, c x ∈ Ioo a x ∧ f x * g' (c x) = g x * f' (c x)<VAR>this : ∀ x ∈ Ioo a b, ((fun x' => f' x' / g' x') ∘ c) x = f x / g x<VAR>cmp : ∀ x ∈ Ioo a b, a < c x ∧ c x < x<GOAL>∀ᶠ (x : ℝ) in 𝓝[Ioo a b] a, c x ∈ Ioi a
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n k : ℕ<VAR>x✝ : Nat.Prime k<VAR>kx : k ∣ xn a1 n<VAR>ky : k ∣ yn a1 n<GOAL>k ∣ 1
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n k : ℕ<VAR>x✝ : Nat.Prime k<VAR>kx : k ∣ xn a1 n<VAR>ky : k ∣ yn a1 n<VAR>p : xn a1 n * xn a1 n - Pell.d a1 * yn a1 n * yn a1 n = 1 := pell_eq a1 n<GOAL>k ∣ 1
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n k : ℕ<VAR>x✝ : Nat.Prime k<VAR>kx : k ∣ xn a1 n<VAR>ky : k ∣ yn a1 n<VAR>p : xn a1 n * xn a1 n - Pell.d a1 * yn a1 n * yn a1 n = 1 := pell_eq a1 n<GOAL>k ∣ xn a1 n * xn a1 n - Pell.d a1 * yn a1 n * yn a1 n
<VAR>a b c d b' : List Γ'<GOAL>update (elim a b c d) rev b' = elim a b' c d
<VAR>a b c d b' : List Γ'<VAR>x : K'<GOAL>update (elim a b c d) rev b' x = elim a b' c d x
<VAR>α β : Type u<VAR>β' : Type v<GOAL>#(α ↪ β') = 0 ↔ lift.{u, v} #β' < lift.{v, u} #α
<VAR>C₁ : Type u₁<VAR>C₂ : Type u₂<VAR>D₁ : Type u₃<VAR>D₂ : Type u₄<VAR>inst✝⁶ : Category.{v₁, u₁} C₁<VAR>inst✝⁵ : Category.{v₂, u₂} C₂<VAR>inst✝⁴ : Category.{v₃, u₃} D₁<VAR>inst✝³ : Category.{v₄, u₄} D₂<VAR>L₁ : C₁ ⥤ D₁<VAR>W₁ : MorphismProperty C₁<VAR>L₂ : C₂ ⥤ D₂<VAR>W₂ : MorphismProperty C₂<VAR>E : Type u₅<VAR>inst✝² : Category.{v₅, u₅} E<VAR>F : C₁ × C₂ ⥤ E<VAR>hF : (W₁.prod W₂).IsInvertedBy F<VAR>inst✝¹ : W₁.ContainsIdentities<VAR>inst✝ : W₂.ContainsIdentities<GOAL>W₁.Q.prod W₂.Q ⋙ prodLift F hF = F
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>f : Filter X<VAR>s t s₁ s₂ t₁ t₂ : Set X<VAR>x : X<VAR>h : IsClosed t<GOAL>𝓝ˢ s = 𝓝ˢ (s ∩ t ∪ s ∩ tᶜ)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>f : Filter X<VAR>s t s₁ s₂ t₁ t₂ : Set X<VAR>x : X<VAR>h : IsClosed t<GOAL>𝓝ˢ (s ∩ t ∪ s ∩ tᶜ) = 𝓝ˢ (s ∩ t) ⊔ 𝓝ˢ (s ∩ tᶜ)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>f : Filter X<VAR>s t s₁ s₂ t₁ t₂ : Set X<VAR>x : X<VAR>h : IsClosed t<GOAL>𝓝ˢ (s ∩ t) ⊔ 𝓝ˢ tᶜ = 𝓝ˢ (s ∩ t) ⊔ 𝓟 tᶜ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>a✝ b✝ : α<VAR>inst✝ : LT α<VAR>a : WithBot α<VAR>b : α<GOAL>a < ↑b ↔ ∃ p, ↑b = ↑p ∧ a < ↑p
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>P X✝ Y Z : C<VAR>fst : P ⟶ X✝<VAR>snd : P ⟶ Y<VAR>f : X✝ ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝¹ : HasZeroObject C<VAR>inst✝ : HasZeroMorphisms C<VAR>X : C<GOAL>((zeroProdIso X).symm ≪≫ (pullbackZeroZeroIso 0 X).symm).hom ≫ pullback.fst 0 0 = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ✝ : Kernel α β<VAR>inst✝ : Countable ι<VAR>κ η : ι → Kernel α β<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>((Kernel.sum fun n => κ n + η n) a) s = ((Kernel.sum κ + Kernel.sum η) a) s
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>A B C : Set α<VAR>D E : Set ↑A<VAR>S : Set (Set α)<VAR>T : Set (Set ↑A)<VAR>s : ι → Set α<VAR>t : ι → Set ↑A<VAR>h : A ⊆ B<GOAL>A ↓∩ B = univ
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>A B C : Set α<VAR>D E : Set ↑A<VAR>S : Set (Set α)<VAR>T : Set (Set ↑A)<VAR>s : ι → Set α<VAR>t : ι → Set ↑A<VAR>h : A ⊆ B<GOAL>∀ (a : α) (b : a ∈ A), ⟨a, b⟩ ∈ A ↓∩ B
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>g : ι → α<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : UniformSpace γ<VAR>f : γ → β<VAR>hf : UniformContinuous f<GOAL>UniformContinuous (⇑ofFun ∘ (fun x => f ∘ x) ∘ ⇑toFun)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>g : ι → α<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : UniformSpace γ<VAR>f : γ → β<VAR>hf : UniformContinuous f<GOAL>uniformSpace α γ ≤ UniformSpace.comap (⇑ofFun ∘ (fun x => f ∘ x) ∘ ⇑toFun) (uniformSpace α β)
<VAR>R : Type u_1<VAR>inst✝¹⁶ : CommSemiring R<VAR>R' : Type u_2<VAR>inst✝¹⁵ : Monoid R'<VAR>R'' : Type u_3<VAR>inst✝¹⁴ : Semiring R''<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>S : Type u_8<VAR>T : Type u_9<VAR>inst✝¹³ : AddCommMonoid M<VAR>inst✝¹² : AddCommMonoid N<VAR>inst✝¹¹ : AddCommMonoid P<VAR>inst✝¹⁰ : AddCommMonoid Q<VAR>inst✝⁹ : AddCommMonoid S<VAR>inst✝⁸ : AddCommMonoid T<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R N<VAR>inst✝⁵ : Module R P<VAR>inst✝⁴ : Module R Q<VAR>inst✝³ : Module R S<VAR>inst✝² : Module R T<VAR>inst✝¹ : DistribMulAction R' M<VAR>inst✝ : Module R'' M<VAR>g : P →ₗ[R] Q<VAR>f : N →ₗ[R] P<VAR>x : M ⊗[R] N<GOAL>(lTensor M id) x = 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>m : M<GOAL>(ι R) m ∈ ⋀[R]^1 M
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : EDist α<VAR>x y : α<VAR>s✝ t : Set α<VAR>d : ℝ≥0∞<VAR>f : β → α<VAR>s : Set β<GOAL>d ≤ (f '' s).einfsep ↔ ∀ x ∈ s, ∀ y ∈ s, f x ≠ f y → d ≤ edist (f x) (f y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>f : ι → Set α<GOAL>⋃ i, f i = univ ↔ ∀ (x : α), ∃ i, x ∈ f i
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>f : α → ι<VAR>inst✝³ : Fintype α<VAR>inst✝² : Fintype ι<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq ι<GOAL>Fintype.card { g // f ∘ ⇑g = f } = ∏ i : ι, (Fintype.card { a // f a = i })!
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>f : α → ι<VAR>inst✝³ : Fintype α<VAR>inst✝² : Fintype ι<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq ι<GOAL>∏ a : ι, Nat.card (Perm { a_1 // f a_1 = a }) = ∏ i : ι, (Fintype.card { a // f a = i })!
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>f : α → ι<VAR>inst✝³ : Fintype α<VAR>inst✝² : Fintype ι<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq ι<VAR>x✝ : Perm α<GOAL>f ∘ ⇑x✝ = f ↔ mk x✝ ∈ stabilizer (Perm α)ᵈᵐᵃ f
<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>r : R<GOAL>Associates.mk (Ideal.span {r}) ≠ 0 ↔ r ≠ 0
<VAR>R : Type u_1<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : TopologicalSpace R<VAR>inst✝² : TopologicalSemiring R<VAR>A : Type u_2<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>s : Set R<VAR>φ ψ : C(↑s, R) →ₐ[R] A<VAR>h : φ ((toContinuousMapOnAlgHom s) X) = ψ ((toContinuousMapOnAlgHom s) X)<GOAL>polynomialFunctions s ≤ AlgHom.equalizer φ ψ
<VAR>R : Type u_1<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : TopologicalSpace R<VAR>inst✝² : TopologicalSemiring R<VAR>A : Type u_2<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>s : Set R<VAR>φ ψ : C(↑s, R) →ₐ[R] A<VAR>h : φ ((toContinuousMapOnAlgHom s) X) = ψ ((toContinuousMapOnAlgHom s) X)<GOAL>Algebra.adjoin R {(toContinuousMapOnAlgHom s) X} ≤ AlgHom.equalizer φ ψ
<VAR>R : Type u<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDedekindDomain R<VAR>K : Type v<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>v : HeightOneSpectrum R<VAR>x : Kˣ<GOAL>↑(v.valuationOfNeZeroToFun x) = ↑v.intValuation.toMonoidWithZeroHom ((IsLocalization.toLocalizationMap R⁰ K).sec ↑x).1 * ↑((IsUnit.liftRight ((↑v.intValuation.toMonoidWithZeroHom).restrict R⁰) ⋯) ((IsLocalization.toLocalizationMap R⁰ K).sec ↑x).2)⁻¹
<VAR>R : Type u<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDedekindDomain R<VAR>K : Type v<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>v : HeightOneSpectrum R<VAR>x : Kˣ<GOAL>↑(v.valuationOfNeZeroToFun x) = ↑v.intValuation.toMonoidWithZeroHom ((IsLocalization.toLocalizationMap R⁰ K).sec ↑x).1 * (↑((IsUnit.liftRight ((↑v.intValuation.toMonoidWithZeroHom).restrict R⁰) ⋯) ((IsLocalization.toLocalizationMap R⁰ K).sec ↑x).2))⁻¹
<VAR>R : Type u<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDedekindDomain R<VAR>K : Type v<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>v : HeightOneSpectrum R<VAR>x : Kˣ<GOAL>↑(v.valuationOfNeZeroToFun x) = (if ((IsLocalization.toLocalizationMap R⁰ K).sec ↑x).1 = 0 then 0 else ↑(Multiplicative.ofAdd (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {((IsLocalization.toLocalizationMap R⁰ K).sec ↑x).1})).factors)))) * (if (SubmonoidClass.subtype R⁰) ((IsLocalization.toLocalizationMap R⁰ K).sec ↑x).2 = 0 then 0 else ↑(Multiplicative.ofAdd (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {(SubmonoidClass.subtype R⁰) ((IsLocalization.toLocalizationMap R⁰ K).sec ↑x).2})).factors))))⁻¹
<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>f : α × β → ℝ≥0∞<VAR>hf : AEMeasurable f (μ.prod ν)<GOAL>∫⁻ (z : α × β), f z ∂μ.prod ν = ∫⁻ (y : β), ∫⁻ (x : α), f (x, y) ∂μ ∂ν
<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>f : α × β → ℝ≥0∞<VAR>hf : AEMeasurable f (μ.prod ν)<GOAL>∫⁻ (z : β × α), f z.swap ∂ν.prod μ = ∫⁻ (y : β), ∫⁻ (x : α), f (x, y) ∂μ ∂ν
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module ℝ E<VAR>s t : Set E<VAR>x : E<VAR>a : ℝ<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : TopologicalAddGroup E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>hc : Convex ℝ s<VAR>hs₀ : s ∈ 𝓝 0<GOAL>{x | gauge s x < 1} = interior s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module ℝ E<VAR>s t : Set E<VAR>x✝ : E<VAR>a : ℝ<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : TopologicalAddGroup E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>hc : Convex ℝ s<VAR>hs₀ : s ∈ 𝓝 0<VAR>x : E<VAR>hx : x ∈ {x | gauge s x < 1}<GOAL>x ∈ interior s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module ℝ E<VAR>s t : Set E<VAR>x✝ : E<VAR>a : ℝ<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : TopologicalAddGroup E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>hc : Convex ℝ s<VAR>hs₀ : s ∈ 𝓝 0<VAR>x : E<VAR>hx : x ∈ {x | gauge s x < 1}<VAR>y : E<VAR>hys : y ∈ s<VAR>hxy : x ∈ openSegment ℝ 0 y<GOAL>x ∈ interior s
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : MonoidalCategory C<VAR>X : Center C<GOAL>(λ_ X).inv.f = (λ_ X.fst).inv
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : MonoidalCategory C<VAR>X : Center C<GOAL>(λ_ X.fst).hom ≫ (λ_ X).inv.f = 𝟙 (𝟙_ (Center C) ⊗ X).fst
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : MonoidalCategory C<VAR>X : Center C<GOAL>(𝟙 (𝟙_ (Center C) ⊗ X)).f = 𝟙 (𝟙_ (Center C) ⊗ X).fst
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>inst✝² : AddCommGroup M<VAR>R : Type u_3<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Module R M<VAR>I : Ideal R<VAR>v : ι → M<VAR>hv : Submodule.span R (Set.range v) = ⊤<VAR>f : ι →₀ ↥I<GOAL>(Finsupp.total ι M R v) (Finsupp.mapRange Subtype.val ⋯ f) = f.sum fun i x => ↑x • v i
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>inst✝² : AddCommGroup M<VAR>R : Type u_3<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Module R M<VAR>I : Ideal R<VAR>v : ι → M<VAR>hv : Submodule.span R (Set.range v) = ⊤<VAR>f : ι →₀ ↥I<GOAL>∀ (a : ι), 0 • v a = 0
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>F : Type u_1<VAR>inst✝⁴ : Ring R<VAR>inst✝³ : Ring S<VAR>inst✝² : IsDomain S<VAR>inst✝¹ : FunLike F R S<VAR>inst✝ : RingHomClass F R S<VAR>f : F<GOAL>ker f ≠ ⊤
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>F : Type u_1<VAR>inst✝⁴ : Ring R<VAR>inst✝³ : Ring S<VAR>inst✝² : IsDomain S<VAR>inst✝¹ : FunLike F R S<VAR>inst✝ : RingHomClass F R S<VAR>f : F<GOAL>1 ∉ ker f
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>F : Type u_1<VAR>inst✝⁴ : Ring R<VAR>inst✝³ : Ring S<VAR>inst✝² : IsDomain S<VAR>inst✝¹ : FunLike F R S<VAR>inst✝ : RingHomClass F R S<VAR>f : F<VAR>x y : R<GOAL>x * y ∈ ker f → x ∈ ker f ∨ y ∈ ker f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>f : X → Y<VAR>inst✝ : SeqCompactSpace X<VAR>f_cont : SeqContinuous f<GOAL>IsSeqCompact (Set.range f)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>inst✝⁸ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>inst✝⁵ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : FirstCountableTopology X<VAR>ν : Measure α<VAR>inst✝ : MeasurableSingletonClass α<VAR>s : Finset α<VAR>f : α → E<VAR>hf : Integrable f (μ.restrict ↑s)<GOAL>∫ (x : α) in ↑s, f x ∂μ = ∑ x ∈ s, (μ {x}).toReal • f x
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μ : Measure α<VAR>inst✝¹ : LinearOrder ι<VAR>inst✝ : IsMarkovKernel κ<VAR>s : ι → Set Ω<VAR>hsm : ∀ (n : ι), MeasurableSet (s n)<VAR>hs : iIndepSet s κ μ<VAR>i k : ι<VAR>hk : i < k<GOAL>Indep (generateFrom {s k}) (generateFrom {t | ∃ j ≤ i, s j = t}) κ μ
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μ : Measure α<VAR>inst✝¹ : LinearOrder ι<VAR>inst✝ : IsMarkovKernel κ<VAR>s : ι → Set Ω<VAR>hsm : ∀ (n : ι), MeasurableSet (s n)<VAR>hs : iIndepSet s κ μ<VAR>i k : ι<VAR>hk : i < k<GOAL>{s k} = {t | ∃ n ∈ {k}, s n = t}
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝³ : DecidableEq ι<VAR>δ : Type u_1<VAR>inst✝² : (i : ι) → AddZeroClass (β i)<VAR>inst✝¹ : AddCommMonoid γ<VAR>inst✝ : AddCommMonoid δ<VAR>g : γ →+ δ<VAR>f : (i : ι) → β i →+ γ<VAR>a : ι<GOAL>liftAddHom.symm (g.comp (liftAddHom f)) a = g.comp (f a)
<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>fi : Filter ι<VAR>f : ι → ℝ≥0<VAR>x : ℝ≥0<GOAL>Tendsto (fun n => ((fun i => ↑(f i)) n).toReal) fi (𝓝 (↑x).toReal) ↔ Tendsto (fun i => ↑(f i)) fi (𝓝 ↑x)