ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : AddCommGroup M'<VAR>inst✝⁴ : AddCommGroup M''<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R M'<VAR>inst✝¹ : Module R M''<VAR>a b : R<VAR>x y : M<VAR>inst✝ : Nontrivial R<VAR>hv : LinearIndependent R v<VAR>f : ι' ↪ ι<VAR>hss : range v ⊆ ↑(span R (range (v ∘ ⇑f)))<VAR>i : ι<VAR>repr : ↥(span R (range (v ∘ ⇑f))) → ι' →₀ R := ⇑⋯.repr<VAR>l : ι →₀ R := Finsupp.mapDomain (⇑f) (repr ⟨v i, ⋯⟩)<VAR>h_total_l : (Finsupp.total ι M R v) l = v i<VAR>h_total_eq : (Finsupp.total ι M R v) l = (Finsupp.total ι M R v) (Finsupp.single i 1)<VAR>l_eq : Finsupp.embDomain f (repr ⟨v i, ⋯⟩) = Finsupp.single i 1<GOAL>∃ a, f a = i
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : AddCommGroup M'<VAR>inst✝⁴ : AddCommGroup M''<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R M'<VAR>inst✝¹ : Module R M''<VAR>a b : R<VAR>x y : M<VAR>inst✝ : Nontrivial R<VAR>hv : LinearIndependent R v<VAR>f : ι' ↪ ι<VAR>hss : range v ⊆ ↑(span R (range (v ∘ ⇑f)))<VAR>i : ι<VAR>repr : ↥(span R (range (v ∘ ⇑f))) → ι' →₀ R := ⇑⋯.repr<VAR>l : ι →₀ R := Finsupp.mapDomain (⇑f) (repr ⟨v i, ⋯⟩)<VAR>h_total_l : (Finsupp.total ι M R v) l = v i<VAR>h_total_eq : (Finsupp.total ι M R v) l = (Finsupp.total ι M R v) (Finsupp.single i 1)<VAR>l_eq : Finsupp.embDomain f (repr ⟨v i, ⋯⟩) = Finsupp.single i 1<VAR>i' : ι'<VAR>hi' : repr ⟨v i, ⋯⟩ = Finsupp.single i' 1 ∧ f i' = i<GOAL>∃ a, f a = i
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : AddCommGroup M'<VAR>inst✝⁴ : AddCommGroup M''<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R M'<VAR>inst✝¹ : Module R M''<VAR>a b : R<VAR>x y : M<VAR>inst✝ : Nontrivial R<VAR>hv : LinearIndependent R v<VAR>f : ι' ↪ ι<VAR>hss : range v ⊆ ↑(span R (range (v ∘ ⇑f)))<VAR>i : ι<VAR>repr : ↥(span R (range (v ∘ ⇑f))) → ι' →₀ R := ⇑⋯.repr<VAR>l : ι →₀ R := Finsupp.mapDomain (⇑f) (repr ⟨v i, ⋯⟩)<VAR>h_total_l : (Finsupp.total ι M R v) l = v i<VAR>h_total_eq : (Finsupp.total ι M R v) l = (Finsupp.total ι M R v) (Finsupp.single i 1)<VAR>l_eq : Finsupp.embDomain f (repr ⟨v i, ⋯⟩) = Finsupp.single i 1<VAR>i' : ι'<VAR>hi' : repr ⟨v i, ⋯⟩ = Finsupp.single i' 1 ∧ f i' = i<GOAL>f i' = i
<VAR>n : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : Monoid α<VAR>v : Vector α n<VAR>i : Fin n<VAR>a : α<GOAL>(v.set i a).toList.prod = (take (↑i) v).toList.prod * a * (drop (↑i + 1) v).toList.prod
<VAR>n : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : Monoid α<VAR>v : Vector α n<VAR>i : Fin n<VAR>a : α<GOAL>((List.take (↑i) v.toList).prod * if ↑i < v.toList.length then a else 1) * (List.drop (↑i + 1) v.toList).prod = (take (↑i) v).toList.prod * a * (drop (↑i + 1) v).toList.prod
<VAR>x y : ℝ<VAR>a b : CauSeq ℚ abs<GOAL>{ cauchy := ⟦a ⊔ b⟧ } = Real.sup { cauchy := ⟦a⟧ } { cauchy := ⟦b⟧ }
<VAR>x y : ℝ<VAR>a b : CauSeq ℚ abs<GOAL>{ cauchy := ⟦a ⊔ b⟧ } = match { cauchy := ⟦a⟧ }, { cauchy := ⟦b⟧ } with | { cauchy := x }, { cauchy := y } => { cauchy := Quotient.map₂ (fun x x_1 => x ⊔ x_1) ⋯ x y }
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : LinearOrderedAddCommGroup α<VAR>inst✝ : Archimedean α<VAR>a : α<VAR>ha : 0 < a<VAR>b c : α<GOAL>∃! x, b + (Equiv.neg ℤ) x • a ∈ Ico c (c + a)
<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✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedAddCommGroup F<VAR>inst✝¹¹ : NormedAddCommGroup G<VAR>inst✝¹⁰ : NormedAddCommGroup Fₗ<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NontriviallyNormedField 𝕜₂<VAR>inst✝⁷ : NontriviallyNormedField 𝕜₃<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedSpace 𝕜₂ F<VAR>inst✝⁴ : NormedSpace 𝕜₃ G<VAR>inst✝³ : NormedSpace 𝕜 Fₗ<VAR>c : 𝕜<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>f✝ g : E →SL[σ₁₂] F<VAR>x y z : E<VAR>E' : Type u_11<VAR>inst✝² : SeminormedAddCommGroup E'<VAR>inst✝¹ : NormedSpace 𝕜 E'<VAR>inst✝ : RingHomIsometric σ₁₂<VAR>f₀ : E' →SL[σ₁₂] F<VAR>r : ℝ<VAR>f : E' →SL[σ₁₂] F<VAR>hf : ⇑f ∈ closure (DFunLike.coe '' closedBall f₀ r)<GOAL>f ∈ closedBall f₀ r
<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✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedAddCommGroup F<VAR>inst✝¹¹ : NormedAddCommGroup G<VAR>inst✝¹⁰ : NormedAddCommGroup Fₗ<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NontriviallyNormedField 𝕜₂<VAR>inst✝⁷ : NontriviallyNormedField 𝕜₃<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedSpace 𝕜₂ F<VAR>inst✝⁴ : NormedSpace 𝕜₃ G<VAR>inst✝³ : NormedSpace 𝕜 Fₗ<VAR>c : 𝕜<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>f✝ g : E →SL[σ₁₂] F<VAR>x y z : E<VAR>E' : Type u_11<VAR>inst✝² : SeminormedAddCommGroup E'<VAR>inst✝¹ : NormedSpace 𝕜 E'<VAR>inst✝ : RingHomIsometric σ₁₂<VAR>f₀ : E' →SL[σ₁₂] F<VAR>r : ℝ<VAR>f : E' →SL[σ₁₂] F<VAR>hf : ⇑f ∈ closure (DFunLike.coe '' closedBall f₀ r)<VAR>hr : 0 ≤ r<GOAL>f ∈ closedBall f₀ r
<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✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedAddCommGroup F<VAR>inst✝¹¹ : NormedAddCommGroup G<VAR>inst✝¹⁰ : NormedAddCommGroup Fₗ<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NontriviallyNormedField 𝕜₂<VAR>inst✝⁷ : NontriviallyNormedField 𝕜₃<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedSpace 𝕜₂ F<VAR>inst✝⁴ : NormedSpace 𝕜₃ G<VAR>inst✝³ : NormedSpace 𝕜 Fₗ<VAR>c : 𝕜<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>f✝ g : E →SL[σ₁₂] F<VAR>x✝ y z : E<VAR>E' : Type u_11<VAR>inst✝² : SeminormedAddCommGroup E'<VAR>inst✝¹ : NormedSpace 𝕜 E'<VAR>inst✝ : RingHomIsometric σ₁₂<VAR>f₀ : E' →SL[σ₁₂] F<VAR>r : ℝ<VAR>f : E' →SL[σ₁₂] F<VAR>hf : ⇑f ∈ closure (DFunLike.coe '' closedBall f₀ r)<VAR>hr : 0 ≤ r<VAR>x : E'<GOAL>‖(f - f₀) x‖ ≤ r * ‖x‖
<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✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedAddCommGroup F<VAR>inst✝¹¹ : NormedAddCommGroup G<VAR>inst✝¹⁰ : NormedAddCommGroup Fₗ<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NontriviallyNormedField 𝕜₂<VAR>inst✝⁷ : NontriviallyNormedField 𝕜₃<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedSpace 𝕜₂ F<VAR>inst✝⁴ : NormedSpace 𝕜₃ G<VAR>inst✝³ : NormedSpace 𝕜 Fₗ<VAR>c : 𝕜<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>f✝ g : E →SL[σ₁₂] F<VAR>x✝ y z : E<VAR>E' : Type u_11<VAR>inst✝² : SeminormedAddCommGroup E'<VAR>inst✝¹ : NormedSpace 𝕜 E'<VAR>inst✝ : RingHomIsometric σ₁₂<VAR>f₀ : E' →SL[σ₁₂] F<VAR>r : ℝ<VAR>f : E' →SL[σ₁₂] F<VAR>hf : ⇑f ∈ closure (DFunLike.coe '' closedBall f₀ r)<VAR>hr : 0 ≤ r<VAR>x : E'<VAR>this : IsClosed {g | ‖g x - f₀ x‖ ≤ r * ‖x‖}<GOAL>‖(f - f₀) x‖ ≤ r * ‖x‖
<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✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedAddCommGroup F<VAR>inst✝¹¹ : NormedAddCommGroup G<VAR>inst✝¹⁰ : NormedAddCommGroup Fₗ<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NontriviallyNormedField 𝕜₂<VAR>inst✝⁷ : NontriviallyNormedField 𝕜₃<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedSpace 𝕜₂ F<VAR>inst✝⁴ : NormedSpace 𝕜₃ G<VAR>inst✝³ : NormedSpace 𝕜 Fₗ<VAR>c : 𝕜<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>f✝ g✝ : E →SL[σ₁₂] F<VAR>x✝ y z : E<VAR>E' : Type u_11<VAR>inst✝² : SeminormedAddCommGroup E'<VAR>inst✝¹ : NormedSpace 𝕜 E'<VAR>inst✝ : RingHomIsometric σ₁₂<VAR>f₀ : E' →SL[σ₁₂] F<VAR>r : ℝ<VAR>f : E' →SL[σ₁₂] F<VAR>hf : ⇑f ∈ closure (DFunLike.coe '' closedBall f₀ r)<VAR>hr : 0 ≤ r<VAR>x : E'<VAR>this : IsClosed {g | ‖g x - f₀ x‖ ≤ r * ‖x‖}<VAR>g : E' →SL[σ₁₂] F<VAR>hg : g ∈ closedBall f₀ r<GOAL>g ∈ DFunLike.coe ⁻¹' {g | ‖g x - f₀ x‖ ≤ r * ‖x‖}
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s t : Multiset α<GOAL>s + t = s ∪ t ↔ s.Disjoint t
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹¹ : CommSemiring R<VAR>inst✝¹⁰ : StarRing R<VAR>inst✝⁹ : MetricSpace R<VAR>inst✝⁸ : TopologicalSemiring R<VAR>inst✝⁷ : ContinuousStar R<VAR>inst✝⁶ : TopologicalSpace A<VAR>inst✝⁵ : Ring A<VAR>inst✝⁴ : StarRing A<VAR>inst✝³ : Algebra R A<VAR>inst✝² : ContinuousFunctionalCalculus R p<VAR>f g : R → R<VAR>a : A<VAR>ha : autoParam (p a) _auto✝<VAR>hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝<VAR>hg : autoParam (ContinuousOn g (spectrum R a)) _auto✝<VAR>inst✝¹ : UniqueContinuousFunctionalCalculus R A<VAR>inst✝ : Nontrivial A<GOAL>spectrum R 0 = {0}
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹¹ : CommSemiring R<VAR>inst✝¹⁰ : StarRing R<VAR>inst✝⁹ : MetricSpace R<VAR>inst✝⁸ : TopologicalSemiring R<VAR>inst✝⁷ : ContinuousStar R<VAR>inst✝⁶ : TopologicalSpace A<VAR>inst✝⁵ : Ring A<VAR>inst✝⁴ : StarRing A<VAR>inst✝³ : Algebra R A<VAR>inst✝² : ContinuousFunctionalCalculus R p<VAR>f g : R → R<VAR>a : A<VAR>ha : autoParam (p a) _auto✝<VAR>hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝<VAR>hg : autoParam (ContinuousOn g (spectrum R a)) _auto✝<VAR>inst✝¹ : UniqueContinuousFunctionalCalculus R A<VAR>inst✝ : Nontrivial A<VAR>this : 0 = (algebraMap R A) 0<GOAL>spectrum R 0 = {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>s : Set β<VAR>f : α → β<VAR>hs : s.Countable<GOAL>μ (f ⁻¹' s) = 0 ↔ ∀ x ∈ s, μ (f ⁻¹' {x}) = 0
<VAR>p n✝ k✝ n k : ℕ<VAR>hkn : k ≤ n<GOAL>∏ p ∈ Finset.range (n + 1), p ^ (n.choose k).factorization p = n.choose k
<VAR>p n✝ k✝ n k : ℕ<VAR>hkn : k ≤ n<GOAL>∏ p ∈ Finset.range (n + 1), p ^ (n.choose k).factorization p = (n.choose k).factorization.prod fun x x_1 => x ^ x_1
<VAR>p n✝ k✝ n k : ℕ<VAR>hkn : k ≤ n<GOAL>((n.choose k).factorization.prod fun x x_1 => x ^ x_1) = ∏ p ∈ Finset.range (n + 1), p ^ (n.choose k).factorization p
<VAR>p n✝ k✝ n k : ℕ<VAR>hkn : k ≤ n<GOAL>(n.choose k).factorization.support ⊆ Finset.range (n + 1)
<VAR>p n✝ k✝ n k : ℕ<VAR>hkn : k ≤ n<GOAL>∀ x ∈ Finset.range (n + 1), x ∉ (n.choose k).factorization.support → (fun x x_1 => x ^ x_1) x ((n.choose k).factorization x) = 1
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedSemiring α<VAR>m n : PosNum<GOAL>↑m ≤ ↑n ↔ m ≤ n
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedSemiring α<VAR>m n : PosNum<GOAL>¬↑n < ↑m ↔ m ≤ n
<VAR>E : Type u_1<VAR>inst✝ : MeasurableSpace E<VAR>m μ : Measure E<VAR>Ω : Type u_2<VAR>x✝ : MeasurableSpace Ω<VAR>ℙ : Measure Ω<VAR>X : Ω → E<VAR>s : Set E<VAR>hu : Measure.map X ℙ = ProbabilityTheory.cond μ s<GOAL>Measure.map X ℙ = ProbabilityTheory.cond μ (toMeasurable μ s)
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝⁴ : Ring R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>ι : Type w<VAR>ι' : Type w'<VAR>inst✝¹ : StrongRankCondition R<VAR>inst✝ : Module.Finite R M<GOAL>↑(finrank R M) = Module.rank R M
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>a : α<VAR>f : Stream' (Option α)<VAR>al : f.IsSeq<GOAL>tail ⟨some a :: ↑⟨f, al⟩, ⋯⟩ = ⟨f, al⟩
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>a : α<VAR>f : Stream' (Option α)<VAR>al : f.IsSeq<GOAL>↑(tail ⟨some a :: ↑⟨f, al⟩, ⋯⟩) = ↑⟨f, al⟩
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>l : List ℤ<VAR>h : l.prod = -1<GOAL>-1 ∈ l
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>l : List ℤ<VAR>h : l.prod = -1<VAR>x : ℤ<VAR>h₁ : x ∈ l<VAR>h₂ : x ≠ 1<GOAL>-1 ∈ l
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : WeierstrassCurve R<VAR>C✝ C'✝ C''✝ C C' C'' : VariableChange R<GOAL>(C.comp C').comp C'' = C.comp (C'.comp C'')
<VAR>q : ℤ[X]<VAR>k m n : ℕ<VAR>hkm : k < m<VAR>hmn : m < n<VAR>u v w : ℤˣ<GOAL>¬IsUnit (trinomial k m n ↑u ↑v ↑w)
<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>hb : IsBoundedBilinearMap 𝕜 b<GOAL>ContDiff 𝕜 n b
<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>hb : IsBoundedBilinearMap 𝕜 b<GOAL>ContDiff 𝕜 ⊤ b
<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>hb : IsBoundedBilinearMap 𝕜 b<GOAL>Differentiable 𝕜 b ∧ ContDiff 𝕜 ⊤ fun y => fderiv 𝕜 b y
<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>hb : IsBoundedBilinearMap 𝕜 b<GOAL>ContDiff 𝕜 ⊤ fun y => fderiv 𝕜 b y
<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>hb : IsBoundedBilinearMap 𝕜 b<GOAL>ContDiff 𝕜 ⊤ fun y => hb.deriv y
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>g : Perm α<VAR>x✝ y✝ : α<VAR>inst✝ : DecidableEq α<VAR>x y : α<VAR>hxy : x ≠ y<GOAL>(swap x y).IsCycle
<VAR>R : Type u<VAR>S✝ : Type v<VAR>A✝ : Type w<VAR>B : Type u₁<VAR>M : Type v₁<VAR>inst✝¹² : CommSemiring R<VAR>inst✝¹¹ : CommSemiring S✝<VAR>inst✝¹⁰ : Semiring A✝<VAR>inst✝⁹ : Semiring B<VAR>inst✝⁸ : Algebra R S✝<VAR>inst✝⁷ : Algebra S✝ A✝<VAR>inst✝⁶ : Algebra S✝ B<VAR>inst✝⁵ : Algebra R A✝<VAR>inst✝⁴ : Algebra R B<VAR>inst✝³ : IsScalarTower R S✝ A✝<VAR>inst✝² : IsScalarTower R S✝ B<VAR>S : Type u<VAR>A : Type v<VAR>inst✝¹ : CommSemiring S<VAR>inst✝ : Semiring A<VAR>h1 h2 : Algebra S A<VAR>h : ∀ (r : S) (x : A), (let_fun I := h1; r • x) = r • x<VAR>r : S<GOAL>(algebraMap S A) r = (algebraMap S A) r
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>m' : o → Type u_5<VAR>n' : o → Type u_6<VAR>R : Type u_7<VAR>S : Type u_8<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>inst✝⁴ : NonUnitalNonAssocSemiring α<VAR>inst✝³ : Fintype n<VAR>inst✝² : Monoid R<VAR>inst✝¹ : DistribMulAction R α<VAR>inst✝ : IsScalarTower R α α<VAR>a : R<VAR>A : Matrix m n α<VAR>b : n → α<VAR>x✝ : m<GOAL>((a • A) *ᵥ b) x✝ = (a • A *ᵥ b) x✝
<VAR>ι✝ : Type u_1<VAR>α : Type u_2<VAR>M : Matroid α<VAR>F X Y : Set α<VAR>e : α<VAR>ι : Sort u_3<VAR>I J B : Set α<VAR>f x y : α<VAR>hI : M.Indep I<GOAL>x ∈ M.closure I ↔ x ∈ M.E ∧ (M.Indep (insert x I) → x ∈ I)
<VAR>ι✝ : Type u_1<VAR>α : Type u_2<VAR>M : Matroid α<VAR>F X Y : Set α<VAR>e : α<VAR>ι : Sort u_3<VAR>I J B : Set α<VAR>f x y : α<VAR>hI : M.Indep I<GOAL>¬M.Indep (insert x I) ∧ x ∈ M.E ∨ x ∈ I ↔ x ∈ M.E ∧ (¬M.Indep (insert x I) ∨ x ∈ I)
<VAR>ι✝ : Type u_1<VAR>α : Type u_2<VAR>M : Matroid α<VAR>F X Y : Set α<VAR>e : α<VAR>ι : Sort u_3<VAR>I J B : Set α<VAR>f x y : α<VAR>hI : M.Indep I<VAR>this : I ⊆ M.E<GOAL>¬M.Indep (insert x I) ∧ x ∈ M.E ∨ x ∈ I ↔ x ∈ M.E ∧ (¬M.Indep (insert x I) ∨ x ∈ I)
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>n : ℕ<VAR>φ : R⟦X⟧<GOAL>(coeff R (n + 1)) (X * φ) = (coeff R n) φ
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>n : ℕ<VAR>φ : R⟦X⟧<GOAL>(MvPowerSeries.coeff R (single () 1 + single () n)) (X * φ) = (MvPowerSeries.coeff R (single () n)) φ
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>n : ℕ<VAR>φ : R⟦X⟧<GOAL>(MvPowerSeries.coeff R (single () n)) φ = 1 * (MvPowerSeries.coeff R (single () n)) φ
<VAR>B : Type u<VAR>inst✝ : Bicategory B<VAR>a b c : B<VAR>f : a ⟶ b<VAR>g : a ⟶ c<VAR>s t : LeftExtension f g<VAR>i : s ⟶ t<VAR>x : B<VAR>h : c ⟶ x<GOAL>(s.whisker h).hom ≫ (precomp x f).map (i.right ▷ h) = (t.whisker h).hom
<VAR>B : Type u<VAR>inst✝ : Bicategory B<VAR>a b c : B<VAR>f : a ⟶ b<VAR>g : a ⟶ c<VAR>s t : LeftExtension f g<VAR>i : s ⟶ t<VAR>x : B<VAR>h : c ⟶ x<GOAL>((s.whisker h).hom ≫ (precomp x f).map (i.right ▷ h)) ≫ (α_ f t.extension h).inv = (t.whisker h).hom ≫ (α_ f t.extension h).inv
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>x : FreeCommRing α<VAR>s : Set α<VAR>hfs : s.Finite<VAR>hxs : x.IsSupported s<GOAL>x.IsSupported ↑hfs.toFinset
<VAR>X Y : Compactum<VAR>f : X ⟶ Y<VAR>xs : Ultrafilter X.A<GOAL>(X.a ≫ f.f) xs = Y.str (Ultrafilter.map f.f xs)
<VAR>X Y : Compactum<VAR>f : X ⟶ Y<VAR>xs : Ultrafilter X.A<GOAL>(β.map f.f ≫ Y.a) xs = Y.str (Ultrafilter.map f.f xs)
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.115347, u_1} C<VAR>inst✝ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>e : S₁ ≅ S₂<VAR>h₁ : S₁.LeftHomologyData<VAR>h₂ : S₂.LeftHomologyData<GOAL>cyclesMap' e.hom h₁ h₂ ≫ cyclesMap' e.inv h₂ h₁ = 𝟙 h₁.K
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.115347, u_1} C<VAR>inst✝ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>e : S₁ ≅ S₂<VAR>h₁ : S₁.LeftHomologyData<VAR>h₂ : S₂.LeftHomologyData<GOAL>cyclesMap' e.inv h₂ h₁ ≫ cyclesMap' e.hom h₁ h₂ = 𝟙 h₂.K
<VAR>G : Type u_1<VAR>inst✝² : SeminormedAddCommGroup G<VAR>H : Type u_2<VAR>inst✝¹ : SeminormedAddCommGroup H<VAR>K : Type u_3<VAR>inst✝ : SeminormedAddCommGroup K<VAR>f : NormedAddGroupHom G H<VAR>g : G<VAR>h₀ : f g = 0<GOAL>(toCompl.comp (incl f.ker)).toAddMonoidHom ⟨g, h₀⟩ ∈ f.completion.ker
<VAR>R✝ : Type u<VAR>M✝ M₁ : Type v<VAR>M' : Type v'<VAR>ι : Type w<VAR>inst✝¹² : Ring R✝<VAR>inst✝¹¹ : AddCommGroup M✝<VAR>inst✝¹⁰ : AddCommGroup M'<VAR>inst✝⁹ : AddCommGroup M₁<VAR>inst✝⁸ : Module R✝ M✝<VAR>inst✝⁷ : Module R✝ M'<VAR>inst✝⁶ : Module R✝ M₁<VAR>inst✝⁵ : Nontrivial R✝<VAR>inst✝⁴ : NoZeroSMulDivisors R✝ M✝<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<GOAL>Module.rank R M = 0 ↔ Module.IsTorsion R M
<VAR>R✝ : Type u<VAR>M✝ M₁ : Type v<VAR>M' : Type v'<VAR>ι : Type w<VAR>inst✝¹² : Ring R✝<VAR>inst✝¹¹ : AddCommGroup M✝<VAR>inst✝¹⁰ : AddCommGroup M'<VAR>inst✝⁹ : AddCommGroup M₁<VAR>inst✝⁸ : Module R✝ M✝<VAR>inst✝⁷ : Module R✝ M'<VAR>inst✝⁶ : Module R✝ M₁<VAR>inst✝⁵ : Nontrivial R✝<VAR>inst✝⁴ : NoZeroSMulDivisors R✝ M✝<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<GOAL>(∀ (x : M), ∃ a, a ≠ 0 ∧ a • x = 0) ↔ ∀ ⦃x : M⦄, ∃ a, a • x = 0
<VAR>x : ℝ<GOAL>sin x = 0 ↔ cos x = 1 ∨ cos x = -1
<VAR>x : ℝ<GOAL>sin x = 0 ↔ 0 = sin x * sin x
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>U : Set ℂ<VAR>hU : IsOpen U<VAR>c w₀ : ℂ<VAR>R : ℝ<VAR>f : ℂ → E<VAR>hc : closedBall c R ⊆ U<VAR>hf : DifferentiableOn ℂ f U<VAR>hw₀ : w₀ ∈ ball c R<GOAL>((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), ((z - w₀) ^ 2)⁻¹ • f z) = deriv f w₀
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>U : Set ℂ<VAR>hU : IsOpen U<VAR>c w₀ : ℂ<VAR>R : ℝ<VAR>f : ℂ → E<VAR>hc : closedBall c R ⊆ U<VAR>hf : DifferentiableOn ℂ f U<VAR>hw₀ : w₀ ∈ ball c R<VAR>hf' : DifferentiableOn ℂ (dslope f w₀) U<GOAL>((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), ((z - w₀) ^ 2)⁻¹ • f z) = deriv f w₀
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>U : Set ℂ<VAR>hU : IsOpen U<VAR>c w₀ : ℂ<VAR>R : ℝ<VAR>f : ℂ → E<VAR>hc : closedBall c R ⊆ U<VAR>hf : DifferentiableOn ℂ f U<VAR>hw₀ : w₀ ∈ ball c R<VAR>hf' : DifferentiableOn ℂ (dslope f w₀) U<VAR>h0 : ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - w₀)⁻¹ • dslope f w₀ z) = dslope f w₀ w₀<GOAL>((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), ((z - w₀) ^ 2)⁻¹ • f z) = deriv f w₀
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>U : Set ℂ<VAR>hU : IsOpen U<VAR>c w₀ : ℂ<VAR>R : ℝ<VAR>f : ℂ → E<VAR>hc : closedBall c R ⊆ U<VAR>hf : DifferentiableOn ℂ f U<VAR>hw₀ : w₀ ∈ ball c R<VAR>hf' : DifferentiableOn ℂ (dslope f w₀) U<VAR>h0 : ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - w₀)⁻¹ • dslope f w₀ z) = dslope f w₀ w₀<GOAL>((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), ((z - w₀) ^ 2)⁻¹ • f z) = (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - w₀)⁻¹ • dslope f w₀ z
<VAR>α β : Type u<VAR>ι : Type u_1<VAR>f : ι → Cardinal.{u}<GOAL>prod f = 0 ↔ ∃ i, f i = 0
<VAR>α β : Type u<VAR>ι : Type u_1<VAR>f : ι → Type u<GOAL>(prod fun i => #(f i)) = 0 ↔ ∃ i, (fun i => #(f i)) i = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort u_6<VAR>s t u : Set α<VAR>m : MeasurableSpace α<VAR>s₁ s₂ : Set α<VAR>h₁ : MeasurableSet s₁<VAR>h₂ : MeasurableSet s₂<GOAL>MeasurableSet (s₁ ∩ s₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort u_6<VAR>s t u : Set α<VAR>m : MeasurableSpace α<VAR>s₁ s₂ : Set α<VAR>h₁ : MeasurableSet s₁<VAR>h₂ : MeasurableSet s₂<GOAL>MeasurableSet (s₁ᶜ ∪ s₂ᶜ)ᶜ
<VAR>F : Type u_1<VAR>inst✝³ : Field F<VAR>inst✝² : Fintype F<VAR>inst✝¹ : DecidableEq F<VAR>hF : ringChar F ≠ 2<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>hp₁ : p ≠ 2<VAR>hp₂ : ringChar F ≠ p<GOAL>(quadraticChar F) ↑p = (quadraticChar (ZMod p)) (↑(χ₄ ↑(Fintype.card F)) * ↑(Fintype.card F))
<VAR>F : Type u_1<VAR>inst✝³ : Field F<VAR>inst✝² : Fintype F<VAR>inst✝¹ : DecidableEq F<VAR>hF : ringChar F ≠ 2<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>hp₁ : p ≠ 2<VAR>hp₂ : ringChar F ≠ p<GOAL>(quadraticChar F) ↑p = (quadraticChar (ZMod p)) (↑((quadraticChar F) (-1)) * ↑(Fintype.card F))