ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝³ : TopologicalSpace α<VAR>s✝ t✝ u v : Set α<VAR>inst✝² : LinearOrder β<VAR>inst✝¹ : SuccOrder β<VAR>inst✝ : IsSuccArchimedean β<VAR>s : β → Set α<VAR>t : Set β<VAR>ht : t.OrdConnected<VAR>H : ∀ n ∈ t, IsPreconnected (s n)<VAR>K : ∀ n ∈ t, succ n ∈ t → (s n ∩ s (succ n)).Nonempty<VAR>h1 : ∀ {i j k : β}, i ∈ t → j ∈ t → k ∈ Ico i j → k ∈ t<VAR>h2 : ∀ {i j k : β}, i ∈ t → j ∈ t → k ∈ Ico i j → succ k ∈ t<VAR>h3 : ∀ {i j k : β}, i ∈ t → j ∈ t → k ∈ Ico i j → (s k ∩ s (succ k)).Nonempty<VAR>i : β<VAR>hi : i ∈ t<VAR>j : β<VAR>hj : j ∈ t<GOAL>ReflTransGen (fun i j => (s i ∩ s j).Nonempty ∧ i ∈ t) i j
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m✝ : MeasurableSpace α<VAR>μ✝ ν✝ : Measure α<VAR>m : MeasurableSpace α<VAR>f : α → ℝ≥0∞<VAR>μ ν : Measure α<GOAL>∫⁻ (a : α), f a ∂(μ + ν) = ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), f a ∂ν
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>l : List α<VAR>n : ℕ<GOAL>dropWhile p (dropWhile p l) = dropWhile p l
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>l : List α<VAR>n : ℕ<GOAL>∀ (hl : 0 < (dropWhile p l).length), ¬p ((dropWhile p l).get ⟨0, hl⟩) = true
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>P : RootPairing ι R M N<VAR>i j✝ j : ι<GOAL>(P.coreflection i) (P.coroot j) ∈ range ⇑P.coroot
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>l : Filter γ<VAR>f : γ → α<VAR>e : α ≃o β<GOAL>Tendsto (fun x => e (f x)) l atTop ↔ Tendsto f l atTop
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>n : ℕ<VAR>f : 𝕜 → F<VAR>s : Set 𝕜<VAR>x✝ x : 𝕜<GOAL>iteratedDerivWithin n f univ x = iteratedDeriv n f x
<VAR>l : List Char<VAR>c : Char<VAR>r : List Char<VAR>it : Iterator<VAR>h : ValidFor l (c :: r) it<GOAL>ValidFor (c :: l) r it.next
<VAR>l : List Char<VAR>c : Char<VAR>r : List Char<VAR>h : ValidFor l (c :: r) { s := { data := l.reverse ++ c :: r }, i := { byteIdx := utf8Len l.reverse } }<GOAL>ValidFor (c :: l) r { s := { data := l.reverse ++ c :: r }, i := { byteIdx := utf8Len l.reverse } }.next
<VAR>l : List Char<VAR>c : Char<VAR>r : List Char<VAR>h : ValidFor l (c :: r) { s := { data := l.reverse ++ c :: r }, i := { byteIdx := utf8Len l.reverse } }<GOAL>ValidFor (c :: l) r { s := { data := l.reverse ++ c :: r }, i := { byteIdx := utf8Len l.reverse + c.utf8Size } }
<VAR>l : List Char<VAR>c : Char<VAR>r : List Char<VAR>h : ValidFor l (c :: r) { s := { data := l.reverse ++ c :: r }, i := { byteIdx := utf8Len l.reverse } }<GOAL>ValidFor (c :: l) r { s := { data := l.reverseAux (c :: r) }, i := { byteIdx := utf8Len l + c.utf8Size } }
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝³ : Group G<VAR>inst✝² : Group G'<VAR>inst✝¹ : Group G''<VAR>A : Type u_4<VAR>inst✝ : AddGroup A<VAR>H K : Subgroup G<VAR>k : Set G<GOAL>closure {1} = ⊥
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>κ✝ η✝ : Kernel α γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>κ η : Kernel α γ<VAR>a : α<GOAL>Measurable ((Function.uncurry fun a b => ENNReal.ofReal (κ.rnDerivAux (κ + η) a b) - ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a b) * κ.rnDeriv η a b) ∘ fun b => (a, b))
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>ι : Type u_4<VAR>f : X → Y<VAR>g : Y → Z<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>hg : OpenEmbedding g<GOAL>IsOpenMap f ↔ IsOpenMap (g ∘ f)
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : 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✝⁶ : Module.Free R M<VAR>inst✝⁵ : Module.Finite R M<VAR>inst✝⁴ : Module.Free R L<VAR>inst✝³ : Module.Finite R L<VAR>I : LieIdeal R L<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : IsPrincipalIdealRing R<VAR>inst✝ : IsLieAbelian ↥↑I<VAR>x : L<VAR>hx : x ∈ I<GOAL>x ∈ killingCompl R L ⊤
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : 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✝⁶ : Module.Free R M<VAR>inst✝⁵ : Module.Finite R M<VAR>inst✝⁴ : Module.Free R L<VAR>inst✝³ : Module.Finite R L<VAR>I : LieIdeal R L<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : IsPrincipalIdealRing R<VAR>inst✝ : IsLieAbelian ↥↑I<VAR>x : L<VAR>hx : x ∈ I<GOAL>∀ (y : L), ((killingForm R L) y) x = 0
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : 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✝⁶ : Module.Free R M<VAR>inst✝⁵ : Module.Finite R M<VAR>inst✝⁴ : Module.Free R L<VAR>inst✝³ : Module.Finite R L<VAR>I : LieIdeal R L<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : IsPrincipalIdealRing R<VAR>inst✝ : IsLieAbelian ↥↑I<VAR>x : L<VAR>hx : x ∈ I<VAR>y : L<GOAL>((killingForm R L) y) x = 0
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : 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✝⁶ : Module.Free R M<VAR>inst✝⁵ : Module.Finite R M<VAR>inst✝⁴ : Module.Free R L<VAR>inst✝³ : Module.Finite R L<VAR>I : LieIdeal R L<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : IsPrincipalIdealRing R<VAR>inst✝ : IsLieAbelian ↥↑I<VAR>x : L<VAR>hx : x ∈ I<VAR>y : L<GOAL>(trace R L) ((LieModule.toEnd R L L) y ∘ₗ (LieModule.toEnd R L L) x) = 0
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝³ : CommRing R<VAR>inst✝² : Ring S<VAR>inst✝¹ : Algebra R S<VAR>M N : Submodule R S<VAR>H : M.LinearDisjoint N<VAR>inst✝ : Module.Flat R ↥M<VAR>κ : Type u_1<VAR>ι : Type u_2<VAR>m : κ → ↥M<VAR>n : ι → ↥N<VAR>hm : LinearIndependent R m<VAR>hn : LinearIndependent R n<GOAL>LinearIndependent R fun i => ↑(m i.1) * ↑(n i.2)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝³ : CommRing R<VAR>inst✝² : Ring S<VAR>inst✝¹ : Algebra R S<VAR>M N : Submodule R S<VAR>H : M.LinearDisjoint N<VAR>inst✝ : Module.Flat R ↥M<VAR>κ : Type u_1<VAR>ι : Type u_2<VAR>m : κ → ↥M<VAR>n : ι → ↥N<VAR>hm : Function.Injective ⇑(Finsupp.total κ (↥M) R m)<VAR>hn : Function.Injective ⇑(Finsupp.total ι (↥N) R n)<GOAL>Function.Injective ⇑(Finsupp.total (κ × ι) S R fun i => ↑(m i.1) * ↑(n i.2))
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝³ : CommRing R<VAR>inst✝² : Ring S<VAR>inst✝¹ : Algebra R S<VAR>M N : Submodule R S<VAR>H : M.LinearDisjoint N<VAR>inst✝ : Module.Flat R ↥M<VAR>κ : Type u_1<VAR>ι : Type u_2<VAR>m : κ → ↥M<VAR>n : ι → ↥N<VAR>hm : Function.Injective ⇑(Finsupp.total κ (↥M) R m)<VAR>hn : Function.Injective ⇑(Finsupp.total ι (↥N) R n)<VAR>i0 : (κ × ι →₀ R) ≃ₗ[R] (κ →₀ R) ⊗[R] (ι →₀ R) := (finsuppTensorFinsupp' R κ ι).symm<VAR>i1 : (κ →₀ R) ⊗[R] (ι →₀ R) →ₗ[R] ↥M ⊗[R] (ι →₀ R) := LinearMap.rTensor (ι →₀ R) (Finsupp.total κ (↥M) R m)<VAR>i2 : ↥M ⊗[R] (ι →₀ R) →ₗ[R] ↥M ⊗[R] ↥N := LinearMap.lTensor (↥M) (Finsupp.total ι (↥N) R n)<VAR>i : (κ × ι →₀ R) →ₗ[R] S := M.mulMap N ∘ₗ i2 ∘ₗ i1 ∘ₗ ↑i0<GOAL>Function.Injective ⇑(Finsupp.total (κ × ι) S R fun i => ↑(m i.1) * ↑(n i.2))
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝³ : CommRing R<VAR>inst✝² : Ring S<VAR>inst✝¹ : Algebra R S<VAR>M N : Submodule R S<VAR>H : M.LinearDisjoint N<VAR>inst✝ : Module.Flat R ↥M<VAR>κ : Type u_1<VAR>ι : Type u_2<VAR>m : κ → ↥M<VAR>n : ι → ↥N<VAR>hm : Function.Injective ⇑(Finsupp.total κ (↥M) R m)<VAR>hn : Function.Injective ⇑(Finsupp.total ι (↥N) R n)<VAR>i0 : (κ × ι →₀ R) ≃ₗ[R] (κ →₀ R) ⊗[R] (ι →₀ R) := (finsuppTensorFinsupp' R κ ι).symm<VAR>i1 : (κ →₀ R) ⊗[R] (ι →₀ R) →ₗ[R] ↥M ⊗[R] (ι →₀ R) := LinearMap.rTensor (ι →₀ R) (Finsupp.total κ (↥M) R m)<VAR>i2 : ↥M ⊗[R] (ι →₀ R) →ₗ[R] ↥M ⊗[R] ↥N := LinearMap.lTensor (↥M) (Finsupp.total ι (↥N) R n)<VAR>i : (κ × ι →₀ R) →ₗ[R] S := M.mulMap N ∘ₗ i2 ∘ₗ i1 ∘ₗ ↑i0<VAR>h1 : Function.Injective ⇑i1<GOAL>Function.Injective ⇑(Finsupp.total (κ × ι) S R fun i => ↑(m i.1) * ↑(n i.2))
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝³ : CommRing R<VAR>inst✝² : Ring S<VAR>inst✝¹ : Algebra R S<VAR>M N : Submodule R S<VAR>H : M.LinearDisjoint N<VAR>inst✝ : Module.Flat R ↥M<VAR>κ : Type u_1<VAR>ι : Type u_2<VAR>m : κ → ↥M<VAR>n : ι → ↥N<VAR>hm : Function.Injective ⇑(Finsupp.total κ (↥M) R m)<VAR>hn : Function.Injective ⇑(Finsupp.total ι (↥N) R n)<VAR>i0 : (κ × ι →₀ R) ≃ₗ[R] (κ →₀ R) ⊗[R] (ι →₀ R) := (finsuppTensorFinsupp' R κ ι).symm<VAR>i1 : (κ →₀ R) ⊗[R] (ι →₀ R) →ₗ[R] ↥M ⊗[R] (ι →₀ R) := LinearMap.rTensor (ι →₀ R) (Finsupp.total κ (↥M) R m)<VAR>i2 : ↥M ⊗[R] (ι →₀ R) →ₗ[R] ↥M ⊗[R] ↥N := LinearMap.lTensor (↥M) (Finsupp.total ι (↥N) R n)<VAR>i : (κ × ι →₀ R) →ₗ[R] S := M.mulMap N ∘ₗ i2 ∘ₗ i1 ∘ₗ ↑i0<VAR>h1 : Function.Injective ⇑i1<VAR>h2 : Function.Injective ⇑i2<GOAL>Function.Injective ⇑(Finsupp.total (κ × ι) S R fun i => ↑(m i.1) * ↑(n i.2))
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝³ : CommRing R<VAR>inst✝² : Ring S<VAR>inst✝¹ : Algebra R S<VAR>M N : Submodule R S<VAR>H : M.LinearDisjoint N<VAR>inst✝ : Module.Flat R ↥M<VAR>κ : Type u_1<VAR>ι : Type u_2<VAR>m : κ → ↥M<VAR>n : ι → ↥N<VAR>hm : Function.Injective ⇑(Finsupp.total κ (↥M) R m)<VAR>hn : Function.Injective ⇑(Finsupp.total ι (↥N) R n)<VAR>i0 : (κ × ι →₀ R) ≃ₗ[R] (κ →₀ R) ⊗[R] (ι →₀ R) := (finsuppTensorFinsupp' R κ ι).symm<VAR>i1 : (κ →₀ R) ⊗[R] (ι →₀ R) →ₗ[R] ↥M ⊗[R] (ι →₀ R) := LinearMap.rTensor (ι →₀ R) (Finsupp.total κ (↥M) R m)<VAR>i2 : ↥M ⊗[R] (ι →₀ R) →ₗ[R] ↥M ⊗[R] ↥N := LinearMap.lTensor (↥M) (Finsupp.total ι (↥N) R n)<VAR>i : (κ × ι →₀ R) →ₗ[R] S := M.mulMap N ∘ₗ i2 ∘ₗ i1 ∘ₗ ↑i0<VAR>h1 : Function.Injective ⇑i1<VAR>h2 : Function.Injective ⇑i2<VAR>h : Function.Injective ⇑i<GOAL>Function.Injective ⇑(Finsupp.total (κ × ι) S R fun i => ↑(m i.1) * ↑(n i.2))
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝³ : CommRing R<VAR>inst✝² : Ring S<VAR>inst✝¹ : Algebra R S<VAR>M N : Submodule R S<VAR>H : M.LinearDisjoint N<VAR>inst✝ : Module.Flat R ↥M<VAR>κ : Type u_1<VAR>ι : Type u_2<VAR>m : κ → ↥M<VAR>n : ι → ↥N<VAR>hm : Function.Injective ⇑(Finsupp.total κ (↥M) R m)<VAR>hn : Function.Injective ⇑(Finsupp.total ι (↥N) R n)<VAR>i0 : (κ × ι →₀ R) ≃ₗ[R] (κ →₀ R) ⊗[R] (ι →₀ R) := (finsuppTensorFinsupp' R κ ι).symm<VAR>i1 : (κ →₀ R) ⊗[R] (ι →₀ R) →ₗ[R] ↥M ⊗[R] (ι →₀ R) := LinearMap.rTensor (ι →₀ R) (Finsupp.total κ (↥M) R m)<VAR>i2 : ↥M ⊗[R] (ι →₀ R) →ₗ[R] ↥M ⊗[R] ↥N := LinearMap.lTensor (↥M) (Finsupp.total ι (↥N) R n)<VAR>i : (κ × ι →₀ R) →ₗ[R] S := M.mulMap N ∘ₗ i2 ∘ₗ i1 ∘ₗ ↑i0<VAR>h1 : Function.Injective ⇑i1<VAR>h2 : Function.Injective ⇑i2<VAR>h : Function.Injective ⇑i<VAR>this : i = Finsupp.total (κ × ι) S R fun i => ↑(m i.1) * ↑(n i.2)<GOAL>Function.Injective ⇑(Finsupp.total (κ × ι) S R fun i => ↑(m i.1) * ↑(n i.2))
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁶ : OrderedSemiring 𝕜<VAR>inst✝⁵ : AddCommMonoid E<VAR>inst✝⁴ : AddCommMonoid F<VAR>inst✝³ : OrderedAddCommMonoid α<VAR>inst✝² : OrderedAddCommMonoid β<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 β<VAR>f : E →ₗ[𝕜] β<VAR>s : Set E<VAR>hs : Convex 𝕜 s<VAR>x✝⁸ : E<VAR>x✝⁷ : x✝⁸ ∈ s<VAR>x✝⁶ : E<VAR>x✝⁵ : x✝⁶ ∈ s<VAR>x✝⁴ x✝³ : 𝕜<VAR>x✝² : 0 ≤ x✝⁴<VAR>x✝¹ : 0 ≤ x✝³<VAR>x✝ : x✝⁴ + x✝³ = 1<GOAL>f (x✝⁴ • x✝⁸ + x✝³ • x✝⁶) ≤ x✝⁴ • f x✝⁸ + x✝³ • f x✝⁶
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : Group G'<VAR>inst✝³ : Group G''<VAR>A : Type u_4<VAR>inst✝² : AddGroup A<VAR>H✝ : Type u_5<VAR>inst✝¹ : Group H✝<VAR>H : Type u_6<VAR>inst✝ : Group H<VAR>f : G ≃* H<VAR>sg : Subgroup G<GOAL>Subgroup.map (↑f.symm) (Subgroup.map (↑f) sg) = sg
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : Group G'<VAR>inst✝³ : Group G''<VAR>A : Type u_4<VAR>inst✝² : AddGroup A<VAR>H✝ : Type u_5<VAR>inst✝¹ : Group H✝<VAR>H : Type u_6<VAR>inst✝ : Group H<VAR>f : G ≃* H<VAR>sh : Subgroup H<GOAL>Subgroup.map (↑f) (Subgroup.map (↑f.symm) sh) = sh
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : Group G'<VAR>inst✝³ : Group G''<VAR>A : Type u_4<VAR>inst✝² : AddGroup A<VAR>H✝ : Type u_5<VAR>inst✝¹ : Group H✝<VAR>H : Type u_6<VAR>inst✝ : Group H<VAR>f : G ≃* H<VAR>sg1 sg2 : Subgroup G<VAR>h : { toFun := Subgroup.map ↑f, invFun := Subgroup.map ↑f.symm, left_inv := ⋯, right_inv := ⋯ } sg1 ≤ { toFun := Subgroup.map ↑f, invFun := Subgroup.map ↑f.symm, left_inv := ⋯, right_inv := ⋯ } sg2<GOAL>sg1 ≤ sg2
<VAR>α : Type u_1<VAR>inst✝⁴ : TopologicalSpace α<VAR>β : Type u_2<VAR>inst✝³ : Preorder β<VAR>f✝ g✝ : α → β<VAR>x : α<VAR>s t : Set α<VAR>y z : β<VAR>ι : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : LinearOrderedAddCommMonoid γ<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : OrderTopology γ<VAR>f g : α → γ<VAR>hf : LowerSemicontinuousAt f x<VAR>hg : LowerSemicontinuousAt g x<VAR>hcont : ContinuousAt (fun p => p.1 + p.2) (f x, g x)<GOAL>LowerSemicontinuousAt (fun z => f z + g z) x
<VAR>α : Type u_1<VAR>inst✝⁴ : TopologicalSpace α<VAR>β : Type u_2<VAR>inst✝³ : Preorder β<VAR>f✝ g✝ : α → β<VAR>x : α<VAR>s t : Set α<VAR>y z : β<VAR>ι : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : LinearOrderedAddCommMonoid γ<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : OrderTopology γ<VAR>f g : α → γ<VAR>hcont : ContinuousAt (fun p => p.1 + p.2) (f x, g x)<VAR>hf : LowerSemicontinuousWithinAt f univ x<VAR>hg : LowerSemicontinuousWithinAt g univ x<GOAL>LowerSemicontinuousWithinAt (fun z => f z + g z) univ x
<VAR>o : Ordinal.{u_1}<GOAL>(nim o).birthday = o
<VAR>o : Ordinal.{u_1}<VAR>IH : ∀ k < o, (nim k).birthday = k<GOAL>(nim o).birthday = o
<VAR>o : Ordinal.{u_1}<VAR>IH : ∀ k < o, (nim k).birthday = k<GOAL>max (lsub fun i => ((mk (Quotient.out o).α (Quotient.out o).α (fun o₂ => nim (typein (fun x x_1 => x < x_1) o₂)) fun o₂ => nim (typein (fun x x_1 => x < x_1) o₂)).moveLeft i).birthday) (lsub fun i => ((mk (Quotient.out o).α (Quotient.out o).α (fun o₂ => nim (typein (fun x x_1 => x < x_1) o₂)) fun o₂ => nim (typein (fun x x_1 => x < x_1) o₂)).moveRight i).birthday) = o
<VAR>o : Ordinal.{u_1}<VAR>IH : ∀ k < o, (nim k).birthday = k<GOAL>max (lsub fun i => (nim (typein (fun x x_1 => x < x_1) i)).birthday) (lsub fun i => (nim (typein (fun x x_1 => x < x_1) i)).birthday) = o
<VAR>o : Ordinal.{u_1}<VAR>IH : ∀ k < o, (nim k).birthday = k<GOAL>(lsub fun i => (nim (typein (fun x x_1 => x < x_1) i)).birthday) = o
<VAR>o : Ordinal.{u_1}<VAR>IH : ∀ k < o, (nim k).birthday = k<VAR>i : (Quotient.out o).α<GOAL>(nim (typein (fun x x_1 => x < x_1) i)).birthday = typein (fun x x_1 => x < x_1) i
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>p : K[X]<GOAL>((algebraMap K[X] (RatFunc K)) p).denom = 1
<VAR>α : Type u_1<VAR>inst✝² : CanonicallyLinearOrderedAddCommMonoid α<VAR>inst✝¹ : Sub α<VAR>inst✝ : OrderedSub α<VAR>a b c d : α<GOAL>0 < a - b ↔ b < a
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝¹ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g : ι → α<VAR>inst✝ : TopologicalSpace α<VAR>L : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝 x, ∃ F, ContinuousAt F x ∧ ∀ y ∈ t, (f y, F y) ∈ u<GOAL>ContinuousAt f x
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝¹ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g : ι → α<VAR>inst✝ : TopologicalSpace α<VAR>L : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝 x, ∃ F, ContinuousAt F x ∧ ∀ y ∈ t, (f y, F y) ∈ u<GOAL>ContinuousWithinAt f univ x
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝¹ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g : ι → α<VAR>inst✝ : TopologicalSpace α<VAR>L : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝 x, ∃ F, ContinuousAt F x ∧ ∀ y ∈ t, (f y, F y) ∈ u<GOAL>∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝[univ] x, ∃ F, ContinuousWithinAt F univ x ∧ ∀ y ∈ t, (f y, F y) ∈ u
<VAR>E : Type u_1<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module ℂ E<GOAL>finrank ℝ E = 2 * finrank ℂ E
<VAR>R : Type u<VAR>ι✝ : Type u_1<VAR>inst✝ : CommSemiring R<VAR>I✝ J K L : Ideal R<VAR>ι : Type u_2<VAR>s : Finset ι<VAR>I : ι → R<VAR>hI : (↑s).Pairwise (IsCoprime on I)<VAR>x : R<GOAL>(x ∈ s.inf fun i => span {I i}) ↔ x ∈ span {∏ i ∈ s, I i}
<VAR>R : Type u<VAR>ι✝ : Type u_1<VAR>inst✝ : CommSemiring R<VAR>I✝ J K L : Ideal R<VAR>ι : Type u_2<VAR>s : Finset ι<VAR>I : ι → R<VAR>hI : (↑s).Pairwise (IsCoprime on I)<VAR>x : R<GOAL>(∀ i ∈ s, I i ∣ x) ↔ ∏ i ∈ s, I i ∣ x
<VAR>N : ℕ<VAR>s : Finset ℕ<VAR>h : N.primesBelow ≤ s<VAR>n : ℕ<VAR>hn : n ∈ (factoredNumbers s)ᶜ \ {0}<GOAL>n ∈ {n | N ≤ n}
<VAR>N : ℕ<VAR>s : Finset ℕ<VAR>h : N.primesBelow ≤ s<VAR>n : ℕ<VAR>hn : (¬n = 0 → ∃ x ∈ n.primeFactorsList, x ∉ s) ∧ ¬n = 0<GOAL>n ∈ {n | N ≤ n}
<VAR>N : ℕ<VAR>s : Finset ℕ<VAR>h : N.primesBelow ≤ s<VAR>n : ℕ<VAR>hn : (¬n = 0 → ∃ x ∈ n.primeFactorsList, x ∉ s) ∧ ¬n = 0<GOAL>N ≤ n
<VAR>N : ℕ<VAR>s : Finset ℕ<VAR>h : N.primesBelow ≤ s<VAR>n : ℕ<VAR>hn : (¬n = 0 → ∃ x ∈ n.primeFactorsList, x ∉ s) ∧ ¬n = 0<VAR>p : ℕ<VAR>hp₁ : p ∈ n.primeFactorsList<VAR>hp₂ : p ∉ s<GOAL>N ≤ n
<VAR>N : ℕ<VAR>s : Finset ℕ<VAR>h : N.primesBelow ≤ s<VAR>n : ℕ<VAR>hn : (¬n = 0 → ∃ x ∈ n.primeFactorsList, x ∉ s) ∧ ¬n = 0<VAR>p : ℕ<VAR>hp₁ : p ∈ n.primeFactorsList<VAR>hp₂ : p ∉ s<VAR>this : N ≤ p<GOAL>N ≤ n
<VAR>α : Type u<VAR>β : Type v<VAR>R r : α → α → Prop<VAR>l✝ l₁ l₂ : List α<VAR>a b : α<VAR>f : β → α<VAR>l : List β<GOAL>Chain' R (map f l) ↔ Chain' (fun a b => R (f a) (f b)) l
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝ : Category.{v', u'} D<VAR>W : MorphismProperty C<VAR>F : C ⥤ D<GOAL>W.IsInvertedBy F ↔ W.map F ≤ isomorphisms D
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝¹ : GroupWithZero α<VAR>inst✝ : MulAction α β<VAR>s✝ t : Set β<VAR>a✝ a : α<VAR>s : Set α<GOAL>(a • s)⁻¹ = op a⁻¹ • s⁻¹
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝¹ : GroupWithZero α<VAR>inst✝ : MulAction α β<VAR>s✝ t : Set β<VAR>a : α<VAR>s : Set α<GOAL>(0 • s)⁻¹ = op 0⁻¹ • s⁻¹
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝¹ : GroupWithZero α<VAR>inst✝ : MulAction α β<VAR>s✝ t : Set β<VAR>a✝ a : α<VAR>s : Set α<VAR>ha : a ≠ 0<GOAL>(a • s)⁻¹ = op a⁻¹ • s⁻¹
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : SeminormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : PseudoMetricSpace P<VAR>inst✝ : NormedAddTorsor E P<VAR>s✝ t✝ s t : Set E<VAR>x y : E<VAR>hx : x ∈ (convexHull ℝ) s<VAR>hy : y ∈ (convexHull ℝ) t<GOAL>∃ x' ∈ s, ∃ y' ∈ t, dist x y ≤ dist x' y'
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : SeminormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : PseudoMetricSpace P<VAR>inst✝ : NormedAddTorsor E P<VAR>s✝ t✝ s t : Set E<VAR>x y : E<VAR>hx : x ∈ (convexHull ℝ) s<VAR>hy : y ∈ (convexHull ℝ) t<VAR>x' : E<VAR>hx' : x' ∈ s<VAR>Hx' : dist x y ≤ dist x' y<GOAL>∃ x' ∈ s, ∃ y' ∈ t, dist x y ≤ dist x' y'
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : SeminormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : PseudoMetricSpace P<VAR>inst✝ : NormedAddTorsor E P<VAR>s✝ t✝ s t : Set E<VAR>x y : E<VAR>hx : x ∈ (convexHull ℝ) s<VAR>hy : y ∈ (convexHull ℝ) t<VAR>x' : E<VAR>hx' : x' ∈ s<VAR>Hx' : dist x y ≤ dist x' y<VAR>y' : E<VAR>hy' : y' ∈ t<VAR>Hy' : dist y x' ≤ dist y' x'<GOAL>∃ x' ∈ s, ∃ y' ∈ t, dist x y ≤ dist x' y'
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : SeminormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : PseudoMetricSpace P<VAR>inst✝ : NormedAddTorsor E P<VAR>s✝ t✝ s t : Set E<VAR>x y : E<VAR>hx : x ∈ (convexHull ℝ) s<VAR>hy : y ∈ (convexHull ℝ) t<VAR>x' : E<VAR>hx' : x' ∈ s<VAR>Hx' : dist x y ≤ dist x' y<VAR>y' : E<VAR>hy' : y' ∈ t<VAR>Hy' : dist y x' ≤ dist y' x'<GOAL>dist x y ≤ dist x' y'
<VAR>x y : ℂ<GOAL>sin x ^ 2 = 1 - cos x ^ 2
<VAR>P : MorphismProperty Scheme<VAR>Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>inst✝ : HasRingHomProperty P Q<VAR>X Y Z : Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>P f ↔ ∀ (U : ↑Y.affineOpens) (V : ↑X.affineOpens) (e : ↑V ≤ f ⁻¹ᵁ ↑U), Q (Scheme.Hom.appLE f (↑U) (↑V) e)
<VAR>α β : Type u<VAR>a : Cardinal.{u}<GOAL>1 < lift.{v, u} a ↔ 1 < a
<VAR>α : Type u_1<VAR>inst✝¹ : DivisionRing α<VAR>K : Type u_2<VAR>inst✝ : DivisionRing K<VAR>q : ℚ≥0<GOAL>↑↑q = ↑q
<VAR>α : Type u_1<VAR>inst✝¹ : DivisionRing α<VAR>K : Type u_2<VAR>inst✝ : DivisionRing K<VAR>q : ℚ≥0<GOAL>↑(↑q.num / ↑q.den).num / ↑(↑q.num / ↑q.den).den = ↑q.num / ↑q.den
<VAR>α : Type u_1<VAR>inst✝¹ : DivisionRing α<VAR>K : Type u_2<VAR>inst✝ : DivisionRing K<VAR>q : ℚ≥0<VAR>hn : (↑↑q.num / ↑↑q.den).num = ↑q.num<GOAL>↑(↑q.num / ↑q.den).num / ↑(↑q.num / ↑q.den).den = ↑q.num / ↑q.den
<VAR>α : Type u_1<VAR>inst✝¹ : DivisionRing α<VAR>K : Type u_2<VAR>inst✝ : DivisionRing K<VAR>q : ℚ≥0<GOAL>0 < ↑q.den
<VAR>α : Type u_1<VAR>inst✝¹ : DivisionRing α<VAR>K : Type u_2<VAR>inst✝ : DivisionRing K<VAR>q : ℚ≥0<VAR>hn : (↑↑q.num / ↑↑q.den).num = ↑q.num<VAR>hd : ↑(↑↑q.num / ↑↑q.den).den = ↑q.den<GOAL>↑(↑q.num / ↑q.den).num / ↑(↑q.num / ↑q.den).den = ↑q.num / ↑q.den
<VAR>α : Type u_1<VAR>inst✝¹ : DivisionRing α<VAR>K : Type u_2<VAR>inst✝ : DivisionRing K<VAR>q : ℚ≥0<VAR>hn : (↑q.num / ↑q.den).num = ↑q.num<VAR>hd : (↑q.num / ↑q.den).den = q.den<GOAL>↑(↑q.num / ↑q.den).num / ↑(↑q.num / ↑q.den).den = ↑q.num / ↑q.den
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : Semiring S<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>inst✝² : Module S M<VAR>inst✝¹ : SMul S R<VAR>inst✝ : IsScalarTower S R M<VAR>p✝ q p : Submodule R M<GOAL>p ≠ ⊥ ↔ ∃ x ∈ p, x ≠ 0
<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>inst✝¹ : CompleteLattice α<VAR>inst✝ : DecidableRel fun x x_1 => x ≤ x_1<VAR>f : (i : ι) → κ i → Interval α<GOAL>↑(⨅ i, ⨅ j, f i j) = ⋂ i, ⋂ j, ↑(f i j)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝² : BooleanRing α<VAR>inst✝¹ : BooleanRing β<VAR>inst✝ : BooleanRing γ<VAR>a b : α<GOAL>a + a * b + a * (a * b) = a
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s t u : Finset α<VAR>P : Finpartition s<VAR>a : α<VAR>ha : a ∈ s<GOAL>∃! t, t ∈ P.parts ∧ a ∈ t
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s t✝ u : Finset α<VAR>P : Finpartition s<VAR>a : α<VAR>ha : a ∈ s<VAR>t : Finset α<VAR>ht : t ∈ P.parts<VAR>ht' : a ∈ t<GOAL>∃! t, t ∈ P.parts ∧ a ∈ t
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s t✝ u✝ : Finset α<VAR>P : Finpartition s<VAR>a : α<VAR>ha : a ∈ s<VAR>t : Finset α<VAR>ht : t ∈ P.parts<VAR>ht' : a ∈ t<VAR>u : Finset α<VAR>hu : u ∈ P.parts<VAR>hu' : a ∈ u<GOAL>u = t
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>n : ℕ<VAR>hζ : (primitiveRoots n K).Nonempty<VAR>hn : 0 < n<VAR>a : K<VAR>H : Irreducible (X ^ n - C a)<VAR>σ : K[n√a] ≃ₐ[K] K[n√a]<VAR>this : Fact (Irreducible (X ^ n - C a))<GOAL>↑((autAdjoinRootXPowSubCEquiv hζ hn H).symm σ) • root (X ^ n - C a) = σ (root (X ^ n - C a))
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>n : ℕ<VAR>hζ : (primitiveRoots n K).Nonempty<VAR>hn : 0 < n<VAR>a : K<VAR>H : Irreducible (X ^ n - C a)<VAR>σ : K[n√a] ≃ₐ[K] K[n√a]<VAR>this : Fact (Irreducible (X ^ n - C a))<GOAL>(if a = 0 then 1 else σ (root (X ^ n - C a)) / root (X ^ n - C a)) * root (X ^ n - C a) = σ (root (X ^ n - C a))
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>n : ℕ<VAR>hζ : (primitiveRoots n K).Nonempty<VAR>hn : 0 < n<VAR>a : K<VAR>H : Irreducible (X ^ n - C a)<VAR>σ : K[n√a] ≃ₐ[K] K[n√a]<VAR>this : Fact (Irreducible (X ^ n - C a))<GOAL>(if root (X ^ n - C a) = 0 then 1 else σ (root (X ^ n - C a)) / root (X ^ n - C a)) * root (X ^ n - C a) = σ (root (X ^ n - C a))
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>D : Type u'<VAR>inst✝¹ : Category.{v', u'} D<VAR>inst✝ : Preadditive D<VAR>K : CochainComplex C ℤ<VAR>a b ab : ℤ<VAR>h : a + b = ab<VAR>n : ℤ<GOAL>n + ab = n + b + a