ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F✝ : Type u_3<VAR>ι : Type u_4<VAR>π : ι → Type u_5<VAR>inst✝² : OrderedSemiring 𝕜<VAR>inst✝¹ : AddCommMonoid E<VAR>inst✝ : SMul 𝕜 E<VAR>A B C : Set E<VAR>x : E<VAR>F : Set (Set E)<VAR>hF : F.Nonempty<VAR>hA : ∀ B ∈ F, IsExtreme 𝕜 A B<VAR>this : Nonempty ↑F<GOAL>IsExtreme 𝕜 A (⋂ B ∈ F, B)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>κ : ι → Sort u_1<VAR>a a₁ a₂ : α<VAR>b b₁ b₂ : β<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>e : α ≃o β<VAR>s : Set β<GOAL>BddBelow (⇑e ⁻¹' s) ↔ BddBelow s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>inst✝ : Nonempty α<VAR>s : Set α<VAR>f : α → β<VAR>a : α<VAR>b : β<VAR>h : ¬∃ a ∈ s, f a = b<GOAL>invFunOn f s b = Classical.choice inst✝
<VAR>z : ℂ<GOAL>abs z ≤ |z.re| + |z.im|
<VAR>R : Type u1<VAR>inst✝⁴ : CommRing R<VAR>M : Type u2<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>A : Type u_1<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>x : M<GOAL>(ι R) x = 0 ↔ x = 0
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : IsDomain S<VAR>inst✝ : Algebra R S<VAR>b : Basis ι R S<VAR>x : S<VAR>hx : x ≠ 0<VAR>i : ι<GOAL>↑((basisSpanSingleton b hx) i) = x * b i
<VAR>α : Type u_1<VAR>f g h : Perm α<GOAL>f⁻¹.Disjoint g ↔ f.Disjoint g
<VAR>α : Type u_1<VAR>f g h✝ : Perm α<VAR>h : f⁻¹.Disjoint g<GOAL>f.Disjoint g
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝ : PseudoEMetricSpace E<VAR>f : ℝ → E<VAR>s : Set ℝ<VAR>l : ℝ≥0<VAR>h : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal (↑l * (y - x))<VAR>x : ℝ<VAR>xs : x ∈ s<VAR>y : ℝ<VAR>ys : y ∈ s<GOAL>eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal (↑l * (y - x))
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝ : PseudoEMetricSpace E<VAR>f : ℝ → E<VAR>s : Set ℝ<VAR>l : ℝ≥0<VAR>h : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal (↑l * (y - x))<VAR>x : ℝ<VAR>xs : x ∈ s<VAR>y : ℝ<VAR>ys : y ∈ s<VAR>xy : x ≤ y<GOAL>eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal (↑l * (y - x))
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝ : PseudoEMetricSpace E<VAR>f : ℝ → E<VAR>s : Set ℝ<VAR>l : ℝ≥0<VAR>h : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal (↑l * (y - x))<VAR>x : ℝ<VAR>xs : x ∈ s<VAR>y : ℝ<VAR>ys : y ∈ s<VAR>yx : y ≤ x<GOAL>eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal (↑l * (y - x))
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝¹ : MonoidWithZero M₀<VAR>inst✝ : GroupWithZero G₀<VAR>a✝ b c d : G₀<VAR>m n : ℕ<VAR>a : G₀<VAR>hc : c ≠ 0<GOAL>a / c / (b / c) = a / b
<VAR>α : Type u<VAR>β : α → Type v<VAR>inst✝ : DecidableEq α<VAR>s₁✝ s₂✝ s₃✝ : Finmap β<VAR>s₁ s₂ s₃ : AList β<GOAL>⟦s₁⟧ ∪ ⟦s₂⟧ ∪ ⟦s₃⟧ = ⟦s₁⟧ ∪ (⟦s₂⟧ ∪ ⟦s₃⟧)
<VAR>α : Type u_1<VAR>inst✝⁵ : AddCommSemigroup α<VAR>inst✝⁴ : PartialOrder α<VAR>inst✝³ : ExistsAddOfLE α<VAR>inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝¹ : Sub α<VAR>inst✝ : OrderedSub α<VAR>a b c d : α<VAR>hab : AddLECancellable (a - b)<VAR>h₁ : b ≤ a<VAR>h₂ : c ≤ a<VAR>h₃ : a - b = a - c<GOAL>b = c
<VAR>α : Type u_1<VAR>inst✝⁵ : AddCommSemigroup α<VAR>inst✝⁴ : PartialOrder α<VAR>inst✝³ : ExistsAddOfLE α<VAR>inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝¹ : Sub α<VAR>inst✝ : OrderedSub α<VAR>a b c d : α<VAR>hab : AddLECancellable (a - b)<VAR>h₁ : b ≤ a<VAR>h₂ : c ≤ a<VAR>h₃ : a - b = a - c<GOAL>a - b + b = a - b + c
<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>m0 : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>inst✝ : MeasurableSpace δ<VAR>f✝ g : α → β<VAR>μ✝ ν : Measure α<VAR>mβ : MeasurableSpace β<VAR>μ : Measure α<VAR>f : α → β<VAR>h : NeZero (Measure.map f μ)<GOAL>AEMeasurable f μ
<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>m0 : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>inst✝ : MeasurableSpace δ<VAR>f✝ g : α → β<VAR>μ✝ ν : Measure α<VAR>mβ : MeasurableSpace β<VAR>μ : Measure α<VAR>f : α → β<VAR>h : NeZero (Measure.map f μ)<VAR>h' : ¬AEMeasurable f μ<GOAL>False
<VAR>C : Type u<VAR>𝒞 : Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<VAR>inst✝¹ : HasColimit (pair Y Z)<VAR>inst✝ : HasColimit (parallelPair (f ≫ coprod.inl) (g ≫ coprod.inr))<VAR>ι₁ : Y ⟶ Y ⨿ Z := coprod.inl<VAR>ι₂ : Z ⟶ Y ⨿ Z := coprod.inr<VAR>c : Y ⨿ Z ⟶ coequalizer (f ≫ ι₁) (g ≫ ι₂) := coequalizer.π (f ≫ ι₁) (g ≫ ι₂)<GOAL>f ≫ ι₁ ≫ c = g ≫ ι₂ ≫ c
<VAR>C : Type u<VAR>𝒞 : Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<VAR>inst✝¹ : HasColimit (pair Y Z)<VAR>inst✝ : HasColimit (parallelPair (f ≫ coprod.inl) (g ≫ coprod.inr))<VAR>ι₁ : Y ⟶ Y ⨿ Z := coprod.inl<VAR>ι₂ : Z ⟶ Y ⨿ Z := coprod.inr<VAR>c : Y ⨿ Z ⟶ coequalizer (f ≫ ι₁) (g ≫ ι₂) := coequalizer.π (f ≫ ι₁) (g ≫ ι₂)<VAR>s : PushoutCocone f g<GOAL>(f ≫ ι₁) ≫ coprod.desc (s.ι.app WalkingSpan.left) (s.ι.app WalkingSpan.right) = (g ≫ ι₂) ≫ coprod.desc (s.ι.app WalkingSpan.left) (s.ι.app WalkingSpan.right)
<VAR>C : Type u<VAR>𝒞 : Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<VAR>inst✝¹ : HasColimit (pair Y Z)<VAR>inst✝ : HasColimit (parallelPair (f ≫ coprod.inl) (g ≫ coprod.inr))<VAR>ι₁ : Y ⟶ Y ⨿ Z := coprod.inl<VAR>ι₂ : Z ⟶ Y ⨿ Z := coprod.inr<VAR>c : Y ⨿ Z ⟶ coequalizer (f ≫ ι₁) (g ≫ ι₂) := coequalizer.π (f ≫ ι₁) (g ≫ ι₂)<VAR>s : PushoutCocone f g<GOAL>f ≫ (BinaryCofan.mk (s.ι.app WalkingSpan.left) (s.ι.app WalkingSpan.right)).ι.app { as := WalkingPair.left } = g ≫ (BinaryCofan.mk (s.ι.app WalkingSpan.left) (s.ι.app WalkingSpan.right)).ι.app { as := WalkingPair.right }
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f g : α → β<VAR>c c₁ c₂ x : α<VAR>inst✝³ : AddMonoid α<VAR>inst✝² : Neg β<VAR>inst✝¹ : Group γ<VAR>inst✝ : DistribMulAction γ α<VAR>h : Antiperiodic f c<VAR>a : γ<GOAL>Antiperiodic (fun x => f (a⁻¹ • x)) (a • c)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>𝒜 ℬ : Finset (Finset α)<VAR>s✝ t : Finset α<VAR>a : α<VAR>s : Finset α<GOAL>s.powerset ⊻ s.powerset = s.powerset
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>s : Set α<VAR>hs : μ s ≠ ⊤<VAR>f : α → ℝ≥0∞<VAR>M : ℝ≥0<VAR>hM : ∀ x ∈ s, f x ≤ ↑M<GOAL>∫⁻ (x : α) in s, f x ∂μ < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>s : Set α<VAR>hs : μ s ≠ ⊤<VAR>f : α → ℝ≥0∞<VAR>M : ℝ≥0<VAR>hM : ∀ x ∈ s, f x ≤ ↑M<GOAL>∫⁻ (x : α) in s, ↑M ∂μ < ⊤
<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>N : Type u_9<VAR>inst✝⁵ : AddCommMonoid N<VAR>inst✝⁴ : Module R N<VAR>b : Basis ι R M<VAR>b' : Basis ι' R M<VAR>c : Basis κ R N<VAR>c' : Basis κ' R N<VAR>f : M →ₗ[R] N<VAR>inst✝³ : Fintype ι'<VAR>inst✝² : Fintype κ<VAR>inst✝¹ : Finite ι<VAR>inst✝ : DecidableEq κ<VAR>b₁ : Basis ι R M<VAR>b₂ : Basis ι' R M<VAR>b₃ : Basis κ R N<VAR>A : Matrix ι' κ R<GOAL>b₁.toMatrix ⇑b₂ * A = (toMatrix b₃ b₁) ((toLin b₃ b₂) A)
<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>N : Type u_9<VAR>inst✝⁵ : AddCommMonoid N<VAR>inst✝⁴ : Module R N<VAR>b : Basis ι R M<VAR>b' : Basis ι' R M<VAR>c : Basis κ R N<VAR>c' : Basis κ' R N<VAR>f : M →ₗ[R] N<VAR>inst✝³ : Fintype ι'<VAR>inst✝² : Fintype κ<VAR>inst✝¹ : Finite ι<VAR>inst✝ : DecidableEq κ<VAR>b₁ : Basis ι R M<VAR>b₂ : Basis ι' R M<VAR>b₃ : Basis κ R N<VAR>A : Matrix ι' κ R<VAR>this : b₁.toMatrix ⇑b₂ * (toMatrix b₃ b₂) ((toLin b₃ b₂) A) = (toMatrix b₃ b₁) ((toLin b₃ b₂) A)<GOAL>b₁.toMatrix ⇑b₂ * A = (toMatrix b₃ b₁) ((toLin b₃ b₂) A)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>z : ℤ<VAR>a✝ a b : α<VAR>x✝ : ℤ<GOAL>x✝ ∈ Int.cast ⁻¹' Ioo a b ↔ x✝ ∈ Ioo ⌊a⌋ ⌈b⌉
<VAR>α : Type u_1<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : UniqueFactorizationMonoid α<VAR>inst✝ : Subsingleton α<VAR>a : Associates α<VAR>this : Subsingleton (Associates α)<GOAL>a.factors = ⊤
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>inst✝ : CommRing R<VAR>r x y z : R<VAR>a b c : ℍ[R]<VAR>n : ℕ<GOAL>normSq ↑n = ↑n ^ 2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>s : Finset α<VAR>k : ℕ<VAR>h : k ≤ s.card<VAR>a : Fin k<GOAL>(s.orderEmbOfCardLe h) a ∈ s
<VAR>ι : Type u_1<VAR>k : Type u_2<VAR>V : Type u_3<VAR>P : Type u_4<VAR>inst✝⁴ : Ring k<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module k V<VAR>inst✝¹ : AffineSpace V P<VAR>inst✝ : Nontrivial k<VAR>s : Finset ι<VAR>w : ι → k<VAR>h : ∑ i ∈ s, w i = 1<VAR>p : ι → P<GOAL>(Finset.affineCombination k s p) w ∈ affineSpan k (Set.range p)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f✝ : α ↪ β<VAR>s : Finset α<VAR>f : α ≃ β<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<GOAL>map f.toEmbedding (filter p s) = filter (p ∘ ⇑f.symm) (map f.toEmbedding s)
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>f : α → α<VAR>s : Set α<VAR>μ : Measure α<VAR>hf : Ergodic f μ<VAR>hs : MeasurableSet s<VAR>hs' : s ≤ᶠ[ae μ] f ⁻¹' s<VAR>h_fin : μ s ≠ ⊤<GOAL>s =ᶠ[ae μ] ∅ ∨ s =ᶠ[ae μ] univ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>f : α → α<VAR>s : Set α<VAR>μ : Measure α<VAR>hf : Ergodic f μ<VAR>hs : MeasurableSet s<VAR>hs' : s ≤ᶠ[ae μ] f ⁻¹' s<VAR>h_fin : μ (f ⁻¹' s) ≠ ⊤<GOAL>s =ᶠ[ae μ] ∅ ∨ s =ᶠ[ae μ] univ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>f : α → α<VAR>s : Set α<VAR>μ : Measure α<VAR>hf : Ergodic f μ<VAR>hs : MeasurableSet s<VAR>hs' : s ≤ᶠ[ae μ] f ⁻¹' s<VAR>h_fin : μ (f ⁻¹' s) ≠ ⊤<GOAL>f ⁻¹' s =ᶠ[ae μ] s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>f✝ : ℕ → α<VAR>a : α<VAR>f : ℕ → ℝ≥0<GOAL>(¬Summable fun i => ↑(f i)) ↔ Tendsto (fun n => ∑ i ∈ range n, (fun i => ↑(f i)) i) atTop atTop
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>a b c u v✝ w : V<VAR>e✝ : Sym2 V<VAR>G₁ G₂ : SimpleGraph V<VAR>e : Sym2 V<VAR>he : e ∈ G.edgeSet<VAR>v : V<VAR>h : v ∈ e<GOAL>Sym2.Mem.other h ≠ v
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>a b c u v✝ w : V<VAR>e✝ : Sym2 V<VAR>G₁ G₂ : SimpleGraph V<VAR>e : Sym2 V<VAR>v : V<VAR>h : v ∈ e<VAR>he : s(Sym2.Mem.other h, v) ∈ G.edgeSet<GOAL>Sym2.Mem.other h ≠ v
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α (β × ℝ)<VAR>ν : Kernel α β<VAR>f : α × β → ℚ → ℝ<VAR>hf : IsRatCondKernelCDFAux f κ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>a : α<GOAL>∀ᵐ (t : β) ∂ν a, Tendsto (f (a, t)) atBot (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α (β × ℝ)<VAR>ν : Kernel α β<VAR>f : α × β → ℚ → ℝ<VAR>hf : IsRatCondKernelCDFAux f κ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>a : α<GOAL>∀ᵐ (t : β) ∂ν a, Tendsto (fun q => f (a, t) (-q)) atTop (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α (β × ℝ)<VAR>ν : Kernel α β<VAR>f : α × β → ℚ → ℝ<VAR>hf : IsRatCondKernelCDFAux f κ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>a : α<GOAL>∀ᵐ (t : β) ∂ν a, Tendsto (fun n => f (a, t) (-↑n)) atTop (𝓝 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>ι : Type u_3<VAR>f : ι → R → R<VAR>a : A<VAR>ha : autoParam (p a) _auto✝<VAR>hf : autoParam (∀ (i : ι), ContinuousOn (f i) (spectrum R a)) _auto✝<VAR>i : ι<GOAL>cfc (f i) a = (cfcHom ha) { toFun := (spectrum R a).restrict (f i), continuous_toFun := ⋯ }
<VAR>α✝ : Type u_1<VAR>r : α✝ → α✝ → Prop<VAR>β α : Type u<VAR>f : β → α<VAR>w : #α < #β<VAR>w' : Infinite α<GOAL>∃ a, Infinite ↑(f ⁻¹' {a})
<VAR>α✝ : Type u_1<VAR>r : α✝ → α✝ → Prop<VAR>β α : Type u<VAR>f : β → α<VAR>w : #α < #β<VAR>w' : ℵ₀ ≤ #α<GOAL>∃ a, ℵ₀ ≤ #↑(f ⁻¹' {a})
<VAR>α✝ : Type u_1<VAR>r : α✝ → α✝ → Prop<VAR>β α : Type u<VAR>f : β → α<VAR>w : #α < #β<VAR>w' : ℵ₀ ≤ #α<VAR>a : α<VAR>ha : #α < #↑(f ⁻¹' {a})<GOAL>∃ a, ℵ₀ ≤ #↑(f ⁻¹' {a})
<VAR>α : Type u_1<VAR>β : Type u_2<GOAL>[].permutations = [[]]
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<GOAL>StrictMonoOn (fun x => 1 - ε x) (Set.Ioi 1)
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<GOAL>StrictMonoOn (fun x => 1 + -ε x) (Set.Ioi 1)
<VAR>R✝ : Type u_1<VAR>A✝ : Type u_2<VAR>inst✝⁷ : CommSemiring R✝<VAR>inst✝⁶ : NonUnitalRing A✝<VAR>inst✝⁵ : Module R✝ A✝<VAR>inst✝⁴ : IsScalarTower R✝ A✝ A✝<VAR>inst✝³ : SMulCommClass R✝ A✝ A✝<VAR>R : Type u_3<VAR>A : Type u_4<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra R A<VAR>a : A<VAR>r : R<GOAL>r ∈ {r | ∀ (hr : IsUnit r), ¬IsQuasiregular (-(hr.unit⁻¹ • a))} ↔ r ∈ spectrum R a ∪ {r | ¬IsUnit r}
<VAR>R✝ : Type u_1<VAR>A✝ : Type u_2<VAR>inst✝⁷ : CommSemiring R✝<VAR>inst✝⁶ : NonUnitalRing A✝<VAR>inst✝⁵ : Module R✝ A✝<VAR>inst✝⁴ : IsScalarTower R✝ A✝ A✝<VAR>inst✝³ : SMulCommClass R✝ A✝ A✝<VAR>R : Type u_3<VAR>A : Type u_4<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra R A<VAR>a : A<VAR>r : R<GOAL>(∀ (hr : IsUnit r), ¬IsQuasiregular (-(hr.unit⁻¹ • a))) ↔ IsUnit r → ¬IsUnit ((algebraMap R A) r - a)
<VAR>R✝ : Type u_1<VAR>A✝ : Type u_2<VAR>inst✝⁷ : CommSemiring R✝<VAR>inst✝⁶ : NonUnitalRing A✝<VAR>inst✝⁵ : Module R✝ A✝<VAR>inst✝⁴ : IsScalarTower R✝ A✝ A✝<VAR>inst✝³ : SMulCommClass R✝ A✝ A✝<VAR>R : Type u_3<VAR>A : Type u_4<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra R A<VAR>a : A<VAR>r : R<VAR>hr : IsUnit r<GOAL>¬IsQuasiregular (-(hr.unit⁻¹ • a)) ↔ ¬IsUnit ((algebraMap R A) r - a)
<VAR>R✝ : Type u_1<VAR>A✝ : Type u_2<VAR>inst✝⁷ : CommSemiring R✝<VAR>inst✝⁶ : NonUnitalRing A✝<VAR>inst✝⁵ : Module R✝ A✝<VAR>inst✝⁴ : IsScalarTower R✝ A✝ A✝<VAR>inst✝³ : SMulCommClass R✝ A✝ A✝<VAR>R : Type u_3<VAR>A : Type u_4<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra R A<VAR>a : A<VAR>r : R<VAR>hr : IsUnit r<GOAL>IsUnit (1 - hr.unit⁻¹ • a) ↔ IsUnit (r • 1 - a)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Ring R<VAR>p✝ q✝ p q : R[X]<VAR>hq : q.Monic<VAR>a✝ : Nontrivial R<GOAL>(p %ₘ q).degree ≤ q.degree
<VAR>ι : Type w<VAR>R : Type u<VAR>M : Type v₁<VAR>N : Type v₂<VAR>P : Type v₃<VAR>Q : Type v₄<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : AddCommMonoid N<VAR>inst✝⁷ : AddCommMonoid P<VAR>inst✝⁶ : AddCommMonoid Q<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module R N<VAR>inst✝³ : Module R P<VAR>inst✝² : Module R Q<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<VAR>b : Basis ι R M<VAR>f : Dual R M<VAR>p : P<VAR>g : Dual R N<VAR>q : Q<VAR>m : M<VAR>n : N<GOAL>(((TensorProduct.mk R M N).compr₂ (TensorProduct.map ((dualTensorHom R M P) (f ⊗ₜ[R] p)) ((dualTensorHom R N Q) (g ⊗ₜ[R] q)))) m) n = (((TensorProduct.mk R M N).compr₂ ((dualTensorHom R (M ⊗[R] N) (P ⊗[R] Q)) ((dualDistrib R M N) (f ⊗ₜ[R] g) ⊗ₜ[R] p ⊗ₜ[R] q))) m) n
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>A : Type u_3<VAR>T : Type u_4<VAR>B : Type u_5<VAR>ι : Type u_6<VAR>inst✝¹¹ : SemilatticeSup B<VAR>inst✝¹⁰ : OrderBot B<VAR>inst✝⁹ : SemilatticeInf T<VAR>inst✝⁸ : OrderTop T<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddMonoid A<VAR>inst✝⁵ : AddMonoid B<VAR>inst✝⁴ : CovariantClass B B (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝³ : CovariantClass B B (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝² : AddMonoid T<VAR>inst✝¹ : CovariantClass T T (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : CovariantClass T T (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>degb : A → B<VAR>degt : A → T<VAR>degb0 : degb 0 ≤ 0<VAR>degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b<VAR>n : ℕ<VAR>f : R[A]<GOAL>(f ^ n).support.sup degb ≤ n • f.support.sup degb
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>A : Type u_3<VAR>T : Type u_4<VAR>B : Type u_5<VAR>ι : Type u_6<VAR>inst✝¹¹ : SemilatticeSup B<VAR>inst✝¹⁰ : OrderBot B<VAR>inst✝⁹ : SemilatticeInf T<VAR>inst✝⁸ : OrderTop T<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddMonoid A<VAR>inst✝⁵ : AddMonoid B<VAR>inst✝⁴ : CovariantClass B B (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝³ : CovariantClass B B (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝² : AddMonoid T<VAR>inst✝¹ : CovariantClass T T (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : CovariantClass T T (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>degb : A → B<VAR>degt : A → T<VAR>degb0 : degb 0 ≤ 0<VAR>degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b<VAR>n : ℕ<VAR>f : R[A]<GOAL>(List.replicate n f).prod.support.sup degb ≤ (List.replicate n (f.support.sup degb)).sum
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>A : Type u_3<VAR>T : Type u_4<VAR>B : Type u_5<VAR>ι : Type u_6<VAR>inst✝¹¹ : SemilatticeSup B<VAR>inst✝¹⁰ : OrderBot B<VAR>inst✝⁹ : SemilatticeInf T<VAR>inst✝⁸ : OrderTop T<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddMonoid A<VAR>inst✝⁵ : AddMonoid B<VAR>inst✝⁴ : CovariantClass B B (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝³ : CovariantClass B B (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝² : AddMonoid T<VAR>inst✝¹ : CovariantClass T T (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : CovariantClass T T (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>degb : A → B<VAR>degt : A → T<VAR>degb0 : degb 0 ≤ 0<VAR>degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b<VAR>n : ℕ<VAR>f : R[A]<GOAL>(List.map (fun f => f.support.sup degb) (List.replicate n f)).sum = (List.replicate n (f.support.sup degb)).sum
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>p : Type u_3<VAR>R : Type u_4<VAR>inst✝⁷ : Fintype m<VAR>inst✝⁶ : Fintype n<VAR>inst✝⁵ : Fintype p<VAR>inst✝⁴ : PartialOrder R<VAR>inst✝³ : NonUnitalRing R<VAR>inst✝² : StarRing R<VAR>inst✝¹ : StarOrderedRing R<VAR>inst✝ : NoZeroDivisors R<VAR>A : Matrix m n R<VAR>B : Matrix n p R<GOAL>Aᴴ * A * B = 0 ↔ A * B = 0
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>p : Type u_3<VAR>R : Type u_4<VAR>inst✝⁷ : Fintype m<VAR>inst✝⁶ : Fintype n<VAR>inst✝⁵ : Fintype p<VAR>inst✝⁴ : PartialOrder R<VAR>inst✝³ : NonUnitalRing R<VAR>inst✝² : StarRing R<VAR>inst✝¹ : StarOrderedRing R<VAR>inst✝ : NoZeroDivisors R<VAR>A : Matrix m n R<VAR>B : Matrix n p R<VAR>h : Aᴴ * A * B = 0<GOAL>A * B = 0
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>p : Type u_3<VAR>R : Type u_4<VAR>inst✝⁷ : Fintype m<VAR>inst✝⁶ : Fintype n<VAR>inst✝⁵ : Fintype p<VAR>inst✝⁴ : PartialOrder R<VAR>inst✝³ : NonUnitalRing R<VAR>inst✝² : StarRing R<VAR>inst✝¹ : StarOrderedRing R<VAR>inst✝ : NoZeroDivisors R<VAR>A : Matrix m n R<VAR>B : Matrix n p R<VAR>h : Bᴴ * (Aᴴ * A * B) = Bᴴ * 0<GOAL>A * B = 0
<VAR>s : Finset ℕ<VAR>m : ℕ<GOAL>m ∈ factoredNumbers s ↔ m ≠ 0 ∧ ∀ p ≤ m, Prime p → p ∣ m → p ∈ s
<VAR>s : Finset ℕ<VAR>m : ℕ<GOAL>(m ≠ 0 ∧ ∀ (p : ℕ), Prime p ∧ p ∣ m ∧ m ≠ 0 → p ∈ s) ↔ m ≠ 0 ∧ ∀ p ≤ m, Prime p → p ∣ m → p ∈ s
<VAR>X : Type u_1<VAR>inst✝ : TopologicalSpace X<VAR>s✝ : Set (OnePoint X)<VAR>t s : Set X<GOAL>IsClosed (some '' s) ↔ IsClosed s ∧ IsCompact s
<VAR>R : Type u<VAR>ι : Type u_1<VAR>inst✝ : CommSemiring R<VAR>I J K L : Ideal R<VAR>n : ℕ<VAR>h : I ⊔ J = ⊤<GOAL>I ^ n ⊔ J = ⊤
<VAR>R : Type u<VAR>ι : Type u_1<VAR>inst✝ : CommSemiring R<VAR>I J K L : Ideal R<VAR>n : ℕ<VAR>h : I ⊔ J = ⊤<GOAL>(∏ _x ∈ Finset.range n, I) ⊔ J = ⊤
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M✝ : Matroid α<VAR>F X Y : Set α<VAR>e : α<VAR>M : Matroid α<VAR>Xs : ι → Set α<VAR>A : Set ι<GOAL>M.closure (⋃ i ∈ A, M.closure (Xs i)) = M.closure (⋃ i ∈ A, Xs i)
<VAR>N : ℕ<VAR>hN : N ≠ 0<VAR>χ : DirichletCharacter ℂ N<GOAL>¬LSeriesSummable (fun n => χ ↑n) 1
<VAR>N : ℕ<VAR>hN : N ≠ 0<VAR>χ : DirichletCharacter ℂ N<VAR>h : LSeriesSummable (fun n => χ ↑n) 1<GOAL>Summable ({n | ↑n = 1}.indicator fun n => 1 / ↑n)
<VAR>N : ℕ<VAR>hN : N ≠ 0<VAR>χ : DirichletCharacter ℂ N<VAR>h : LSeriesSummable (fun n => χ ↑n) 1<VAR>n : ℕ<GOAL>{n | ↑n = 1}.indicator (fun n => 1 / ↑n) n ≤ ‖term (fun n => χ ↑n) 1 n‖
<VAR>N : ℕ<VAR>hN : N ≠ 0<VAR>χ : DirichletCharacter ℂ N<VAR>h : LSeriesSummable (fun n => χ ↑n) 1<VAR>n : ℕ<GOAL>(if n ∈ {n | ↑n = 1} then 1 / ↑n else 0) ≤ if n = 0 then 0 else ‖χ ↑n‖ / ↑n
<VAR>R : Type u_1<VAR>inst✝¹⁶ : Semiring R<VAR>M : Type u_2<VAR>inst✝¹⁵ : AddCommMonoid M<VAR>inst✝¹⁴ : Module R M<VAR>N : Type u_3<VAR>inst✝¹³ : AddCommMonoid N<VAR>inst✝¹² : Module R N<VAR>P : Type u_4<VAR>inst✝¹¹ : AddCommMonoid P<VAR>inst✝¹⁰ : Module R P<VAR>M' : Type u_5<VAR>inst✝⁹ : AddCommGroup M'<VAR>inst✝⁸ : Module R M'<VAR>N' : Type u_6<VAR>inst✝⁷ : AddCommGroup N'<VAR>inst✝⁶ : Module R N'<VAR>ι : Type u_7<VAR>ι' : Type u_8<VAR>ι'' : Type u_9<VAR>M₂ : Type u_10<VAR>inst✝⁵ : AddCommMonoid M₂<VAR>inst✝⁴ : Module R M₂<VAR>M₃ : Type u_11<VAR>inst✝³ : AddCommMonoid M₃<VAR>inst✝² : Module R M₃<VAR>f f' : M [⋀^ι]→ₗ[R] N<VAR>g g₂ : M [⋀^ι]→ₗ[R] N'<VAR>g' : M' [⋀^ι]→ₗ[R] N'<VAR>v✝ : ι → M<VAR>v' : ι → M'<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<VAR>v : ι → M<VAR>σ : Equiv.Perm ι<GOAL>g (v ∘ ⇑σ) = Equiv.Perm.sign σ • g v
<VAR>R : Type u_1<VAR>inst✝¹⁶ : Semiring R<VAR>M : Type u_2<VAR>inst✝¹⁵ : AddCommMonoid M<VAR>inst✝¹⁴ : Module R M<VAR>N : Type u_3<VAR>inst✝¹³ : AddCommMonoid N<VAR>inst✝¹² : Module R N<VAR>P : Type u_4<VAR>inst✝¹¹ : AddCommMonoid P<VAR>inst✝¹⁰ : Module R P<VAR>M' : Type u_5<VAR>inst✝⁹ : AddCommGroup M'<VAR>inst✝⁸ : Module R M'<VAR>N' : Type u_6<VAR>inst✝⁷ : AddCommGroup N'<VAR>inst✝⁶ : Module R N'<VAR>ι : Type u_7<VAR>ι' : Type u_8<VAR>ι'' : Type u_9<VAR>M₂ : Type u_10<VAR>inst✝⁵ : AddCommMonoid M₂<VAR>inst✝⁴ : Module R M₂<VAR>M₃ : Type u_11<VAR>inst✝³ : AddCommMonoid M₃<VAR>inst✝² : Module R M₃<VAR>f f' : M [⋀^ι]→ₗ[R] N<VAR>g g₂ : M [⋀^ι]→ₗ[R] N'<VAR>g' : M' [⋀^ι]→ₗ[R] N'<VAR>v✝ : ι → M<VAR>v' : ι → M'<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<VAR>v : ι → M<GOAL>g (v ∘ ⇑1) = Equiv.Perm.sign 1 • g v
<VAR>R : Type u_1<VAR>inst✝¹⁶ : Semiring R<VAR>M : Type u_2<VAR>inst✝¹⁵ : AddCommMonoid M<VAR>inst✝¹⁴ : Module R M<VAR>N : Type u_3<VAR>inst✝¹³ : AddCommMonoid N<VAR>inst✝¹² : Module R N<VAR>P : Type u_4<VAR>inst✝¹¹ : AddCommMonoid P<VAR>inst✝¹⁰ : Module R P<VAR>M' : Type u_5<VAR>inst✝⁹ : AddCommGroup M'<VAR>inst✝⁸ : Module R M'<VAR>N' : Type u_6<VAR>inst✝⁷ : AddCommGroup N'<VAR>inst✝⁶ : Module R N'<VAR>ι : Type u_7<VAR>ι' : Type u_8<VAR>ι'' : Type u_9<VAR>M₂ : Type u_10<VAR>inst✝⁵ : AddCommMonoid M₂<VAR>inst✝⁴ : Module R M₂<VAR>M₃ : Type u_11<VAR>inst✝³ : AddCommMonoid M₃<VAR>inst✝² : Module R M₃<VAR>f f' : M [⋀^ι]→ₗ[R] N<VAR>g g₂ : M [⋀^ι]→ₗ[R] N'<VAR>g' : M' [⋀^ι]→ₗ[R] N'<VAR>v✝ : ι → M<VAR>v' : ι → M'<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<VAR>v : ι → M<VAR>s : Equiv.Perm ι<VAR>x y : ι<VAR>hxy : x ≠ y<VAR>hI : g (v ∘ ⇑s) = Equiv.Perm.sign s • g v<GOAL>g (v ∘ ⇑(s * Equiv.swap x y)) = Equiv.Perm.sign (s * Equiv.swap x y) • g v
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a a₁ a₂ b b₁ b₂ c d : α<VAR>h₁ : c ≤ b<VAR>x : α<GOAL>x ∈ Iio b ∪ Ico c d ↔ x ∈ Iio (max b d)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a a₁ a₂ b b₁ b₂ c d : α<VAR>h₁ : c ≤ b<VAR>x : α<GOAL>x < b ∨ c ≤ x ∧ x < d ↔ x < b ∨ x < d