ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>K : Type u<VAR>V V₁ : Type v<VAR>V' V'₁ : Type v'<VAR>V'' : Type v''<VAR>inst✝⁶ : DivisionRing K<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module K V<VAR>inst✝³ : AddCommGroup V₁<VAR>inst✝² : Module K V₁<VAR>inst✝¹ : AddCommGroup V'<VAR>inst✝ : Module K V'<VAR>n : ℕ<VAR>f : V →ₗ[K] V'<GOAL>(∃ s, (∃ t, ↑t = s ∧ t.card = n) ∧ LinearIndependent K fun (x : ↑s) => f ↑x) ↔ ∃ s, s.card = n ∧ LinearIndependent K fun (x : ↑↑s) => f ↑x
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedSemiring α<VAR>inst✝ : FloorSemiring α<VAR>a : α<VAR>n✝ : ℕ<VAR>ha : 0 ≤ a<VAR>n b : ℕ<GOAL>⌈a + ↑n⌉₊ ≤ b ↔ ⌈a⌉₊ + n ≤ b
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedSemiring α<VAR>inst✝ : FloorSemiring α<VAR>a : α<VAR>n✝ : ℕ<VAR>ha : 0 ≤ a<VAR>n b : ℕ<GOAL>↑b < a + ↑n ↔ b < ⌈a⌉₊ + n
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedSemiring α<VAR>inst✝ : FloorSemiring α<VAR>a : α<VAR>n✝ : ℕ<VAR>ha : 0 ≤ a<VAR>n b : ℕ<VAR>hb : n ≤ b<GOAL>↑b < a + ↑n ↔ b < ⌈a⌉₊ + n
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedSemiring α<VAR>inst✝ : FloorSemiring α<VAR>a : α<VAR>n✝ : ℕ<VAR>ha : 0 ≤ a<VAR>n b : ℕ<VAR>hb : b < n<GOAL>↑b < a + ↑n ↔ b < ⌈a⌉₊ + n
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>F : C ⥤ C<VAR>V V₀ V₁ V₂ : Coalgebra F<VAR>f✝ : V₀ ⟶ V₁<VAR>g : V₁ ⟶ V₂<VAR>f : V₀ ⟶ V₁<VAR>inst✝ : IsIso f.f<GOAL>V₁.str ≫ F.map (inv f.f) = inv f.f ≫ V₀.str
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>F : C ⥤ C<VAR>V V₀ V₁ V₂ : Coalgebra F<VAR>f✝ : V₀ ⟶ V₁<VAR>g : V₁ ⟶ V₂<VAR>f : V₀ ⟶ V₁<VAR>inst✝ : IsIso f.f<GOAL>V₀.str ≫ F.map f.f ≫ F.map (inv f.f) = V₀.str
<VAR>a b c : ℕ<VAR>h1 : a.pow b = c<GOAL>a.pow (2 * b + 1) = c.mul (c.mul a)
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>L : C ⥤ D<VAR>R : D ⥤ C<VAR>h : L ⊣ R<VAR>inst✝ : ∀ (X : C), Mono (h.unit.app X)<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>hfg : L.map f = L.map g<GOAL>f = g
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>L : C ⥤ D<VAR>R : D ⥤ C<VAR>h : L ⊣ R<VAR>inst✝ : ∀ (X : C), Mono (h.unit.app X)<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>hfg : L.map f = L.map g<GOAL>f ≫ h.unit.app Y = g ≫ h.unit.app Y
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>L : C ⥤ D<VAR>R : D ⥤ C<VAR>h : L ⊣ R<VAR>inst✝ : ∀ (X : C), Mono (h.unit.app X)<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>hfg : L.map f = L.map g<GOAL>(h.homEquiv X (L.obj Y)).symm (f ≫ h.unit.app Y) = (h.homEquiv X (L.obj Y)).symm (g ≫ h.unit.app Y)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : CommRing T<VAR>α : Type u_4<VAR>β : Type u_5<VAR>x y : 𝕎 R<VAR>i : ℕ<GOAL>WittVector.ghostFun i.unaryCast = ↑i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>β₂ : Type u_3<VAR>γ : Type u_4<VAR>ι : Sort u_5<VAR>ι' : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ' : ι' → Sort u_8<VAR>inst✝¹ : CompleteLattice α<VAR>f✝ g s t : ι → α<VAR>a✝ b : α<VAR>inst✝ : Nonempty ι<VAR>f : ι → α<VAR>a : α<GOAL>a ⊓ ⨅ x, f x = ⨅ x, a ⊓ f x
<VAR>α : Type u<VAR>inst✝ : LinearOrder α<VAR>a b : α<GOAL>min a b ≤ b
<VAR>E : Type u_1<VAR>inst✝ : SeminormedCommGroup E<VAR>ε δ : ℝ<VAR>s t : Set E<VAR>x y : E<GOAL>ball x δ * s = x • thickening δ s
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ✝ μ₁ μ₂ ν✝ ν₁ ν₂ μ ν : Measure α<VAR>h_ac : μ ≪ ν<VAR>h_ms : μ ⟂ₘ ν<GOAL>μ = 0
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ✝ μ₁ μ₂ ν✝ ν₁ ν₂ μ ν : Measure α<VAR>h_ac : μ ≪ ν<VAR>h_ms : μ ⟂ₘ ν<GOAL>μ ⟂ₘ μ
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>z x : K<GOAL>∃ c, ‖c‖ = 1 ∧ c * ↑‖x‖ = x
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>z : K<GOAL>∃ c, ‖c‖ = 1 ∧ c * ↑‖0‖ = 0
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>z x : K<VAR>hx : x ≠ 0<GOAL>∃ c, ‖c‖ = 1 ∧ c * ↑‖x‖ = x
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ S₄ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.HomologyData<VAR>h₂ : S₂.HomologyData<VAR>A : C<VAR>inst✝ : S.HasHomology<GOAL>(S.leftHomologyπ ≫ S.leftHomologyIso.hom) ≫ S.leftHomologyIso.inv = S.leftHomologyπ
<VAR>F✝ : Type u_1<VAR>E✝ : Type u_2<VAR>inst✝¹¹ : Field F✝<VAR>inst✝¹⁰ : Field E✝<VAR>inst✝⁹ : Algebra F✝ E✝<VAR>inst✝⁸ : FiniteDimensional F✝ E✝<VAR>inst✝⁷ : Algebra.IsSeparable F✝ E✝<VAR>F : Type u_3<VAR>E : Type u_4<VAR>inst✝⁶ : Field F<VAR>inst✝⁵ : Field E<VAR>inst✝⁴ : Algebra F E<VAR>inst✝³ : FiniteDimensional F E<VAR>inst✝² : Algebra.IsSeparable F E<VAR>A : Type u_5<VAR>inst✝¹ : Field A<VAR>inst✝ : Algebra F A<VAR>hA : ∀ (x : E), Splits (algebraMap F A) (minpoly F x)<VAR>α : E<GOAL>F⟮α⟯ = ⊤ ↔ Function.Injective fun φ => φ α
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>x✝ y z : X<VAR>ι : Type u_3<VAR>F U W : Set X<VAR>hWU : W ⊆ U<VAR>x : X<VAR>x_in : x ∈ W<VAR>hx : ∀ {y : X}, y ∈ W → JoinedIn W x y<GOAL>IsPathConnected (Subtype.val ⁻¹' W)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>x✝ y z : X<VAR>ι : Type u_3<VAR>F U W : Set X<VAR>hWU : W ⊆ U<VAR>x : X<VAR>x_in : x ∈ W<VAR>hx : ∀ {y : X}, y ∈ W → JoinedIn W x y<GOAL>∀ {y : { x // x ∈ U }}, y ∈ Subtype.val ⁻¹' W → JoinedIn (Subtype.val ⁻¹' W) ⟨x, ⋯⟩ y
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>x✝ y✝ z : X<VAR>ι : Type u_3<VAR>F U W : Set X<VAR>hWU : W ⊆ U<VAR>x : X<VAR>x_in : x ∈ W<VAR>hx : ∀ {y : X}, y ∈ W → JoinedIn W x y<VAR>y : X<VAR>hyU : y ∈ U<VAR>hyW : ⟨y, hyU⟩ ∈ Subtype.val ⁻¹' W<GOAL>JoinedIn (Subtype.val ⁻¹' W) ⟨x, ⋯⟩ ⟨y, hyU⟩
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : CommSemiring S<VAR>inst✝⁶ : Semiring A<VAR>inst✝⁵ : Semiring B<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra S A<VAR>inst✝¹ : Algebra R B<VAR>inst✝ : IsScalarTower R S A<VAR>s t : Set A<VAR>p : A → A → Prop<VAR>a b : A<VAR>ha : a ∈ adjoin R s<VAR>hb : b ∈ adjoin R s<VAR>Hs : ∀ x ∈ s, ∀ y ∈ s, p x y<VAR>Halg : ∀ (r₁ r₂ : R), p ((algebraMap R A) r₁) ((algebraMap R A) r₂)<VAR>Halg_left : ∀ (r : R), ∀ x ∈ s, p ((algebraMap R A) r) x<VAR>Halg_right : ∀ (r : R), ∀ x ∈ s, p x ((algebraMap R A) r)<VAR>Hadd_left : ∀ (x₁ x₂ y : A), p x₁ y → p x₂ y → p (x₁ + x₂) y<VAR>Hadd_right : ∀ (x y₁ y₂ : A), p x y₁ → p x y₂ → p x (y₁ + y₂)<VAR>Hmul_left : ∀ (x₁ x₂ y : A), p x₁ y → p x₂ y → p (x₁ * x₂) y<VAR>Hmul_right : ∀ (x y₁ y₂ : A), p x y₁ → p x y₂ → p x (y₁ * y₂)<GOAL>p a b
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : CommSemiring S<VAR>inst✝⁶ : Semiring A<VAR>inst✝⁵ : Semiring B<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra S A<VAR>inst✝¹ : Algebra R B<VAR>inst✝ : IsScalarTower R S A<VAR>s t : Set A<VAR>p : A → A → Prop<VAR>a b : A<VAR>ha : a ∈ adjoin R s<VAR>hb : b ∈ adjoin R s<VAR>Hs : ∀ x ∈ s, ∀ y ∈ s, p x y<VAR>Halg : ∀ (r₁ r₂ : R), p ((algebraMap R A) r₁) ((algebraMap R A) r₂)<VAR>Halg_left : ∀ (r : R), ∀ x ∈ s, p ((algebraMap R A) r) x<VAR>Halg_right : ∀ (r : R), ∀ x ∈ s, p x ((algebraMap R A) r)<VAR>Hadd_left : ∀ (x₁ x₂ y : A), p x₁ y → p x₂ y → p (x₁ + x₂) y<VAR>Hadd_right : ∀ (x y₁ y₂ : A), p x y₁ → p x y₂ → p x (y₁ + y₂)<VAR>Hmul_left : ∀ (x₁ x₂ y : A), p x₁ y → p x₂ y → p (x₁ * x₂) y<VAR>Hmul_right : ∀ (x y₁ y₂ : A), p x y₁ → p x y₂ → p x (y₁ * y₂)<GOAL>∀ x ∈ s, p a x
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : CommSemiring S<VAR>inst✝⁶ : Semiring A<VAR>inst✝⁵ : Semiring B<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra S A<VAR>inst✝¹ : Algebra R B<VAR>inst✝ : IsScalarTower R S A<VAR>s t : Set A<VAR>p : A → A → Prop<VAR>a b : A<VAR>ha : a ∈ adjoin R s<VAR>hb : b ∈ adjoin R s<VAR>Hs : ∀ x ∈ s, ∀ y ∈ s, p x y<VAR>Halg : ∀ (r₁ r₂ : R), p ((algebraMap R A) r₁) ((algebraMap R A) r₂)<VAR>Halg_left : ∀ (r : R), ∀ x ∈ s, p ((algebraMap R A) r) x<VAR>Halg_right : ∀ (r : R), ∀ x ∈ s, p x ((algebraMap R A) r)<VAR>Hadd_left : ∀ (x₁ x₂ y : A), p x₁ y → p x₂ y → p (x₁ + x₂) y<VAR>Hadd_right : ∀ (x y₁ y₂ : A), p x y₁ → p x y₂ → p x (y₁ + y₂)<VAR>Hmul_left : ∀ (x₁ x₂ y : A), p x₁ y → p x₂ y → p (x₁ * x₂) y<VAR>Hmul_right : ∀ (x y₁ y₂ : A), p x y₁ → p x y₂ → p x (y₁ * y₂)<VAR>r : R<GOAL>p a ((algebraMap R A) r)
<VAR>m n k : ℕ<GOAL>m.gcd (n + k * m) = m.gcd n
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>inst✝² : Group G<VAR>inst✝¹ : MulAction G α<VAR>inst✝ : DecidableEq α<VAR>S : Set G<VAR>T : Set α<VAR>a : α<VAR>hS : ∀ g ∈ S, g⁻¹ ∈ S<VAR>subset : T ⊆ orbit (↥(closure S)) a<VAR>not_mem : a ∉ T<VAR>nonempty : T.Nonempty<GOAL>∃ σ ∈ S, ∃ a ∈ T, σ • a ∉ T
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>inst✝² : Group G<VAR>inst✝¹ : MulAction G α<VAR>inst✝ : DecidableEq α<VAR>S : Set G<VAR>T : Set α<VAR>a : α<VAR>hS : ∀ g ∈ S, g⁻¹ ∈ S<VAR>subset : T ⊆ orbit (↥(closure S)) a<VAR>not_mem : a ∉ T<VAR>nonempty : T.Nonempty<VAR>key0 : ¬closure S ≤ stabilizer G T<GOAL>∃ σ ∈ S, ∃ a ∈ T, σ • a ∉ T
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>inst✝² : Group G<VAR>inst✝¹ : MulAction G α<VAR>inst✝ : DecidableEq α<VAR>S : Set G<VAR>T : Set α<VAR>a : α<VAR>hS : ∀ g ∈ S, g⁻¹ ∈ S<VAR>subset : T ⊆ orbit (↥(closure S)) a<VAR>not_mem : a ∉ T<VAR>nonempty : T.Nonempty<VAR>key0 : ∀ σ ∈ S, ∀ a ∈ T, σ • a ∈ T<GOAL>closure S ≤ stabilizer G T
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>inst✝² : Group G<VAR>inst✝¹ : MulAction G α<VAR>inst✝ : DecidableEq α<VAR>S : Set G<VAR>T : Set α<VAR>a : α<VAR>hS : ∀ g ∈ S, g⁻¹ ∈ S<VAR>subset : T ⊆ orbit (↥(closure S)) a<VAR>not_mem : a ∉ T<VAR>nonempty : T.Nonempty<VAR>key0 : ∀ σ ∈ S, ∀ a ∈ T, σ • a ∈ T<VAR>σ : G<VAR>hσ : σ ∈ S<GOAL>σ ∈ ↑(stabilizer G T)
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>inst✝² : Group G<VAR>inst✝¹ : MulAction G α<VAR>inst✝ : DecidableEq α<VAR>S : Set G<VAR>T : Set α<VAR>a : α<VAR>hS : ∀ g ∈ S, g⁻¹ ∈ S<VAR>subset : T ⊆ orbit (↥(closure S)) a<VAR>not_mem : a ∉ T<VAR>nonempty : T.Nonempty<VAR>key0 : ∀ σ ∈ S, ∀ a ∈ T, σ • a ∈ T<VAR>σ : G<VAR>hσ : σ ∈ S<GOAL>∀ (x : α), σ⁻¹ • x ∈ T ↔ x ∈ T
<VAR>A B : Grp<VAR>f : A ⟶ B<VAR>b b' : ↑B<VAR>x : X'<VAR>y : ↑(Set.range fun x => x • ↑(MonoidHom.range f))<GOAL>fromCoset ⟨(b * b') • ↑y, ⋯⟩ = fromCoset ⟨b • ↑⟨b' • ↑y, ⋯⟩, ⋯⟩
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>p q : R[X]<VAR>h : Associated p q<VAR>u : R[X]ˣ<VAR>hu : p * ↑u = q<GOAL>p.degree = q.degree
<VAR>𝓕 : Type u_1<VAR>𝕜 : Type u_2<VAR>α : Type u_3<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>E : Type u_6<VAR>F : Type u_7<VAR>G : Type u_8<VAR>inst✝² : SeminormedGroup E<VAR>inst✝¹ : SeminormedGroup F<VAR>inst✝ : SeminormedGroup G<VAR>s : Set E<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>h : b ∈ ball a r<GOAL>‖b / a‖ < r
<VAR>R : Type uR<VAR>inst✝⁴ : Semiring R<VAR>S : Type uS<VAR>inst✝³ : CommSemiring S<VAR>T : Type uT<VAR>A : Type uA<VAR>inst✝² : Semiring A<VAR>inst✝¹ : Algebra S A<VAR>r : R → R → Prop<VAR>inst✝ : Semiring T<VAR>s : A → A → Prop<VAR>x y : A<VAR>w : s x y<GOAL>(mkAlgHom S s) x = (mkAlgHom S s) y
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>P : Type u_5<VAR>M₀ : Type u_6<VAR>G : Type u_7<VAR>R : Type u_8<VAR>inst✝ : OrderedCommMonoid M<VAR>a b : M<VAR>l : List M<VAR>hl₁ : ∀ x ∈ a :: b :: l, 1 < x<VAR>x✝ : a :: b :: l ≠ []<GOAL>1 < (a :: b :: l).prod
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>P : Type u_5<VAR>M₀ : Type u_6<VAR>G : Type u_7<VAR>R : Type u_8<VAR>inst✝ : OrderedCommMonoid M<VAR>a b : M<VAR>l : List M<VAR>x✝ : a :: b :: l ≠ []<VAR>hl₁ : 1 < a ∧ 1 < b ∧ ∀ a ∈ l, 1 < a<GOAL>1 < (a :: b :: l).prod
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>P : Type u_5<VAR>M₀ : Type u_6<VAR>G : Type u_7<VAR>R : Type u_8<VAR>inst✝ : OrderedCommMonoid M<VAR>a b : M<VAR>l : List M<VAR>x✝ : a :: b :: l ≠ []<VAR>hl₁ : 1 < a ∧ 1 < b ∧ ∀ a ∈ l, 1 < a<GOAL>1 < a * (b :: l).prod
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>P : Type u_5<VAR>M₀ : Type u_6<VAR>G : Type u_7<VAR>R : Type u_8<VAR>inst✝ : OrderedCommMonoid M<VAR>a b : M<VAR>l : List M<VAR>x✝ : a :: b :: l ≠ []<VAR>hl₁ : 1 < a ∧ 1 < b ∧ ∀ a ∈ l, 1 < a<GOAL>1 ≤ (b :: l).prod
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>P : Type u_5<VAR>M₀ : Type u_6<VAR>G : Type u_7<VAR>R : Type u_8<VAR>inst✝ : OrderedCommMonoid M<VAR>a b : M<VAR>l : List M<VAR>x✝ : a :: b :: l ≠ []<VAR>hl₁ : 1 < a ∧ 1 < b ∧ ∀ a ∈ l, 1 < a<GOAL>∀ x ∈ b :: l, 1 < x
<VAR>G : Type u_1<VAR>inst✝¹³ : Group G<VAR>inst✝¹² : MeasurableSpace G<VAR>inst✝¹¹ : TopologicalSpace G<VAR>inst✝¹⁰ : TopologicalGroup G<VAR>inst✝⁹ : BorelSpace G<VAR>inst✝⁸ : PolishSpace G<VAR>Γ : Subgroup G<VAR>inst✝⁷ : Countable ↥Γ<VAR>inst✝⁶ : Γ.Normal<VAR>inst✝⁵ : T2Space (G ⧸ Γ)<VAR>inst✝⁴ : SecondCountableTopology (G ⧸ Γ)<VAR>μ : Measure (G ⧸ Γ)<VAR>ν : Measure G<VAR>inst✝³ : ν.IsMulLeftInvariant<VAR>inst✝² : ν.IsMulRightInvariant<VAR>inst✝¹ : SigmaFinite ν<VAR>hasFun : HasFundamentalDomain (↥Γ.op) G ν<VAR>inst✝ : QuotientMeasureEqMeasurePreimage ν μ<VAR>x : G ⧸ Γ<VAR>A : Set (G ⧸ Γ)<VAR>hA : MeasurableSet A<GOAL>(map (fun x_1 => x * x_1) μ) A = μ A
<VAR>G : Type u_1<VAR>inst✝¹³ : Group G<VAR>inst✝¹² : MeasurableSpace G<VAR>inst✝¹¹ : TopologicalSpace G<VAR>inst✝¹⁰ : TopologicalGroup G<VAR>inst✝⁹ : BorelSpace G<VAR>inst✝⁸ : PolishSpace G<VAR>Γ : Subgroup G<VAR>inst✝⁷ : Countable ↥Γ<VAR>inst✝⁶ : Γ.Normal<VAR>inst✝⁵ : T2Space (G ⧸ Γ)<VAR>inst✝⁴ : SecondCountableTopology (G ⧸ Γ)<VAR>μ : Measure (G ⧸ Γ)<VAR>ν : Measure G<VAR>inst✝³ : ν.IsMulLeftInvariant<VAR>inst✝² : ν.IsMulRightInvariant<VAR>inst✝¹ : SigmaFinite ν<VAR>hasFun : HasFundamentalDomain (↥Γ.op) G ν<VAR>inst✝ : QuotientMeasureEqMeasurePreimage ν μ<VAR>x : G ⧸ Γ<VAR>A : Set (G ⧸ Γ)<VAR>hA : MeasurableSet A<VAR>x₁ : G<VAR>h : ⟦x₁⟧ = x<GOAL>(map (fun x_1 => x * x_1) μ) A = μ A
<VAR>G : Type u_1<VAR>inst✝¹³ : Group G<VAR>inst✝¹² : MeasurableSpace G<VAR>inst✝¹¹ : TopologicalSpace G<VAR>inst✝¹⁰ : TopologicalGroup G<VAR>inst✝⁹ : BorelSpace G<VAR>inst✝⁸ : PolishSpace G<VAR>Γ : Subgroup G<VAR>inst✝⁷ : Countable ↥Γ<VAR>inst✝⁶ : Γ.Normal<VAR>inst✝⁵ : T2Space (G ⧸ Γ)<VAR>inst✝⁴ : SecondCountableTopology (G ⧸ Γ)<VAR>μ : Measure (G ⧸ Γ)<VAR>ν : Measure G<VAR>inst✝³ : ν.IsMulLeftInvariant<VAR>inst✝² : ν.IsMulRightInvariant<VAR>inst✝¹ : SigmaFinite ν<VAR>hasFun : HasFundamentalDomain (↥Γ.op) G ν<VAR>inst✝ : QuotientMeasureEqMeasurePreimage ν μ<VAR>x : G ⧸ Γ<VAR>A : Set (G ⧸ Γ)<VAR>hA : MeasurableSet A<VAR>x₁ : G<VAR>h : ⟦x₁⟧ = x<GOAL>(map (fun x_1 => x * x_1) μ) A = μ ((fun x => x₁ • x) ⁻¹' A)
<VAR>G : Type u_1<VAR>inst✝¹³ : Group G<VAR>inst✝¹² : MeasurableSpace G<VAR>inst✝¹¹ : TopologicalSpace G<VAR>inst✝¹⁰ : TopologicalGroup G<VAR>inst✝⁹ : BorelSpace G<VAR>inst✝⁸ : PolishSpace G<VAR>Γ : Subgroup G<VAR>inst✝⁷ : Countable ↥Γ<VAR>inst✝⁶ : Γ.Normal<VAR>inst✝⁵ : T2Space (G ⧸ Γ)<VAR>inst✝⁴ : SecondCountableTopology (G ⧸ Γ)<VAR>μ : Measure (G ⧸ Γ)<VAR>ν : Measure G<VAR>inst✝³ : ν.IsMulLeftInvariant<VAR>inst✝² : ν.IsMulRightInvariant<VAR>inst✝¹ : SigmaFinite ν<VAR>hasFun : HasFundamentalDomain (↥Γ.op) G ν<VAR>inst✝ : QuotientMeasureEqMeasurePreimage ν μ<VAR>x : G ⧸ Γ<VAR>A : Set (G ⧸ Γ)<VAR>hA : MeasurableSet A<VAR>x₁ : G<VAR>h : ⟦x₁⟧ = x<GOAL>SMulInvariantMeasure G (G ⧸ Γ) μ
<VAR>α : Type u_1<VAR>inst✝² : OrderedCancelAddCommMonoid α<VAR>inst✝¹ : ExistsAddOfLE α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a b c : α<GOAL>map (fun x => c + x) (Ioc a b) = Ioc (c + a) (c + b)
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>R : Type u_5<VAR>α : Type v<VAR>β : Type w<VAR>ι : Type u_6<VAR>M : Matrix m n α<VAR>i✝ : m<VAR>j : n<VAR>b✝ : n → α<VAR>c : m → α<VAR>inst✝ : Subsingleton m<VAR>A : Matrix m n R<VAR>i : m<VAR>b : n → R<VAR>x : m<VAR>y : n<GOAL>A.updateRow i b x y = (row (Fin 1) b).submatrix (Function.const m 0) id x y
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Ring k<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>w : ι → k<VAR>p₂ : ι → P<VAR>p₁ b : P<GOAL>∑ i ∈ s, w i • (p₁ -ᵥ p₂ i) = (∑ i ∈ s, w i) • (p₁ -ᵥ b) - (s.weightedVSubOfPoint p₂ b) w
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : BooleanAlgebra α<VAR>a b c d : α<GOAL>a ⇔ (b ⇔ c) = b ⇔ (a ⇔ c)
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>α✝ : E<VAR>α β γ : ↥(solvableByRad F E)<VAR>hγ : γ ∈ F⟮α, β⟯<VAR>hα : P α<VAR>hβ : P β<VAR>p : F[X] := minpoly F α<VAR>q : F[X] := minpoly F β<GOAL>P γ
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>α✝ : E<VAR>α β γ : ↥(solvableByRad F E)<VAR>hγ : γ ∈ F⟮α, β⟯<VAR>hα : P α<VAR>hβ : P β<VAR>p : F[X] := minpoly F α<VAR>q : F[X] := minpoly F β<VAR>hpq : Splits (algebraMap F (p * q).SplittingField) (minpoly F α) ∧ Splits (algebraMap F (p * q).SplittingField) (minpoly F β)<GOAL>P γ
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>α✝ : E<VAR>α β γ : ↥(solvableByRad F E)<VAR>hγ : γ ∈ F⟮α, β⟯<VAR>hα : P α<VAR>hβ : P β<VAR>p : F[X] := minpoly F α<VAR>q : F[X] := minpoly F β<VAR>hpq : Splits (algebraMap F (p * q).SplittingField) (minpoly F α) ∧ Splits (algebraMap F (p * q).SplittingField) (minpoly F β)<VAR>f : ↥F⟮α, β⟯ →ₐ[F] (p * q).SplittingField := Classical.choice ⋯<GOAL>P γ
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>α✝ : E<VAR>α β γ : ↥(solvableByRad F E)<VAR>hγ : γ ∈ F⟮α, β⟯<VAR>hα : P α<VAR>hβ : P β<VAR>p : F[X] := minpoly F α<VAR>q : F[X] := minpoly F β<VAR>hpq : Splits (algebraMap F (p * q).SplittingField) (minpoly F α) ∧ Splits (algebraMap F (p * q).SplittingField) (minpoly F β)<VAR>f : ↥F⟮α, β⟯ →ₐ[F] (p * q).SplittingField := Classical.choice ⋯<VAR>key : minpoly F γ = minpoly F (f ⟨γ, hγ⟩)<GOAL>P γ
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>α✝ : E<VAR>α β γ : ↥(solvableByRad F E)<VAR>hγ : γ ∈ F⟮α, β⟯<VAR>hα : P α<VAR>hβ : P β<VAR>p : F[X] := minpoly F α<VAR>q : F[X] := minpoly F β<VAR>hpq : Splits (algebraMap F (p * q).SplittingField) (minpoly F α) ∧ Splits (algebraMap F (p * q).SplittingField) (minpoly F β)<VAR>f : ↥F⟮α, β⟯ →ₐ[F] (p * q).SplittingField := Classical.choice ⋯<VAR>key : minpoly F γ = minpoly F (f ⟨γ, hγ⟩)<GOAL>IsSolvable (minpoly F (f ⟨γ, hγ⟩)).Gal
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>α✝ : E<VAR>α β γ : ↥(solvableByRad F E)<VAR>hγ : γ ∈ F⟮α, β⟯<VAR>hα : P α<VAR>hβ : P β<VAR>p : F[X] := minpoly F α<VAR>q : F[X] := minpoly F β<VAR>hpq : Splits (algebraMap F (p * q).SplittingField) (minpoly F α) ∧ Splits (algebraMap F (p * q).SplittingField) (minpoly F β)<VAR>f : ↥F⟮α, β⟯ →ₐ[F] (p * q).SplittingField := Classical.choice ⋯<VAR>key : minpoly F γ = minpoly F (f ⟨γ, hγ⟩)<GOAL>Normal F (p * q).SplittingField
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LT α<VAR>a b : α<VAR>h : a < b<GOAL>¬a ⋖ b ↔ ∃ c, a < c ∧ c < b
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>α : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>f : σ → τ<VAR>φ : MvPolynomial σ R<VAR>d : τ →₀ ℕ<VAR>h : coeff d ((rename f) φ) ≠ 0<GOAL>∃ u, Finsupp.mapDomain f u = d ∧ coeff u φ ≠ 0
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>α : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>f : σ → τ<VAR>φ : MvPolynomial σ R<VAR>d : τ →₀ ℕ<VAR>h : ∀ (u : σ →₀ ℕ), Finsupp.mapDomain f u = d → coeff u φ = 0<GOAL>coeff d ((rename f) φ) = 0
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝³ : CommRing S<VAR>inst✝² : Algebra R S<VAR>P : Type u_3<VAR>inst✝¹ : CommRing P<VAR>inst✝ : IsLocalization M S<VAR>p : S[X]<VAR>b : ↥M<VAR>hb : ∀ (i : ℕ), (algebraMap R S) ((integerNormalization M p).coeff i) = ↑b • p.coeff i<VAR>i : ℕ<GOAL>(Polynomial.map (algebraMap R S) (integerNormalization M p)).coeff i = (↑b • p).coeff i
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝³ : CommRing S<VAR>inst✝² : Algebra R S<VAR>P : Type u_3<VAR>inst✝¹ : CommRing P<VAR>inst✝ : IsLocalization M S<VAR>p : S[X]<VAR>b : ↥M<VAR>hb : ∀ (i : ℕ), (algebraMap R S) ((integerNormalization M p).coeff i) = ↑b • p.coeff i<VAR>i : ℕ<GOAL>(algebraMap R S) ((integerNormalization M p).coeff i) = ↑b • p.coeff i
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s t u : Finset α<VAR>P : Finpartition s<VAR>a : α<VAR>p : Finset α<VAR>hp : p ∈ ↑P.parts<GOAL>p ∈ P.part '' ↑s
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s t u : Finset α<VAR>P : Finpartition s<VAR>a : α<VAR>p : Finset α<VAR>hp : p ∈ ↑P.parts<VAR>x : α<VAR>hx : x ∈ p<GOAL>p ∈ P.part '' ↑s
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s t u : Finset α<VAR>P : Finpartition s<VAR>a : α<VAR>p : Finset α<VAR>hp : p ∈ ↑P.parts<VAR>x : α<VAR>hx : x ∈ p<VAR>hx' : x ∈ s<GOAL>p ∈ P.part '' ↑s
<VAR>𝕜 : Type u_1<VAR>𝕝 : Type u_2<VAR>E : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝⁸ : NormedField 𝕜<VAR>inst✝⁷ : NormedRing 𝕝<VAR>inst✝⁶ : NormedSpace 𝕜 𝕝<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module 𝕜 E<VAR>inst✝³ : SMulWithZero 𝕝 E<VAR>inst✝² : IsScalarTower 𝕜 𝕝 E<VAR>s t u v A B : Set E<VAR>x : E<VAR>a b : 𝕜<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : ContinuousSMul 𝕜 E<VAR>hA : Balanced 𝕜 A<VAR>h : 0 ∈ interior A<GOAL>Balanced 𝕜 (interior A)
<VAR>𝕜 : Type u_1<VAR>𝕝 : Type u_2<VAR>E : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝⁸ : NormedField 𝕜<VAR>inst✝⁷ : NormedRing 𝕝<VAR>inst✝⁶ : NormedSpace 𝕜 𝕝<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module 𝕜 E<VAR>inst✝³ : SMulWithZero 𝕝 E<VAR>inst✝² : IsScalarTower 𝕜 𝕝 E<VAR>s t u v A B : Set E<VAR>x : E<VAR>a b : 𝕜<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : ContinuousSMul 𝕜 E<VAR>hA : Balanced 𝕜 A<VAR>h : 0 ∈ interior A<GOAL>Balanced 𝕜 (insert 0 (interior A))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>a : α<VAR>t : ℝ<GOAL>stieltjesFunctionAux f a t = ⨅ r, f a ↑r
<VAR>α : Type u_1<VAR>I B X : Set α<VAR>Indep : Set α → Prop<VAR>M : Matroid α<VAR>h : ∀ (I : Set α), M.Indep I ↔ Indep I<GOAL>∃ M_1, M.E = M_1.E ∧ M_1.Indep = Indep
<VAR>α : Type u_1<VAR>I B X E : Set α<VAR>M : Matroid α<VAR>hM : ∃ M_1, E = M_1.E ∧ ∀ (I : Set α), M_1.Indep I ↔ M.Indep I<GOAL>M.Indep ∅
<VAR>α : Type u_1<VAR>I B X E : Set α<VAR>M : Matroid α<VAR>hM : ∃ M_1, E = M_1.E ∧ ∀ (I : Set α), M_1.Indep I ↔ M.Indep I<GOAL>∀ ⦃I J : Set α⦄, M.Indep J → I ⊆ J → M.Indep I
<VAR>α : Type u_1<VAR>I B X E : Set α<VAR>M : Matroid α<VAR>hM : ∃ M_1, E = M_1.E ∧ ∀ (I : Set α), M_1.Indep I ↔ M.Indep I<GOAL>∀ ⦃I B : Set α⦄, M.Indep I → I ∉ maximals (fun x x_1 => x ⊆ x_1) {I | M.Indep I} → B ∈ maximals (fun x x_1 => x ⊆ x_1) {I | M.Indep I} → ∃ x ∈ B \ I, M.Indep (insert x I)
<VAR>α : Type u_1<VAR>I B X : Set α<VAR>M : Matroid α<VAR>hM : ∃ M_1, M.E = M_1.E ∧ ∀ (I : Set α), M_1.Indep I ↔ M.Indep I<GOAL>∀ X ⊆ M.E, ExistsMaximalSubsetProperty M.Indep X
<VAR>α : Type u_1<VAR>I B X : Set α<VAR>M : Matroid α<VAR>hM : ∃ M_1, M.E = M_1.E ∧ ∀ (I : Set α), M_1.Indep I ↔ M.Indep I<GOAL>∀ (I : Set α), M.Indep I → I ⊆ M.E
<VAR>α : Type u_1<VAR>β : α → Type u_2<VAR>inst✝ : DecidableEq α<VAR>f g : Π₀ (_a : α), ℕ<GOAL>toMultiset f ≤ toMultiset g ↔ f ≤ g