ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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✝¹¹ : Semiring S✝<VAR>inst✝¹⁰ : AddCommMonoid A<VAR>inst✝⁹ : Algebra R S✝<VAR>inst✝⁸ : Module S✝ A<VAR>inst✝⁷ : Module R A<VAR>inst✝⁶ : IsScalarTower R S✝ A<VAR>S : Type u_1<VAR>T : Type u_2<VAR>inst✝⁵ : CommSemiring S<VAR>inst✝⁴ : Semiring T<VAR>inst✝³ : Algebra R S<VAR>inst✝² : Algebra R T<VAR>inst✝¹ : Algebra S T<VAR>inst✝ : IsScalarTower R S T<VAR>x : S<VAR>a : Set S<VAR>hx : x ∈ span R a<GOAL>∃ y ∈ span R a, (↑R (Algebra.linearMap S T)) y = (algebraMap S T) x
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝³ : LinearOrder ι<VAR>f : Filtration ι m<VAR>τ π : Ω → ι<VAR>inst✝² : TopologicalSpace ι<VAR>inst✝¹ : OrderTopology ι<VAR>inst✝ : FirstCountableTopology ι<VAR>hτ : IsStoppingTime f τ<VAR>i : ι<GOAL>MeasurableSet {ω | τ ω < i}
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝³ : LinearOrder ι<VAR>f : Filtration ι m<VAR>τ π : Ω → ι<VAR>inst✝² : TopologicalSpace ι<VAR>inst✝¹ : OrderTopology ι<VAR>inst✝ : FirstCountableTopology ι<VAR>hτ : IsStoppingTime f τ<VAR>i : ι<VAR>this : {ω | τ ω < i} = {ω | τ ω ≤ i} \ {ω | τ ω = i}<GOAL>MeasurableSet {ω | τ ω < i}
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝³ : LinearOrder ι<VAR>f : Filtration ι m<VAR>τ π : Ω → ι<VAR>inst✝² : TopologicalSpace ι<VAR>inst✝¹ : OrderTopology ι<VAR>inst✝ : FirstCountableTopology ι<VAR>hτ : IsStoppingTime f τ<VAR>i : ι<VAR>this : {ω | τ ω < i} = {ω | τ ω ≤ i} \ {ω | τ ω = i}<GOAL>MeasurableSet ({ω | τ ω ≤ i} \ {ω | τ ω = i})
<VAR>ι✝ : Type u_1<VAR>κ✝ : Type u_2<VAR>α✝¹ : Type u_3<VAR>β✝ : Type u_4<VAR>γ : Type u_5<VAR>s s₁ s₂ : Finset α✝¹<VAR>a✝ : α✝¹<VAR>f✝ g : α✝¹ → β✝<VAR>ι : Type u_6<VAR>κ : Type u_7<VAR>α✝ : Type u_8<VAR>inst✝⁵ : Fintype ι<VAR>inst✝⁴ : Fintype κ<VAR>inst✝³ : CommMonoid α✝<VAR>α : Type u_9<VAR>β : Type u_10<VAR>inst✝² : CommMonoid β<VAR>inst✝¹ : Subsingleton α<VAR>inst✝ : Fintype α<VAR>f : α → β<VAR>a : α<VAR>this : Unique α<GOAL>∏ x : α, f x = f a
<VAR>n : ℕ<VAR>this : ∃ x < n + 1, (n + 1).gcd x = 1<GOAL>φ (n + 1) = 0 ↔ n + 1 = 0
<VAR>n : ℕ<GOAL>(n + 1).gcd (1 % (n + 1)) = 1
<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✝ : CancelMonoidWithZero M₀<VAR>a b c : M₀<GOAL>a * b = a ↔ a * b = a * 1
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>m : ℕ<VAR>hm : n ≤ m<VAR>x✝ : TruncatedWittVector p m (ZMod p)<GOAL>((zmodEquivTrunc p n).symm.toRingHom.comp (truncate hm)) x✝ = ((ZMod.castHom ⋯ (ZMod (p ^ n))).comp (zmodEquivTrunc p m).symm.toRingHom) x✝
<VAR>F : Type u_1<VAR>inst✝² : AddCommGroup F<VAR>inst✝¹ : Module ℝ F<VAR>inst✝ : TopologicalSpace F<VAR>s t : Set F<VAR>hs : AmpleSet s<VAR>ht : AmpleSet t<VAR>x : F<VAR>hx : x ∈ s ∪ t<GOAL>(convexHull ℝ) (connectedComponentIn (s ∪ t) x) = univ
<VAR>ι : Type u_1<VAR>α✝ : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : TopologicalSpace α✝<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : TopologicalSpace γ<VAR>α : Type u_5<VAR>t₁ t₂ : TopologicalSpace α<VAR>Us : Set (Opens α)<VAR>hUs : IsBasis Us<GOAL>t₁ ≤ t₂ ↔ ∀ U ∈ Us, IsOpen ↑U
<VAR>ι : Type u_1<VAR>α✝ : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : TopologicalSpace α✝<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : TopologicalSpace γ<VAR>α : Type u_5<VAR>t₁ t₂ : TopologicalSpace α<VAR>Us : Set (Opens α)<VAR>hUs : IsBasis Us<GOAL>t₁ ≤ generateFrom (SetLike.coe '' Us) ↔ ∀ U ∈ Us, IsOpen ↑U
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν : Measure α<VAR>s : SignedMeasure α<VAR>μ : Measure α<GOAL>s.singularPart μ ⟂ᵥ μ.toENNRealVectorMeasure
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν : Measure α<VAR>s : SignedMeasure α<VAR>μ : Measure α<GOAL>s.toJordanDecomposition.posPart.singularPart μ + s.toJordanDecomposition.negPart.singularPart μ ⟂ₘ μ
<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>inst✝⁴ : DivisionRing K<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module K V<VAR>inst✝ : Module K V'<VAR>v✝ : ι → V<VAR>s t : Set V<VAR>x y z : V<VAR>n : ℕ<VAR>v : Fin n → V<GOAL>LinearIndependent K (Fin.cons x v) ↔ LinearIndependent K v ∧ x ∉ span K (range v)
<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>inst✝⁴ : DivisionRing K<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module K V<VAR>inst✝ : Module K V'<VAR>v✝ : ι → V<VAR>s t : Set V<VAR>x y z : V<VAR>n : ℕ<VAR>v : Fin n → V<GOAL>LinearIndependent K ((Fin.cons x v ∘ ⇑(finSuccEquiv n).symm) ∘ some) ∧ (Fin.cons x v ∘ ⇑(finSuccEquiv n).symm) none ∉ span K (range ((Fin.cons x v ∘ ⇑(finSuccEquiv n).symm) ∘ some)) ↔ LinearIndependent K v ∧ x ∉ span K (range v)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Multiset α<GOAL>card s.antidiagonal = 2 ^ card s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Multiset α<VAR>this : card s.powerset = 2 ^ card s<GOAL>card s.antidiagonal = 2 ^ card s
<VAR>α✝ : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>α : Sort u_3<VAR>x y : α<VAR>dist : α → α → ℝ<VAR>dist_self : ∀ (x : α), dist x x = 0<VAR>dist_comm : ∀ (x y : α), dist x y = dist y x<VAR>dist_triangle : ∀ (x y z : α), dist x z ≤ dist x y + dist y z<GOAL>dist x y + dist y x = 2 * dist x y
<VAR>α : Type u_1<VAR>β : Type u_2<GOAL>Nat.card α ≠ 0 ↔ Nonempty α ∧ Finite α
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : NormalSpace Y<VAR>f : X →ᵇ ℝ<VAR>e : X → Y<VAR>he : ClosedEmbedding e<GOAL>∃ g, ‖g‖ = ‖f‖ ∧ ⇑g ∘ e = ⇑f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : NormalSpace Y<VAR>e : X → Y<VAR>he : ClosedEmbedding e<VAR>g : Y →ᵇ ℝ<VAR>hg : ‖g‖ = ‖g.compContinuous { toFun := e, continuous_toFun := ⋯ }‖<GOAL>∃ g_1, ‖g_1‖ = ‖g.compContinuous { toFun := e, continuous_toFun := ⋯ }‖ ∧ ⇑g_1 ∘ e = ⇑(g.compContinuous { toFun := e, continuous_toFun := ⋯ })
<VAR>ι : Type u_1<VAR>k : ℕ<VAR>m : Multiset ℕ<GOAL>k.Coprime m.prod ↔ ∀ n ∈ m, k.Coprime n
<VAR>ι : Type u_1<VAR>k : ℕ<VAR>a✝ : List ℕ<GOAL>k.Coprime (Multiset.prod ⟦a✝⟧) ↔ ∀ n ∈ ⟦a✝⟧, k.Coprime n
<VAR>C : Type u<VAR>inst✝ : Groupoid C<VAR>S✝ S : Subgroupoid C<VAR>Sw : S.IsWide<VAR>c : C<GOAL>eqToHom ⋯ ∈ S.arrows c c
<VAR>C : Type u<VAR>inst✝ : Groupoid C<VAR>S✝ S : Subgroupoid C<VAR>Sw : S.IsWide<VAR>c : C<GOAL>𝟙 c ∈ S.arrows c c
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<GOAL>↑(Pi.basisFun ℝ ι).parallelepiped = ↑(PositiveCompacts.piIcc01 ι)
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<GOAL>↑(Pi.basisFun ℝ ι).parallelepiped = uIcc (fun i => 0) fun i => 1
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<GOAL>(fun i => 0) ≤ fun i => 1
<VAR>V : Type u<VAR>inst✝ : Quiver V<VAR>X✝¹ Y✝ X Y : Paths (Quiver.Symmetrify V)<VAR>X✝ Z : Quiver.Symmetrify V<VAR>f : X✝ ⟶ Z<VAR>XW : X✝¹ ⟶ Paths.of.obj X✝<VAR>WY : Paths.of.obj X✝ ⟶ Y✝<VAR>this : Quotient.CompClosure redStep (Quiver.Path.reverse WY ≫ 𝟙 (Paths.of.obj X✝) ≫ Quiver.Path.reverse XW) (Quiver.Path.reverse WY ≫ (f.toPath ≫ (Quiver.reverse f).toPath) ≫ Quiver.Path.reverse XW)<GOAL>Quotient.CompClosure redStep (Quiver.Path.reverse (XW ≫ 𝟙 (Paths.of.obj X✝) ≫ WY)) (Quiver.Path.reverse (XW ≫ (f.toPath ≫ (Quiver.reverse f).toPath) ≫ WY))
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>X : SimplicialObject C<VAR>n : ℕ<GOAL>(𝟙 K[X] - PInfty).f n ≫ PInfty.f n = 0
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<GOAL>(o.oangle x (x + y)).cos * ‖x + y‖ = ‖x‖
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<VAR>hs : (o.oangle x (x + y)).sign = 1<GOAL>(o.oangle x (x + y)).cos * ‖x + y‖ = ‖x‖
<VAR>α✝ : Type u<VAR>β : Type v<VAR>ι✝ : Sort w<VAR>γ : Type x<VAR>s✝ t : Set α✝<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>inst✝³ : Preorder ι'<VAR>inst✝² : Nonempty ι'<VAR>inst✝¹ : IsDirected ι' fun x x_1 => x ≤ x_1<VAR>inst✝ : Order.Frame α<VAR>s : Set ι<VAR>hs : s.Finite<VAR>f : ι → ι' → α<VAR>hf : ∀ i ∈ s, Monotone (f i)<GOAL>⨆ j, ⨅ i ∈ s, f i j = ⨅ i ∈ s, ⨆ j, f i j
<VAR>α✝ : Type u<VAR>β : Type v<VAR>ι✝ : Sort w<VAR>γ : Type x<VAR>s✝ t : Set α✝<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>inst✝³ : Preorder ι'<VAR>inst✝² : Nonempty ι'<VAR>inst✝¹ : IsDirected ι' fun x x_1 => x ≤ x_1<VAR>inst✝ : Order.Frame α<VAR>s : Set ι<VAR>f : ι → ι' → α<VAR>hf : ∀ i ∈ ∅, Monotone (f i)<GOAL>⨆ j, ⨅ i ∈ ∅, f i j = ⨅ i ∈ ∅, ⨆ j, f i j
<VAR>α✝ : Type u<VAR>β : Type v<VAR>ι✝ : Sort w<VAR>γ : Type x<VAR>s✝¹ t : Set α✝<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>inst✝³ : Preorder ι'<VAR>inst✝² : Nonempty ι'<VAR>inst✝¹ : IsDirected ι' fun x x_1 => x ≤ x_1<VAR>inst✝ : Order.Frame α<VAR>s✝ : Set ι<VAR>f : ι → ι' → α<VAR>a : ι<VAR>s : Set ι<VAR>a✝ : a ∉ s<VAR>h✝ : s.Finite<VAR>ihs : (∀ i ∈ s, Monotone (f i)) → ⨆ j, ⨅ i ∈ s, f i j = ⨅ i ∈ s, ⨆ j, f i j<VAR>hf : ∀ i ∈ insert a s, Monotone (f i)<GOAL>⨆ j, ⨅ i ∈ insert a s, f i j = ⨅ i ∈ insert a s, ⨆ j, f i j
<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>f : ι → α<VAR>val✝ : Multiset ι<VAR>l : List ι<VAR>hl : Multiset.Nodup (Quot.mk Setoid.r l)<VAR>hs : { val := Quot.mk Setoid.r l, nodup := hl }.Nonempty<VAR>this : List.map f l ≠ []<GOAL>‖∏ i ∈ { val := Quot.mk Setoid.r l, nodup := hl }, f i‖ ≤ ∏ i ∈ { val := Quot.mk Setoid.r l, nodup := hl }, ‖f i‖
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : L.Structure N<VAR>inst✝ : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>φ : L ≃ᴸ L'<GOAL>Function.LeftInverse φ.invLHom.onTerm φ.toLHom.onTerm
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : L.Structure N<VAR>inst✝ : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>φ : L ≃ᴸ L'<GOAL>Function.RightInverse φ.invLHom.onTerm φ.toLHom.onTerm
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>σ : Type u_3<VAR>inst✝ : CanonicallyLinearOrderedAddCommMonoid M<VAR>w : σ → M<VAR>φ : MvPolynomial σ R<VAR>hw : NonTorsionWeight w<VAR>m : σ →₀ ℕ<GOAL>(weight w) m = 0 ↔ ∀ (x : σ), m x = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>σ : Type u_3<VAR>inst✝ : CanonicallyLinearOrderedAddCommMonoid M<VAR>w : σ → M<VAR>φ : MvPolynomial σ R<VAR>hw : NonTorsionWeight w<VAR>m : σ →₀ ℕ<GOAL>(m.sum fun i c => c • w i) = 0 ↔ ∀ (x : σ), m x = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>σ : Type u_3<VAR>inst✝ : CanonicallyLinearOrderedAddCommMonoid M<VAR>w : σ → M<VAR>φ : MvPolynomial σ R<VAR>hw : NonTorsionWeight w<VAR>m : σ →₀ ℕ<GOAL>(∀ x ∈ m.support, m x • w x = 0) ↔ ∀ (x : σ), m x = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>σ : Type u_3<VAR>inst✝ : CanonicallyLinearOrderedAddCommMonoid M<VAR>w : σ → M<VAR>φ : MvPolynomial σ R<VAR>hw : NonTorsionWeight w<VAR>m : σ →₀ ℕ<GOAL>∀ (a : σ), a ∈ m.support → m a • w a = 0 ↔ m a = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>σ : Type u_3<VAR>inst✝ : CanonicallyLinearOrderedAddCommMonoid M<VAR>w : σ → M<VAR>φ : MvPolynomial σ R<VAR>hw : NonTorsionWeight w<VAR>m : σ →₀ ℕ<VAR>x : σ<GOAL>x ∈ m.support → m x • w x = 0 ↔ m x = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>σ : Type u_3<VAR>inst✝ : CanonicallyLinearOrderedAddCommMonoid M<VAR>w : σ → M<VAR>φ : MvPolynomial σ R<VAR>hw : NonTorsionWeight w<VAR>m : σ →₀ ℕ<VAR>x : σ<GOAL>m x ≠ 0 → m x • w x = 0 ↔ m x = 0
<VAR>α : Type u_1<VAR>inst✝ : OrderedCancelCommMonoid α<VAR>s : Submonoid α<VAR>a₁ b₁ : α<VAR>a₂ b₂ b✝ : ↥s<VAR>a b : α<GOAL>{ toFun := fun a => mk a b✝, inj' := ⋯ } a ≤ { toFun := fun a => mk a b✝, inj' := ⋯ } b ↔ a ≤ b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s t m : Multiset α<GOAL>m.dedup.toFinset = m.toFinset
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>f : α → β<VAR>s : (i : ι) → κ i → Set α<GOAL>f '' ⋃ i, ⋃ j, s i j = ⋃ i, ⋃ j, f '' s i j
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝³ : CommRing R<VAR>inst✝² : Ring S<VAR>f : R[X]<VAR>inst✝¹ : Algebra R S<VAR>T : Type u_1<VAR>inst✝ : CommRing T<VAR>i : R →+* T<VAR>x : T<VAR>hx : eval₂ i x f = 0<VAR>h : IsAdjoinRoot S f<GOAL>(lift i x hx h) h.root = x
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>H K : Subgroup G<VAR>S T : Set G<VAR>hST : IsComplement S T<VAR>hHT : IsComplement (↑H) T<VAR>hSK : IsComplement S ↑K<VAR>g : G<GOAL>LeftCosetEquivalence (↑K) g ↑(hSK.equiv g).1
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>H K : Subgroup G<VAR>S T : Set G<VAR>hST : IsComplement S T<VAR>hHT : IsComplement (↑H) T<VAR>hSK : IsComplement S ↑K<VAR>g : G<GOAL>LeftCosetEquivalence (↑K) g (g * (↑(hSK.equiv g).2)⁻¹)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>s : Set α<VAR>t : Set β<VAR>hs : s.Countable<VAR>ht : t.Countable<VAR>f : α → β → γ<GOAL>(Set.image2 f s t).Countable
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>s : Set α<VAR>t : Set β<VAR>hs : s.Countable<VAR>ht : t.Countable<VAR>f : α → β → γ<GOAL>((fun x => f x.1 x.2) '' s ×ˢ t).Countable
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>M' : Type u_4<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : LieRingModule L M'<VAR>inst✝ : LieModule R L M'<VAR>N N₁ N₂ : LieSubmodule R L M<VAR>m : M<VAR>hm : m ∈ N<GOAL>m ∈ N.normalizer
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>M' : Type u_4<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : LieRingModule L M'<VAR>inst✝ : LieModule R L M'<VAR>N N₁ N₂ : LieSubmodule R L M<VAR>m : M<VAR>hm : m ∈ N<GOAL>∀ (x : L), ⁅x, m⁆ ∈ N
<VAR>R : Type u_1<VAR>inst✝¹ : DivisionRing R<VAR>inst✝ : CharZero R<VAR>p r : R<VAR>z : ℤ<VAR>hz : z ≠ 0<GOAL>(∃ k, k • p = z • r) ↔ ∃ k, r - ↑k • (p / ↑z) ∈ zmultiples p
<VAR>R : Type u_1<VAR>inst✝¹ : DivisionRing R<VAR>inst✝ : CharZero R<VAR>p r : R<VAR>z : ℤ<VAR>hz : z ≠ 0<GOAL>(∃ k, k • p = z • r) ↔ ∃ k k_1, k_1 • p + ↑k • p * (↑z)⁻¹ = r
<VAR>R : Type u_1<VAR>inst✝¹ : DivisionRing R<VAR>inst✝ : CharZero R<VAR>p r : R<VAR>z : ℤ<VAR>hz : z ≠ 0<VAR>hz' : ↑z ≠ 0<GOAL>(∃ k, k • p = z • r) ↔ ∃ k k_1, k_1 • p + ↑k • p * (↑z)⁻¹ = r
<VAR>R : Type u_1<VAR>inst✝¹ : DivisionRing R<VAR>inst✝ : CharZero R<VAR>p r : R<VAR>z : ℤ<VAR>hz : z ≠ 0<VAR>hz' : ↑z ≠ 0<GOAL>(∃ k, k • p = z • r) ↔ ∃ k k_1, ↑z * (k_1 • p + ↑k • p * (↑z)⁻¹) = ↑z * r
<VAR>R : Type u_1<VAR>inst✝¹ : DivisionRing R<VAR>inst✝ : CharZero R<VAR>p r : R<VAR>z : ℤ<VAR>hz : z ≠ 0<VAR>hz' : ↑z ≠ 0<GOAL>(∃ k, k • p = z • r) ↔ ∃ k k_1, (z * k_1 + ↑↑k) • p = z • r
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a✝ b✝ c✝ d a b c : α<GOAL>filter (fun x => x < c) (Ico a b) = Ico a (min b c)
<VAR>F : Type u_1<VAR>inst✝¹ : NormedField F<VAR>inst✝ : CompleteSpace F<VAR>f : ℕ →* F<VAR>hsum : Summable ⇑f<VAR>N : ℕ<GOAL>∏ p ∈ N.primesBelow, (1 - f p)⁻¹ = ∑' (m : ↑N.smoothNumbers), f ↑m
<VAR>F : Type u_1<VAR>inst✝¹ : NormedField F<VAR>inst✝ : CompleteSpace F<VAR>f : ℕ →* F<VAR>hsum : Summable ⇑f<VAR>N : ℕ<GOAL>∏ p ∈ filter (fun p => Nat.Prime p) (range N), (1 - f p)⁻¹ = ∑' (m : ↑(factoredNumbers (range N))), f ↑m
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace 𝕜 F<VAR>K : Submodule 𝕜 E<VAR>x : E<GOAL>x ∈ ⊤ᗮ ↔ x ∈ ⊥
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace 𝕜 F<VAR>K : Submodule 𝕜 E<VAR>x : E<GOAL>(∀ u ∈ ⊤, ⟪u, x⟫_𝕜 = 0) ↔ x = 0
<VAR>α : Type u_1<VAR>inst✝ : Ring α<VAR>na nb nc : ℤ<VAR>da db dc k : ℕ<VAR>inv✝¹ : Invertible ↑da<VAR>inv✝ : Invertible ↑db<VAR>h₁ : na * nb = ↑k * nc<VAR>h₂ : da * db = k * dc<VAR>this✝ : Invertible ↑(da * db)<VAR>this : Invertible ↑dc<GOAL>↑na * ⅟↑da * (↑nb * ⅟↑db) = ↑nc * ⅟↑dc
<VAR>α : Type u_1<VAR>inst✝ : Ring α<VAR>na nb nc : ℤ<VAR>da db dc k : ℕ<VAR>inv✝¹ : Invertible ↑da<VAR>inv✝ : Invertible ↑db<VAR>h₁ : na * nb = ↑k * nc<VAR>h₂ : da * db = k * dc<VAR>this✝ : Invertible ↑(da * db)<VAR>this : Invertible ↑dc<VAR>H : ∀ (a : α), a * ⅟↑da * ⅟↑db = a * ⅟↑db * ⅟↑da<GOAL>↑na * ⅟↑da * (↑nb * ⅟↑db) = ↑nc * ⅟↑dc
<VAR>α : Type u_1<VAR>inst✝ : Ring α<VAR>na nb nc : ℤ<VAR>da db dc k : ℕ<VAR>inv✝¹ : Invertible ↑da<VAR>inv✝ : Invertible ↑db<VAR>h₁✝ : na * nb = ↑k * nc<VAR>h₂ : da * db = k * dc<VAR>this✝ : Invertible ↑(da * db)<VAR>this : Invertible ↑dc<VAR>H : ∀ (a : α), a * ⅟↑da * ⅟↑db = a * ⅟↑db * ⅟↑da<VAR>h₁ : ↑(na * nb) = ↑(↑k * nc)<GOAL>↑na * ⅟↑da * (↑nb * ⅟↑db) = ↑nc * ⅟↑dc
<VAR>α : Type u_1<VAR>inst✝ : Ring α<VAR>na nb nc : ℤ<VAR>da db dc k : ℕ<VAR>inv✝¹ : Invertible ↑da<VAR>inv✝ : Invertible ↑db<VAR>h₁✝ : na * nb = ↑k * nc<VAR>h₂ : da * db = k * dc<VAR>this✝ : Invertible ↑(da * db)<VAR>this : Invertible ↑dc<VAR>H : ∀ (a : α), a * ⅟↑da * ⅟↑db = a * ⅟↑db * ⅟↑da<VAR>h₁ : ↑na * ↑nb = ↑k * ↑nc<GOAL>↑na * ⅟↑da * (↑nb * ⅟↑db) = ↑nc * ⅟↑dc
<VAR>α : Type u_1<VAR>inst✝ : Ring α<VAR>na nb nc : ℤ<VAR>da db dc k : ℕ<VAR>inv✝¹ : Invertible ↑da<VAR>inv✝ : Invertible ↑db<VAR>h₁✝ : na * nb = ↑k * nc<VAR>h₂ : da * db = k * dc<VAR>this✝ : Invertible ↑(da * db)<VAR>this : Invertible ↑dc<VAR>H : ∀ (a : α), a * ⅟↑da * ⅟↑db = a * ⅟↑db * ⅟↑da<VAR>h₁ : ↑na * ↑nb = ↑k * ↑nc<GOAL>↑k * ↑nc * ⅟↑da * ⅟↑db = ↑nc * ⅟↑dc
<VAR>α : Type u_1<VAR>inst✝ : Ring α<VAR>na nb nc : ℤ<VAR>da db dc k : ℕ<VAR>inv✝¹ : Invertible ↑da<VAR>inv✝ : Invertible ↑db<VAR>h₁✝ : na * nb = ↑k * nc<VAR>h₂✝ : da * db = k * dc<VAR>this✝ : Invertible ↑(da * db)<VAR>this : Invertible ↑dc<VAR>H : ∀ (a : α), a * ⅟↑da * ⅟↑db = a * ⅟↑db * ⅟↑da<VAR>h₁ : ↑na * ↑nb = ↑k * ↑nc<VAR>h₂ : (fun x => ↑nc * ↑x * (⅟↑da * ⅟↑db * ⅟↑dc)) (da * db) = (fun x => ↑nc * ↑x * (⅟↑da * ⅟↑db * ⅟↑dc)) (k * dc)<GOAL>↑k * ↑nc * ⅟↑da * ⅟↑db = ↑nc * ⅟↑dc
<VAR>α : Type u_1<VAR>inst✝ : Ring α<VAR>na nb nc : ℤ<VAR>da db dc k : ℕ<VAR>inv✝¹ : Invertible ↑da<VAR>inv✝ : Invertible ↑db<VAR>h₁✝ : na * nb = ↑k * nc<VAR>h₂✝ : da * db = k * dc<VAR>this✝ : Invertible ↑(da * db)<VAR>this : Invertible ↑dc<VAR>H : ∀ (a : α), a * ⅟↑da * ⅟↑db = a * ⅟↑db * ⅟↑da<VAR>h₁ : ↑na * ↑nb = ↑k * ↑nc<VAR>h₂ : ↑nc * ↑da * ↑db * ⅟↑da * ⅟↑db * ⅟↑dc = ↑nc * ↑k * ↑dc * ⅟↑da * ⅟↑db * ⅟↑dc<GOAL>↑k * ↑nc * ⅟↑da * ⅟↑db = ↑nc * ⅟↑dc
<VAR>α : Type u_1<VAR>inst✝ : Ring α<VAR>na nb nc : ℤ<VAR>da db dc k : ℕ<VAR>inv✝¹ : Invertible ↑da<VAR>inv✝ : Invertible ↑db<VAR>h₁✝ : na * nb = ↑k * nc<VAR>h₂✝ : da * db = k * dc<VAR>this✝ : Invertible ↑(da * db)<VAR>this : Invertible ↑dc<VAR>H : ∀ (a : α), a * ⅟↑da * ⅟↑db = a * ⅟↑db * ⅟↑da<VAR>h₁ : ↑na * ↑nb = ↑k * ↑nc<VAR>h₂ : ↑nc * ↑da * ↑db * ⅟↑db * ⅟↑da * ⅟↑dc = ↑nc * ↑k * ↑dc * ⅟↑da * ⅟↑db * ⅟↑dc<GOAL>↑k * ↑nc * ⅟↑da * ⅟↑db = ↑nc * ⅟↑dc
<VAR>α : Type u_1<VAR>inst✝ : Ring α<VAR>na nb nc : ℤ<VAR>da db dc k : ℕ<VAR>inv✝¹ : Invertible ↑da<VAR>inv✝ : Invertible ↑db<VAR>h₁✝ : na * nb = ↑k * nc<VAR>h₂✝ : da * db = k * dc<VAR>this✝ : Invertible ↑(da * db)<VAR>this : Invertible ↑dc<VAR>H : ∀ (a : α), a * ⅟↑da * ⅟↑db = a * ⅟↑db * ⅟↑da<VAR>h₁ : ↑na * ↑nb = ↑k * ↑nc<VAR>h₂ : ↑nc * ⅟↑dc = ↑nc * ↑k * ↑dc * ⅟↑da * ⅟↑db * ⅟↑dc<GOAL>↑k * ↑nc * ⅟↑da * ⅟↑db = ↑nc * ⅟↑dc
<VAR>α : Type u_1<VAR>inst✝ : Ring α<VAR>na nb nc : ℤ<VAR>da db dc k : ℕ<VAR>inv✝¹ : Invertible ↑da<VAR>inv✝ : Invertible ↑db<VAR>h₁✝ : na * nb = ↑k * nc<VAR>h₂✝ : da * db = k * dc<VAR>this✝ : Invertible ↑(da * db)<VAR>this : Invertible ↑dc<VAR>H : ∀ (a : α), a * ⅟↑da * ⅟↑db = a * ⅟↑db * ⅟↑da<VAR>h₁ : ↑na * ↑nb = ↑k * ↑nc<VAR>h₂ : ↑nc * ⅟↑dc = ↑nc * ↑k * ↑dc * ⅟↑da * ⅟↑db * ⅟↑dc<GOAL>↑nc * ↑k * ⅟↑da * ⅟↑db = ↑nc * ↑k * ↑dc * ⅟↑da * ⅟↑db * ⅟↑dc
<VAR>m : Type u<VAR>n : Type v<VAR>α : Type w<VAR>inst✝⁵ : DecidableEq n<VAR>inst✝⁴ : Fintype n<VAR>inst✝³ : DecidableEq m<VAR>inst✝² : Fintype m<VAR>inst✝¹ : CommRing α<VAR>A✝ : Matrix n n α<VAR>b✝ : n → α<VAR>inst✝ : Subsingleton n<VAR>A : Matrix n n α<VAR>b : n → α<VAR>i : n<GOAL>A.cramer b i = b i
<VAR>a b : Cardinal.{u_1}<GOAL>a + b = a ↔ max ℵ₀ b ≤ a ∨ b = 0
<VAR>a b : Cardinal.{u_1}<GOAL>a + b = a ↔ ℵ₀ ≤ a ∧ b ≤ a ∨ b = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m✝ : OuterMeasure α<VAR>s t : Set α<VAR>m : OuterMeasure α<GOAL>((restrict s) m) t = m (t ∩ s)
<VAR>F : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝⁹ : CommSemiring R<VAR>inst✝⁸ : StarRing R<VAR>inst✝⁷ : Semiring A<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : StarRing A<VAR>inst✝⁴ : StarModule R A<VAR>inst✝³ : Semiring B<VAR>inst✝² : Algebra R B<VAR>inst✝¹ : StarRing B<VAR>inst✝ : StarModule R B<VAR>s : Set A<VAR>a✝ : A<VAR>hx : a✝ ∈ __src✝.carrier<GOAL>star a✝ ∈ __src✝.carrier
<VAR>n : ℕ<VAR>c : Composition n<VAR>j : ℕ<VAR>h : j < n<GOAL>∃ i, j < c.sizeUpTo (i + 1) ∧ i < c.length
<VAR>n : ℕ<VAR>c : Composition n<VAR>j : ℕ<VAR>h : j < n<VAR>n_pos : 0 < n<GOAL>∃ i, j < c.sizeUpTo (i + 1) ∧ i < c.length
<VAR>n : ℕ<VAR>c : Composition n<VAR>j : ℕ<VAR>h : j < n<VAR>n_pos : 0 < n<VAR>this : 0 < c.blocks.sum<GOAL>∃ i, j < c.sizeUpTo (i + 1) ∧ i < c.length
<VAR>n : ℕ<VAR>c : Composition n<VAR>j : ℕ<VAR>h : j < n<VAR>n_pos : 0 < n<VAR>this : 0 < c.blocks.sum<VAR>length_pos : 0 < c.blocks.length<GOAL>∃ i, j < c.sizeUpTo (i + 1) ∧ i < c.length
<VAR>n : ℕ<VAR>c : Composition n<VAR>j : ℕ<VAR>h : j < n<VAR>n_pos : 0 < n<VAR>this : 0 < c.blocks.sum<VAR>length_pos : 0 < c.blocks.length<GOAL>j < c.sizeUpTo (c.length - 1 + 1)
<VAR>n : ℕ<VAR>c : Composition n<VAR>j : ℕ<VAR>h : j < n<VAR>n_pos : 0 < n<VAR>this✝ : 0 < c.blocks.sum<VAR>length_pos : 0 < c.blocks.length<VAR>this : c.length - 1 + 1 = c.length<GOAL>j < c.sizeUpTo (c.length - 1 + 1)
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>P Q U : Cᵒᵖ ⥤ Type w<VAR>X Y : C<VAR>S : Sieve X<VAR>R : Presieve X<VAR>x₁ x₂ : FamilyOfElements P (generate R).arrows<VAR>t₁ : x₁.Compatible<VAR>t₂ : x₂.Compatible<VAR>h : FamilyOfElements.restrict ⋯ x₁ = FamilyOfElements.restrict ⋯ x₂<GOAL>x₁ = x₂
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>P Q U : Cᵒᵖ ⥤ Type w<VAR>X Y : C<VAR>S : Sieve X<VAR>R : Presieve X<VAR>x₁ x₂ : FamilyOfElements P (generate R).arrows<VAR>t₁ : x₁.Compatible<VAR>t₂ : x₂.Compatible<VAR>h : FamilyOfElements.restrict ⋯ x₁ = FamilyOfElements.restrict ⋯ x₂<GOAL>(FamilyOfElements.restrict ⋯ x₁).sieveExtend = (FamilyOfElements.restrict ⋯ x₂).sieveExtend
<VAR>f : ℕ → ℂ<VAR>c s a : ℂ<VAR>hf : LSeriesHasSum f s a<GOAL>LSeriesHasSum (c • f) s (c * a)
<VAR>α : Sort u_1<VAR>inst✝ : Unique α<VAR>β : α → Sort v<VAR>f : (a : α) → β a<VAR>i x✝¹ : α<VAR>x✝ : HEq i x✝¹<GOAL>HEq (f i) (Function.const α (f default) x✝¹)
<VAR>α : Sort u_1<VAR>inst✝ : Unique α<VAR>β : α → Sort v<VAR>f : (a : α) → β a<VAR>i x✝¹ : α<VAR>x✝ : HEq i x✝¹<GOAL>HEq (f default) (Function.const α (f default) x✝¹)
<VAR>R✝ S✝ : Type u<VAR>inst✝⁷ : CommRing R✝<VAR>inst✝⁶ : CommRing S✝<VAR>M : Submonoid R✝<VAR>N : Submonoid S✝<VAR>R' S' : Type u<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>f✝ : R✝ →+* S✝<VAR>inst✝³ : Algebra R✝ R'<VAR>inst✝² : Algebra S✝ S'<VAR>R S : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>s : Set R<VAR>e : Ideal.span s = ⊤<VAR>H : ∀ (r : ↑s), (fun {R S} x x_1 f => Function.Surjective ⇑f) OreLocalization.instCommRing OreLocalization.instCommRing (Localization.awayMap f ↑r)<GOAL>Function.Surjective ⇑f