ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>r r' s : α → α → Prop<VAR>f : ι → α<GOAL>Directed r f ↔ DirectedOn r (Set.range f)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<GOAL>sublistsAux = fun a r => (Array.foldl (fun r l => (r.push l).push (a :: l)) #[] (toArray r) 0).toList
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>a : α<VAR>r : List (List α)<GOAL>sublistsAux a r = (Array.foldl (fun r l => (r.push l).push (a :: l)) #[] (toArray r) 0).toList
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>a : α<VAR>r : List (List α)<GOAL>foldl (fun r l => r ++ [l, a :: l]) [] r = (foldl (fun r l => (r.push l).push (a :: l)) #[] (toArray r).data).toList
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>a : α<VAR>r : List (List α)<VAR>this : foldl (fun r l => r ++ [l, a :: l]) #[].toList r = (foldl (fun r l => (r.push l).push (a :: l)) #[] r).toList<GOAL>foldl (fun r l => r ++ [l, a :: l]) [] r = (foldl (fun r l => (r.push l).push (a :: l)) #[] (toArray r).data).toList
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r✝ : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>ι : Type u<VAR>r r' : ι → ι → Prop<VAR>inst✝¹ : IsWellOrder ι r<VAR>inst✝ : IsWellOrder ι r'<VAR>f : ι → Ordinal.{max u v}<GOAL>(type r).bsup (bfamilyOfFamily' r f) = (type r').bsup (bfamilyOfFamily' r' f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : PseudoEMetricSpace α<VAR>a b : ℝ<VAR>h : a ≤ b<GOAL>Metric.diam (Ioc a b) = b - a
<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>op' : γ → γ → γ<VAR>inst✝¹ : Std.Commutative op'<VAR>inst✝ : Std.Associative op'<VAR>m : β → γ<VAR>hm : ∀ (x y : β), m (op x y) = op' (m x) (m y)<GOAL>fold op' (m b) (fun x => m (f x)) s = m (fold op b f s)
<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>op' : γ → γ → γ<VAR>inst✝¹ : Std.Commutative op'<VAR>inst✝ : Std.Associative op'<VAR>m : β → γ<VAR>hm : ∀ (x y : β), m (op x y) = op' (m x) (m y)<GOAL>Multiset.fold op' (m b) (Multiset.map (fun x => m (f x)) s.val) = Multiset.fold op' (m b) (Multiset.map (m ∘ f) s.val)
<VAR>α : Type u_1<VAR>inst✝ : AddMonoidWithOne α<VAR>n : Num<GOAL>↑n.succ' = ↑n + 1
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>S : Type v<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>t : Set R<VAR>ht : Ideal.span t = ⊤<VAR>H : ∀ (g : ↑t), (ker (Localization.awayMap f ↑g)).FG<GOAL>(ker f).FG
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>S : Type v<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>t : Set R<VAR>ht : Ideal.span t = ⊤<VAR>H : ∀ (g : ↑t), (ker (Localization.awayMap f ↑g)).FG<GOAL>∀ (g : ↑t), (Ideal.map (algebraMap R (Localization.Away ↑g)) (ker f)).FG
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>S : Type v<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>t : Set R<VAR>ht : Ideal.span t = ⊤<VAR>H : ∀ (g : ↑t), (ker (Localization.awayMap f ↑g)).FG<VAR>g : ↑t<GOAL>(Ideal.map (algebraMap R (Localization.Away ↑g)) (ker f)).FG
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>S : Type v<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>t : Set R<VAR>ht : Ideal.span t = ⊤<VAR>H : ∀ (g : ↑t), (ker (Localization.awayMap f ↑g)).FG<VAR>g : ↑t<GOAL>(ker (IsLocalization.map (Localization.Away (f ↑g)) f ⋯)).FG
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>inst✝⁸ : CommRing R<VAR>Ms : ι → Type u_3<VAR>inst✝⁷ : (i : ι) → AddCommGroup (Ms i)<VAR>inst✝⁶ : (i : ι) → Module R (Ms i)<VAR>N : Type u_4<VAR>inst✝⁵ : AddCommGroup N<VAR>inst✝⁴ : Module R N<VAR>Ns : ι → Type u_5<VAR>inst✝³ : (i : ι) → AddCommGroup (Ns i)<VAR>inst✝² : (i : ι) → Module R (Ns i)<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>p : (i : ι) → Submodule R (Ms i)<VAR>q : Submodule R N<VAR>f : (i : ι) → Ms i →ₗ[R] N<VAR>hf : ∀ (i : ι), p i ≤ comap (f i) q<VAR>i : ι<VAR>x : Ms i ⧸ p i<GOAL>(piQuotientLift p q f hf) (Pi.single i x) = ((p i).mapQ q (f i) ⋯) x
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>inst✝⁸ : CommRing R<VAR>Ms : ι → Type u_3<VAR>inst✝⁷ : (i : ι) → AddCommGroup (Ms i)<VAR>inst✝⁶ : (i : ι) → Module R (Ms i)<VAR>N : Type u_4<VAR>inst✝⁵ : AddCommGroup N<VAR>inst✝⁴ : Module R N<VAR>Ns : ι → Type u_5<VAR>inst✝³ : (i : ι) → AddCommGroup (Ns i)<VAR>inst✝² : (i : ι) → Module R (Ns i)<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>p : (i : ι) → Submodule R (Ms i)<VAR>q : Submodule R N<VAR>f : (i : ι) → Ms i →ₗ[R] N<VAR>hf : ∀ (i : ι), p i ≤ comap (f i) q<VAR>i : ι<VAR>x : Ms i ⧸ p i<GOAL>∑ x_1 : ι, ((p x_1).mapQ q (f x_1) ⋯) (Pi.single i x x_1) = ((p i).mapQ q (f i) ⋯) x
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>inst✝⁸ : CommRing R<VAR>Ms : ι → Type u_3<VAR>inst✝⁷ : (i : ι) → AddCommGroup (Ms i)<VAR>inst✝⁶ : (i : ι) → Module R (Ms i)<VAR>N : Type u_4<VAR>inst✝⁵ : AddCommGroup N<VAR>inst✝⁴ : Module R N<VAR>Ns : ι → Type u_5<VAR>inst✝³ : (i : ι) → AddCommGroup (Ns i)<VAR>inst✝² : (i : ι) → Module R (Ns i)<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>p : (i : ι) → Submodule R (Ms i)<VAR>q : Submodule R N<VAR>f : (i : ι) → Ms i →ₗ[R] N<VAR>hf : ∀ (i : ι), p i ≤ comap (f i) q<VAR>i : ι<VAR>x : Ms i ⧸ p i<GOAL>((p i).mapQ q (f i) ⋯) (Pi.single i x i) = ((p i).mapQ q (f i) ⋯) x
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>inst✝⁸ : CommRing R<VAR>Ms : ι → Type u_3<VAR>inst✝⁷ : (i : ι) → AddCommGroup (Ms i)<VAR>inst✝⁶ : (i : ι) → Module R (Ms i)<VAR>N : Type u_4<VAR>inst✝⁵ : AddCommGroup N<VAR>inst✝⁴ : Module R N<VAR>Ns : ι → Type u_5<VAR>inst✝³ : (i : ι) → AddCommGroup (Ns i)<VAR>inst✝² : (i : ι) → Module R (Ns i)<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>p : (i : ι) → Submodule R (Ms i)<VAR>q : Submodule R N<VAR>f : (i : ι) → Ms i →ₗ[R] N<VAR>hf : ∀ (i : ι), p i ≤ comap (f i) q<VAR>i : ι<VAR>x : Ms i ⧸ p i<GOAL>∀ b ∈ Finset.univ, b ≠ i → ((p b).mapQ q (f b) ⋯) (Pi.single i x b) = 0
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>inst✝⁸ : CommRing R<VAR>Ms : ι → Type u_3<VAR>inst✝⁷ : (i : ι) → AddCommGroup (Ms i)<VAR>inst✝⁶ : (i : ι) → Module R (Ms i)<VAR>N : Type u_4<VAR>inst✝⁵ : AddCommGroup N<VAR>inst✝⁴ : Module R N<VAR>Ns : ι → Type u_5<VAR>inst✝³ : (i : ι) → AddCommGroup (Ns i)<VAR>inst✝² : (i : ι) → Module R (Ns i)<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>p : (i : ι) → Submodule R (Ms i)<VAR>q : Submodule R N<VAR>f : (i : ι) → Ms i →ₗ[R] N<VAR>hf : ∀ (i : ι), p i ≤ comap (f i) q<VAR>i : ι<VAR>x : Ms i ⧸ p i<GOAL>i ∉ Finset.univ → ((p i).mapQ q (f i) ⋯) (Pi.single i x i) = 0
<VAR>x y : ℝ<GOAL>√x ≤ 0 ↔ √x = 0
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝⁴ : Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>f✝ g : ι → Ω → E<VAR>ℱ : Filtration ι m0<VAR>𝒢 : Filtration ℕ m0<VAR>inst✝ : IsFiniteMeasure μ<VAR>f : ℕ → Ω → ℝ<VAR>hadp : Adapted 𝒢 f<VAR>hint : ∀ (i : ℕ), Integrable (f i) μ<VAR>hf : ∀ (i : ℕ), 0 ≤ᶠ[ae μ] μ[f i - f (i + 1)|↑𝒢 i]<GOAL>Supermartingale f 𝒢 μ
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝⁴ : Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>f✝ g : ι → Ω → E<VAR>ℱ : Filtration ι m0<VAR>𝒢 : Filtration ℕ m0<VAR>inst✝ : IsFiniteMeasure μ<VAR>f : ℕ → Ω → ℝ<VAR>hadp : Adapted 𝒢 f<VAR>hint : ∀ (i : ℕ), Integrable (f i) μ<VAR>hf : ∀ (i : ℕ), 0 ≤ᶠ[ae μ] μ[f i - f (i + 1)|↑𝒢 i]<GOAL>Supermartingale (- -f) 𝒢 μ
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝⁴ : Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>f✝ g : ι → Ω → E<VAR>ℱ : Filtration ι m0<VAR>𝒢 : Filtration ℕ m0<VAR>inst✝ : IsFiniteMeasure μ<VAR>f : ℕ → Ω → ℝ<VAR>hadp : Adapted 𝒢 f<VAR>hint : ∀ (i : ℕ), Integrable (f i) μ<VAR>hf : ∀ (i : ℕ), 0 ≤ᶠ[ae μ] μ[f i - f (i + 1)|↑𝒢 i]<GOAL>∀ (i : ℕ), 0 ≤ᶠ[ae μ] μ[(-f) (i + 1) - (-f) i|↑𝒢 i]
<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>R : Type u_7<VAR>R₂ : Type u_8<VAR>M : Type u_9<VAR>M₂ : Type u_10<VAR>inst✝⁹ : Semiring R<VAR>inst✝⁸ : Semiring R₂<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : AddCommMonoid M₂<VAR>inst✝⁴ : Module R₂ M₂<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : TopologicalSpace M₂<VAR>σ : R →+* R₂<VAR>σ' : R₂ →+* R<VAR>inst✝¹ : RingHomInvPair σ σ'<VAR>inst✝ : RingHomInvPair σ' σ<VAR>f : ι → M<VAR>e : M ≃SL[σ] M₂<VAR>x : M<GOAL>HasSum (fun b => e (f b)) (e x) ↔ HasSum f x
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : Preadditive C<VAR>P Q R : C<VAR>f f' : P ⟶ Q<VAR>g g' : Q ⟶ R<VAR>inst✝ : IsIso g<GOAL>f ≫ g = 0 ↔ f = 0
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>inst✝ : DecidableEq α<VAR>k : ℕ<VAR>𝒜 : Finset (Finset α)<VAR>s✝ : Finset α<VAR>m n : ℕ<VAR>h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜<VAR>s : Finset α<VAR>h₁ : s ∈ ∂ (falling n 𝒜)<VAR>h₂ : s ∈ 𝒜 # m<GOAL>False
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>inst✝ : DecidableEq α<VAR>k : ℕ<VAR>𝒜 : Finset (Finset α)<VAR>s✝ : Finset α<VAR>m n : ℕ<VAR>h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜<VAR>s : Finset α<VAR>h₂ : s ∈ 𝒜 # m<VAR>h₁ : ∃ s_1, ((∃ t ∈ 𝒜, s_1 ⊆ t) ∧ s_1.card = n) ∧ ∃ a ∈ s_1, s_1.erase a = s<GOAL>False
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>inst✝ : DecidableEq α<VAR>k : ℕ<VAR>𝒜 : Finset (Finset α)<VAR>s✝ : Finset α<VAR>m n : ℕ<VAR>h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜<VAR>s : Finset α<VAR>right✝ : s.card = n<VAR>t : Finset α<VAR>ht : t ∈ 𝒜<VAR>hst : s ⊆ t<VAR>a : α<VAR>ha : a ∈ s<VAR>h₂ : s.erase a ∈ 𝒜 # m<GOAL>False
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>inst✝ : DecidableEq α<VAR>k : ℕ<VAR>𝒜 : Finset (Finset α)<VAR>s✝ : Finset α<VAR>m n : ℕ<VAR>h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜<VAR>s : Finset α<VAR>right✝ : s.card = n<VAR>t : Finset α<VAR>ht : t ∈ 𝒜<VAR>hst : s ⊆ t<VAR>a : α<VAR>ha : a ∈ s<VAR>h₂ : s.erase a ∈ 𝒜 # m<GOAL>s.erase a ≠ t
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>inst✝ : DecidableEq α<VAR>k : ℕ<VAR>𝒜 : Finset (Finset α)<VAR>s✝ : Finset α<VAR>m n : ℕ<VAR>h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜<VAR>s : Finset α<VAR>right✝ : s.card = n<VAR>a : α<VAR>ha : a ∈ s<VAR>h₂ : s.erase a ∈ 𝒜 # m<VAR>ht : s.erase a ∈ 𝒜<VAR>hst : s ⊆ s.erase a<GOAL>False
<VAR>α : Type u<VAR>β : Type v<VAR>p : α → Bool<VAR>xs : List α<VAR>i : ℕ<VAR>h : i < xs.length<VAR>h2 : ∀ (j : ℕ) (hji : j ≤ i), ¬p (xs.get ⟨j, ⋯⟩) = true<GOAL>i < findIdx p xs
<VAR>α : Type u<VAR>β : Type v<VAR>p : α → Bool<VAR>xs : List α<VAR>i : ℕ<VAR>h : i < xs.length<VAR>h2 : ∀ (j : ℕ) (hji : j ≤ i), ¬p (xs.get ⟨j, ⋯⟩) = true<VAR>f : findIdx p xs ≤ i<GOAL>False
<VAR>C : Type u₁<VAR>inst✝³ : Category.{u₂, u₁} C<VAR>inst✝² : PreGaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝¹ : FiberFunctor F<VAR>A X : C<VAR>inst✝ : IsConnected A<GOAL>Nat.card (A ⟶ X) ≤ Nat.card ↑(F.obj X)
<VAR>C : Type u₁<VAR>inst✝³ : Category.{u₂, u₁} C<VAR>inst✝² : PreGaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝¹ : FiberFunctor F<VAR>A X : C<VAR>inst✝ : IsConnected A<GOAL>Function.Injective ?f
<VAR>C : Type u₁<VAR>inst✝³ : Category.{u₂, u₁} C<VAR>inst✝² : PreGaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝¹ : FiberFunctor F<VAR>A X : C<VAR>inst✝ : IsConnected A<GOAL>(A ⟶ X) → ↑(F.obj X)
<VAR>R : Type u_1<VAR>G : Type u_2<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Group G<VAR>inst✝² : MulAction G R<VAR>inst✝¹ : SMulCommClass G R R<VAR>inst✝ : IsScalarTower G R R<VAR>x : G<VAR>y z : R<VAR>x✝ : IsCoprime (x • y) z<VAR>a b : R<VAR>h : a * x • y + b * z = 1<GOAL>x • a * y + b * z = 1
<VAR>R : Type u_1<VAR>G : Type u_2<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Group G<VAR>inst✝² : MulAction G R<VAR>inst✝¹ : SMulCommClass G R R<VAR>inst✝ : IsScalarTower G R R<VAR>x : G<VAR>y z : R<VAR>x✝ : IsCoprime y z<VAR>a b : R<VAR>h : a * y + b * z = 1<GOAL>x⁻¹ • a * x • y + b * z = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k N : ℕ<VAR>x✝ : Fin n → ℕ<VAR>x : ℝ<VAR>hx : 50 / 19 ≤ x<GOAL>↑⌈x⌉₊ < 1.38 * x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k N : ℕ<VAR>x✝ : Fin n → ℕ<VAR>x : ℝ<VAR>hx : 50 / 19 ≤ x<GOAL>x + 1 ≤ 1.38 * x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k N : ℕ<VAR>x✝ : Fin n → ℕ<VAR>x : ℝ<VAR>hx : 50 / 19 ≤ x<GOAL>1 ≤ (1.38 - 1) * x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k N : ℕ<VAR>x✝ : Fin n → ℕ<VAR>x : ℝ<VAR>hx : 50 / 19 ≤ x<VAR>this : 1.38 = 69 / 50<GOAL>1 ≤ (1.38 - 1) * x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k N : ℕ<VAR>x✝ : Fin n → ℕ<VAR>x : ℝ<VAR>hx : 50 / 19 ≤ x<VAR>this : 1.38 = 69 / 50<GOAL>0 < 50 / 19
<VAR>𝕜 : Type u<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f✝ f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>f : 𝕜 → F<VAR>x₀ : 𝕜<VAR>C : ℝ≥0<VAR>hlip : LipschitzWith C f<GOAL>‖deriv f x₀‖ ≤ ↑C
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>I✝ J✝ : Ideal R<VAR>f : R →+* S<VAR>hf : Function.Surjective ⇑f<VAR>I J : Ideal S<VAR>h : J ∈ I.minimalPrimes<GOAL>comap f J ∈ (comap f I).minimalPrimes
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>I✝ J✝ : Ideal R<VAR>f : R →+* S<VAR>hf : Function.Surjective ⇑f<VAR>I J : Ideal S<VAR>h : J ∈ I.minimalPrimes<VAR>this : J.IsPrime<GOAL>comap f J ∈ (comap f I).minimalPrimes
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>I✝ J✝ : Ideal R<VAR>f : R →+* S<VAR>hf : Function.Surjective ⇑f<VAR>I J : Ideal S<VAR>h : J ∈ I.minimalPrimes<VAR>this : J.IsPrime<GOAL>∀ ⦃b : Ideal R⦄, b ∈ {p | p.IsPrime ∧ comap f I ≤ p} → (fun x x_1 => x ≤ x_1) b (comap f J) → (fun x x_1 => x ≤ x_1) (comap f J) b
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>I✝ J✝ : Ideal R<VAR>f : R →+* S<VAR>hf : Function.Surjective ⇑f<VAR>I J : Ideal S<VAR>h : J ∈ I.minimalPrimes<VAR>this : J.IsPrime<VAR>K : Ideal R<VAR>hK : K.IsPrime<VAR>e₁ : comap f I ≤ K<VAR>e₂ : K ≤ comap f J<GOAL>comap f J ≤ K
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>I✝ J✝ : Ideal R<VAR>f : R →+* S<VAR>hf : Function.Surjective ⇑f<VAR>I J : Ideal S<VAR>h : J ∈ I.minimalPrimes<VAR>this✝ : J.IsPrime<VAR>K : Ideal R<VAR>hK : K.IsPrime<VAR>e₁ : comap f I ≤ K<VAR>e₂ : K ≤ comap f J<VAR>this : RingHom.ker f ≤ K<GOAL>comap f J ≤ K
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>I✝ J✝ : Ideal R<VAR>f : R →+* S<VAR>hf : Function.Surjective ⇑f<VAR>I J : Ideal S<VAR>h : J ∈ I.minimalPrimes<VAR>this✝ : J.IsPrime<VAR>K : Ideal R<VAR>hK : K.IsPrime<VAR>e₁ : comap f I ≤ K<VAR>e₂ : K ≤ comap f J<VAR>this : RingHom.ker f ≤ K<GOAL>comap f J ≤ comap f (map f K)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>I✝ J✝ : Ideal R<VAR>f : R →+* S<VAR>hf : Function.Surjective ⇑f<VAR>I J : Ideal S<VAR>h : J ∈ I.minimalPrimes<VAR>this✝ : J.IsPrime<VAR>K : Ideal R<VAR>hK : K.IsPrime<VAR>e₁ : comap f I ≤ K<VAR>e₂ : K ≤ comap f J<VAR>this : RingHom.ker f ≤ K<GOAL>J ≤ map f K
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>I✝ J✝ : Ideal R<VAR>f : R →+* S<VAR>hf : Function.Surjective ⇑f<VAR>I J : Ideal S<VAR>h : J ∈ I.minimalPrimes<VAR>this✝ : J.IsPrime<VAR>K : Ideal R<VAR>hK : K.IsPrime<VAR>e₁ : comap f I ≤ K<VAR>e₂ : K ≤ comap f J<VAR>this : RingHom.ker f ≤ K<GOAL>map f K ∈ {p | p.IsPrime ∧ I ≤ p}
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>I✝ J✝ : Ideal R<VAR>f : R →+* S<VAR>hf : Function.Surjective ⇑f<VAR>I J : Ideal S<VAR>h : J ∈ I.minimalPrimes<VAR>this✝ : J.IsPrime<VAR>K : Ideal R<VAR>hK : K.IsPrime<VAR>e₁ : comap f I ≤ K<VAR>e₂ : K ≤ comap f J<VAR>this : RingHom.ker f ≤ K<GOAL>map f K ≤ J
<VAR>ι : Sort u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s✝ t✝ u✝ : Set E<VAR>x y : E<VAR>s t u : Set E<GOAL>convexJoin 𝕜 s (convexJoin 𝕜 t u) = convexJoin 𝕜 t (convexJoin 𝕜 s u)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>R : Type u_3<VAR>inst✝⁶ : Zero X<VAR>inst✝⁵ : Zero Y<VAR>inst✝⁴ : Zero R<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace R<VAR>inst✝ : T1Space R<GOAL>IsClosed (range _root_.toContinuousMap)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>R : Type u_3<VAR>inst✝⁶ : Zero X<VAR>inst✝⁵ : Zero Y<VAR>inst✝⁴ : Zero R<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace R<VAR>inst✝ : T1Space R<GOAL>IsClosed {f | f 0 = 0}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>t : TopologicalSpace α<VAR>s : Set β<VAR>f : α → β<GOAL>IsClosed s ↔ IsClosed (f ⁻¹' s)
<VAR>R : Type u_1<VAR>inst✝¹² : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : AddCommMonoid M'<VAR>inst✝⁹ : AddCommMonoid M''<VAR>A : Type u_5<VAR>inst✝⁸ : CommSemiring A<VAR>inst✝⁷ : Algebra R A<VAR>inst✝⁶ : Module A M'<VAR>inst✝⁵ : IsLocalization S A<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module R M''<VAR>inst✝¹ : IsScalarTower R A M'<VAR>f : M →ₗ[R] M'<VAR>g : M →ₗ[R] M''<VAR>inst✝ : IsLocalizedModule S f<VAR>m : M<VAR>s : ↥S<GOAL>mk' f m s = 0 ↔ f m = 0
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>p✝ q p : R[X]<GOAL>∃ q, (Multiset.map (fun a => X - C a) p.roots).prod * q = p ∧ Multiset.card p.roots + q.natDegree = p.natDegree ∧ q.roots = 0
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>p✝ q✝ p q : R[X]<VAR>he : p = (Multiset.map (fun a => X - C a) p.roots).prod * q<GOAL>∃ q, (Multiset.map (fun a => X - C a) p.roots).prod * q = p ∧ Multiset.card p.roots + q.natDegree = p.natDegree ∧ q.roots = 0
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>p✝ q✝ p q : R[X]<VAR>he : p = (Multiset.map (fun a => X - C a) p.roots).prod * q<GOAL>Multiset.card p.roots + q.natDegree = p.natDegree ∧ q.roots = 0
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>p✝ q p : R[X]<VAR>he : p = (Multiset.map (fun a => X - C a) p.roots).prod * 0<GOAL>Multiset.card p.roots + natDegree 0 = p.natDegree ∧ roots 0 = 0
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>p✝ q✝ p q : R[X]<VAR>he : p = (Multiset.map (fun a => X - C a) p.roots).prod * q<VAR>hq : q ≠ 0<GOAL>Multiset.card p.roots + q.natDegree = p.natDegree ∧ q.roots = 0
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E : Type u_4<VAR>Eₗ : Type u_5<VAR>F : Type u_6<VAR>Fₗ : Type u_7<VAR>G : Type u_8<VAR>Gₗ : Type u_9<VAR>𝓕 : Type u_10<VAR>inst✝¹⁷ : SeminormedAddCommGroup E<VAR>inst✝¹⁶ : SeminormedAddCommGroup Eₗ<VAR>inst✝¹⁵ : SeminormedAddCommGroup F<VAR>inst✝¹⁴ : SeminormedAddCommGroup Fₗ<VAR>inst✝¹³ : SeminormedAddCommGroup G<VAR>inst✝¹² : SeminormedAddCommGroup Gₗ<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜₂<VAR>inst✝⁹ : NontriviallyNormedField 𝕜₃<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : NormedSpace 𝕜 Eₗ<VAR>inst✝⁶ : NormedSpace 𝕜₂ F<VAR>inst✝⁵ : NormedSpace 𝕜 Fₗ<VAR>inst✝⁴ : NormedSpace 𝕜₃ G<VAR>inst✝³ : NormedSpace 𝕜 Gₗ<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>σ₁₃ : 𝕜 →+* 𝕜₃<VAR>inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>inst✝¹ : FunLike 𝓕 E F<VAR>inst✝ : RingHomIsometric σ₂₃<VAR>f : E →ₛₗ[σ₁₃] F →ₛₗ[σ₂₃] G<VAR>C : ℝ<VAR>h : ∀ (x : E) (y : F), ‖(f x) y‖ ≤ C * ‖x‖ * ‖y‖<VAR>x : E<GOAL>max (C * ‖x‖) 0 = max C 0 * ‖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>ι : Sort u_9<VAR>p : ι → Submodule R M<VAR>m : M<GOAL>m ∈ ⨆ i, p i ↔ ∀ (N : Submodule R M), (∀ (i : ι), p i ≤ N) → m ∈ N
<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>ι : Sort u_9<VAR>p : ι → Submodule R M<VAR>m : M<GOAL>(∀ (b : Submodule R M), (∀ (i : ι), p i ≤ b) → span R {m} ≤ b) ↔ ∀ (N : Submodule R M), (∀ (i : ι), p i ≤ N) → m ∈ N
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s t u : Set α<VAR>inst✝² : MeasurableSpace α<VAR>μ : Measure ℝ<VAR>inst✝¹ : IsFiniteMeasureOnCompacts μ<VAR>inst✝ : NoAtoms μ<VAR>b : ℝ<GOAL>Tendsto (fun δ => μ (Icc (b - δ) (b + δ))) (𝓝 0) (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s t u : Set α<VAR>inst✝² : MeasurableSpace α<VAR>μ : Measure ℝ<VAR>inst✝¹ : IsFiniteMeasureOnCompacts μ<VAR>inst✝ : NoAtoms μ<VAR>b : ℝ<GOAL>Tendsto (fun δ => μ (Icc (b - δ) (b + δ))) (𝓝[<] 0) (𝓝 0) ∧ Tendsto (fun δ => μ (Icc (b - δ) (b + δ))) (𝓝[≥] 0) (𝓝 0)
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W : WeierstrassCurve R<VAR>A : Type v<VAR>inst✝ : CommRing A<VAR>φ : R →+* A<GOAL>(W.map φ).b₄ = φ W.b₄
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W : WeierstrassCurve R<VAR>A : Type v<VAR>inst✝ : CommRing A<VAR>φ : R →+* A<GOAL>2 * φ W.a₄ + φ W.a₁ * φ W.a₃ = φ (2 * W.a₄ + W.a₁ * W.a₃)
<VAR>R : Type u_1<VAR>inst✝³ : CommMonoid R<VAR>inst✝² : Fintype R<VAR>R' : Type u_2<VAR>inst✝¹ : CommRing R'<VAR>inst✝ : IsDomain R'<VAR>χ : MulChar R R'<VAR>hχ : χ ≠ 1<GOAL>∑ a : R, χ a = 0
<VAR>R : Type u_1<VAR>inst✝³ : CommMonoid R<VAR>inst✝² : Fintype R<VAR>R' : Type u_2<VAR>inst✝¹ : CommRing R'<VAR>inst✝ : IsDomain R'<VAR>χ : MulChar R R'<VAR>hχ : χ ≠ 1<VAR>b : Rˣ<VAR>hb : χ ↑b ≠ 1<GOAL>∑ a : R, χ a = 0
<VAR>R : Type u_1<VAR>inst✝³ : CommMonoid R<VAR>inst✝² : Fintype R<VAR>R' : Type u_2<VAR>inst✝¹ : CommRing R'<VAR>inst✝ : IsDomain R'<VAR>χ : MulChar R R'<VAR>hχ : χ ≠ 1<VAR>b : Rˣ<VAR>hb : χ ↑b ≠ 1<GOAL>χ ↑b * ∑ a : R, χ a = ∑ a : R, χ a
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Linear R C<VAR>F G K L : CochainComplex C ℤ<VAR>n m : ℤ<VAR>ψ : (p : ℤ) → F.X p ⟶ G.X p<VAR>p q q' : ℤ<VAR>hpq : p + 0 = q<GOAL>(ofHoms ψ).v p q hpq ≫ G.d q q' = ψ p ≫ G.d p q'
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Linear R C<VAR>F G K L : CochainComplex C ℤ<VAR>n m : ℤ<VAR>ψ : (p : ℤ) → F.X p ⟶ G.X p<VAR>p q q' : ℤ<VAR>hpq✝ : p + 0 = q<VAR>hpq : p = q<GOAL>(ofHoms ψ).v p q hpq✝ ≫ G.d q q' = ψ p ≫ G.d p q'
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Linear R C<VAR>F G K L : CochainComplex C ℤ<VAR>n m : ℤ<VAR>ψ : (p : ℤ) → F.X p ⟶ G.X p<VAR>p q' : ℤ<VAR>hpq : p + 0 = p<GOAL>(ofHoms ψ).v p p hpq ≫ G.d p q' = ψ p ≫ G.d p q'
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>V : Type u_3<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing A<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Algebra R A<VAR>inst✝³ : Module R V<VAR>inst✝² : Module A V<VAR>inst✝¹ : IsScalarTower R A V<VAR>inst✝ : Invertible 2<VAR>Q : QuadraticForm R V<VAR>x : CliffordAlgebra (QuadraticForm.baseChange A Q)<GOAL>(toBaseChange A Q) (reverse x) = (TensorProduct.map LinearMap.id reverse) ((toBaseChange A Q) x)