ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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✝² : RankCondition R<VAR>ι : Type u_1<VAR>inst✝¹ : Fintype ι<VAR>b : Basis ι R M<VAR>w : Set M<VAR>inst✝ : Fintype ↑w<VAR>s : span R w = ⊤<GOAL>(↑w →₀ R) →ₗ[R] ι →₀ R
<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✝² : RankCondition R<VAR>ι : Type u_1<VAR>inst✝¹ : Fintype ι<VAR>b : Basis ι R M<VAR>w : Set M<VAR>inst✝ : Fintype ↑w<VAR>s : span R w = ⊤<GOAL>Surjective ⇑?f
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝¹ : SeminormedRing α✝<VAR>α : Type u_5<VAR>inst✝ : NormedCommRing α<VAR>s : Finset ι<VAR>hs : s.Nonempty<VAR>f : ι → α<GOAL>∏ i ∈ s, ‖f i‖ = (fun a => ↑a) (∏ i ∈ s, ‖f i‖₊)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁴ : Semigroup α<VAR>inst✝³ : Semigroup β<VAR>F : Type u_3<VAR>inst✝² : EquivLike F α β<VAR>inst✝¹ : MulEquivClass F α β<VAR>f : F<VAR>inst✝ : DecompositionMonoid β<VAR>a b c : α<VAR>h : a ∣ b * c<GOAL>∃ a₁ a₂, a₁ ∣ b ∧ a₂ ∣ c ∧ a = a₁ * a₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁴ : Semigroup α<VAR>inst✝³ : Semigroup β<VAR>F : Type u_3<VAR>inst✝² : EquivLike F α β<VAR>inst✝¹ : MulEquivClass F α β<VAR>f : F<VAR>inst✝ : DecompositionMonoid β<VAR>a b c : α<VAR>h : f a ∣ f b * f c<GOAL>∃ a₁ a₂, a₁ ∣ b ∧ a₂ ∣ c ∧ a = a₁ * a₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁴ : Semigroup α<VAR>inst✝³ : Semigroup β<VAR>F : Type u_3<VAR>inst✝² : EquivLike F α β<VAR>inst✝¹ : MulEquivClass F α β<VAR>f : F<VAR>inst✝ : DecompositionMonoid β<VAR>a b c : α<VAR>h✝ : f a ∣ f b * f c<VAR>a₁ a₂ : β<VAR>h : a₁ ∣ f b ∧ a₂ ∣ f c ∧ f a = a₁ * a₂<GOAL>∃ a₁ a₂, a₁ ∣ b ∧ a₂ ∣ c ∧ a = a₁ * a₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁴ : Semigroup α<VAR>inst✝³ : Semigroup β<VAR>F : Type u_3<VAR>inst✝² : EquivLike F α β<VAR>inst✝¹ : MulEquivClass F α β<VAR>f : F<VAR>inst✝ : DecompositionMonoid β<VAR>a b c : α<VAR>h✝ : f a ∣ f b * f c<VAR>a₁ a₂ : β<VAR>h : a₁ ∣ f b ∧ a₂ ∣ f c ∧ f a = a₁ * a₂<GOAL>(↑f).symm a₁ ∣ b ∧ (↑f).symm a₂ ∣ c ∧ a = (↑f).symm a₁ * (↑f).symm a₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁴ : Semigroup α<VAR>inst✝³ : Semigroup β<VAR>F : Type u_3<VAR>inst✝² : EquivLike F α β<VAR>inst✝¹ : MulEquivClass F α β<VAR>f : F<VAR>inst✝ : DecompositionMonoid β<VAR>a b c : α<VAR>h✝ : f a ∣ f b * f c<VAR>a₁ a₂ : β<VAR>h : a₁ ∣ f b ∧ a₂ ∣ f c ∧ f a = a₁ * a₂<GOAL>f ((↑f).symm a₁) ∣ f b ∧ f ((↑f).symm a₂) ∣ f c ∧ ↑f a = a₁ * a₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁴ : Semigroup α<VAR>inst✝³ : Semigroup β<VAR>F : Type u_3<VAR>inst✝² : EquivLike F α β<VAR>inst✝¹ : MulEquivClass F α β<VAR>f : F<VAR>inst✝ : DecompositionMonoid β<VAR>a b c : α<VAR>h✝ : f a ∣ f b * f c<VAR>a₁ a₂ : β<VAR>h : a₁ ∣ f b ∧ a₂ ∣ f c ∧ f a = a₁ * a₂<GOAL>a₁ ∣ f b ∧ a₂ ∣ f c ∧ ↑f a = a₁ * a₂
<VAR>α : Type u_1<VAR>inst✝² : SemilatticeInf α<VAR>inst✝¹ : OrderBot α<VAR>s✝ t : Set α<VAR>a b c : α<VAR>inst✝ : Subsingleton α<VAR>s : Set α<GOAL>s.Intersecting ↔ s = ∅
<VAR>α : Type u_1<VAR>inst✝² : SemilatticeInf α<VAR>inst✝¹ : OrderBot α<VAR>s✝ t : Set α<VAR>a b c : α<VAR>inst✝ : Subsingleton α<VAR>s : Set α<VAR>h : ¬s = ∅<GOAL>⊥ ∈ s
<VAR>α : Type u_1<VAR>inst✝² : SemilatticeInf α<VAR>inst✝¹ : OrderBot α<VAR>s✝ t : Set α<VAR>a b c : α<VAR>inst✝ : Subsingleton α<VAR>s : Set α<GOAL>s = ∅ → s ≠ {⊥}
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>a : α<VAR>m n : ℕ<VAR>inst✝ : Subsingleton αˣ<VAR>c d : α<VAR>hcd : a = a * c * d<GOAL>a = a * c
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>a : α<VAR>m n : ℕ<VAR>inst✝ : Subsingleton αˣ<VAR>c d : α<VAR>hcd : c = 1 ∧ d = 1 ∨ a = 0<GOAL>a = a * c
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>inst✝ : LinearOrderedSemiring R<VAR>a b : R<VAR>m n : ℕ<VAR>ha : 0 ≤ a<VAR>hn : n ≠ 0<GOAL>a ^ n ≤ 1 ↔ a ≤ 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Multiset α<VAR>x : Multiset α × Multiset α<VAR>l : List α<GOAL>x ∈ antidiagonal ⟦l⟧ ↔ x.1 + x.2 = ⟦l⟧
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Multiset α<VAR>x : Multiset α × Multiset α<VAR>l : List α<GOAL>x ∈ ↑(powersetAux l).revzip ↔ x.1 + x.2 = ↑l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Multiset α<VAR>x : Multiset α × Multiset α<VAR>l : List α<VAR>h : x.1 + x.2 = ↑l<GOAL>x ∈ ↑(powersetAux l).revzip
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Multiset α<VAR>x : Multiset α × Multiset α<VAR>l : List α<VAR>h : x.1 + x.2 = ↑l<VAR>this : DecidableEq α<GOAL>x ∈ ↑(powersetAux l).revzip
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Multiset α<VAR>x : Multiset α × Multiset α<VAR>l : List α<VAR>h : x.1 + x.2 = ↑l<VAR>this : DecidableEq α<GOAL>∃ a ≤ x.1 + x.2, (a, x.1 + x.2 - a) = x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Multiset α<VAR>l : List α<VAR>this : DecidableEq α<VAR>x₁ x₂ : Multiset α<VAR>h : (x₁, x₂).1 + (x₁, x₂).2 = ↑l<GOAL>∃ a ≤ (x₁, x₂).1 + (x₁, x₂).2, (a, (x₁, x₂).1 + (x₁, x₂).2 - a) = (x₁, x₂)
<VAR>α : Type u<VAR>β : Type v<VAR>δ : Type w<VAR>s : Stream' α<GOAL>(initsCore [s.head] s.tail).tail = initsCore [s.head, s.tail.head] s.tail.tail
<VAR>α : Type u<VAR>β : Type v<VAR>δ : Type w<VAR>s : Stream' α<GOAL>([s.head] :: initsCore ([s.head] ++ [s.tail.head]) s.tail.tail).tail = initsCore [s.head, s.tail.head] s.tail.tail
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q : QuadraticForm R M<VAR>i' : ZMod 2<VAR>x' : ↥(evenOdd Q i')<GOAL>∀ (m : M), (GradedAlgebra.ι Q) m * (GradedAlgebra.ι Q) m = (algebraMap R (⨁ (i : ZMod 2), ↥(evenOdd Q i))) (Q m)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q : QuadraticForm R M<VAR>i' : ZMod 2<VAR>x' : CliffordAlgebra Q<VAR>hx' : x' ∈ evenOdd Q i'<GOAL>((lift Q) ⟨GradedAlgebra.ι Q, ⋯⟩) ↑⟨x', hx'⟩ = (DirectSum.of (fun i => ↥(evenOdd Q i)) i') ⟨x', hx'⟩
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q : QuadraticForm R M<VAR>i' : ZMod 2<VAR>x' : CliffordAlgebra Q<VAR>hx' : x' ∈ evenOdd Q i'<GOAL>((lift Q) ⟨GradedAlgebra.ι Q, ⋯⟩) x' = (DirectSum.of (fun i => ↥(evenOdd Q i)) i') ⟨x', hx'⟩
<VAR>α : Type u_1<VAR>f : α → α<VAR>n : Nat<VAR>l : List α<GOAL>(modifyNth f n l).get? n = f <$> l.get? n
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s✝ s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<VAR>f : α → X<VAR>l : Filter α<VAR>s : Set α<VAR>h : ∀ a ∉ s, f a = x<GOAL>Tendsto f (l ⊓ 𝓟 s) (𝓝 x) ↔ Tendsto f l (𝓝 x)
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s✝ s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<VAR>f : α → X<VAR>l : Filter α<VAR>s : Set α<VAR>h : ∀ a ∉ s, f a = x<GOAL>l ⊓ 𝓟 s ≤ comap f (𝓝 x) ↔ l ≤ comap f (𝓝 x)
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s✝ s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<VAR>f : α → X<VAR>l : Filter α<VAR>s : Set α<VAR>h : 𝓟 sᶜ ≤ comap f (𝓝 x)<GOAL>l ⊓ 𝓟 s ≤ comap f (𝓝 x) ↔ l ≤ comap f (𝓝 x)
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s✝ s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<VAR>f : α → X<VAR>l : Filter α<VAR>s : Set α<VAR>h : 𝓟 sᶜ ≤ comap f (𝓝 x)<VAR>h' : l ⊓ 𝓟 s ≤ comap f (𝓝 x)<GOAL>l ≤ comap f (𝓝 x)
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s✝ s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<VAR>f : α → X<VAR>l : Filter α<VAR>s : Set α<VAR>h : 𝓟 sᶜ ≤ comap f (𝓝 x)<VAR>h' : l ⊓ 𝓟 s ≤ comap f (𝓝 x)<VAR>this : l ⊓ 𝓟 s ⊔ 𝓟 sᶜ ≤ comap f (𝓝 x)<GOAL>l ≤ comap f (𝓝 x)
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s✝ s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<VAR>f : α → X<VAR>l : Filter α<VAR>s : Set α<VAR>h : 𝓟 sᶜ ≤ comap f (𝓝 x)<VAR>h' : l ⊓ 𝓟 s ≤ comap f (𝓝 x)<VAR>this : l ≤ comap f (𝓝 x) ∧ 𝓟 sᶜ ≤ comap f (𝓝 x)<GOAL>l ≤ comap f (𝓝 x)
<VAR>P : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Membership P L<VAR>inst✝² : ProjectivePlane P L<VAR>inst✝¹ : Finite P<VAR>inst✝ : Finite L<VAR>l m : L<GOAL>pointCount P l = pointCount P m
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>S : Set (ℙ K V)<VAR>W : Subspace K V<GOAL>span S ⊔ W = span (S ∪ ↑W)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>inst✝² : NonAssocSemiring R<VAR>M : Submonoid R<VAR>inst✝¹ : NonAssocSemiring S<VAR>inst✝ : NonAssocSemiring T<VAR>s : Set R<VAR>x : R<GOAL>x ∈ closure ↑(AddSubmonoid.closure s) ↔ x ∈ closure s
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>inst✝² : NonAssocSemiring R<VAR>M : Submonoid R<VAR>inst✝¹ : NonAssocSemiring S<VAR>inst✝ : NonAssocSemiring T<VAR>s : Set R<VAR>x : R<VAR>hx : x ∈ closure ↑(AddSubmonoid.closure s)<GOAL>x ∈ closure s
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>inst✝² : NonAssocSemiring R<VAR>M : Submonoid R<VAR>inst✝¹ : NonAssocSemiring S<VAR>inst✝ : NonAssocSemiring T<VAR>s : Set R<VAR>x : R<VAR>hx : x ∈ closure ↑(AddSubmonoid.closure s)<VAR>H : Subsemiring R<VAR>J : H ∈ {S | s ⊆ ↑S}<GOAL>x ∈ (fun h => ↑H) J
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>inst✝² : NonAssocSemiring R<VAR>M : Submonoid R<VAR>inst✝¹ : NonAssocSemiring S<VAR>inst✝ : NonAssocSemiring T<VAR>s : Set R<VAR>x : R<VAR>hx : x ∈ closure ↑(AddSubmonoid.closure s)<VAR>H : Subsemiring R<VAR>J : H ∈ {S | s ⊆ ↑S}<VAR>y : R<VAR>hy : y ∈ ↑(Submonoid.closure ↑(AddSubmonoid.closure s))<GOAL>y ∈ ↑H.toAddSubmonoid
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>inst✝² : NonAssocSemiring R<VAR>M : Submonoid R<VAR>inst✝¹ : NonAssocSemiring S<VAR>inst✝ : NonAssocSemiring T<VAR>s : Set R<VAR>x : R<VAR>hx : x ∈ closure ↑(AddSubmonoid.closure s)<VAR>H : Subsemiring R<VAR>J : H ∈ {S | s ⊆ ↑S}<VAR>y : R<VAR>hy : y ∈ ↑(Submonoid.closure ↑(AddSubmonoid.closure s))<VAR>z : R<VAR>hz : z ∈ ↑(AddSubmonoid.closure s)<GOAL>z ∈ ↑H.toSubmonoid
<VAR>a b c d m n✝ : ℤ<VAR>n : ℕ<GOAL>0 + ↑n = ofNat n
<VAR>a b c d m n✝ : ℤ<VAR>n : ℕ<GOAL>↑n = ofNat n
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>s : Set P<VAR>t t₀ : Triangle ℝ P<VAR>ht : Set.range t.points ⊆ insert t₀.orthocenter (Set.range t₀.points)<VAR>ht₀o : t₀.orthocenter ∉ Set.range t₀.points<VAR>ht₀s : s = insert t₀.orthocenter (Set.range t₀.points)<GOAL>s = insert t.orthocenter (Set.range t.points)
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>s : Set P<VAR>t t₀ : Triangle ℝ P<VAR>ht : Set.range t.points ⊆ insert t₀.orthocenter (Set.range t₀.points)<VAR>ht₀o : t₀.orthocenter ∉ Set.range t₀.points<VAR>ht₀s : s = insert t₀.orthocenter (Set.range t₀.points)<VAR>i₁ i₂ i₃ j₂ j₃ : Fin 3<VAR>h₁₂ : i₁ ≠ i₂<VAR>h₁₃ : i₁ ≠ i₃<VAR>h₂₃ : i₂ ≠ i₃<VAR>h₁₂₃ : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃<VAR>h₁ : t.points i₁ = t₀.orthocenter<VAR>hj₂₃ : j₂ ≠ j₃<VAR>h₂ : t₀.points j₂ = t.points i₂<VAR>h₃ : t₀.points j₃ = t.points i₃<GOAL>s = insert t.orthocenter (Set.range t.points)
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>s : Set P<VAR>t t₀ : Triangle ℝ P<VAR>ht : Set.range t.points ⊆ insert t₀.orthocenter (Set.range t₀.points)<VAR>ht₀o : t₀.orthocenter ∉ Set.range t₀.points<VAR>ht₀s : s = insert t₀.orthocenter (Set.range t₀.points)<VAR>hs : Set.range t.points = Set.range t₀.points<GOAL>s = insert t.orthocenter (Set.range t.points)
<VAR>α : Type u_1<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : PredOrder α<VAR>a b : α<VAR>C : α → Sort u_2<VAR>inst✝ : WellFoundedGT α<VAR>H_pred : (a : α) → ¬IsMin a → C a → C (pred a)<VAR>H_lim : (a : α) → IsPredLimit a → ((b : α) → b > a → C b) → C a<VAR>ha : IsPredLimit a<GOAL>PredOrder.limitRecOn a H_pred H_lim = H_lim a ha fun x x_1 => PredOrder.limitRecOn x H_pred H_lim
<VAR>α : Type u_1<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : PredOrder α<VAR>a b : α<VAR>C : α → Sort u_2<VAR>inst✝ : WellFoundedGT α<VAR>H_pred : (a : α) → ¬IsMin a → C a → C (pred a)<VAR>H_lim : (a : α) → IsPredLimit a → ((b : α) → b > a → C b) → C a<VAR>ha : IsPredLimit a<GOAL>(H_lim a ha fun y x => ⋯.fix (fun a IH => if h : IsPredLimit a then H_lim a h IH else let x := Classical.indefiniteDescription (fun x => ¬IsMin x ∧ pred x = a) ⋯; ⋯ ▸ H_pred ↑x ⋯ (IH ↑x ⋯)) y) = H_lim a ha fun x x_1 => PredOrder.limitRecOn x H_pred H_lim
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>x y : α<VAR>s t : Set α<VAR>Φ : α → β<VAR>hy : y ∈ s<GOAL>edist x y ≤ infEdist x s + diam s
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>x y : α<VAR>s t : Set α<VAR>Φ : α → β<VAR>hy : y ∈ s<GOAL>edist x y ≤ ⨅ i ∈ s, edist x i + diam s
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>x y : α<VAR>s t : Set α<VAR>Φ : α → β<VAR>hy : y ∈ s<VAR>i : α<VAR>hi : i ∈ s<GOAL>edist x y ≤ edist x i + diam s
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>F✝ : Type u_4<VAR>G : Type u_5<VAR>inst✝⁶ : PseudoEMetricSpace α✝<VAR>inst✝⁵ : PseudoEMetricSpace β✝<VAR>inst✝⁴ : FunLike F✝ α✝ β✝<VAR>α : Type u_6<VAR>β : Type u_7<VAR>F : Type u_8<VAR>inst✝³ : PseudoMetricSpace α<VAR>inst✝² : PseudoMetricSpace β<VAR>inst✝¹ : FunLike F α β<VAR>inst✝ : DilationClass F α β<VAR>f : F<VAR>x y : α<GOAL>nndist (f x) (f y) = ratio f * nndist x y
<VAR>n : Nat<GOAL>(list n).reverse = List.map rev (list n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<GOAL>StrictMono ⇑toMultiset
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace Y<VAR>inst✝³ : TopologicalSpace Z<VAR>inst✝² : TopologicalSpace W<VAR>inst✝¹ : TopologicalSpace ε<VAR>inst✝ : TopologicalSpace ζ<VAR>f : X → Y → Z<VAR>x : X<VAR>y : Y<VAR>s : Set X<VAR>t : Set Y<VAR>u : Set Z<VAR>hf : Continuous (uncurry f)<VAR>hx : x ∈ closure s<VAR>hy : y ∈ closure t<VAR>h : ∀ a ∈ s, ∀ b ∈ t, f a b ∈ u<GOAL>(x, y) ∈ closure (s ×ˢ t)
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>s : Finset α<VAR>P : Finpartition s<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<GOAL>0 ≤ P.energy G
<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>G✝ : Type u_1<VAR>inst✝³ : NormedAddCommGroup G✝<VAR>inst✝² : NormedSpace 𝕜 G✝<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>G : Type u_2<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>c : 𝕜 → F →L[𝕜] G<VAR>c' : F →L[𝕜] G<VAR>d : 𝕜 → E →L[𝕜] F<VAR>d' : E →L[𝕜] F<VAR>u : 𝕜 → F<VAR>u' : F<VAR>hc : HasDerivAt c c' x<VAR>hd : HasDerivAt d d' x<GOAL>HasDerivAt (fun y => (c y).comp (d y)) (c'.comp (d x) + (c x).comp d') x
<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>G✝ : Type u_1<VAR>inst✝³ : NormedAddCommGroup G✝<VAR>inst✝² : NormedSpace 𝕜 G✝<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>G : Type u_2<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>c : 𝕜 → F →L[𝕜] G<VAR>c' : F →L[𝕜] G<VAR>d : 𝕜 → E →L[𝕜] F<VAR>d' : E →L[𝕜] F<VAR>u : 𝕜 → F<VAR>u' : F<VAR>hc : HasDerivWithinAt c c' univ x<VAR>hd : HasDerivWithinAt d d' univ x<GOAL>HasDerivWithinAt (fun y => (c y).comp (d y)) (c'.comp (d x) + (c x).comp d') univ x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>f : β → γ<VAR>g : γ → α<VAR>η : Kernel β γ<VAR>κ : Kernel α β<VAR>a : α<VAR>s : Set γ<VAR>hs : MeasurableSet s<GOAL>((η ∘ₖ κ) a) s = ∫⁻ (b : β), (η b) s ∂κ a
<VAR>ds₁ ds₂ ds₃ is : List ℕ<VAR>h : Forall₂ (fun x x_1 => x < x_1) is (ds₁ ++ ds₂ ++ ds₃)<GOAL>↑(assocRight ⟨is, h⟩).drop.drop = ↑(drop ⟨is, h⟩)
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : Affine R<VAR>x y : R<GOAL>evalEval x y (C (C W.a₁) * Y - C (C 3 * X ^ 2 + C (2 * W.a₂) * X + C W.a₄)) = W.a₁ * y - (3 * x ^ 2 + 2 * W.a₂ * x + W.a₄)
<VAR>α : Type u_1<VAR>inst✝¹⁰ : MetricSpace α<VAR>β : Type u<VAR>inst✝⁹ : SecondCountableTopology α<VAR>inst✝⁸ : MeasurableSpace α<VAR>inst✝⁷ : OpensMeasurableSpace α<VAR>inst✝⁶ : HasBesicovitchCovering α<VAR>inst✝⁵ : MetricSpace β<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : BorelSpace β<VAR>inst✝² : SecondCountableTopology β<VAR>inst✝¹ : HasBesicovitchCovering β<VAR>μ : Measure β<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>s : Set β<GOAL>∀ᵐ (x : β) ∂μ.restrict s, Tendsto (fun r => μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 1)
<VAR>α : Type u_1<VAR>inst✝ : OrderedAddCommGroup α<VAR>a b c : α<GOAL>(fun x => a - x) ⁻¹' Ioo b c = Ioo (a - c) (a - b)
<VAR>C : Type u₁<VAR>inst✝¹³ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹² : Category.{v₂, u₂} D<VAR>W : MorphismProperty C<VAR>M : Type w'<VAR>inst✝¹¹ : AddMonoid M<VAR>inst✝¹⁰ : HasShift C M<VAR>inst✝⁹ : HasShift D M<VAR>inst✝⁸ : W.IsCompatibleWithShift M<VAR>X Y Z T : C<VAR>a₁ a₂ a₃ a₁₂ a₂₃ a : M<VAR>inst✝⁷ : HasSmallLocalizedShiftedHom W M X Y<VAR>inst✝⁶ : HasSmallLocalizedShiftedHom W M X Z<VAR>inst✝⁵ : HasSmallLocalizedShiftedHom W M X T<VAR>inst✝⁴ : HasSmallLocalizedShiftedHom W M Y Z<VAR>inst✝³ : HasSmallLocalizedShiftedHom W M Y T<VAR>inst✝² : HasSmallLocalizedShiftedHom W M Z T<VAR>inst✝¹ : HasSmallLocalizedShiftedHom W M Z Z<VAR>inst✝ : HasSmallLocalizedShiftedHom W M T T<VAR>α : SmallShiftedHom W X Y a₁<VAR>β : SmallShiftedHom W Y Z a₂<VAR>γ : SmallShiftedHom W Z T a₃<VAR>h₁₂ : a₂ + a₁ = a₁₂<VAR>h₂₃ : a₃ + a₂ = a₂₃<VAR>h : a₃ + a₂ + a₁ = a<GOAL>a₃ + a₁₂ = a
<VAR>C : Type u₁<VAR>inst✝¹³ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹² : Category.{v₂, u₂} D<VAR>W : MorphismProperty C<VAR>M : Type w'<VAR>inst✝¹¹ : AddMonoid M<VAR>inst✝¹⁰ : HasShift C M<VAR>inst✝⁹ : HasShift D M<VAR>inst✝⁸ : W.IsCompatibleWithShift M<VAR>X Y Z T : C<VAR>a₁ a₂ a₃ a₁₂ a₂₃ a : M<VAR>inst✝⁷ : HasSmallLocalizedShiftedHom W M X Y<VAR>inst✝⁶ : HasSmallLocalizedShiftedHom W M X Z<VAR>inst✝⁵ : HasSmallLocalizedShiftedHom W M X T<VAR>inst✝⁴ : HasSmallLocalizedShiftedHom W M Y Z<VAR>inst✝³ : HasSmallLocalizedShiftedHom W M Y T<VAR>inst✝² : HasSmallLocalizedShiftedHom W M Z T<VAR>inst✝¹ : HasSmallLocalizedShiftedHom W M Z Z<VAR>inst✝ : HasSmallLocalizedShiftedHom W M T T<VAR>α : SmallShiftedHom W X Y a₁<VAR>β : SmallShiftedHom W Y Z a₂<VAR>γ : SmallShiftedHom W Z T a₃<VAR>h₁₂ : a₂ + a₁ = a₁₂<VAR>h₂₃ : a₃ + a₂ = a₂₃<VAR>h : a₃ + a₂ + a₁ = a<GOAL>(α.comp β h₁₂).comp γ ⋯ = α.comp (β.comp γ h₂₃) ⋯
<VAR>C : Type u₁<VAR>inst✝¹³ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹² : Category.{v₂, u₂} D<VAR>W : MorphismProperty C<VAR>M : Type w'<VAR>inst✝¹¹ : AddMonoid M<VAR>inst✝¹⁰ : HasShift C M<VAR>inst✝⁹ : HasShift D M<VAR>inst✝⁸ : W.IsCompatibleWithShift M<VAR>X Y Z T : C<VAR>a₁ a₂ a₃ a₁₂ a₂₃ a : M<VAR>inst✝⁷ : HasSmallLocalizedShiftedHom W M X Y<VAR>inst✝⁶ : HasSmallLocalizedShiftedHom W M X Z<VAR>inst✝⁵ : HasSmallLocalizedShiftedHom W M X T<VAR>inst✝⁴ : HasSmallLocalizedShiftedHom W M Y Z<VAR>inst✝³ : HasSmallLocalizedShiftedHom W M Y T<VAR>inst✝² : HasSmallLocalizedShiftedHom W M Z T<VAR>inst✝¹ : HasSmallLocalizedShiftedHom W M Z Z<VAR>inst✝ : HasSmallLocalizedShiftedHom W M T T<VAR>α : SmallShiftedHom W X Y a₁<VAR>β : SmallShiftedHom W Y Z a₂<VAR>γ : SmallShiftedHom W Z T a₃<VAR>h₁₂ : a₂ + a₁ = a₁₂<VAR>h₂₃ : a₃ + a₂ = a₂₃<VAR>h : a₃ + a₂ + a₁ = a<GOAL>(equiv W W.Q) ((α.comp β h₁₂).comp γ ⋯) = (equiv W W.Q) (α.comp (β.comp γ h₂₃) ⋯)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : (i : ι) → TopologicalSpace (π i)<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : TopologicalSpace δ<VAR>f : α → β<VAR>g : β → γ<VAR>h : QuotientMap f<VAR>s : Set β<VAR>hs : IsOpen s<GOAL>ContinuousOn g s ↔ ContinuousOn (g ∘ f) (f ⁻¹' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : (i : ι) → TopologicalSpace (π i)<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : TopologicalSpace δ<VAR>f : α → β<VAR>g : β → γ<VAR>h : QuotientMap f<VAR>s : Set β<VAR>hs : IsOpen s<GOAL>Continuous (s.restrict g ∘ s.restrictPreimage f) ↔ Continuous ((f ⁻¹' s).restrict (g ∘ f))
<VAR>𝒮 : Type u₁<VAR>𝒳 : Type u₂<VAR>inst✝³ : Category.{v₁, u₂} 𝒳<VAR>inst✝² : Category.{v₂, u₁} 𝒮<VAR>p : 𝒳 ⥤ 𝒮<VAR>R S : 𝒮<VAR>a b c : 𝒳<VAR>f : R ⟶ S<VAR>φ : a ⟶ b<VAR>inst✝¹ : p.IsHomLift f φ<VAR>T : 𝒮<VAR>ψ : b ⟶ c<VAR>inst✝ : p.IsHomLift (𝟙 T) ψ<GOAL>p.IsHomLift f (φ ≫ ψ)
<VAR>𝒮 : Type u₁<VAR>𝒳 : Type u₂<VAR>inst✝³ : Category.{v₁, u₂} 𝒳<VAR>inst✝² : Category.{v₂, u₁} 𝒮<VAR>p : 𝒳 ⥤ 𝒮<VAR>R S : 𝒮<VAR>a b c : 𝒳<VAR>f : R ⟶ S<VAR>φ : a ⟶ b<VAR>inst✝¹ : p.IsHomLift f φ<VAR>ψ : b ⟶ c<VAR>inst✝ : p.IsHomLift (𝟙 S) ψ<GOAL>p.IsHomLift f (φ ≫ ψ)
<VAR>R✝ : Type u_1<VAR>inst✝¹ : Semiring R✝<VAR>φ✝ : R✝⟦X⟧<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>φ ψ : R⟦X⟧<VAR>n : ℕ<VAR>h : ↑n < ψ.order<GOAL>(coeff R n) (φ * (1 - ψ)) = (coeff R n) φ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s✝ s : Finset α<GOAL>↑s = ∅ ↔ s = ∅
<VAR>K : Type u_1<VAR>σ : Type u_2<VAR>ι : Type u_3<VAR>inst✝³ : Fintype K<VAR>inst✝² : Field K<VAR>inst✝¹ : Fintype σ<VAR>inst✝ : DecidableEq σ<VAR>f : MvPolynomial σ K<VAR>h : f.totalDegree < (q - 1) * Fintype.card σ<VAR>this : DecidableEq K<GOAL>∑ x : σ → K, (eval x) f = 0
<VAR>K : Type u_1<VAR>σ : Type u_2<VAR>ι : Type u_3<VAR>inst✝³ : Fintype K<VAR>inst✝² : Field K<VAR>inst✝¹ : Fintype σ<VAR>inst✝ : DecidableEq σ<VAR>f : MvPolynomial σ K<VAR>h : f.totalDegree < (q - 1) * Fintype.card σ<VAR>this : DecidableEq K<GOAL>∀ x ∈ f.support, ∑ x_1 : σ → K, coeff x f * ∏ i : σ, x_1 i ^ x i = 0
<VAR>K : Type u_1<VAR>σ : Type u_2<VAR>ι : Type u_3<VAR>inst✝³ : Fintype K<VAR>inst✝² : Field K<VAR>inst✝¹ : Fintype σ<VAR>inst✝ : DecidableEq σ<VAR>f : MvPolynomial σ K<VAR>h : f.totalDegree < (q - 1) * Fintype.card σ<VAR>this : DecidableEq K<VAR>d : σ →₀ ℕ<VAR>hd : d ∈ f.support<GOAL>∑ x : σ → K, coeff d f * ∏ i : σ, x i ^ d i = 0
<VAR>K : Type u_1<VAR>σ : Type u_2<VAR>ι : Type u_3<VAR>inst✝³ : Fintype K<VAR>inst✝² : Field K<VAR>inst✝¹ : Fintype σ<VAR>inst✝ : DecidableEq σ<VAR>f : MvPolynomial σ K<VAR>h : f.totalDegree < (q - 1) * Fintype.card σ<VAR>this : DecidableEq K<VAR>d : σ →₀ ℕ<VAR>hd : d ∈ f.support<VAR>i : σ<VAR>hi : d i < q - 1<GOAL>∑ x : σ → K, coeff d f * ∏ i : σ, x i ^ d i = 0
<VAR>K : Type u_1<VAR>σ : Type u_2<VAR>ι : Type u_3<VAR>inst✝³ : Fintype K<VAR>inst✝² : Field K<VAR>inst✝¹ : Fintype σ<VAR>inst✝ : DecidableEq σ<VAR>f : MvPolynomial σ K<VAR>h : f.totalDegree < (q - 1) * Fintype.card σ<VAR>this : DecidableEq K<VAR>d : σ →₀ ℕ<VAR>hd : d ∈ f.support<VAR>i : σ<VAR>hi : d i < q - 1<GOAL>∑ x : σ → K, ∏ i : σ, x i ^ d i = 0
<VAR>K : Type u_1<VAR>σ : Type u_2<VAR>ι : Type u_3<VAR>inst✝³ : Fintype K<VAR>inst✝² : Field K<VAR>inst✝¹ : Fintype σ<VAR>inst✝ : DecidableEq σ<VAR>f : MvPolynomial σ K<VAR>h : f.totalDegree < (q - 1) * Fintype.card σ<VAR>this : DecidableEq K<VAR>d : σ →₀ ℕ<VAR>hd : d ∈ f.support<VAR>i : σ<VAR>hi : d i < q - 1<GOAL>∀ (a : { j // j ≠ i } → K), ∑ x : { x // x ∘ Subtype.val = a }, ∏ j : σ, ↑x j ^ d j = 0
<VAR>K : Type u_1<VAR>σ : Type u_2<VAR>ι : Type u_3<VAR>inst✝³ : Fintype K<VAR>inst✝² : Field K<VAR>inst✝¹ : Fintype σ<VAR>inst✝ : DecidableEq σ<VAR>f : MvPolynomial σ K<VAR>h : f.totalDegree < (q - 1) * Fintype.card σ<VAR>this : DecidableEq K<VAR>d : σ →₀ ℕ<VAR>hd : d ∈ f.support<VAR>i : σ<VAR>hi : d i < q - 1<VAR>x₀ : { j // j ≠ i } → K<VAR>e : K ≃ { x // x ∘ Subtype.val = x₀ } := (Equiv.subtypeEquivCodomain x₀).symm<GOAL>∑ x : { x // x ∘ Subtype.val = x₀ }, ∏ j : σ, ↑x j ^ d j = 0