ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>F : Type u_1<VAR>α✝ : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝⁴ : LinearOrder α✝<VAR>inst✝³ : OrderBot α✝<VAR>s✝ : Finset ι<VAR>f✝ : ι → α✝<VAR>a : α✝<VAR>α : Type u_7<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : BoundedOrder α<VAR>inst✝ : Nontrivial α<VAR>s : Finset ι<VAR>f : ι → α<GOAL>⊤ ≤ s.sup f ↔ ∃ b ∈ s, ⊤ ≤ f b
<VAR>G : Type u<VAR>M✝ : Type v<VAR>α✝ : Type w<VAR>s : Set α✝<VAR>M : Type uM<VAR>N : Type uN<VAR>α : Type uα<VAR>β : Type uβ<VAR>inst✝⁷ : MeasurableSpace M<VAR>inst✝⁶ : MeasurableSpace N<VAR>inst✝⁵ : MeasurableSpace α<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : SMul M α<VAR>inst✝² : SMul M β<VAR>inst✝¹ : MeasurableSMul M β<VAR>μ : Measure α<VAR>inst✝ : SMulInvariantMeasure M α μ<VAR>f : α → β<VAR>hsmul : ∀ (m : M) (a : α), f (m • a) = m • f a<VAR>hf : Measurable f<VAR>m : M<VAR>S : Set β<VAR>hS : MeasurableSet S<GOAL>μ (f ⁻¹' ((fun x => m • x) ⁻¹' S)) = μ ((fun x => m • f x) ⁻¹' S)
<VAR>G : Type u<VAR>M✝ : Type v<VAR>α✝ : Type w<VAR>s : Set α✝<VAR>M : Type uM<VAR>N : Type uN<VAR>α : Type uα<VAR>β : Type uβ<VAR>inst✝⁷ : MeasurableSpace M<VAR>inst✝⁶ : MeasurableSpace N<VAR>inst✝⁵ : MeasurableSpace α<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : SMul M α<VAR>inst✝² : SMul M β<VAR>inst✝¹ : MeasurableSMul M β<VAR>μ : Measure α<VAR>inst✝ : SMulInvariantMeasure M α μ<VAR>f : α → β<VAR>hsmul : ∀ (m : M) (a : α), f (m • a) = m • f a<VAR>hf : Measurable f<VAR>m : M<VAR>S : Set β<VAR>hS : MeasurableSet S<GOAL>μ ((fun x => f (m • x)) ⁻¹' S) = μ ((fun x => m • x) ⁻¹' (f ⁻¹' S))
<VAR>G : Type u<VAR>M✝ : Type v<VAR>α✝ : Type w<VAR>s : Set α✝<VAR>M : Type uM<VAR>N : Type uN<VAR>α : Type uα<VAR>β : Type uβ<VAR>inst✝⁷ : MeasurableSpace M<VAR>inst✝⁶ : MeasurableSpace N<VAR>inst✝⁵ : MeasurableSpace α<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : SMul M α<VAR>inst✝² : SMul M β<VAR>inst✝¹ : MeasurableSMul M β<VAR>μ : Measure α<VAR>inst✝ : SMulInvariantMeasure M α μ<VAR>f : α → β<VAR>hsmul : ∀ (m : M) (a : α), f (m • a) = m • f a<VAR>hf : Measurable f<VAR>m : M<VAR>S : Set β<VAR>hS : MeasurableSet S<GOAL>μ ((fun x => m • x) ⁻¹' (f ⁻¹' S)) = μ (f ⁻¹' S)
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>x✝ y✝ : α<VAR>s t u : Set α<VAR>Φ : α → β<VAR>x : α<VAR>xs : x ∈ s<VAR>y : α<VAR>yt : y ∈ t<GOAL>hausdorffEdist s t ≤ diam (s ∪ t)
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>x✝ y✝ : α<VAR>s t u : Set α<VAR>Φ : α → β<VAR>x : α<VAR>xs : x ∈ s<VAR>y : α<VAR>yt : y ∈ t<GOAL>∀ x ∈ s, ∃ y ∈ t, edist x y ≤ diam (s ∪ t)
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>x✝ y✝ : α<VAR>s t u : Set α<VAR>Φ : α → β<VAR>x : α<VAR>xs : x ∈ s<VAR>y : α<VAR>yt : y ∈ t<GOAL>∀ x ∈ t, ∃ y ∈ s, edist x y ≤ diam (s ∪ t)
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝² : Category.{v', u'} D<VAR>inst✝¹ : HasZeroMorphisms C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>inst✝ : Epi f<VAR>h : f ≫ g = 0<GOAL>g = 0
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝² : Category.{v', u'} D<VAR>inst✝¹ : HasZeroMorphisms C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>inst✝ : Epi f<VAR>h✝ : f ≫ g = 0<VAR>h : g = 0<GOAL>g = 0
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<GOAL>(o.oangle x (y - x)).sign = (o.oangle x y).sign
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f fa : α → α<VAR>fb : β → β<VAR>x y : α<VAR>m n : ℕ<VAR>hn : 0 < n<VAR>hx : IsPeriodicPt f n x<GOAL>minimalPeriod f x ≤ n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f fa : α → α<VAR>fb : β → β<VAR>x y : α<VAR>m n : ℕ<VAR>hn : 0 < n<VAR>hx : IsPeriodicPt f n x<GOAL>Nat.find ⋯ ≤ n
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>x y : PrimeSpectrum R<GOAL>x ≤ y ↔ y ∈ closure {x}
<VAR>s : Set Ordinal.{u}<VAR>a✝ : Ordinal.{u}<VAR>a : Ordinal.{u_1}<GOAL>𝓝[<] a = 𝓝[≠] a
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>L' : Type u_3<VAR>inst✝⁸ : Field K<VAR>inst✝⁷ : Field L<VAR>inst✝⁶ : Field L'<VAR>inst✝⁵ : Algebra K L<VAR>inst✝⁴ : Algebra K L'<VAR>S : IntermediateField K L<VAR>R : Type u_4<VAR>inst✝³ : CommRing R<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : Algebra R L<VAR>inst✝ : IsScalarTower R K L<VAR>x : ↥S<VAR>P : R[X]<GOAL>(aeval ↑x) P = ↑((aeval x) P)
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>L' : Type u_3<VAR>inst✝⁸ : Field K<VAR>inst✝⁷ : Field L<VAR>inst✝⁶ : Field L'<VAR>inst✝⁵ : Algebra K L<VAR>inst✝⁴ : Algebra K L'<VAR>S : IntermediateField K L<VAR>R : Type u_4<VAR>inst✝³ : CommRing R<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : Algebra R L<VAR>inst✝ : IsScalarTower R K L<VAR>x : ↥S<VAR>P f g : R[X]<VAR>hf : (aeval ↑x) f = ↑((aeval x) f)<VAR>hg : (aeval ↑x) g = ↑((aeval x) g)<GOAL>(aeval ↑x) (f + g) = ↑((aeval x) (f + g))
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>L' : Type u_3<VAR>inst✝⁸ : Field K<VAR>inst✝⁷ : Field L<VAR>inst✝⁶ : Field L'<VAR>inst✝⁵ : Algebra K L<VAR>inst✝⁴ : Algebra K L'<VAR>S : IntermediateField K L<VAR>R : Type u_4<VAR>inst✝³ : CommRing R<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : Algebra R L<VAR>inst✝ : IsScalarTower R K L<VAR>x : ↥S<VAR>P : R[X]<VAR>n : ℕ<VAR>r : R<GOAL>(aeval ↑x) ((monomial n) r) = ↑((aeval x) ((monomial n) r))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p q : α → Prop<VAR>inst✝² : DecidablePred p<VAR>inst✝¹ : DecidablePred q<VAR>s t : Finset α<VAR>inst✝ : DecidableEq α<VAR>s₁ s₂ : Finset α<VAR>x✝ : α<GOAL>x✝ ∈ filter p (s₁ ∪ s₂) ↔ x✝ ∈ filter p s₁ ∪ filter p s₂
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : LinearOrderedField R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>s : AffineSubspace R P<VAR>x p : P<VAR>hx : x ∉ s<VAR>hp : p ∈ s<VAR>y : P<GOAL>y ∈ {y | s.WSameSide x y} ↔ y ∈ Set.image2 (fun t q => t • (x -ᵥ p) +ᵥ q) (Set.Ici 0) ↑s
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : LinearOrderedField R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>s : AffineSubspace R P<VAR>x p : P<VAR>hx : x ∉ s<VAR>hp : p ∈ s<VAR>y : P<GOAL>s.WSameSide x y ↔ ∃ a, 0 ≤ a ∧ ∃ b ∈ ↑s, a • (x -ᵥ p) +ᵥ b = y
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>D : Type u_1<VAR>inst✝⁴ : Category.{u_2, u_1} D<VAR>inst✝³ : Abelian C<VAR>inst✝² : HasProjectiveResolutions C<VAR>inst✝¹ : Abelian D<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>P : ProjectiveResolution X<VAR>Q : ProjectiveResolution Y<VAR>φ : P.complex ⟶ Q.complex<VAR>comm : φ.f 0 ≫ Q.π.f 0 = P.π.f 0 ≫ f<VAR>F : C ⥤ D<VAR>inst✝ : F.Additive<GOAL>HomologicalComplex.opcyclesMap ((F.mapHomologicalComplex (ComplexShape.down ℕ)).map φ) 0 ≫ Q.fromLeftDerivedZero' F = P.fromLeftDerivedZero' F ≫ F.map f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>l₂ : List α<VAR>a : α<VAR>l₁ : List α<VAR>IH : (l₁ ++ l₂).dedup = l₁ ∪ l₂.dedup<GOAL>(a :: l₁ ++ l₂).dedup = a :: l₁ ∪ l₂.dedup
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>l₂ : List α<VAR>a : α<VAR>l₁ : List α<VAR>IH : (l₁ ++ l₂).dedup = l₁ ∪ l₂.dedup<GOAL>(a :: l₁ ++ l₂).dedup = List.insert a (l₁ ∪ l₂.dedup)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>l₂ : List α<VAR>a : α<VAR>l₁ : List α<VAR>IH : (l₁ ++ l₂).dedup = l₁ ∪ l₂.dedup<GOAL>(a :: (l₁ ++ l₂)).dedup = List.insert a (l₁ ++ l₂).dedup
<VAR>ι α β : Type u<VAR>c : Cardinal.{u}<VAR>hreg : c.IsRegular<VAR>l : Filter α<VAR>x : α<GOAL>∀ᶠ (a : α) in cocardinal α hreg, a ≠ x
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : CancelCommMonoid β<VAR>A : Set α<VAR>B : Set β<VAR>f : α → β<VAR>m n : ℕ<VAR>hmn : m ≤ n<VAR>hf : IsMulFreimanHom n A B f<VAR>s t : Multiset α<VAR>hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A<VAR>htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A<VAR>hs : card s = m<VAR>ht : card t = m<VAR>h : s.prod = t.prod<GOAL>(map f s).prod = (map f t).prod
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : CancelCommMonoid β<VAR>A : Set α<VAR>B : Set β<VAR>f : α → β<VAR>n : ℕ<VAR>hf : IsMulFreimanHom n A B f<VAR>s t : Multiset α<VAR>hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A<VAR>htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A<VAR>h : s.prod = t.prod<VAR>hmn : 0 ≤ n<VAR>hs : card s = 0<VAR>ht : card t = 0<GOAL>(map f s).prod = (map f t).prod
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : CancelCommMonoid β<VAR>A : Set α<VAR>B : Set β<VAR>f : α → β<VAR>m n : ℕ<VAR>hmn : m ≤ n<VAR>hf : IsMulFreimanHom n A B f<VAR>s t : Multiset α<VAR>hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A<VAR>htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A<VAR>hs : card s = m<VAR>ht : card t = m<VAR>h : s.prod = t.prod<VAR>hm : m > 0<GOAL>(map f s).prod = (map f t).prod
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : CancelCommMonoid β<VAR>A : Set α<VAR>B : Set β<VAR>f : α → β<VAR>m n : ℕ<VAR>hmn : m ≤ n<VAR>hf : IsMulFreimanHom n A B f<VAR>s t : Multiset α<VAR>hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A<VAR>htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A<VAR>hs : card s = m<VAR>ht : card t = m<VAR>h : s.prod = t.prod<VAR>hm : ∃ a, a ∈ s<GOAL>(map f s).prod = (map f t).prod
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : CancelCommMonoid β<VAR>A : Set α<VAR>B : Set β<VAR>f : α → β<VAR>m n : ℕ<VAR>hmn : m ≤ n<VAR>hf : IsMulFreimanHom n A B f<VAR>s t : Multiset α<VAR>hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A<VAR>htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A<VAR>hs : card s = m<VAR>ht : card t = m<VAR>h : s.prod = t.prod<VAR>a : α<VAR>ha : a ∈ s<GOAL>(map f s).prod = (map f t).prod
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : CancelCommMonoid β<VAR>A : Set α<VAR>B : Set β<VAR>f : α → β<VAR>m n : ℕ<VAR>hmn : m ≤ n<VAR>hf : IsMulFreimanHom n A B f<VAR>s t : Multiset α<VAR>hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A<VAR>htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A<VAR>hs : card s = m<VAR>ht : card t = m<VAR>h : s.prod = t.prod<VAR>a : α<VAR>ha : a ∈ s<GOAL>(map f (s + replicate (n - m) a)).prod = (map f (t + replicate (n - m) a)).prod
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : CancelCommMonoid β<VAR>A : Set α<VAR>B : Set β<VAR>f : α → β<VAR>m n : ℕ<VAR>hmn : m ≤ n<VAR>hf : IsMulFreimanHom n A B f<VAR>s t : Multiset α<VAR>hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A<VAR>htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A<VAR>hs : card s = m<VAR>ht : card t = m<VAR>h : s.prod = t.prod<VAR>a : α<VAR>ha : a ∈ A<GOAL>(map f (s + replicate (n - m) a)).prod = (map f (t + replicate (n - m) a)).prod
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : CancelCommMonoid β<VAR>A : Set α<VAR>B : Set β<VAR>f : α → β<VAR>m n : ℕ<VAR>hmn : m ≤ n<VAR>hf : IsMulFreimanHom n A B f<VAR>s t : Multiset α<VAR>hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A<VAR>htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A<VAR>hs : card s = m<VAR>ht : card t = m<VAR>h : s.prod = t.prod<VAR>a✝ : α<VAR>ha✝ : a✝ ∈ A<VAR>a : α<VAR>ha : a ∈ s + replicate (n - m) a✝<GOAL>a ∈ A
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : CancelCommMonoid β<VAR>A : Set α<VAR>B : Set β<VAR>f : α → β<VAR>m n : ℕ<VAR>hmn : m ≤ n<VAR>hf : IsMulFreimanHom n A B f<VAR>s t : Multiset α<VAR>hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A<VAR>htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A<VAR>hs : card s = m<VAR>ht : card t = m<VAR>h : s.prod = t.prod<VAR>a✝ : α<VAR>ha✝ : a✝ ∈ A<VAR>a : α<VAR>ha : a ∈ t + replicate (n - m) a✝<GOAL>a ∈ A
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : CancelCommMonoid β<VAR>A : Set α<VAR>B : Set β<VAR>f : α → β<VAR>m n : ℕ<VAR>hmn : m ≤ n<VAR>hf : IsMulFreimanHom n A B f<VAR>s t : Multiset α<VAR>hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A<VAR>htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A<VAR>hs : card s = m<VAR>ht : card t = m<VAR>h : s.prod = t.prod<VAR>a : α<VAR>ha : a ∈ A<GOAL>card (s + replicate (n - m) a) = n
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : CancelCommMonoid β<VAR>A : Set α<VAR>B : Set β<VAR>f : α → β<VAR>m n : ℕ<VAR>hmn : m ≤ n<VAR>hf : IsMulFreimanHom n A B f<VAR>s t : Multiset α<VAR>hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A<VAR>htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A<VAR>hs : card s = m<VAR>ht : card t = m<VAR>h : s.prod = t.prod<VAR>a : α<VAR>ha : a ∈ A<GOAL>card (t + replicate (n - m) a) = n
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : CancelCommMonoid β<VAR>A : Set α<VAR>B : Set β<VAR>f : α → β<VAR>m n : ℕ<VAR>hmn : m ≤ n<VAR>hf : IsMulFreimanHom n A B f<VAR>s t : Multiset α<VAR>hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A<VAR>htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A<VAR>hs : card s = m<VAR>ht : card t = m<VAR>h : s.prod = t.prod<VAR>a : α<VAR>ha : a ∈ A<GOAL>(s + replicate (n - m) a).prod = (t + replicate (n - m) a).prod
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : CharZero K<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : IsKilling K L<VAR>inst✝² : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝¹ : H.IsCartanSubalgebra<VAR>inst✝ : IsTriangularizable K (↥H) L<VAR>α✝ β✝ : Weight K (↥H) L<VAR>hα : α✝.IsNonZero<VAR>α β : { α // α.IsNonZero }<GOAL>((rootSystem H).toLin ((rootSystem H).root α)) ((rootSystem H).coroot β) ∈ ↑(AddSubgroup.zmultiples 1)
<VAR>R M : Type u<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>I : Ideal R<VAR>F F' : I.Filtration M<VAR>inst✝² : IsNoetherianRing R<VAR>inst✝¹ : LocalRing R<VAR>inst✝ : Module.Finite R M<VAR>h : I ≠ ⊤<GOAL>⨅ i, I ^ i • ⊤ = ⊥
<VAR>R M : Type u<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>I : Ideal R<VAR>F F' : I.Filtration M<VAR>inst✝² : IsNoetherianRing R<VAR>inst✝¹ : LocalRing R<VAR>inst✝ : Module.Finite R M<VAR>h : I ≠ ⊤<GOAL>⨅ i, I ^ i • ⊤ ≤ ⊥
<VAR>R M : Type u<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>I : Ideal R<VAR>F F' : I.Filtration M<VAR>inst✝² : IsNoetherianRing R<VAR>inst✝¹ : LocalRing R<VAR>inst✝ : Module.Finite R M<VAR>h : I ≠ ⊤<VAR>x : M<VAR>hx : x ∈ ⨅ i, I ^ i • ⊤<GOAL>x ∈ ⊥
<VAR>R M : Type u<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>I : Ideal R<VAR>F F' : I.Filtration M<VAR>inst✝² : IsNoetherianRing R<VAR>inst✝¹ : LocalRing R<VAR>inst✝ : Module.Finite R M<VAR>h : I ≠ ⊤<VAR>x : M<VAR>hx : x ∈ ⨅ i, I ^ i • ⊤<VAR>r : ↥I<VAR>hr : ↑r • x = x<GOAL>x ∈ ⊥
<VAR>R M : Type u<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>I : Ideal R<VAR>F F' : I.Filtration M<VAR>inst✝² : IsNoetherianRing R<VAR>inst✝¹ : LocalRing R<VAR>inst✝ : Module.Finite R M<VAR>h : I ≠ ⊤<VAR>x : M<VAR>hx : x ∈ ⨅ i, I ^ i • ⊤<VAR>r : ↥I<VAR>hr : ↑r • x = x<VAR>this : IsUnit (1 - ↑r)<GOAL>x ∈ ⊥
<VAR>R M : Type u<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>I : Ideal R<VAR>F F' : I.Filtration M<VAR>inst✝² : IsNoetherianRing R<VAR>inst✝¹ : LocalRing R<VAR>inst✝ : Module.Finite R M<VAR>h : I ≠ ⊤<VAR>x : M<VAR>hx : x ∈ ⨅ i, I ^ i • ⊤<VAR>r : ↥I<VAR>hr : ↑r • x = x<VAR>this : IsUnit (1 - ↑r)<GOAL>(1 - ↑r) • x = (1 - ↑r) • 0
<VAR>M✝ : Type u_1<VAR>N✝ : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝⁵ : CommMonoid M✝<VAR>inst✝⁴ : CommMonoid N✝<VAR>inst✝³ : DivisionCommMonoid G<VAR>k l : ℕ<VAR>ζ✝ : M✝<VAR>f : F<VAR>h : IsPrimitiveRoot ζ✝ k<VAR>M : Type u_7<VAR>B : Type u_8<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : SetLike B M<VAR>inst✝ : SubmonoidClass B M<VAR>N : B<VAR>ζ : ↥N<GOAL>IsPrimitiveRoot (↑ζ) k ↔ IsPrimitiveRoot ζ k
<VAR>M✝ : Type u_1<VAR>N✝ : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝⁵ : CommMonoid M✝<VAR>inst✝⁴ : CommMonoid N✝<VAR>inst✝³ : DivisionCommMonoid G<VAR>k l : ℕ<VAR>ζ✝ : M✝<VAR>f : F<VAR>h : IsPrimitiveRoot ζ✝ k<VAR>M : Type u_7<VAR>B : Type u_8<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : SetLike B M<VAR>inst✝ : SubmonoidClass B M<VAR>N : B<VAR>ζ : ↥N<GOAL>(↑ζ ^ k = 1 ∧ ∀ (l : ℕ), ↑ζ ^ l = 1 → k ∣ l) ↔ ζ ^ k = 1 ∧ ∀ (l : ℕ), ζ ^ l = 1 → k ∣ l
<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>a : A<VAR>g : R → R<VAR>ha : p a<VAR>f : C(↑(spectrum R a), R)<GOAL>(cfcHom ha) f = cfc (Function.extend Subtype.val (⇑f) g) a
<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>a : A<VAR>g : R → R<VAR>ha : p a<VAR>f : C(↑(spectrum R a), R)<VAR>h : ⇑f = (spectrum R a).restrict (Function.extend Subtype.val (⇑f) g)<GOAL>(cfcHom ha) f = cfc (Function.extend Subtype.val (⇑f) g) a
<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>a : A<VAR>g : R → R<VAR>ha : p a<VAR>f : C(↑(spectrum R a), R)<VAR>h : ⇑f = (spectrum R a).restrict (Function.extend Subtype.val (⇑f) g)<VAR>hg : ContinuousOn (Function.extend Subtype.val (⇑f) g) (spectrum R a)<GOAL>(cfcHom ha) f = cfc (Function.extend Subtype.val (⇑f) g) a
<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>a : A<VAR>g : R → R<VAR>ha : p a<VAR>f : C(↑(spectrum R a), R)<VAR>h : ⇑f = (spectrum R a).restrict (Function.extend Subtype.val (⇑f) g)<VAR>hg : ContinuousOn (Function.extend Subtype.val (⇑f) g) (spectrum R a)<GOAL>(cfcHom ha) f = (cfcHom ha) { toFun := (spectrum R a).restrict (Function.extend Subtype.val (⇑f) g), continuous_toFun := ⋯ }
<VAR>R : Type u_1<VAR>M₁ : Type u_2<VAR>M₂ : Type u_3<VAR>N : Type u_4<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M₁<VAR>inst✝⁴ : AddCommGroup M₂<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R M₁<VAR>inst✝¹ : Module R M₂<VAR>inst✝ : Module R N<VAR>Q₁ : QuadraticForm R M₁<VAR>Q₂ : QuadraticForm R M₂<VAR>Qₙ : QuadraticForm R N<VAR>m₁ : M₁<VAR>m₂ : M₂<GOAL>(ofProd Q₁ Q₂) ((ι (QuadraticMap.prod Q₁ Q₂)) (m₁, m₂)) = (ι Q₁) m₁ ᵍ⊗ₜ[R] 1 + 1 ᵍ⊗ₜ[R] (ι Q₂) m₂
<VAR>R : Type u_1<VAR>M₁ : Type u_2<VAR>M₂ : Type u_3<VAR>N : Type u_4<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M₁<VAR>inst✝⁴ : AddCommGroup M₂<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R M₁<VAR>inst✝¹ : Module R M₂<VAR>inst✝ : Module R N<VAR>Q₁ : QuadraticForm R M₁<VAR>Q₂ : QuadraticForm R M₂<VAR>Qₙ : QuadraticForm R N<VAR>m₁ : M₁<VAR>m₂ : M₂<GOAL>(((GradedTensorProduct.includeLeft (evenOdd Q₁) (evenOdd Q₂)).toLinearMap ∘ₗ (evenOdd Q₁ 1).subtype ∘ₗ LinearMap.codRestrict (evenOdd Q₁ 1) (ι Q₁) ⋯).coprod ((GradedTensorProduct.includeRight (evenOdd Q₁) (evenOdd Q₂)).toLinearMap ∘ₗ (evenOdd Q₂ 1).subtype ∘ₗ LinearMap.codRestrict (evenOdd Q₂ 1) (ι Q₂) ⋯)) (m₁, m₂) = (ι Q₁) m₁ ᵍ⊗ₜ[R] 1 + 1 ᵍ⊗ₜ[R] (ι Q₂) m₂
<VAR>α β ι : Type u<VAR>f : ι → Cardinal.{v}<VAR>hf : BddAbove (range f)<VAR>g : Cardinal.{v} → Cardinal.{max v w}<GOAL>BddAbove (range (g ∘ f))
<VAR>α β ι : Type u<VAR>f : ι → Cardinal.{v}<VAR>hf : BddAbove (range f)<VAR>g : Cardinal.{v} → Cardinal.{max v w}<GOAL>BddAbove (g '' range f)
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝⁹ : CommSemiring ι<VAR>inst✝⁸ : Module ι (Additive ℤˣ)<VAR>inst✝⁷ : DecidableEq ι<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : Ring A<VAR>inst✝⁴ : Ring B<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra R B<VAR>𝒜 : ι → Submodule R A<VAR>ℬ : ι → Submodule R B<VAR>inst✝¹ : GradedAlgebra 𝒜<VAR>inst✝ : GradedAlgebra ℬ<VAR>j₁ : ι<VAR>a₁ : A<VAR>b₁ : ↥(ℬ j₁)<VAR>a₂ : ↥(𝒜 0)<VAR>b₂ : B<GOAL>a₁ ᵍ⊗ₜ[R] ↑b₁ * ↑a₂ ᵍ⊗ₜ[R] b₂ = (a₁ * ↑a₂) ᵍ⊗ₜ[R] (↑b₁ * b₂)
<VAR>R : Type u_1<VAR>inst✝³ : Ring R<VAR>S : Submonoid R<VAR>inst✝² : OreSet S<VAR>X : Type u_2<VAR>inst✝¹ : AddCommGroup X<VAR>inst✝ : Module R X<GOAL>Subsingleton (OreLocalization S R) ↔ 0 ∈ S
<VAR>R : Type u_1<VAR>inst✝³ : Ring R<VAR>S : Submonoid R<VAR>inst✝² : OreSet S<VAR>X : Type u_2<VAR>inst✝¹ : AddCommGroup X<VAR>inst✝ : Module R X<GOAL>(∃ u v, u • 1 = v • 0 ∧ ↑u * ↑1 = v * ↑1) ↔ 0 ∈ S
<VAR>p : ℕ<VAR>inst✝ : Fact (Prime p)<VAR>hp : p % 4 ≠ 3<GOAL>∃ a b, a ^ 2 + b ^ 2 = p
<VAR>p : ℕ<VAR>inst✝ : Fact (Prime p)<VAR>hp : p % 4 ≠ 3<GOAL>¬Irreducible ↑p
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>κ : Type u_3<VAR>κ' : Type u_4<VAR>R : Type u_5<VAR>M : Type u_6<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Module R M<VAR>R₂ : Type u_7<VAR>M₂ : Type u_8<VAR>inst✝⁵ : CommRing R₂<VAR>inst✝⁴ : AddCommGroup M₂<VAR>inst✝³ : Module R₂ M₂<VAR>e : Basis ι R M<VAR>v✝ : ι' → M<VAR>i✝ : ι<VAR>j : ι'<VAR>inst✝² : Finite ι<VAR>inst✝¹ : Fintype ι'<VAR>inst✝ : DecidableEq ι'<VAR>v : Basis ι' R M<VAR>i : ι'<GOAL>((toLin v e) (e.toMatrix ⇑v)) (v i) = LinearMap.id (v i)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>κ : Type u_3<VAR>κ' : Type u_4<VAR>R : Type u_5<VAR>M : Type u_6<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Module R M<VAR>R₂ : Type u_7<VAR>M₂ : Type u_8<VAR>inst✝⁵ : CommRing R₂<VAR>inst✝⁴ : AddCommGroup M₂<VAR>inst✝³ : Module R₂ M₂<VAR>e : Basis ι R M<VAR>v✝ : ι' → M<VAR>i✝ : ι<VAR>j : ι'<VAR>inst✝² : Finite ι<VAR>inst✝¹ : Fintype ι'<VAR>inst✝ : DecidableEq ι'<VAR>v : Basis ι' R M<VAR>i : ι'<VAR>val✝ : Fintype ι<GOAL>((toLin v e) (e.toMatrix ⇑v)) (v i) = LinearMap.id (v i)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹¹ : CommSemiring R<VAR>inst✝¹⁰ : AddCommMonoid M<VAR>inst✝⁹ : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝⁸ : CommRing R₁<VAR>inst✝⁷ : AddCommGroup M₁<VAR>inst✝⁶ : Module R₁ M₁<VAR>V : Type u_5<VAR>K : Type u_6<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : Module K V<VAR>B✝ : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>M₂' : Type u_7<VAR>inst✝² : AddCommMonoid M₂'<VAR>inst✝¹ : Module R M₂'<VAR>n : Type w<VAR>inst✝ : Nontrivial R<VAR>B : BilinForm R M<VAR>v : Basis n R M<VAR>h : B.iIsOrtho ⇑v<VAR>hB : B.Nondegenerate<VAR>i : n<VAR>ho : B.IsOrtho (v i) (v i)<GOAL>False