ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>inst✝² : WellPowered C<VAR>inst✝¹ : HasLimits C<VAR>𝒢 : Set C<VAR>inst✝ : Small.{v₁, u₁} ↑𝒢<VAR>h𝒢 : IsCoseparating 𝒢<GOAL>HasInitial C
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>inst✝² : WellPowered C<VAR>inst✝¹ : HasLimits C<VAR>𝒢 : Set C<VAR>inst✝ : Small.{v₁, u₁} ↑𝒢<VAR>h𝒢 : IsCoseparating 𝒢<VAR>this : HasProductsOfShape (↑𝒢) C<GOAL>HasInitial C
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>inst✝² : WellPowered C<VAR>inst✝¹ : HasLimits C<VAR>𝒢 : Set C<VAR>inst✝ : Small.{v₁, u₁} ↑𝒢<VAR>h𝒢 : IsCoseparating 𝒢<VAR>this✝ : HasProductsOfShape (↑𝒢) C<VAR>this : ∀ (A : C), HasProductsOfShape ((G : ↑𝒢) × (A ⟶ ↑G)) C<GOAL>HasInitial C
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>inst✝² : WellPowered C<VAR>inst✝¹ : HasLimits C<VAR>𝒢 : Set C<VAR>inst✝ : Small.{v₁, u₁} ↑𝒢<VAR>h𝒢 : IsCoseparating 𝒢<VAR>this✝¹ : HasProductsOfShape (↑𝒢) C<VAR>this✝ : ∀ (A : C), HasProductsOfShape ((G : ↑𝒢) × (A ⟶ ↑G)) C<VAR>this : CompleteLattice (Subobject (∏ᶜ Subtype.val)) := completeLatticeOfCompleteSemilatticeInf (Subobject (∏ᶜ Subtype.val))<GOAL>HasInitial C
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>inst✝² : WellPowered C<VAR>inst✝¹ : HasLimits C<VAR>𝒢 : Set C<VAR>inst✝ : Small.{v₁, u₁} ↑𝒢<VAR>h𝒢 : IsCoseparating 𝒢<VAR>this✝¹ : HasProductsOfShape (↑𝒢) C<VAR>this✝ : ∀ (A : C), HasProductsOfShape ((G : ↑𝒢) × (A ⟶ ↑G)) C<VAR>this : CompleteLattice (Subobject (∏ᶜ Subtype.val)) := completeLatticeOfCompleteSemilatticeInf (Subobject (∏ᶜ Subtype.val))<GOAL>(A : C) → Unique (Subobject.underlying.obj ⊥ ⟶ A)
<VAR>τ : Type u_1<VAR>inst✝³ : TopologicalSpace τ<VAR>inst✝² : AddCommGroup τ<VAR>inst✝¹ : TopologicalAddGroup τ<VAR>α : Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>f : Filter τ<VAR>ϕ : Flow τ α<VAR>s : Set α<VAR>hf : ∀ (t : τ), Tendsto (fun x => t + x) f f<GOAL>ω f ϕ.toFun (ω f ϕ.toFun s) ⊆ ω f ϕ.toFun s
<VAR>τ : Type u_1<VAR>inst✝³ : TopologicalSpace τ<VAR>inst✝² : AddCommGroup τ<VAR>inst✝¹ : TopologicalAddGroup τ<VAR>α : Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>f : Filter τ<VAR>ϕ : Flow τ α<VAR>s : Set α<VAR>hf : ∀ (t : τ), Tendsto (fun x => t + x) f f<GOAL>∀ (x : α), (∀ n ∈ 𝓝 x, ∀ {U : Set τ}, U ∈ f → ∃ x ∈ U, (ϕ.toFun x '' ω f ϕ.toFun s ∩ n).Nonempty) → ∀ n ∈ 𝓝 x, ∀ {U : Set τ}, U ∈ f → ∃ x ∈ U, (ϕ.toFun x '' s ∩ n).Nonempty
<VAR>τ : Type u_1<VAR>inst✝³ : TopologicalSpace τ<VAR>inst✝² : AddCommGroup τ<VAR>inst✝¹ : TopologicalAddGroup τ<VAR>α : Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>f : Filter τ<VAR>ϕ : Flow τ α<VAR>s : Set α<VAR>hf : ∀ (t : τ), Tendsto (fun x => t + x) f f<VAR>x✝ : α<VAR>h : ∀ n ∈ 𝓝 x✝, ∀ {U : Set τ}, U ∈ f → ∃ x ∈ U, (ϕ.toFun x '' ω f ϕ.toFun s ∩ n).Nonempty<VAR>n : Set α<VAR>hn : n ∈ 𝓝 x✝<VAR>u : Set τ<VAR>hu : u ∈ f<GOAL>∃ x ∈ u, (ϕ.toFun x '' s ∩ n).Nonempty
<VAR>τ : Type u_1<VAR>inst✝³ : TopologicalSpace τ<VAR>inst✝² : AddCommGroup τ<VAR>inst✝¹ : TopologicalAddGroup τ<VAR>α : Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>f : Filter τ<VAR>ϕ : Flow τ α<VAR>s : Set α<VAR>hf : ∀ (t : τ), Tendsto (fun x => t + x) f f<VAR>x✝ : α<VAR>h : ∀ n ∈ 𝓝 x✝, ∀ {U : Set τ}, U ∈ f → ∃ x ∈ U, (ϕ.toFun x '' ω f ϕ.toFun s ∩ n).Nonempty<VAR>n : Set α<VAR>hn : n ∈ 𝓝 x✝<VAR>u : Set τ<VAR>hu : u ∈ f<VAR>o : Set α<VAR>ho₁ : o ⊆ n<VAR>ho₂ : IsOpen o<VAR>ho₃ : x✝ ∈ o<GOAL>∃ x ∈ u, (ϕ.toFun x '' s ∩ n).Nonempty
<VAR>τ : Type u_1<VAR>inst✝³ : TopologicalSpace τ<VAR>inst✝² : AddCommGroup τ<VAR>inst✝¹ : TopologicalAddGroup τ<VAR>α : Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>f : Filter τ<VAR>ϕ : Flow τ α<VAR>s : Set α<VAR>hf : ∀ (t : τ), Tendsto (fun x => t + x) f f<VAR>x✝ : α<VAR>h : ∀ n ∈ 𝓝 x✝, ∀ {U : Set τ}, U ∈ f → ∃ x ∈ U, (ϕ.toFun x '' ω f ϕ.toFun s ∩ n).Nonempty<VAR>n : Set α<VAR>hn : n ∈ 𝓝 x✝<VAR>u : Set τ<VAR>hu : u ∈ f<VAR>o : Set α<VAR>ho₁ : o ⊆ n<VAR>ho₂ : IsOpen o<VAR>ho₃ : x✝ ∈ o<VAR>t : τ<VAR>_ht₁ : t ∈ u<VAR>ht₂ : (ϕ.toFun t '' ω f ϕ.toFun s ∩ o).Nonempty<GOAL>∃ x ∈ u, (ϕ.toFun x '' s ∩ n).Nonempty
<VAR>τ : Type u_1<VAR>inst✝³ : TopologicalSpace τ<VAR>inst✝² : AddCommGroup τ<VAR>inst✝¹ : TopologicalAddGroup τ<VAR>α : Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>f : Filter τ<VAR>ϕ : Flow τ α<VAR>s : Set α<VAR>hf : ∀ (t : τ), Tendsto (fun x => t + x) f f<VAR>x✝ : α<VAR>h : ∀ n ∈ 𝓝 x✝, ∀ {U : Set τ}, U ∈ f → ∃ x ∈ U, (ϕ.toFun x '' ω f ϕ.toFun s ∩ n).Nonempty<VAR>n : Set α<VAR>hn : n ∈ 𝓝 x✝<VAR>u : Set τ<VAR>hu : u ∈ f<VAR>o : Set α<VAR>ho₁ : o ⊆ n<VAR>ho₂ : IsOpen o<VAR>ho₃ : x✝ ∈ o<VAR>t : τ<VAR>_ht₁ : t ∈ u<VAR>ht₂ : (ϕ.toFun t '' ω f ϕ.toFun s ∩ o).Nonempty<VAR>l₁ : (ω f ϕ.toFun s ∩ o).Nonempty<GOAL>∃ x ∈ u, (ϕ.toFun x '' s ∩ n).Nonempty
<VAR>τ : Type u_1<VAR>inst✝³ : TopologicalSpace τ<VAR>inst✝² : AddCommGroup τ<VAR>inst✝¹ : TopologicalAddGroup τ<VAR>α : Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>f : Filter τ<VAR>ϕ : Flow τ α<VAR>s : Set α<VAR>hf : ∀ (t : τ), Tendsto (fun x => t + x) f f<VAR>x✝ : α<VAR>h : ∀ n ∈ 𝓝 x✝, ∀ {U : Set τ}, U ∈ f → ∃ x ∈ U, (ϕ.toFun x '' ω f ϕ.toFun s ∩ n).Nonempty<VAR>n : Set α<VAR>hn : n ∈ 𝓝 x✝<VAR>u : Set τ<VAR>hu : u ∈ f<VAR>o : Set α<VAR>ho₁ : o ⊆ n<VAR>ho₂ : IsOpen o<VAR>ho₃ : x✝ ∈ o<VAR>t : τ<VAR>_ht₁ : t ∈ u<VAR>ht₂ : (ϕ.toFun t '' ω f ϕ.toFun s ∩ o).Nonempty<VAR>l₁ : (ω f ϕ.toFun s ∩ o).Nonempty<VAR>l₂ : (closure (image2 ϕ.toFun u s) ∩ o).Nonempty<GOAL>∃ x ∈ u, (ϕ.toFun x '' s ∩ n).Nonempty
<VAR>τ : Type u_1<VAR>inst✝³ : TopologicalSpace τ<VAR>inst✝² : AddCommGroup τ<VAR>inst✝¹ : TopologicalAddGroup τ<VAR>α : Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>f : Filter τ<VAR>ϕ : Flow τ α<VAR>s : Set α<VAR>hf : ∀ (t : τ), Tendsto (fun x => t + x) f f<VAR>x✝ : α<VAR>h : ∀ n ∈ 𝓝 x✝, ∀ {U : Set τ}, U ∈ f → ∃ x ∈ U, (ϕ.toFun x '' ω f ϕ.toFun s ∩ n).Nonempty<VAR>n : Set α<VAR>hn : n ∈ 𝓝 x✝<VAR>u : Set τ<VAR>hu : u ∈ f<VAR>o : Set α<VAR>ho₁ : o ⊆ n<VAR>ho₂ : IsOpen o<VAR>ho₃ : x✝ ∈ o<VAR>t : τ<VAR>_ht₁ : t ∈ u<VAR>ht₂ : (ϕ.toFun t '' ω f ϕ.toFun s ∩ o).Nonempty<VAR>l₁ : (ω f ϕ.toFun s ∩ o).Nonempty<VAR>l₂ : (closure (image2 ϕ.toFun u s) ∩ o).Nonempty<VAR>l₃ : (o ∩ image2 ϕ.toFun u s).Nonempty<GOAL>∃ x ∈ u, (ϕ.toFun x '' s ∩ n).Nonempty
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝¹ : MonoidWithZero M₀<VAR>inst✝ : GroupWithZero G₀<VAR>a✝ b c d : G₀<VAR>m n : ℕ<VAR>a : G₀<VAR>ha : a ≠ 0<VAR>h : n ≤ m<GOAL>a ^ (m - n) = a ^ m * (a ^ n)⁻¹
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝¹ : MonoidWithZero M₀<VAR>inst✝ : GroupWithZero G₀<VAR>a✝ b c d : G₀<VAR>m n : ℕ<VAR>a : G₀<VAR>ha : a ≠ 0<VAR>h : n ≤ m<VAR>h1 : m - n + n = m<GOAL>a ^ (m - n) = a ^ m * (a ^ n)⁻¹
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝¹ : MonoidWithZero M₀<VAR>inst✝ : GroupWithZero G₀<VAR>a✝ b c d : G₀<VAR>m n : ℕ<VAR>a : G₀<VAR>ha : a ≠ 0<VAR>h : n ≤ m<VAR>h1 : m - n + n = m<VAR>h2 : a ^ (m - n) * a ^ n = a ^ m<GOAL>a ^ (m - n) = a ^ m * (a ^ n)⁻¹
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m✝ : MeasurableSpace α<VAR>μ✝ ν : Measure α<VAR>inst✝ : ConditionallyCompleteLinearOrder β<VAR>x : β<VAR>f✝ : α → β<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α → β<GOAL>sSup {a | ∀ᶠ (n : β) in map f (ae μ), a ≤ n} = sSup {a | μ {x | f x < a} = 0}
<VAR>R : Type u<VAR>S : Type v<VAR>a✝ b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ p q : R[X]<VAR>ι : Type u_1<VAR>a : R<GOAL>(p + C a).natDegree = p.natDegree
<VAR>R : Type u<VAR>S : Type v<VAR>a✝ b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p q : R[X]<VAR>ι : Type u_1<VAR>a : R<GOAL>(0 + C a).natDegree = natDegree 0
<VAR>R : Type u<VAR>S : Type v<VAR>a✝ b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ p q : R[X]<VAR>ι : Type u_1<VAR>a : R<VAR>hp : p ≠ 0<GOAL>(p + C a).natDegree = p.natDegree
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>c : F<VAR>h : DifferentiableWithinAt 𝕜 (fun y => c + f y) s x<GOAL>DifferentiableWithinAt 𝕜 f s x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝¹ : Zero M<VAR>a a' : α<VAR>b : M<VAR>inst✝ : Nonempty α<VAR>f : α →₀ M<GOAL>f.support.card ≤ 1 ↔ ∃ a b, f = single a b
<VAR>ι : Type u_1<VAR>I J J₁ J₂ : Box ι<VAR>π π₁ π₂ : Prepartition I<VAR>x : ι → ℝ<VAR>πi πi₁ πi₂ : (J : Box ι) → Prepartition J<VAR>h : π₂.iUnion = ↑I \ π₁.iUnion<GOAL>π₁.iUnion ∪ π₂.iUnion = ↑I
<VAR>m n a b c d✝ : ℤ<VAR>hm : 0 < m<VAR>h : a * c ≡ b * c [ZMOD m]<VAR>d : ℕ := m.gcd c<GOAL>a ≡ b [ZMOD m / ↑(m.gcd c)]
<VAR>m n a b c d✝ : ℤ<VAR>hm : 0 < m<VAR>h : m ∣ b * c - a * c<VAR>d : ℕ := m.gcd c<GOAL>m / ↑(m.gcd c) ∣ b - a
<VAR>m n a b c d✝ : ℤ<VAR>hm : 0 < m<VAR>h : m ∣ b * c - a * c<VAR>d : ℕ := m.gcd c<GOAL>m / ↑d ∣ c / ↑d * (b - a)
<VAR>m n a b c d✝ : ℤ<VAR>hm : 0 < m<VAR>h : m ∣ b * c - a * c<VAR>d : ℕ := m.gcd c<GOAL>(m / ↑(m.gcd c)).gcd (c / ↑d) = 1
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>E' : Type u_5<VAR>M' : Type u_6<VAR>H' : Type u_7<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>inst✝⁸ : TopologicalSpace H<VAR>inst✝⁷ : TopologicalSpace M<VAR>f f' : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>inst✝⁶ : NormedAddCommGroup E'<VAR>inst✝⁵ : NormedSpace 𝕜 E'<VAR>inst✝⁴ : TopologicalSpace H'<VAR>inst✝³ : TopologicalSpace M'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>s t : Set M<VAR>inst✝² : ChartedSpace H M<VAR>inst✝¹ : ChartedSpace H' M'<VAR>inst✝ : I.Boundaryless<VAR>x : M<GOAL>map (↑((chartAt H x).extend I)) (𝓝 x) = 𝓝 (↑((chartAt H x).extend I) x)
<VAR>G : Type u_1<VAR>inst✝² : SeminormedAddCommGroup G<VAR>H : Type u_2<VAR>inst✝¹ : SeminormedAddCommGroup H<VAR>K : Type u_3<VAR>inst✝ : SeminormedAddCommGroup K<VAR>f : NormedAddGroupHom G H<VAR>x : G<GOAL>‖f x‖ ≤ ‖f.completion‖ * ‖x‖
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝ : LinearOrder α<VAR>i : α<VAR>s : Finset α<VAR>his : IsGLB (↑s) i<VAR>hs : s.Nonempty<GOAL>i ∈ s
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝ : LinearOrder α<VAR>i : α<VAR>s : Finset α<VAR>his : IsGLB (↑s) i<VAR>hs : s.Nonempty<GOAL>i ∈ ↑s
<VAR>R : Type u<VAR>R' : Type u'<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>inst✝⁹ : Ring R<VAR>inst✝⁸ : Ring R'<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup M'<VAR>inst✝⁵ : AddCommGroup M₁<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module R M₁<VAR>inst✝¹ : Module R' M'<VAR>inst✝ : Module R' M₁<VAR>f : M →ₗ[R] M₁<GOAL>Module.rank R ↥(LinearMap.range f) ≤ Module.rank R M
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>m' : o → Type u_5<VAR>n' : o → Type u_6<VAR>R : Type u_7<VAR>S : Type u_8<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>inst✝¹ : NonUnitalNonAssocRing α<VAR>inst✝ : Fintype m<VAR>A B : Matrix m n α<VAR>x : m → α<GOAL>x ᵥ* (A - B) = x ᵥ* A - x ᵥ* B
<VAR>r r₁ r₂ : ℝ≥0<VAR>x y : ℝ<VAR>s : Set ℝ≥0<GOAL>↑(sInf s) = sInf (toReal '' s)
<VAR>r r₁ r₂ : ℝ≥0<VAR>x y : ℝ<GOAL>↑(sInf ∅) = sInf (toReal '' ∅)
<VAR>r r₁ r₂ : ℝ≥0<VAR>x y : ℝ<VAR>s : Set ℝ≥0<VAR>hs : s.Nonempty<GOAL>↑(sInf s) = sInf (toReal '' s)
<VAR>r r₁ r₂ : ℝ≥0<VAR>x y : ℝ<VAR>s : Set ℝ≥0<VAR>hs : s.Nonempty<VAR>A : sInf (Subtype.val '' s) ∈ Set.Ici 0<GOAL>↑(sInf s) = sInf (toReal '' s)
<VAR>x y z : ℤ<VAR>h : PythagoreanTriple x y z<VAR>hc : x.gcd y = 1<GOAL>y.gcd z = 1
<VAR>x y z : ℤ<VAR>h : PythagoreanTriple x y z<VAR>hc : x.gcd y = 1<VAR>H : ¬y.gcd z = 1<GOAL>False
<VAR>x y z : ℤ<VAR>h : PythagoreanTriple x y z<VAR>hc : x.gcd y = 1<VAR>H : ¬y.gcd z = 1<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>hpy : p ∣ y.natAbs<VAR>hpz : p ∣ z.natAbs<GOAL>False
<VAR>x y z : ℤ<VAR>h : PythagoreanTriple x y z<VAR>hc : x.gcd y = 1<VAR>H : ¬y.gcd z = 1<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>hpy : p ∣ y.natAbs<VAR>hpz : p ∣ z.natAbs<GOAL>p ∣ 1
<VAR>x y z : ℤ<VAR>h : PythagoreanTriple x y z<VAR>hc : x.gcd y = 1<VAR>H : ¬y.gcd z = 1<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>hpy : p ∣ y.natAbs<VAR>hpz : p ∣ z.natAbs<GOAL>p ∣ x.gcd y
<VAR>x y z : ℤ<VAR>h : PythagoreanTriple x y z<VAR>hc : x.gcd y = 1<VAR>H : ¬y.gcd z = 1<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>hpy : p ∣ y.natAbs<VAR>hpz : p ∣ z.natAbs<GOAL>↑p ∣ x ^ 2
<VAR>x y z : ℤ<VAR>h : PythagoreanTriple x y z<VAR>hc : x.gcd y = 1<VAR>H : ¬y.gcd z = 1<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>hpy : p ∣ y.natAbs<VAR>hpz : p ∣ z.natAbs<GOAL>↑p ∣ z * z - y * y
<VAR>x y z : ℤ<VAR>h : PythagoreanTriple x y z<VAR>hc : x.gcd y = 1<VAR>H : ¬y.gcd z = 1<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>hpy : ↑p ∣ y<VAR>hpz : ↑p ∣ z<GOAL>↑p ∣ z * z - y * y
<VAR>f : ZFSet → ZFSet<VAR>H : Definable 1 f<VAR>x z : ZFSet<VAR>zx : z ∈ x<VAR>y : ZFSet<VAR>yx : (fun w => z.pair w ∈ map f x) y<GOAL>y = f z
<VAR>f : ZFSet → ZFSet<VAR>H : Definable 1 f<VAR>x z : ZFSet<VAR>zx : z ∈ x<VAR>y : ZFSet<VAR>yx : (fun w => z.pair w ∈ map f x) y<VAR>w : ZFSet<VAR>left✝ : w ∈ x<VAR>we : w.pair (f w) = z.pair y<GOAL>y = f z
<VAR>f : ZFSet → ZFSet<VAR>H : Definable 1 f<VAR>x z : ZFSet<VAR>zx : z ∈ x<VAR>y : ZFSet<VAR>yx : (fun w => z.pair w ∈ map f x) y<VAR>w : ZFSet<VAR>left✝ : w ∈ x<VAR>we : w.pair (f w) = z.pair y<VAR>wz : w = z<VAR>fy : f w = y<GOAL>y = f z
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι✝ : Sort y<VAR>s t u✝ : Set α<VAR>inst✝² : MeasurableSpace α<VAR>ι : Type u_5<VAR>f : ι → α → ℝ≥0∞<VAR>g : α → ℝ≥0∞<VAR>u : Filter ι<VAR>inst✝¹ : u.NeBot<VAR>inst✝ : u.IsCountablyGenerated<VAR>hf : ∀ (i : ι), Measurable (f i)<VAR>lim : Tendsto f u (𝓝 g)<GOAL>Measurable g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι✝ : Sort y<VAR>s t u✝ : Set α<VAR>inst✝² : MeasurableSpace α<VAR>ι : Type u_5<VAR>f : ι → α → ℝ≥0∞<VAR>g : α → ℝ≥0∞<VAR>u : Filter ι<VAR>inst✝¹ : u.NeBot<VAR>inst✝ : u.IsCountablyGenerated<VAR>hf : ∀ (i : ι), Measurable (f i)<VAR>lim : Tendsto f u (𝓝 g)<VAR>x : ℕ → ι<VAR>hx : Tendsto x atTop u<GOAL>Measurable g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι✝ : Sort y<VAR>s t u✝ : Set α<VAR>inst✝² : MeasurableSpace α<VAR>ι : Type u_5<VAR>f : ι → α → ℝ≥0∞<VAR>g : α → ℝ≥0∞<VAR>u : Filter ι<VAR>inst✝¹ : u.NeBot<VAR>inst✝ : u.IsCountablyGenerated<VAR>hf : ∀ (i : ι), Measurable (f i)<VAR>lim : ∀ (x : α), Tendsto (fun i => f i x) u (𝓝 (g x))<VAR>x : ℕ → ι<VAR>hx : Tendsto x atTop u<GOAL>Measurable g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι✝ : Sort y<VAR>s t u✝ : Set α<VAR>inst✝² : MeasurableSpace α<VAR>ι : Type u_5<VAR>f : ι → α → ℝ≥0∞<VAR>g : α → ℝ≥0∞<VAR>u : Filter ι<VAR>inst✝¹ : u.NeBot<VAR>inst✝ : u.IsCountablyGenerated<VAR>hf : ∀ (i : ι), Measurable (f i)<VAR>lim : ∀ (x : α), Tendsto (fun i => f i x) u (𝓝 (g x))<VAR>x : ℕ → ι<VAR>hx : Tendsto x atTop u<VAR>this : (fun y => liminf (fun n => f (x n) y) atTop) = g<GOAL>Measurable g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι✝ : Sort y<VAR>s t u✝ : Set α<VAR>inst✝² : MeasurableSpace α<VAR>ι : Type u_5<VAR>f : ι → α → ℝ≥0∞<VAR>g : α → ℝ≥0∞<VAR>u : Filter ι<VAR>inst✝¹ : u.NeBot<VAR>inst✝ : u.IsCountablyGenerated<VAR>hf : ∀ (i : ι), Measurable (f i)<VAR>lim : ∀ (x : α), Tendsto (fun i => f i x) u (𝓝 (g x))<VAR>x : ℕ → ι<VAR>hx : Tendsto x atTop u<VAR>this : (fun y => liminf (fun n => f (x n) y) atTop) = g<GOAL>Measurable fun y => liminf (fun n => f (x n) y) atTop
<VAR>R M : Type u<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>I : Ideal R<VAR>F F' : I.Filtration M<VAR>n₀ : ℕ<VAR>hn : ∀ n ≥ n₀, I • F.N n = F.N (n + 1)<GOAL>∃ n₀, ∀ (k : ℕ), F.N (n₀ + k) = I ^ k • F.N n₀
<VAR>R M : Type u<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>I : Ideal R<VAR>F F' : I.Filtration M<VAR>n₀ : ℕ<VAR>hn : ∀ n ≥ n₀, I • F.N n = F.N (n + 1)<GOAL>∀ (k : ℕ), F.N (n₀ + k) = I ^ k • F.N n₀
<VAR>a b m n✝ p d n : ℕ<VAR>hd : d ≠ 0<VAR>hdn : d ≤ n<GOAL>d ∣ n ↔ (n / d).factorization = n.factorization - d.factorization
<VAR>a b m n✝ p d n : ℕ<VAR>hd : d ≠ 0<VAR>hdn : d ≤ n<GOAL>(n / d).factorization = n.factorization - d.factorization → d ∣ n
<VAR>a b m n p d : ℕ<VAR>hd : d ≠ 0<VAR>hdn : d ≤ d<GOAL>(d / d).factorization = d.factorization - d.factorization → d ∣ d
<VAR>a b m n✝ p d n : ℕ<VAR>hd : d ≠ 0<VAR>hdn : d ≤ n<VAR>hd_lt_n : d < n<GOAL>(n / d).factorization = n.factorization - d.factorization → d ∣ n
<VAR>a b m n✝ p d n : ℕ<VAR>hd : d ≠ 0<VAR>hdn : d ≤ n<VAR>hd_lt_n : d < n<VAR>h1 : n / d ≠ 0<GOAL>(n / d).factorization = n.factorization - d.factorization → d ∣ n
<VAR>a b m n✝ p d n : ℕ<VAR>hd : d ≠ 0<VAR>hdn : d ≤ n<VAR>hd_lt_n : d < n<VAR>h1 : n / d ≠ 0<VAR>h : (n / d).factorization = n.factorization - d.factorization<GOAL>d ∣ n
<VAR>a b m n✝ p d n : ℕ<VAR>hd : d ≠ 0<VAR>hdn : d ≤ n<VAR>hd_lt_n : d < n<VAR>h1 : n / d ≠ 0<VAR>h : (n / d).factorization = n.factorization - d.factorization<GOAL>n ≤ n / d * d
<VAR>a b m n✝ p d n : ℕ<VAR>hd : d ≠ 0<VAR>hdn : d ≤ n<VAR>hd_lt_n : d < n<VAR>h1 : n / d ≠ 0<VAR>h : (n / d).factorization = n.factorization - d.factorization<VAR>h2 : ¬n ≤ n / d * d<GOAL>False
<VAR>a b m n✝ p✝ d n : ℕ<VAR>hd : d ≠ 0<VAR>hdn : d ≤ n<VAR>hd_lt_n : d < n<VAR>h1 : n / d ≠ 0<VAR>h : (n / d).factorization = n.factorization - d.factorization<VAR>h2 : ¬n ≤ n / d * d<VAR>p : ℕ<VAR>hp : (n / d * d).factorization p < n.factorization p<GOAL>False
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>o : Ordinal.{u_3}<VAR>c : Cardinal.{u_3}<VAR>ho : o ≤ c.ord<GOAL>o.card ≤ c
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>o : Ordinal.{u_3}<VAR>c : Cardinal.{u_3}<VAR>ho : o ≤ c.ord<GOAL>o.card ≤ c.ord.card
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>x : M<VAR>p p' : Submodule R M<VAR>inst✝⁴ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>s t : Set M<GOAL>span R (insert 0 s) = span R s
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>x : M<VAR>p p' : Submodule R M<VAR>inst✝⁴ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>s t : Set M<GOAL>span R (insert 0 s) ≤ span R s
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>x : M<VAR>p p' : Submodule R M<VAR>inst✝⁴ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>s t : Set M<GOAL>0 ∈ ↑(span R s) ∧ s ⊆ ↑(span R s)
<VAR>𝕜 : Type u<VAR>hnorm : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>inst✝¹⁷ : AddCommGroup E<VAR>inst✝¹⁶ : Module 𝕜 E<VAR>inst✝¹⁵ : TopologicalSpace E<VAR>inst✝¹⁴ : TopologicalAddGroup E<VAR>inst✝¹³ : ContinuousSMul 𝕜 E<VAR>F : Type w<VAR>inst✝¹² : AddCommGroup F<VAR>inst✝¹¹ : Module 𝕜 F<VAR>inst✝¹⁰ : TopologicalSpace F<VAR>inst✝⁹ : TopologicalAddGroup F<VAR>inst✝⁸ : ContinuousSMul 𝕜 F<VAR>F' : Type x<VAR>inst✝⁷ : AddCommGroup F'<VAR>inst✝⁶ : Module 𝕜 F'<VAR>inst✝⁵ : TopologicalSpace F'<VAR>inst✝⁴ : TopologicalAddGroup F'<VAR>inst✝³ : ContinuousSMul 𝕜 F'<VAR>inst✝² : CompleteSpace 𝕜<VAR>inst✝¹ : T2Space E<VAR>ι : Type v<VAR>inst✝ : Fintype ι<VAR>ξ : Basis ι 𝕜 E<VAR>this : UniformSpace E := TopologicalAddGroup.toUniformSpace E<GOAL>Continuous ⇑ξ.equivFun
<VAR>𝕜 : Type u<VAR>hnorm : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>inst✝¹⁷ : AddCommGroup E<VAR>inst✝¹⁶ : Module 𝕜 E<VAR>inst✝¹⁵ : TopologicalSpace E<VAR>inst✝¹⁴ : TopologicalAddGroup E<VAR>inst✝¹³ : ContinuousSMul 𝕜 E<VAR>F : Type w<VAR>inst✝¹² : AddCommGroup F<VAR>inst✝¹¹ : Module 𝕜 F<VAR>inst✝¹⁰ : TopologicalSpace F<VAR>inst✝⁹ : TopologicalAddGroup F<VAR>inst✝⁸ : ContinuousSMul 𝕜 F<VAR>F' : Type x<VAR>inst✝⁷ : AddCommGroup F'<VAR>inst✝⁶ : Module 𝕜 F'<VAR>inst✝⁵ : TopologicalSpace F'<VAR>inst✝⁴ : TopologicalAddGroup F'<VAR>inst✝³ : ContinuousSMul 𝕜 F'<VAR>inst✝² : CompleteSpace 𝕜<VAR>inst✝¹ : T2Space E<VAR>ι : Type v<VAR>inst✝ : Fintype ι<VAR>ξ : Basis ι 𝕜 E<VAR>this✝ : UniformSpace E := TopologicalAddGroup.toUniformSpace E<VAR>this : UniformAddGroup E := comm_topologicalAddGroup_is_uniform<GOAL>Continuous ⇑ξ.equivFun
<VAR>C : Type u<VAR>X Y : F C<VAR>f' : X ⟶ᵐ Y<GOAL>(fun n => X.normalizeObj n) = Y.normalizeObj
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>γ : Type u_3<VAR>A : Type u_4<VAR>B : Type u_5<VAR>C : Type u_6<VAR>inst✝³ : AddCommMonoid A<VAR>inst✝² : AddCommMonoid B<VAR>inst✝¹ : AddCommMonoid C<VAR>t : ι → A → C<VAR>h0 : ∀ (i : ι), t i 0 = 0<VAR>h1 : ∀ (i : ι) (x y : A), t i (x + y) = t i x + t i y<VAR>s : Finset α<VAR>f : α → ι →₀ A<VAR>i✝ : ι<VAR>g : ι →₀ A<VAR>k : ι → A → γ → B<VAR>x : γ<VAR>β : Type u_7<VAR>M : Type u_8<VAR>M' : Type u_9<VAR>N : Type u_10<VAR>P : Type u_11<VAR>G : Type u_12<VAR>H : Type u_13<VAR>R : Type u_14<VAR>S : Type u_15<VAR>inst✝ : AddCommMonoid M<VAR>n : ℕ<VAR>σ : Fin n →₀ M<VAR>i : M<GOAL>((cons i σ).sum fun x e => e) = i + σ.sum fun x e => e
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>γ : Type u_3<VAR>A : Type u_4<VAR>B : Type u_5<VAR>C : Type u_6<VAR>inst✝³ : AddCommMonoid A<VAR>inst✝² : AddCommMonoid B<VAR>inst✝¹ : AddCommMonoid C<VAR>t : ι → A → C<VAR>h0 : ∀ (i : ι), t i 0 = 0<VAR>h1 : ∀ (i : ι) (x y : A), t i (x + y) = t i x + t i y<VAR>s : Finset α<VAR>f : α → ι →₀ A<VAR>i✝ : ι<VAR>g : ι →₀ A<VAR>k : ι → A → γ → B<VAR>x : γ<VAR>β : Type u_7<VAR>M : Type u_8<VAR>M' : Type u_9<VAR>N : Type u_10<VAR>P : Type u_11<VAR>G : Type u_12<VAR>H : Type u_13<VAR>R : Type u_14<VAR>S : Type u_15<VAR>inst✝ : AddCommMonoid M<VAR>n : ℕ<VAR>σ : Fin n →₀ M<VAR>i : M<GOAL>∑ i_1 : Fin (n + 1), (cons i σ) i_1 = i + ∑ i : Fin n, σ i
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>κ : ι → Sort u_1<VAR>a✝ a₁ a₂ : α<VAR>b✝ b₁ b₂ : β<VAR>l : α → β<VAR>u : β → α<VAR>inst✝¹ : SemilatticeInf α<VAR>inst✝ : SemilatticeInf β<VAR>gi : GaloisInsertion l u<VAR>a b : β<GOAL>l (u (a ⊓ b)) = a ⊓ b
<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>G : Type u_5<VAR>inst✝² : Group G<VAR>inst✝¹ : DistribMulAction G M<VAR>inst✝ : SMulCommClass G R M<VAR>g : G<VAR>v : ι → M<GOAL>(g • e).det v = e.det (g⁻¹ • v)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n : ℕ<VAR>p : Fin (n + 1) → Prop<VAR>inst✝ : DecidablePred p<GOAL>(filter p univ).card = (if p 0 then 1 else 0) + (filter (p ∘ succ) univ).card
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n : ℕ<VAR>p : Fin (n + 1) → Prop<VAR>inst✝ : DecidablePred p<GOAL>(if p 0 then {0} else ∅).card + (filter (p ∘ ⇑{ toFun := succ, inj' := ⋯ }) univ).card = (if p 0 then 1 else 0) + (filter (p ∘ succ) univ).card
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P : Fin 3 → F<VAR>hPz : P z ≠ 0<GOAL>W.Nonsingular P ↔ W.Equation P ∧ ((eval P) W.polynomialX ≠ 0 ∨ (eval P) W.polynomialY ≠ 0)