ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>inst✝³⁷ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³⁶ : NormedAddCommGroup E<VAR>inst✝³⁵ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝³⁴ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝³³ : TopologicalSpace M<VAR>inst✝³² : ChartedSpace H M<VAR>inst✝³¹ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝³⁰ : NormedAddCommGroup E'<VAR>inst✝²⁹ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝²⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝²⁷ : TopologicalSpace M'<VAR>inst✝²⁶ : ChartedSpace H' M'<VAR>inst✝²⁵ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝²⁴ : NormedAddCommGroup E''<VAR>inst✝²³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝²² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝²¹ : TopologicalSpace M''<VAR>inst✝²⁰ : ChartedSpace H'' M''<VAR>F : Type u_11<VAR>inst✝¹⁹ : NormedAddCommGroup F<VAR>inst✝¹⁸ : NormedSpace 𝕜 F<VAR>G : Type u_12<VAR>inst✝¹⁷ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_13<VAR>inst✝¹⁶ : TopologicalSpace N<VAR>inst✝¹⁵ : ChartedSpace G N<VAR>inst✝¹⁴ : SmoothManifoldWithCorners J N<VAR>F' : Type u_14<VAR>inst✝¹³ : NormedAddCommGroup F'<VAR>inst✝¹² : NormedSpace 𝕜 F'<VAR>G' : Type u_15<VAR>inst✝¹¹ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_16<VAR>inst✝¹⁰ : TopologicalSpace N'<VAR>inst✝⁹ : ChartedSpace G' N'<VAR>inst✝⁸ : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_17<VAR>inst✝⁷ : NormedAddCommGroup F₁<VAR>inst✝⁶ : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_18<VAR>inst✝⁵ : NormedAddCommGroup F₂<VAR>inst✝⁴ : NormedSpace 𝕜 F₂<VAR>F₃ : Type u_19<VAR>inst✝³ : NormedAddCommGroup F₃<VAR>inst✝² : NormedSpace 𝕜 F₃<VAR>F₄ : Type u_20<VAR>inst✝¹ : NormedAddCommGroup F₄<VAR>inst✝ : NormedSpace 𝕜 F₄<VAR>e : PartialHomeomorph M H<VAR>e' : PartialHomeomorph M' H'<VAR>f✝ f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x : M<VAR>m n : ℕ∞<VAR>f : M → E'<VAR>g : M → F'<VAR>hf : ContinuousWithinAt f s x ∧ ContDiffWithinAt 𝕜 n (↑(extChartAt 𝓘(𝕜, E') (f x)) ∘ f ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I x) x)<VAR>hg : ContinuousWithinAt g s x ∧ ContDiffWithinAt 𝕜 n (↑(extChartAt 𝓘(𝕜, F') (g x)) ∘ g ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I x) x)<GOAL>ContinuousWithinAt (fun x => (f x, g x)) s x ∧ ContDiffWithinAt 𝕜 n (↑(extChartAt 𝓘(𝕜, E' × F') (f x, g x)) ∘ (fun x => (f x, g x)) ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I x) x)
<VAR>R : Type u<VAR>A : Type v<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra R A<VAR>a b : A<VAR>r : Rˣ<VAR>h₁ : ∀ (x y : A), IsUnit (1 - x * y) → IsUnit (1 - y * x)<VAR>this : IsUnit (1 - r⁻¹ • a * b) ↔ IsUnit (1 - b * r⁻¹ • a)<GOAL>↑r ∈ σ (a * b) ↔ ↑r ∈ σ (b * a)
<VAR>R : Type u<VAR>A : Type v<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra R A<VAR>a b : A<VAR>r : Rˣ<VAR>h₁ : ∀ (x y : A), IsUnit (1 - x * y) → IsUnit (1 - y * x)<VAR>this : IsUnit (1 - r⁻¹ • a * b) ↔ IsUnit (1 - r⁻¹ • (b * a))<GOAL>↑r ∈ σ (a * b) ↔ ↑r ∈ σ (b * a)
<VAR>x y : ℝ<GOAL>sin x ^ 2 = 1 / 2 - cos (2 * x) / 2
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>inst✝¹ : LinearOrderedSemiring R<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : ExistsAddOfLE R<VAR>hn : Odd n<GOAL>StrictMono fun a => a ^ n
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>inst✝¹ : LinearOrderedSemiring R<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : ExistsAddOfLE R<VAR>hn : Odd n<VAR>hn₀ : n ≠ 0<GOAL>StrictMono fun a => a ^ n
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>inst✝¹ : LinearOrderedSemiring R<VAR>a✝ b✝ : R<VAR>m n : ℕ<VAR>inst✝ : ExistsAddOfLE R<VAR>hn : Odd n<VAR>hn₀ : n ≠ 0<VAR>a b : R<VAR>hab : a < b<GOAL>(fun a => a ^ n) a < (fun a => a ^ n) b
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>inst✝¹ : LinearOrderedSemiring R<VAR>a✝ b✝ : R<VAR>m n : ℕ<VAR>inst✝ : ExistsAddOfLE R<VAR>hn : Odd n<VAR>hn₀ : n ≠ 0<VAR>a b : R<VAR>hab : a < b<VAR>ha : 0 ≤ a<GOAL>(fun a => a ^ n) a < (fun a => a ^ n) b
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>inst✝¹ : LinearOrderedSemiring R<VAR>a✝ b✝ : R<VAR>m n : ℕ<VAR>inst✝ : ExistsAddOfLE R<VAR>hn : Odd n<VAR>hn₀ : n ≠ 0<VAR>a b : R<VAR>hab : a < b<VAR>ha : a ≤ 0<GOAL>(fun a => a ^ n) a < (fun a => a ^ n) b
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>inst✝¹ : LinearOrderedSemiring R<VAR>a✝ b✝ : R<VAR>m n : ℕ<VAR>inst✝ : ExistsAddOfLE R<VAR>hn : Odd n<VAR>hn₀ : n ≠ 0<VAR>a b : R<VAR>hab : a < b<VAR>ha : a ≤ 0<VAR>hb : 0 < b<GOAL>(fun a => a ^ n) a < (fun a => a ^ n) b
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>inst✝¹ : LinearOrderedSemiring R<VAR>a✝ b✝ : R<VAR>m n : ℕ<VAR>inst✝ : ExistsAddOfLE R<VAR>hn : Odd n<VAR>hn₀ : n ≠ 0<VAR>a b : R<VAR>hab : a < b<VAR>ha : a ≤ 0<VAR>hb : b ≤ 0<GOAL>(fun a => a ^ n) a < (fun a => a ^ n) b
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>inst✝¹ : LinearOrderedSemiring R<VAR>a✝ b✝ : R<VAR>m n : ℕ<VAR>inst✝ : ExistsAddOfLE R<VAR>hn : Odd n<VAR>hn₀ : n ≠ 0<VAR>a b : R<VAR>hab : a < b<VAR>ha : a ≤ 0<VAR>hb : b ≤ 0<VAR>c : R<VAR>hac : 0 = a + c<GOAL>(fun a => a ^ n) a < (fun a => a ^ n) b
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>inst✝¹ : LinearOrderedSemiring R<VAR>a✝ b✝ : R<VAR>m n : ℕ<VAR>inst✝ : ExistsAddOfLE R<VAR>hn : Odd n<VAR>hn₀ : n ≠ 0<VAR>a b : R<VAR>hab : a < b<VAR>ha : a ≤ 0<VAR>hb : b ≤ 0<VAR>c : R<VAR>hac : 0 = a + c<VAR>d : R<VAR>hbd : 0 = b + d<GOAL>(fun a => a ^ n) a < (fun a => a ^ n) b
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>inst✝¹ : LinearOrderedSemiring R<VAR>a✝ b✝ : R<VAR>m n : ℕ<VAR>inst✝ : ExistsAddOfLE R<VAR>hn : Odd n<VAR>hn₀ : n ≠ 0<VAR>a b : R<VAR>hab : a < b<VAR>ha : a ≤ 0<VAR>hb : b ≤ 0<VAR>c : R<VAR>hac : 0 = a + c<VAR>d : R<VAR>hbd : 0 = b + d<VAR>hd : 0 ≤ d<GOAL>(fun a => a ^ n) a < (fun a => a ^ n) b
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>inst✝¹ : LinearOrderedSemiring R<VAR>a✝ b✝ : R<VAR>m n : ℕ<VAR>inst✝ : ExistsAddOfLE R<VAR>hn : Odd n<VAR>hn₀ : n ≠ 0<VAR>a b : R<VAR>hab : a < b<VAR>ha : a ≤ 0<VAR>hb : b ≤ 0<VAR>c : R<VAR>hac : 0 = a + c<VAR>d : R<VAR>hbd : 0 = b + d<VAR>hd : 0 ≤ d<GOAL>(fun a => a ^ n) a + (c ^ n + d ^ n) < (fun a => a ^ n) b + (c ^ n + d ^ n)
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>inst✝¹ : LinearOrderedSemiring R<VAR>a✝ b✝ : R<VAR>m n : ℕ<VAR>inst✝ : ExistsAddOfLE R<VAR>hn : Odd n<VAR>hn₀ : n ≠ 0<VAR>a b : R<VAR>hab : a < b<VAR>ha : a ≤ 0<VAR>hb : b ≤ 0<VAR>c : R<VAR>hac : 0 = a + c<VAR>d : R<VAR>hbd : 0 = b + d<VAR>hd : 0 ≤ d<GOAL>a ^ n + (c ^ n + d ^ n) < b ^ n + (c ^ n + d ^ n)
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>inst✝¹ : LinearOrderedSemiring R<VAR>a✝ b✝ : R<VAR>m n : ℕ<VAR>inst✝ : ExistsAddOfLE R<VAR>hn : Odd n<VAR>hn₀ : n ≠ 0<VAR>a b : R<VAR>hab : a < b<VAR>ha : a ≤ 0<VAR>hb : b ≤ 0<VAR>c : R<VAR>hac : 0 = a + c<VAR>d : R<VAR>hbd : 0 = b + d<VAR>hd : 0 ≤ d<GOAL>d < c
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>inst✝¹ : LinearOrderedSemiring R<VAR>a✝ b✝ : R<VAR>m n : ℕ<VAR>inst✝ : ExistsAddOfLE R<VAR>hn : Odd n<VAR>hn₀ : n ≠ 0<VAR>a b : R<VAR>hab : a < b<VAR>ha : a ≤ 0<VAR>hb : b ≤ 0<VAR>c : R<VAR>hac : 0 = a + c<VAR>d : R<VAR>hbd : 0 = b + d<VAR>hd : 0 ≤ d<GOAL>d + (a + b) < c + (a + b)
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>ι : Type u_4<VAR>s : AffineSubspace k P<VAR>p₁ p₂ p₃ : P<VAR>hp₁p₃ : p₁ ≠ p₃<VAR>hp₁ : p₁ ∈ s<VAR>hp₂ : p₂ ∉ s<VAR>hp₃ : p₃ ∈ s<GOAL>AffineIndependent k ![p₁, p₂, p₃]
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>ι : Type u_4<VAR>s : AffineSubspace k P<VAR>p₁ p₂ p₃ : P<VAR>hp₁p₃ : p₁ ≠ p₃<VAR>hp₁ : p₁ ∈ s<VAR>hp₂ : p₂ ∉ s<VAR>hp₃ : p₃ ∈ s<GOAL>AffineIndependent k (![p₁, p₂, p₃] ∘ ⇑(Equiv.swap 1 2))
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>ι : Type u_4<VAR>s : AffineSubspace k P<VAR>p₁ p₂ p₃ : P<VAR>hp₁p₃ : p₁ ≠ p₃<VAR>hp₁ : p₁ ∈ s<VAR>hp₂ : p₂ ∉ s<VAR>hp₃ : p₃ ∈ s<GOAL>![p₁, p₂, p₃] ∘ ⇑(Equiv.swap 1 2) = ![p₁, p₃, p₂]
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>R : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁶ : Fintype m<VAR>inst✝⁵ : Fintype n<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : PartialOrder R<VAR>inst✝² : StarRing R<VAR>inst✝¹ : StarOrderedRing R<VAR>inst✝ : RCLike 𝕜<VAR>M : Matrix n n R<VAR>hM : M.PosSemidef<VAR>e : m → n<GOAL>(M.submatrix e e).PosSemidef
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>inst✝¹⁹ : Field R<VAR>inst✝¹⁸ : AddCommGroup V<VAR>inst✝¹⁷ : TopologicalSpace R<VAR>inst✝¹⁶ : TopologicalSpace V<VAR>inst✝¹⁵ : TopologicalRing R<VAR>inst✝¹⁴ : TopologicalAddGroup V<VAR>inst✝¹³ : Module R V<VAR>inst✝¹² : SeparatingDual R V<VAR>𝕜 : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>inst✝⁶ : SeparatingDual 𝕜 E<VAR>inst✝⁵ : Nontrivial E<VAR>ι : Type u_6<VAR>inst✝⁴ : Finite ι<VAR>M : ι → Type u_7<VAR>inst✝³ : (i : ι) → NormedAddCommGroup (M i)<VAR>inst✝² : (i : ι) → NormedSpace 𝕜 (M i)<VAR>inst✝¹ : ∀ (i : ι), SeparatingDual 𝕜 (M i)<VAR>inst✝ : CompleteSpace (ContinuousMultilinearMap 𝕜 M F)<VAR>m : (i : ι) → M i<VAR>hm : ∀ (i : ι), m i ≠ 0<GOAL>CompleteSpace F
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>inst✝¹⁹ : Field R<VAR>inst✝¹⁸ : AddCommGroup V<VAR>inst✝¹⁷ : TopologicalSpace R<VAR>inst✝¹⁶ : TopologicalSpace V<VAR>inst✝¹⁵ : TopologicalRing R<VAR>inst✝¹⁴ : TopologicalAddGroup V<VAR>inst✝¹³ : Module R V<VAR>inst✝¹² : SeparatingDual R V<VAR>𝕜 : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>inst✝⁶ : SeparatingDual 𝕜 E<VAR>inst✝⁵ : Nontrivial E<VAR>ι : Type u_6<VAR>inst✝⁴ : Finite ι<VAR>M : ι → Type u_7<VAR>inst✝³ : (i : ι) → NormedAddCommGroup (M i)<VAR>inst✝² : (i : ι) → NormedSpace 𝕜 (M i)<VAR>inst✝¹ : ∀ (i : ι), SeparatingDual 𝕜 (M i)<VAR>inst✝ : CompleteSpace (ContinuousMultilinearMap 𝕜 M F)<VAR>m : (i : ι) → M i<VAR>hm : ∀ (i : ι), m i ≠ 0<VAR>f : ℕ → F<VAR>hf : CauchySeq f<GOAL>∃ a, Tendsto f atTop (𝓝 a)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>inst✝¹⁹ : Field R<VAR>inst✝¹⁸ : AddCommGroup V<VAR>inst✝¹⁷ : TopologicalSpace R<VAR>inst✝¹⁶ : TopologicalSpace V<VAR>inst✝¹⁵ : TopologicalRing R<VAR>inst✝¹⁴ : TopologicalAddGroup V<VAR>inst✝¹³ : Module R V<VAR>inst✝¹² : SeparatingDual R V<VAR>𝕜 : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>inst✝⁶ : SeparatingDual 𝕜 E<VAR>inst✝⁵ : Nontrivial E<VAR>ι : Type u_6<VAR>inst✝⁴ : Finite ι<VAR>M : ι → Type u_7<VAR>inst✝³ : (i : ι) → NormedAddCommGroup (M i)<VAR>inst✝² : (i : ι) → NormedSpace 𝕜 (M i)<VAR>inst✝¹ : ∀ (i : ι), SeparatingDual 𝕜 (M i)<VAR>inst✝ : CompleteSpace (ContinuousMultilinearMap 𝕜 M F)<VAR>m : (i : ι) → M i<VAR>hm : ∀ (i : ι), m i ≠ 0<VAR>f : ℕ → F<VAR>hf : CauchySeq f<VAR>this : ∀ (i : ι), ∃ φ, φ (m i) = 1<GOAL>∃ a, Tendsto f atTop (𝓝 a)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>inst✝¹⁹ : Field R<VAR>inst✝¹⁸ : AddCommGroup V<VAR>inst✝¹⁷ : TopologicalSpace R<VAR>inst✝¹⁶ : TopologicalSpace V<VAR>inst✝¹⁵ : TopologicalRing R<VAR>inst✝¹⁴ : TopologicalAddGroup V<VAR>inst✝¹³ : Module R V<VAR>inst✝¹² : SeparatingDual R V<VAR>𝕜 : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>inst✝⁶ : SeparatingDual 𝕜 E<VAR>inst✝⁵ : Nontrivial E<VAR>ι : Type u_6<VAR>inst✝⁴ : Finite ι<VAR>M : ι → Type u_7<VAR>inst✝³ : (i : ι) → NormedAddCommGroup (M i)<VAR>inst✝² : (i : ι) → NormedSpace 𝕜 (M i)<VAR>inst✝¹ : ∀ (i : ι), SeparatingDual 𝕜 (M i)<VAR>inst✝ : CompleteSpace (ContinuousMultilinearMap 𝕜 M F)<VAR>m : (i : ι) → M i<VAR>hm : ∀ (i : ι), m i ≠ 0<VAR>f : ℕ → F<VAR>hf : CauchySeq f<VAR>φ : (i : ι) → M i →L[𝕜] 𝕜<VAR>hφ : ∀ (i : ι), (φ i) (m i) = 1<GOAL>∃ a, Tendsto f atTop (𝓝 a)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>inst✝¹⁹ : Field R<VAR>inst✝¹⁸ : AddCommGroup V<VAR>inst✝¹⁷ : TopologicalSpace R<VAR>inst✝¹⁶ : TopologicalSpace V<VAR>inst✝¹⁵ : TopologicalRing R<VAR>inst✝¹⁴ : TopologicalAddGroup V<VAR>inst✝¹³ : Module R V<VAR>inst✝¹² : SeparatingDual R V<VAR>𝕜 : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>inst✝⁶ : SeparatingDual 𝕜 E<VAR>inst✝⁵ : Nontrivial E<VAR>ι : Type u_6<VAR>inst✝⁴ : Finite ι<VAR>M : ι → Type u_7<VAR>inst✝³ : (i : ι) → NormedAddCommGroup (M i)<VAR>inst✝² : (i : ι) → NormedSpace 𝕜 (M i)<VAR>inst✝¹ : ∀ (i : ι), SeparatingDual 𝕜 (M i)<VAR>inst✝ : CompleteSpace (ContinuousMultilinearMap 𝕜 M F)<VAR>m : (i : ι) → M i<VAR>hm : ∀ (i : ι), m i ≠ 0<VAR>f : ℕ → F<VAR>hf : CauchySeq f<VAR>φ : (i : ι) → M i →L[𝕜] 𝕜<VAR>hφ : ∀ (i : ι), (φ i) (m i) = 1<VAR>val✝ : Fintype ι<GOAL>∃ a, Tendsto f atTop (𝓝 a)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>inst✝¹⁹ : Field R<VAR>inst✝¹⁸ : AddCommGroup V<VAR>inst✝¹⁷ : TopologicalSpace R<VAR>inst✝¹⁶ : TopologicalSpace V<VAR>inst✝¹⁵ : TopologicalRing R<VAR>inst✝¹⁴ : TopologicalAddGroup V<VAR>inst✝¹³ : Module R V<VAR>inst✝¹² : SeparatingDual R V<VAR>𝕜 : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>inst✝⁶ : SeparatingDual 𝕜 E<VAR>inst✝⁵ : Nontrivial E<VAR>ι : Type u_6<VAR>inst✝⁴ : Finite ι<VAR>M : ι → Type u_7<VAR>inst✝³ : (i : ι) → NormedAddCommGroup (M i)<VAR>inst✝² : (i : ι) → NormedSpace 𝕜 (M i)<VAR>inst✝¹ : ∀ (i : ι), SeparatingDual 𝕜 (M i)<VAR>inst✝ : CompleteSpace (ContinuousMultilinearMap 𝕜 M F)<VAR>m : (i : ι) → M i<VAR>hm : ∀ (i : ι), m i ≠ 0<VAR>f : ℕ → F<VAR>hf : CauchySeq f<VAR>φ : (i : ι) → M i →L[𝕜] 𝕜<VAR>hφ : ∀ (i : ι), (φ i) (m i) = 1<VAR>val✝ : Fintype ι<VAR>g : ℕ → ContinuousMultilinearMap 𝕜 M F := fun n => (compContinuousLinearMapL φ) (((smulRightL 𝕜 (fun x => 𝕜) F) (ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι 𝕜)) (f n))<GOAL>∃ a, Tendsto f atTop (𝓝 a)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>inst✝¹⁹ : Field R<VAR>inst✝¹⁸ : AddCommGroup V<VAR>inst✝¹⁷ : TopologicalSpace R<VAR>inst✝¹⁶ : TopologicalSpace V<VAR>inst✝¹⁵ : TopologicalRing R<VAR>inst✝¹⁴ : TopologicalAddGroup V<VAR>inst✝¹³ : Module R V<VAR>inst✝¹² : SeparatingDual R V<VAR>𝕜 : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>inst✝⁶ : SeparatingDual 𝕜 E<VAR>inst✝⁵ : Nontrivial E<VAR>ι : Type u_6<VAR>inst✝⁴ : Finite ι<VAR>M : ι → Type u_7<VAR>inst✝³ : (i : ι) → NormedAddCommGroup (M i)<VAR>inst✝² : (i : ι) → NormedSpace 𝕜 (M i)<VAR>inst✝¹ : ∀ (i : ι), SeparatingDual 𝕜 (M i)<VAR>inst✝ : CompleteSpace (ContinuousMultilinearMap 𝕜 M F)<VAR>m : (i : ι) → M i<VAR>hm : ∀ (i : ι), m i ≠ 0<VAR>f : ℕ → F<VAR>hf : CauchySeq f<VAR>φ : (i : ι) → M i →L[𝕜] 𝕜<VAR>hφ : ∀ (i : ι), (φ i) (m i) = 1<VAR>val✝ : Fintype ι<VAR>g : ℕ → ContinuousMultilinearMap 𝕜 M F := fun n => (compContinuousLinearMapL φ) (((smulRightL 𝕜 (fun x => 𝕜) F) (ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι 𝕜)) (f n))<VAR>this : CauchySeq g<GOAL>∃ a, Tendsto f atTop (𝓝 a)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>inst✝¹⁹ : Field R<VAR>inst✝¹⁸ : AddCommGroup V<VAR>inst✝¹⁷ : TopologicalSpace R<VAR>inst✝¹⁶ : TopologicalSpace V<VAR>inst✝¹⁵ : TopologicalRing R<VAR>inst✝¹⁴ : TopologicalAddGroup V<VAR>inst✝¹³ : Module R V<VAR>inst✝¹² : SeparatingDual R V<VAR>𝕜 : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>inst✝⁶ : SeparatingDual 𝕜 E<VAR>inst✝⁵ : Nontrivial E<VAR>ι : Type u_6<VAR>inst✝⁴ : Finite ι<VAR>M : ι → Type u_7<VAR>inst✝³ : (i : ι) → NormedAddCommGroup (M i)<VAR>inst✝² : (i : ι) → NormedSpace 𝕜 (M i)<VAR>inst✝¹ : ∀ (i : ι), SeparatingDual 𝕜 (M i)<VAR>inst✝ : CompleteSpace (ContinuousMultilinearMap 𝕜 M F)<VAR>m : (i : ι) → M i<VAR>hm : ∀ (i : ι), m i ≠ 0<VAR>f : ℕ → F<VAR>hf : CauchySeq f<VAR>φ : (i : ι) → M i →L[𝕜] 𝕜<VAR>hφ : ∀ (i : ι), (φ i) (m i) = 1<VAR>val✝ : Fintype ι<VAR>g : ℕ → ContinuousMultilinearMap 𝕜 M F := fun n => (compContinuousLinearMapL φ) (((smulRightL 𝕜 (fun x => 𝕜) F) (ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι 𝕜)) (f n))<VAR>this : CauchySeq g<VAR>a : ContinuousMultilinearMap 𝕜 M F<VAR>ha : Tendsto g atTop (𝓝 a)<GOAL>∃ a, Tendsto f atTop (𝓝 a)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>inst✝¹⁹ : Field R<VAR>inst✝¹⁸ : AddCommGroup V<VAR>inst✝¹⁷ : TopologicalSpace R<VAR>inst✝¹⁶ : TopologicalSpace V<VAR>inst✝¹⁵ : TopologicalRing R<VAR>inst✝¹⁴ : TopologicalAddGroup V<VAR>inst✝¹³ : Module R V<VAR>inst✝¹² : SeparatingDual R V<VAR>𝕜 : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>inst✝⁶ : SeparatingDual 𝕜 E<VAR>inst✝⁵ : Nontrivial E<VAR>ι : Type u_6<VAR>inst✝⁴ : Finite ι<VAR>M : ι → Type u_7<VAR>inst✝³ : (i : ι) → NormedAddCommGroup (M i)<VAR>inst✝² : (i : ι) → NormedSpace 𝕜 (M i)<VAR>inst✝¹ : ∀ (i : ι), SeparatingDual 𝕜 (M i)<VAR>inst✝ : CompleteSpace (ContinuousMultilinearMap 𝕜 M F)<VAR>m : (i : ι) → M i<VAR>hm : ∀ (i : ι), m i ≠ 0<VAR>f : ℕ → F<VAR>hf : CauchySeq f<VAR>φ : (i : ι) → M i →L[𝕜] 𝕜<VAR>hφ : ∀ (i : ι), (φ i) (m i) = 1<VAR>val✝ : Fintype ι<VAR>g : ℕ → ContinuousMultilinearMap 𝕜 M F := fun n => (compContinuousLinearMapL φ) (((smulRightL 𝕜 (fun x => 𝕜) F) (ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι 𝕜)) (f n))<VAR>this : CauchySeq g<VAR>a : ContinuousMultilinearMap 𝕜 M F<VAR>ha : Tendsto g atTop (𝓝 a)<GOAL>Tendsto f atTop (𝓝 (a m))
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>inst✝¹⁹ : Field R<VAR>inst✝¹⁸ : AddCommGroup V<VAR>inst✝¹⁷ : TopologicalSpace R<VAR>inst✝¹⁶ : TopologicalSpace V<VAR>inst✝¹⁵ : TopologicalRing R<VAR>inst✝¹⁴ : TopologicalAddGroup V<VAR>inst✝¹³ : Module R V<VAR>inst✝¹² : SeparatingDual R V<VAR>𝕜 : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>inst✝⁶ : SeparatingDual 𝕜 E<VAR>inst✝⁵ : Nontrivial E<VAR>ι : Type u_6<VAR>inst✝⁴ : Finite ι<VAR>M : ι → Type u_7<VAR>inst✝³ : (i : ι) → NormedAddCommGroup (M i)<VAR>inst✝² : (i : ι) → NormedSpace 𝕜 (M i)<VAR>inst✝¹ : ∀ (i : ι), SeparatingDual 𝕜 (M i)<VAR>inst✝ : CompleteSpace (ContinuousMultilinearMap 𝕜 M F)<VAR>m : (i : ι) → M i<VAR>hm : ∀ (i : ι), m i ≠ 0<VAR>f : ℕ → F<VAR>hf : CauchySeq f<VAR>φ : (i : ι) → M i →L[𝕜] 𝕜<VAR>hφ : ∀ (i : ι), (φ i) (m i) = 1<VAR>val✝ : Fintype ι<VAR>g : ℕ → ContinuousMultilinearMap 𝕜 M F := fun n => (compContinuousLinearMapL φ) (((smulRightL 𝕜 (fun x => 𝕜) F) (ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι 𝕜)) (f n))<VAR>this✝ : CauchySeq g<VAR>a : ContinuousMultilinearMap 𝕜 M F<VAR>ha : Tendsto g atTop (𝓝 a)<VAR>this : Tendsto (fun n => (g n) m) atTop (𝓝 (a m))<GOAL>Tendsto f atTop (𝓝 (a m))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f fa : α → α<VAR>fb : β → β<VAR>x y✝ : α<VAR>m n : ℕ<VAR>g : β → β<VAR>y : β<GOAL>minimalPeriod f x = minimalPeriod g y ↔ ∀ (n : ℕ), IsPeriodicPt f n x ↔ IsPeriodicPt g n y
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>f✝ : α → β<VAR>ι : Sort u_2<VAR>T : TopologicalSpace α<VAR>f : β → α<VAR>a : β<VAR>s : Set β<VAR>this : TopologicalSpace β := induced f T<GOAL>s ∈ 𝓝 a ↔ ∃ u ∈ 𝓝 (f a), f ⁻¹' u ⊆ s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>f✝ : α → β<VAR>ι : Sort u_2<VAR>T : TopologicalSpace α<VAR>f : β → α<VAR>a : β<VAR>s : Set β<VAR>this : TopologicalSpace β := induced f T<GOAL>(∃ t ⊆ s, (∃ t_1, IsOpen t_1 ∧ f ⁻¹' t_1 = t) ∧ a ∈ t) ↔ ∃ u, (∃ t ⊆ u, IsOpen t ∧ f a ∈ t) ∧ f ⁻¹' u ⊆ s
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : Ring R<VAR>inst✝ : CommMonoid M<VAR>ψ : AddChar R M<VAR>r s x✝ : R<GOAL>((ψ.mulShift r).mulShift s) x✝ = (ψ.mulShift (r * s)) x✝
<VAR>m n a✝ b✝ c✝ d a b c : ℕ<VAR>hc : a % c + b % c < c<VAR>hc0 : ¬c = 0<GOAL>(a + b) / c = a / c + b / c
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r : ℚ<VAR>x✝ x : ℤ_[p]<GOAL>Monotone x.appr
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r : ℚ<VAR>x✝ x : ℤ_[p]<GOAL>∀ (n : ℕ), x.appr n ≤ x.appr (n + 1)
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r : ℚ<VAR>x✝ x : ℤ_[p]<VAR>n : ℕ<VAR>h✝ : ¬x - ↑(x.appr n) = 0<GOAL>x.appr n ≤ x.appr n + p ^ n * (toZMod (↑(unitCoeff h✝) * ↑p ^ ((x - ↑(x.appr n)).valuation - ↑n).natAbs)).val
<VAR>α : Type u<VAR>r : ℕ → ℕ → Prop<VAR>n : ℕ<GOAL>Chain' r (range n.succ) ↔ ∀ m < n, r m m.succ
<VAR>α : Type u<VAR>r : ℕ → ℕ → Prop<VAR>n : ℕ<GOAL>Chain' r (range n ++ [n]) ↔ ∀ m < n, r m m.succ
<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>inst✝³ : NumberField K<VAR>inst✝² : DecidableEq (K →+* ℂ)<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Fintype β<VAR>a : Matrix α β (𝓞 K)<VAR>ha : a ≠ 0<VAR>p q : ℕ<VAR>cardα : Fintype.card α = p<VAR>cardβ : Fintype.card β = q<VAR>h0p : 0 < p<VAR>hpq : p < q<VAR>x : β × (K →+* ℂ) → ℤ<VAR>hxl : x ≠ 0<VAR>hmulvec0 : NumberField.house.asiegel K a *ᵥ x = 0<VAR>hxbound : ‖x‖ ≤ (↑q * ↑(finrank ℚ K) * ‖NumberField.house.asiegel K a‖) ^ (↑p / (↑q - ↑p))<GOAL>a *ᵥ NumberField.house.ξ K x = 0
<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>inst✝³ : NumberField K<VAR>inst✝² : DecidableEq (K →+* ℂ)<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Fintype β<VAR>a : Matrix α β (𝓞 K)<VAR>ha : a ≠ 0<VAR>p q : ℕ<VAR>cardα : Fintype.card α = p<VAR>cardβ : Fintype.card β = q<VAR>h0p : 0 < p<VAR>hpq : p < q<VAR>x : β × (K →+* ℂ) → ℤ<VAR>hxl : x ≠ 0<VAR>hmulvec0 : NumberField.house.asiegel K a *ᵥ x = 0<VAR>hxbound : ‖x‖ ≤ (↑q * ↑(finrank ℚ K) * ‖NumberField.house.asiegel K a‖) ^ (↑p / (↑q - ↑p))<VAR>k : α<GOAL>(a *ᵥ NumberField.house.ξ K x) k = 0 k
<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>inst✝³ : NumberField K<VAR>inst✝² : DecidableEq (K →+* ℂ)<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Fintype β<VAR>a : Matrix α β (𝓞 K)<VAR>ha : a ≠ 0<VAR>p q : ℕ<VAR>cardα : Fintype.card α = p<VAR>cardβ : Fintype.card β = q<VAR>h0p : 0 < p<VAR>hpq : p < q<VAR>x : β × (K →+* ℂ) → ℤ<VAR>hxl : x ≠ 0<VAR>hmulvec0 : NumberField.house.asiegel K a *ᵥ x = 0<VAR>hxbound : ‖x‖ ≤ (↑q * ↑(finrank ℚ K) * ‖NumberField.house.asiegel K a‖) ^ (↑p / (↑q - ↑p))<VAR>k : α<GOAL>(a *ᵥ NumberField.house.ξ K x) k = 0
<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>inst✝³ : NumberField K<VAR>inst✝² : DecidableEq (K →+* ℂ)<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Fintype β<VAR>a : Matrix α β (𝓞 K)<VAR>ha : a ≠ 0<VAR>p q : ℕ<VAR>cardα : Fintype.card α = p<VAR>cardβ : Fintype.card β = q<VAR>h0p : 0 < p<VAR>hpq : p < q<VAR>x : β × (K →+* ℂ) → ℤ<VAR>hxl : x ≠ 0<VAR>hmulvec0 : NumberField.house.asiegel K a *ᵥ x = 0<VAR>hxbound : ‖x‖ ≤ (↑q * ↑(finrank ℚ K) * ‖NumberField.house.asiegel K a‖) ^ (↑p / (↑q - ↑p))<VAR>k : α<GOAL>0 = (a *ᵥ NumberField.house.ξ K x) k
<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>inst✝³ : NumberField K<VAR>inst✝² : DecidableEq (K →+* ℂ)<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Fintype β<VAR>a : Matrix α β (𝓞 K)<VAR>ha : a ≠ 0<VAR>p q : ℕ<VAR>cardα : Fintype.card α = p<VAR>cardβ : Fintype.card β = q<VAR>h0p : 0 < p<VAR>hpq : p < q<VAR>x : β × (K →+* ℂ) → ℤ<VAR>hxl : x ≠ 0<VAR>hmulvec0 : NumberField.house.asiegel K a *ᵥ x = 0<VAR>hxbound : ‖x‖ ≤ (↑q * ↑(finrank ℚ K) * ‖NumberField.house.asiegel K a‖) ^ (↑p / (↑q - ↑p))<VAR>k : α<VAR>lin_0 : ∀ (u : K →+* ℂ), ∑ r : K →+* ℂ, ∑ l : β, ↑(NumberField.house.a' K a k l r u) * ↑(x (l, r)) = 0<GOAL>0 = (a *ᵥ NumberField.house.ξ K x) k