ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n✝ d✝ k N : ℕ<VAR>x : Fin n✝ → ℕ<VAR>n d : ℕ<GOAL>(range (n * (d - 1) ^ 2 + 1)).card • (↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1)) ≤ ↑(box n d).card
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝⁵ : DecidableEq n<VAR>inst✝⁴ : Fintype n<VAR>inst✝³ : DecidableEq m<VAR>inst✝² : Fintype m<VAR>R : Type v<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsEmpty n<VAR>x✝ : Matrix n n R<GOAL>x✝.det = const (Matrix n n R) 1 x✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l₁ l₂ : List α<VAR>f : α → β<VAR>H : l₁ ⊆ l₂<VAR>x : β<GOAL>x ∈ map f l₁ → x ∈ map f l₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l₁ l₂ : List α<VAR>f : α → β<VAR>H : l₁ ⊆ l₂<VAR>x : β<GOAL>(∃ a, a ∈ l₁ ∧ f a = x) → ∃ a, a ∈ l₂ ∧ f a = x
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>inst✝ : AddGroup G<VAR>T : AddTorsor G P<VAR>p : P<GOAL>p -ᵥ p = 0
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t s : Set α<VAR>ht : NullMeasurableSet t μ<GOAL>μ.restrict (s ∪ t) + μ.restrict (s ∩ t) = μ.restrict s + μ.restrict t
<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>inst✝¹ : CommMonoid β<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<VAR>hp : ∀ x ∈ s, f x ≠ 1 → p x<VAR>x : α<GOAL>x ∈ s → x ∉ filter p s → f x = 1
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f g : Perm α<VAR>p : α → Prop<VAR>x y z : α<GOAL>f.SameCycle (f⁻¹ x) y ↔ f.SameCycle x y
<VAR>Γ : Subgroup SL(2, ℤ)<VAR>k✝ : ℤ<VAR>f✝ : ℍ → ℂ<VAR>k : ℤ<VAR>A : ↥GL(2, ℝ)⁺<VAR>f g : ℍ → ℂ<VAR>x✝ : ℍ<GOAL>((f + g) ∣[k]A) x✝ = (f ∣[k]A + g ∣[k]A) x✝
<VAR>Γ : Subgroup SL(2, ℤ)<VAR>k✝ : ℤ<VAR>f✝ : ℍ → ℂ<VAR>k : ℤ<VAR>A : ↥GL(2, ℝ)⁺<VAR>f g : ℍ → ℂ<VAR>x✝ : ℍ<GOAL>(f (A • x✝) + g (A • x✝)) * ↑(↑↑A).det ^ (k - 1) * ((↑(↑↑A 1 0) * ↑x✝ + ↑(↑↑A 1 1)) ^ k)⁻¹ = f (A • x✝) * ↑(↑↑A).det ^ (k - 1) * ((↑(↑↑A 1 0) * ↑x✝ + ↑(↑↑A 1 1)) ^ k)⁻¹ + g (A • x✝) * ↑(↑↑A).det ^ (k - 1) * ((↑(↑↑A 1 0) * ↑x✝ + ↑(↑↑A 1 1)) ^ k)⁻¹
<VAR>R : Type u_1<VAR>inst✝¹¹ : CommRing R<VAR>M : Type u_2<VAR>inst✝¹⁰ : AddCommGroup M<VAR>inst✝⁹ : Module R M<VAR>M' : Type u_3<VAR>inst✝⁸ : AddCommGroup M'<VAR>inst✝⁷ : Module R M'<VAR>ι✝ : Type u_4<VAR>inst✝⁶ : DecidableEq ι✝<VAR>inst✝⁵ : Fintype ι✝<VAR>e : Basis ι✝ R M<VAR>A : Type u_5<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Module A M<VAR>κ : Type u_6<VAR>inst✝² : Fintype κ<VAR>ι : Type u_7<VAR>inst✝¹ : Finite ι<VAR>inst✝ : Nonempty ι<VAR>b : Basis ι A M<VAR>this : DecidableEq ι<GOAL>LinearMap.det 0 = 0
<VAR>R : Type u_1<VAR>inst✝¹¹ : CommRing R<VAR>M : Type u_2<VAR>inst✝¹⁰ : AddCommGroup M<VAR>inst✝⁹ : Module R M<VAR>M' : Type u_3<VAR>inst✝⁸ : AddCommGroup M'<VAR>inst✝⁷ : Module R M'<VAR>ι✝ : Type u_4<VAR>inst✝⁶ : DecidableEq ι✝<VAR>inst✝⁵ : Fintype ι✝<VAR>e : Basis ι✝ R M<VAR>A : Type u_5<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Module A M<VAR>κ : Type u_6<VAR>inst✝² : Fintype κ<VAR>ι : Type u_7<VAR>inst✝¹ : Finite ι<VAR>inst✝ : Nonempty ι<VAR>b : Basis ι A M<VAR>this : DecidableEq ι<VAR>val✝ : Fintype ι<GOAL>LinearMap.det 0 = 0
<VAR>n a b n' a' b' : ℕ<VAR>H : IsFibAux n a b<VAR>hn : 2 * n = n'<VAR>h1 : a * (2 * b - a) = a'<VAR>h2 : a * a + b * b = b'<GOAL>fib n' = a'
<VAR>n a b n' a' b' : ℕ<VAR>H : IsFibAux n a b<VAR>hn : 2 * n = n'<VAR>h1 : a * (2 * b - a) = a'<VAR>h2 : a * a + b * b = b'<GOAL>fib (n' + 1) = b'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>s : Set α<VAR>a x y : α<GOAL>dirac x ≠ dirac y ↔ ∃ A, MeasurableSet A ∧ x ∈ A ∧ y ∉ A
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>s : Set α<VAR>a x y : α<GOAL>¬dirac x ≠ dirac y ↔ ¬∃ A, MeasurableSet A ∧ x ∈ A ∧ y ∉ A
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>s : Set α<VAR>a x y : α<GOAL>(∀ (A : Set α), MeasurableSet A → (x ∈ A ↔ y ∈ A)) ↔ ∀ (x_1 : Set α), MeasurableSet x_1 → x ∈ x_1 → y ∈ x_1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>s : Set α<VAR>a x y : α<VAR>h : ∀ (x_1 : Set α), MeasurableSet x_1 → x ∈ x_1 → y ∈ x_1<VAR>A : Set α<VAR>A_mble : MeasurableSet A<GOAL>x ∈ A ↔ y ∈ A
<VAR>P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>h₁ : RespectsIso P<VAR>h₂ : ∀ ⦃R S T : Type u⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S] [inst_4 : Algebra R T], P (algebraMap R T) → P Algebra.TensorProduct.includeLeftRingHom<VAR>R S R' S' : Type u<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : CommRing S<VAR>inst✝⁸ : CommRing R'<VAR>inst✝⁷ : CommRing S'<VAR>inst✝⁶ : Algebra R S<VAR>inst✝⁵ : Algebra R R'<VAR>inst✝⁴ : Algebra R S'<VAR>inst✝³ : Algebra S S'<VAR>inst✝² : Algebra R' S'<VAR>inst✝¹ : IsScalarTower R S S'<VAR>inst✝ : IsScalarTower R R' S'<VAR>h : Algebra.IsPushout R S R' S'<VAR>H : P (algebraMap R S)<GOAL>P (algebraMap R' S')
<VAR>P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>h₁ : RespectsIso P<VAR>h₂ : ∀ ⦃R S T : Type u⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S] [inst_4 : Algebra R T], P (algebraMap R T) → P Algebra.TensorProduct.includeLeftRingHom<VAR>R S R' S' : Type u<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : CommRing S<VAR>inst✝⁸ : CommRing R'<VAR>inst✝⁷ : CommRing S'<VAR>inst✝⁶ : Algebra R S<VAR>inst✝⁵ : Algebra R R'<VAR>inst✝⁴ : Algebra R S'<VAR>inst✝³ : Algebra S S'<VAR>inst✝² : Algebra R' S'<VAR>inst✝¹ : IsScalarTower R S S'<VAR>inst✝ : IsScalarTower R R' S'<VAR>h : Algebra.IsPushout R S R' S'<VAR>H : P (algebraMap R S)<VAR>e : TensorProduct R R' S ≃ₛₗ[id R'] S' := ⋯.equiv<GOAL>P (algebraMap R' S')
<VAR>P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>h₁ : RespectsIso P<VAR>h₂ : ∀ ⦃R S T : Type u⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S] [inst_4 : Algebra R T], P (algebraMap R T) → P Algebra.TensorProduct.includeLeftRingHom<VAR>R S R' S' : Type u<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : CommRing S<VAR>inst✝⁸ : CommRing R'<VAR>inst✝⁷ : CommRing S'<VAR>inst✝⁶ : Algebra R S<VAR>inst✝⁵ : Algebra R R'<VAR>inst✝⁴ : Algebra R S'<VAR>inst✝³ : Algebra S S'<VAR>inst✝² : Algebra R' S'<VAR>inst✝¹ : IsScalarTower R S S'<VAR>inst✝ : IsScalarTower R R' S'<VAR>h : Algebra.IsPushout R S R' S'<VAR>H : P (algebraMap R S)<VAR>e : TensorProduct R R' S ≃ₛₗ[id R'] S' := ⋯.equiv<VAR>f' : TensorProduct R R' S →ₐ[R] S' := Algebra.TensorProduct.productMap (IsScalarTower.toAlgHom R R' S') (IsScalarTower.toAlgHom R S S')<GOAL>P (algebraMap R' S')
<VAR>P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>h₁ : RespectsIso P<VAR>h₂ : ∀ ⦃R S T : Type u⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S] [inst_4 : Algebra R T], P (algebraMap R T) → P Algebra.TensorProduct.includeLeftRingHom<VAR>R S R' S' : Type u<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : CommRing S<VAR>inst✝⁸ : CommRing R'<VAR>inst✝⁷ : CommRing S'<VAR>inst✝⁶ : Algebra R S<VAR>inst✝⁵ : Algebra R R'<VAR>inst✝⁴ : Algebra R S'<VAR>inst✝³ : Algebra S S'<VAR>inst✝² : Algebra R' S'<VAR>inst✝¹ : IsScalarTower R S S'<VAR>inst✝ : IsScalarTower R R' S'<VAR>h : Algebra.IsPushout R S R' S'<VAR>H : P (algebraMap R S)<VAR>e : TensorProduct R R' S ≃ₛₗ[id R'] S' := ⋯.equiv<VAR>f' : TensorProduct R R' S →ₐ[R] S' := Algebra.TensorProduct.productMap (IsScalarTower.toAlgHom R R' S') (IsScalarTower.toAlgHom R S S')<VAR>this : ∀ (x : TensorProduct R R' S), e x = f' x<GOAL>P (algebraMap R' S')
<VAR>P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>h₁ : RespectsIso P<VAR>h₂ : ∀ ⦃R S T : Type u⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S] [inst_4 : Algebra R T], P (algebraMap R T) → P Algebra.TensorProduct.includeLeftRingHom<VAR>R S R' S' : Type u<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : CommRing S<VAR>inst✝⁸ : CommRing R'<VAR>inst✝⁷ : CommRing S'<VAR>inst✝⁶ : Algebra R S<VAR>inst✝⁵ : Algebra R R'<VAR>inst✝⁴ : Algebra R S'<VAR>inst✝³ : Algebra S S'<VAR>inst✝² : Algebra R' S'<VAR>inst✝¹ : IsScalarTower R S S'<VAR>inst✝ : IsScalarTower R R' S'<VAR>h : Algebra.IsPushout R S R' S'<VAR>H : P (algebraMap R S)<VAR>e : TensorProduct R R' S ≃ₛₗ[id R'] S' := ⋯.equiv<VAR>f' : TensorProduct R R' S →ₐ[R] S' := Algebra.TensorProduct.productMap (IsScalarTower.toAlgHom R R' S') (IsScalarTower.toAlgHom R S S')<VAR>this : ∀ (x : TensorProduct R R' S), e x = f' x<GOAL>algebraMap R' S' = ?m.49455.toRingHom.comp Algebra.TensorProduct.includeLeftRingHom
<VAR>P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>h₁ : RespectsIso P<VAR>h₂ : ∀ ⦃R S T : Type u⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S] [inst_4 : Algebra R T], P (algebraMap R T) → P Algebra.TensorProduct.includeLeftRingHom<VAR>R S R' S' : Type u<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : CommRing S<VAR>inst✝⁸ : CommRing R'<VAR>inst✝⁷ : CommRing S'<VAR>inst✝⁶ : Algebra R S<VAR>inst✝⁵ : Algebra R R'<VAR>inst✝⁴ : Algebra R S'<VAR>inst✝³ : Algebra S S'<VAR>inst✝² : Algebra R' S'<VAR>inst✝¹ : IsScalarTower R S S'<VAR>inst✝ : IsScalarTower R R' S'<VAR>h : Algebra.IsPushout R S R' S'<VAR>H : P (algebraMap R S)<VAR>e : TensorProduct R R' S ≃ₛₗ[id R'] S' := ⋯.equiv<VAR>f' : TensorProduct R R' S →ₐ[R] S' := Algebra.TensorProduct.productMap (IsScalarTower.toAlgHom R R' S') (IsScalarTower.toAlgHom R S S')<VAR>this : ∀ (x : TensorProduct R R' S), e x = f' x<GOAL>TensorProduct R R' S ≃+* S'
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝ : Category.{v', u'} D<VAR>F₁ F₂ : C ⥤ D<VAR>app : (X : C) → F₁.obj X ⟶ F₂.obj X<VAR>X Y : C<VAR>e : X ≅ Y<VAR>he : F₁.map e.hom ≫ app Y = app X ≫ F₂.map e.hom<GOAL>F₁.map e.inv ≫ app X = app Y ≫ F₂.map e.inv
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝ : Category.{v', u'} D<VAR>F₁ F₂ : C ⥤ D<VAR>app : (X : C) → F₁.obj X ⟶ F₂.obj X<VAR>X Y : C<VAR>e : X ≅ Y<VAR>he : F₁.map e.hom ≫ app Y = app X ≫ F₂.map e.hom<GOAL>F₁.map e.hom ≫ F₁.map e.inv ≫ app X = F₁.map e.hom ≫ app Y ≫ F₂.map e.inv
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝ : Category.{v', u'} D<VAR>F₁ F₂ : C ⥤ D<VAR>app : (X : C) → F₁.obj X ⟶ F₂.obj X<VAR>X Y : C<VAR>e : X ≅ Y<VAR>he : F₁.map e.hom ≫ app Y = app X ≫ F₂.map e.hom<GOAL>F₁.map e.hom ≫ F₁.map e.inv ≫ app X = (app X ≫ F₂.map e.hom) ≫ F₂.map e.inv
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>β : ι → Type u_3<VAR>s s₁ s₂ : Set ι<VAR>t t₁ t₂ : (i : ι) → Set (α i)<VAR>i : ι<VAR>ht₁ : ∀ i ∉ s₁, t₁ i = univ<VAR>ht₂ : ∀ i ∉ s₂, t₂ i = univ<VAR>x : (i : ι) → α i<GOAL>(x ∈ (s₁ ∪ s₂).pi fun i => t₁ i ∩ t₂ i) ↔ x ∈ s₁.pi t₁ ∩ s₂.pi t₂
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>β : ι → Type u_3<VAR>s s₁ s₂ : Set ι<VAR>t t₁ t₂ : (i : ι) → Set (α i)<VAR>i : ι<VAR>ht₁ : ∀ i ∉ s₁, t₁ i = univ<VAR>ht₂ : ∀ i ∉ s₂, t₂ i = univ<VAR>x : (i : ι) → α i<GOAL>(∀ (i : ι), i ∈ s₁ ∨ i ∈ s₂ → x i ∈ t₁ i ∧ x i ∈ t₂ i) ↔ (∀ i ∈ s₁, x i ∈ t₁ i) ∧ ∀ i ∈ s₂, x i ∈ t₂ i
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>β : ι → Type u_3<VAR>s s₁ s₂ : Set ι<VAR>t t₁ t₂ : (i : ι) → Set (α i)<VAR>i✝ : ι<VAR>ht₁ : ∀ i ∉ s₁, t₁ i = univ<VAR>ht₂ : ∀ i ∉ s₂, t₂ i = univ<VAR>x : (i : ι) → α i<VAR>h : (∀ i ∈ s₁, x i ∈ t₁ i) ∧ ∀ i ∈ s₂, x i ∈ t₂ i<VAR>i : ι<VAR>hi : i ∈ s₁ ∨ i ∈ s₂<GOAL>x i ∈ t₁ i ∧ x i ∈ t₂ i
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>o : Ordinal.{u_2}<GOAL>o.cof ≤ o.card
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>o : Ordinal.{u_2}<GOAL>sInf {a | ∃ ι f, lsub f = o ∧ #ι = a} ≤ o.card
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>x y : R<VAR>M : Type v<VAR>inst✝² : Ring R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>f : End R M<VAR>p : Submodule R M<VAR>hp : p ≤ Submodule.comap f p<VAR>k : ℕ<VAR>hk : f ^ k = 0<GOAL>IsNilpotent (p.mapQ p f hp)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>x y : R<VAR>M : Type v<VAR>inst✝² : Ring R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>f : End R M<VAR>p : Submodule R M<VAR>hp : p ≤ Submodule.comap f p<VAR>k : ℕ<VAR>hk : f ^ k = 0<GOAL>p.mapQ p f hp ^ k = 0
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : Group G<VAR>inst✝ : TopologicalGroup G<VAR>s t✝ : Set G<VAR>hs : IsOpen s<VAR>t : Set G<GOAL>s * closure t = s * t
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : Group G<VAR>inst✝ : TopologicalGroup G<VAR>s t✝ : Set G<VAR>hs : IsOpen s<VAR>t : Set G<VAR>a : G<VAR>ha : a ∈ s<VAR>b : G<VAR>hb : b ∈ closure t<GOAL>a * b ∈ s * t
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : Group G<VAR>inst✝ : TopologicalGroup G<VAR>s t✝ : Set G<VAR>hs : IsOpen s<VAR>t : Set G<VAR>a : G<VAR>ha : a ∈ s<VAR>b : G<VAR>hb : ∀ (o : Set G), IsOpen o → b ∈ o → (o ∩ t).Nonempty<GOAL>a * b ∈ s * t
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : Group G<VAR>inst✝ : TopologicalGroup G<VAR>s t✝ : Set G<VAR>hs : IsOpen s<VAR>t : Set G<VAR>a : G<VAR>ha : a ∈ s<VAR>b : G<VAR>hb : ∀ (o : Set G), IsOpen o → b ∈ o → (o ∩ t).Nonempty<VAR>hbU : b ∈ s⁻¹ * {a * b}<GOAL>a * b ∈ s * t
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : Group G<VAR>inst✝ : TopologicalGroup G<VAR>s t✝ : Set G<VAR>hs : IsOpen s<VAR>t : Set G<VAR>a : G<VAR>ha : a ∈ s<VAR>b : G<VAR>hb : ∀ (o : Set G), IsOpen o → b ∈ o → (o ∩ t).Nonempty<VAR>hbU : b ∈ s⁻¹ * {a * b}<VAR>c : G<VAR>hc : c ∈ s⁻¹<VAR>hcs : (fun x x_1 => x * x_1) c (a * b) ∈ t<GOAL>a * b ∈ s * t
<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>P' : Cᵒᵖ ⥤ Type w<VAR>i : P ≅ P'<VAR>h : IsSheafFor P R<VAR>x : FamilyOfElements P' R<VAR>hx : x.Compatible<VAR>x' : FamilyOfElements P R := FamilyOfElements.compPresheafMap i.inv x<GOAL>∃! t, x.IsAmalgamation t
<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>P' : Cᵒᵖ ⥤ Type w<VAR>i : P ≅ P'<VAR>h : IsSheafFor P R<VAR>x : FamilyOfElements P' R<VAR>hx : x.Compatible<VAR>x' : FamilyOfElements P R := FamilyOfElements.compPresheafMap i.inv x<VAR>this : x'.Compatible<GOAL>∃! t, x.IsAmalgamation t
<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>P' : Cᵒᵖ ⥤ Type w<VAR>i : P ≅ P'<VAR>h : IsSheafFor P R<VAR>x : FamilyOfElements P' R<VAR>hx : x.Compatible<VAR>x' : FamilyOfElements P R := FamilyOfElements.compPresheafMap i.inv x<VAR>this : x'.Compatible<VAR>t : P.obj (op X)<VAR>ht1 : x'.IsAmalgamation t<VAR>ht2 : ∀ (y : P.obj (op X)), (fun t => x'.IsAmalgamation t) y → y = t<GOAL>∃! t, x.IsAmalgamation t
<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>P' : Cᵒᵖ ⥤ Type w<VAR>i : P ≅ P'<VAR>h : IsSheafFor P R<VAR>x : FamilyOfElements P' R<VAR>hx : x.Compatible<VAR>x' : FamilyOfElements P R := FamilyOfElements.compPresheafMap i.inv x<VAR>this : x'.Compatible<VAR>t : P.obj (op X)<VAR>ht1 : x'.IsAmalgamation t<VAR>ht2 : ∀ (y : P.obj (op X)), (fun t => x'.IsAmalgamation t) y → y = t<GOAL>(fun t => x.IsAmalgamation t) (i.hom.app (op X) t) ∧ ∀ (y : P'.obj (op X)), (fun t => x.IsAmalgamation t) y → y = i.hom.app (op X) t
<VAR>α : Type u_1<VAR>inst✝ : AddCommGroup α<VAR>x a : α<GOAL>termg 0 x a = a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a b : α<VAR>h✝ : a ≤ b<VAR>x : α<VAR>h : a < b<GOAL>projIcc a b ⋯ x = ⟨b, ⋯⟩ ↔ b ≤ x
<VAR>α : Type u_1<VAR>inst✝⁴ : CancelCommMonoidWithZero α<VAR>inst✝³ : UniqueFactorizationMonoid α<VAR>inst✝² : DecidableEq (Associates α)<VAR>inst✝¹ : (p : Associates α) → Decidable (Irreducible p)<VAR>inst✝ : Nontrivial α<GOAL>factors 1 = 0
<VAR>α : Type u_1<VAR>inst✝⁴ : CancelCommMonoidWithZero α<VAR>inst✝³ : UniqueFactorizationMonoid α<VAR>inst✝² : DecidableEq (Associates α)<VAR>inst✝¹ : (p : Associates α) → Decidable (Irreducible p)<VAR>inst✝ : Nontrivial α<GOAL>(factors 1).prod = FactorSet.prod 0
<VAR>α : Type u_1<VAR>inst✝⁴ : CancelCommMonoidWithZero α<VAR>inst✝³ : UniqueFactorizationMonoid α<VAR>inst✝² : DecidableEq (Associates α)<VAR>inst✝¹ : (p : Associates α) → Decidable (Irreducible p)<VAR>inst✝ : Nontrivial α<GOAL>1 = FactorSet.prod 0
<VAR>α : Type u_1<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : NormalizationMonoid α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>a b c : α<VAR>ha : a ∈ normalizedFactors c<VAR>hb : b ∈ normalizedFactors c<VAR>h : a ~ᵤ b<GOAL>a = b
<VAR>α : Type u_1<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : NormalizationMonoid α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>a b c : α<VAR>ha : a ∈ normalizedFactors c<VAR>hb : b ∈ normalizedFactors c<VAR>h : a ~ᵤ b<GOAL>a ∣ b ∧ b ∣ a
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>E' : ι' → Type wE'<VAR>G : Type wG<VAR>G' : Type wG'<VAR>inst✝¹⁴ : Fintype ι<VAR>inst✝¹³ : Fintype ι'<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>inst✝¹¹ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝¹⁰ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝⁹ : (i : ι) → SeminormedAddCommGroup (E₁ i)<VAR>inst✝⁸ : (i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>inst✝⁷ : (i : ι') → SeminormedAddCommGroup (E' i)<VAR>inst✝⁶ : (i : ι') → NormedSpace 𝕜 (E' i)<VAR>inst✝⁵ : SeminormedAddCommGroup G<VAR>inst✝⁴ : NormedSpace 𝕜 G<VAR>inst✝³ : SeminormedAddCommGroup G'<VAR>inst✝² : NormedSpace 𝕜 G'<VAR>c : 𝕜<VAR>f✝ g : ContinuousMultilinearMap 𝕜 E G<VAR>m✝ : (i : ι) → E i<VAR>n : ℕ<VAR>Ei : Fin n → Type u_1<VAR>inst✝¹ : (i : Fin n) → SeminormedAddCommGroup (Ei i)<VAR>inst✝ : (i : Fin n) → NormedSpace 𝕜 (Ei i)<VAR>f : ContinuousMultilinearMap 𝕜 Ei G<VAR>m : (i : Fin n) → Ei i<VAR>b : ℝ<VAR>hm : ‖m‖ ≤ b<GOAL>‖f m‖ ≤ ‖f‖ * b ^ n
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝ : Monoid G<VAR>a b x y : G<VAR>n m : ℕ<VAR>h : Commute x y<VAR>hy : IsOfFinOrder y<VAR>hdvd : ∀ (p : ℕ), Nat.Prime p → p ∣ orderOf x → p * orderOf x ∣ orderOf y<GOAL>orderOf (x * y) = orderOf y
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝ : Monoid G<VAR>a b x y : G<VAR>n m : ℕ<VAR>h : Commute x y<VAR>hy : IsOfFinOrder y<VAR>hdvd : ∀ (p : ℕ), Nat.Prime p → p ∣ orderOf x → p * orderOf x ∣ orderOf y<VAR>hoy : 0 < orderOf y<GOAL>orderOf (x * y) = orderOf y
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝ : Monoid G<VAR>a b x y : G<VAR>n m : ℕ<VAR>h : Commute x y<VAR>hy : IsOfFinOrder y<VAR>hdvd : ∀ (p : ℕ), Nat.Prime p → p ∣ orderOf x → p * orderOf x ∣ orderOf y<VAR>hoy : 0 < orderOf y<VAR>hxy : orderOf x ∣ orderOf y<GOAL>orderOf (x * y) = orderOf y
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝ : Monoid G<VAR>a b x y : G<VAR>n m : ℕ<VAR>h : Commute x y<VAR>hy : IsOfFinOrder y<VAR>hdvd : ∀ (p : ℕ), Nat.Prime p → p ∣ orderOf x → p * orderOf x ∣ orderOf y<VAR>hoy : 0 < orderOf y<VAR>hxy : orderOf x ∣ orderOf y<GOAL>orderOf (x * y) ∣ orderOf y
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝ : Monoid G<VAR>a b x y : G<VAR>n m : ℕ<VAR>h : Commute x y<VAR>hy : IsOfFinOrder y<VAR>hdvd : ∀ (p : ℕ), Nat.Prime p → p ∣ orderOf x → p * orderOf x ∣ orderOf y<VAR>hoy : 0 < orderOf y<VAR>hxy : orderOf x ∣ orderOf y<GOAL>∀ (p : ℕ), Nat.Prime p → p ∣ orderOf y → ¬orderOf (x * y) ∣ orderOf y / p
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝ : Monoid G<VAR>a b x y : G<VAR>n m : ℕ<VAR>h : Commute x y<VAR>hy : IsOfFinOrder y<VAR>hdvd : ∀ (p : ℕ), Nat.Prime p → p ∣ orderOf x → p * orderOf x ∣ orderOf y<VAR>hoy : 0 < orderOf y<VAR>hxy : orderOf x ∣ orderOf y<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>hpy : p ∣ orderOf y<VAR>hd : orderOf (x * y) ∣ orderOf y / p<GOAL>p = 1
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝ : Monoid G<VAR>a b x y : G<VAR>n m : ℕ<VAR>h : Commute x y<VAR>hy : IsOfFinOrder y<VAR>hdvd : ∀ (p : ℕ), Nat.Prime p → p ∣ orderOf x → p * orderOf x ∣ orderOf y<VAR>hoy : 0 < orderOf y<VAR>hxy : orderOf x ∣ orderOf y<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>hpy : p ∣ orderOf y<VAR>hd : orderOf (x * y) ∣ orderOf y / p<GOAL>orderOf y ∣ orderOf y / p
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝ : Monoid G<VAR>a b x y : G<VAR>n m : ℕ<VAR>h : Commute x y<VAR>hy : IsOfFinOrder y<VAR>hdvd : ∀ (p : ℕ), Nat.Prime p → p ∣ orderOf x → p * orderOf x ∣ orderOf y<VAR>hoy : 0 < orderOf y<VAR>hxy : orderOf x ∣ orderOf y<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>hpy : p ∣ orderOf y<VAR>hd : orderOf (x * y) ∣ orderOf y / p<GOAL>p * orderOf x ∣ orderOf y
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝ : Monoid G<VAR>a b x y : G<VAR>n m : ℕ<VAR>h✝ : Commute x y<VAR>hy : IsOfFinOrder y<VAR>hdvd : ∀ (p : ℕ), Nat.Prime p → p ∣ orderOf x → p * orderOf x ∣ orderOf y<VAR>hoy : 0 < orderOf y<VAR>hxy : orderOf x ∣ orderOf y<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>hpy : p ∣ orderOf y<VAR>hd : orderOf (x * y) ∣ orderOf y / p<VAR>h : p ∣ orderOf x<GOAL>p * orderOf x ∣ orderOf y
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝ : Monoid G<VAR>a b x y : G<VAR>n m : ℕ<VAR>h✝ : Commute x y<VAR>hy : IsOfFinOrder y<VAR>hdvd : ∀ (p : ℕ), Nat.Prime p → p ∣ orderOf x → p * orderOf x ∣ orderOf y<VAR>hoy : 0 < orderOf y<VAR>hxy : orderOf x ∣ orderOf y<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>hpy : p ∣ orderOf y<VAR>hd : orderOf (x * y) ∣ orderOf y / p<VAR>h : ¬p ∣ orderOf x<GOAL>p * orderOf x ∣ orderOf y
<VAR>M : ℝ<VAR>hM : 1 < M<GOAL>Filter.map ofReal' (𝓝[<] 1) ≤ 𝓝[stolzSet M] 1
<VAR>M : ℝ<VAR>hM : 1 < M<GOAL>Tendsto id (Filter.map ofReal' (𝓝[<] 1)) (𝓝[stolzSet M] 1)
<VAR>M : ℝ<VAR>hM : 1 < M<GOAL>∀ᶠ (x : ℝ) in 𝓝[<] 1, ↑x ∈ stolzSet M
<VAR>M : ℝ<VAR>hM : 1 < M<GOAL>∃ u, IsOpen u ∧ 1 ∈ u ∧ u ∩ Set.Iio 1 ⊆ {x | ↑x ∈ stolzSet M}
<VAR>M : ℝ<VAR>hM : 1 < M<VAR>x : ℝ<VAR>hx : x ∈ Set.Ioo 0 2 ∩ Set.Iio 1<GOAL>x ∈ {x | ↑x ∈ stolzSet M}
<VAR>M : ℝ<VAR>hM : 1 < M<VAR>x : ℝ<VAR>hx : (0 < x ∧ x < 2) ∧ x < 1<GOAL>x ∈ {x | ↑x ∈ stolzSet M}
<VAR>M : ℝ<VAR>hM : 1 < M<VAR>x : ℝ<VAR>hx : (0 < x ∧ x < 2) ∧ x < 1<GOAL>x < 1 ∧ 1 - x < M * (1 - x)
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>h : p * q ≠ 0<GOAL>p.natTrailingDegree + q.natTrailingDegree ≤ (p * q).natTrailingDegree
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>h : p * q ≠ 0<VAR>hp : p ≠ 0<GOAL>p.natTrailingDegree + q.natTrailingDegree ≤ (p * q).natTrailingDegree
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>h : p * q ≠ 0<VAR>hp : p ≠ 0<VAR>hq : q ≠ 0<GOAL>p.natTrailingDegree + q.natTrailingDegree ≤ (p * q).natTrailingDegree
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>h : p * q ≠ 0<VAR>hp : p ≠ 0<VAR>hq : q ≠ 0<VAR>this : ∀ (p : R[X]), ↑p.natTrailingDegree = ↑p.natTrailingDegree<GOAL>p.natTrailingDegree + q.natTrailingDegree ≤ (p * q).natTrailingDegree
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>h : p * q ≠ 0<VAR>hp : p ≠ 0<VAR>hq : q ≠ 0<VAR>this : ∀ (p : R[X]), ↑p.natTrailingDegree = ↑p.natTrailingDegree<GOAL>p.trailingDegree + q.trailingDegree ≤ (p * q).trailingDegree
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : Group G<VAR>inst✝ : ContinuousMul G<VAR>h : IsOpen {1}<GOAL>DiscreteTopology G
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : Group G<VAR>inst✝ : ContinuousMul G<VAR>h : IsOpen {1}<GOAL>∀ (a : G), IsOpen {a}
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : Group G<VAR>inst✝ : ContinuousMul G<VAR>h : IsOpen {1}<VAR>g : G<GOAL>{g} = (fun x => g⁻¹ * x) ⁻¹' {1}