ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁵ : TopologicalSpace α<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝⁴ : (i : ι) → TopologicalSpace (π i)<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : TopologicalSpace γ<VAR>inst✝¹ : TopologicalSpace δ<VAR>inst✝ : DiscreteTopology α<VAR>f : α × β → γ<VAR>x : α × β<GOAL>ContinuousAt f x ↔ ContinuousAt (fun x_1 => f (x.1, x_1)) x.2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁵ : TopologicalSpace α<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝⁴ : (i : ι) → TopologicalSpace (π i)<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : TopologicalSpace γ<VAR>inst✝¹ : TopologicalSpace δ<VAR>inst✝ : DiscreteTopology α<VAR>f : α × β → γ<VAR>x : α × β<GOAL>ContinuousWithinAt f univ x ↔ ContinuousWithinAt (fun x_1 => f (x.1, x_1)) univ x.2
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>W : Type u_4<VAR>ι : Type u_5<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace W<VAR>f : X → Y<VAR>g : Y → Z<VAR>hf : IsProperMap f<VAR>hg : IsProperMap g<VAR>ℱ : Filter X<VAR>z : Z<VAR>h : MapClusterPt z ℱ (g ∘ f)<GOAL>∃ x, (g ∘ f) x = z ∧ ClusterPt x ℱ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>W : Type u_4<VAR>ι : Type u_5<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace W<VAR>f : X → Y<VAR>g : Y → Z<VAR>hf : IsProperMap f<VAR>hg : IsProperMap g<VAR>ℱ : Filter X<VAR>z : Z<VAR>h : MapClusterPt z (map f ℱ) g<GOAL>∃ x, (g ∘ f) x = z ∧ ClusterPt x ℱ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>W : Type u_4<VAR>ι : Type u_5<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace W<VAR>f : X → Y<VAR>g : Y → Z<VAR>hf : IsProperMap f<VAR>hg : IsProperMap g<VAR>ℱ : Filter X<VAR>y : Y<VAR>hy : ClusterPt y (map f ℱ)<VAR>h : MapClusterPt (g y) (map f ℱ) g<GOAL>∃ x, (g ∘ f) x = g y ∧ ClusterPt x ℱ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>W : Type u_4<VAR>ι : Type u_5<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace W<VAR>f : X → Y<VAR>g : Y → Z<VAR>hf : IsProperMap f<VAR>hg : IsProperMap g<VAR>ℱ : Filter X<VAR>x : X<VAR>hx : ClusterPt x ℱ<VAR>hy : ClusterPt (f x) (map f ℱ)<VAR>h : MapClusterPt (g (f x)) (map f ℱ) g<GOAL>∃ x_1, (g ∘ f) x_1 = g (f x) ∧ ClusterPt x_1 ℱ
<VAR>F : Type u_1<VAR>inst✝¹ : Field F<VAR>ι : Type u_2<VAR>inst✝ : DecidableEq ι<VAR>s t : Finset ι<VAR>i j : ι<VAR>v r r' : ι → F<VAR>f : F[X]<VAR>hvs : Set.InjOn v ↑s<VAR>degree_f_lt : f.degree < ↑s.card<VAR>eval_f : ∀ i ∈ s, eval (v i) f = r i<GOAL>f = (interpolate s v) r
<VAR>F : Type u_1<VAR>inst✝¹ : Field F<VAR>ι : Type u_2<VAR>inst✝ : DecidableEq ι<VAR>s t : Finset ι<VAR>i j : ι<VAR>v r r' : ι → F<VAR>f : F[X]<VAR>hvs : Set.InjOn v ↑s<VAR>degree_f_lt : f.degree < ↑s.card<VAR>eval_f : ∀ i ∈ s, eval (v i) f = r i<GOAL>((interpolate s v) fun i => eval (v i) f) = (interpolate s v) r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : List α<VAR>f : α → List β<GOAL>(∀ (l_1 : List β), l_1 ∈ map f l → l_1 = []) ↔ ∀ (x : α), x ∈ l → f x = []
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝³ : EMetricSpace X<VAR>inst✝² : EMetricSpace Y<VAR>inst✝¹ : MeasurableSpace X<VAR>inst✝ : BorelSpace X<VAR>m : ℝ≥0∞ → ℝ≥0∞<GOAL>⇑(mkMetric m) = ⇑(Measure.mkMetric m)
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>J : GrothendieckTopology C<VAR>D : Type u₂<VAR>inst✝² : Category.{v₂, u₂} D<VAR>E : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} E<VAR>F : D ⥤ E<VAR>G : E ⥤ D<VAR>inst✝ : HasWeakSheafify J D<VAR>adj : G ⊣ F<VAR>P Q : Cᵒᵖ ⥤ E<VAR>f : P ⟶ Q<VAR>hf : J.W f<GOAL>J.W.inverseImage ((whiskeringRight Cᵒᵖ E D).obj G) f
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>J : GrothendieckTopology C<VAR>D : Type u₂<VAR>inst✝² : Category.{v₂, u₂} D<VAR>E : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} E<VAR>F : D ⥤ E<VAR>G : E ⥤ D<VAR>inst✝ : HasWeakSheafify J D<VAR>adj : G ⊣ F<VAR>P Q : Cᵒᵖ ⥤ E<VAR>f : P ⟶ Q<VAR>hf : J.W f<VAR>this : F.IsRightAdjoint<GOAL>J.W.inverseImage ((whiskeringRight Cᵒᵖ E D).obj G) f
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>J : GrothendieckTopology C<VAR>D : Type u₂<VAR>inst✝² : Category.{v₂, u₂} D<VAR>E : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} E<VAR>F : D ⥤ E<VAR>G : E ⥤ D<VAR>inst✝ : HasWeakSheafify J D<VAR>adj : G ⊣ F<VAR>P Q : Cᵒᵖ ⥤ E<VAR>f : P ⟶ Q<VAR>hf : J.W f<VAR>this : F.IsRightAdjoint<GOAL>J.W (((whiskeringRight Cᵒᵖ E D).obj G).map f)
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>J : GrothendieckTopology C<VAR>D : Type u₂<VAR>inst✝² : Category.{v₂, u₂} D<VAR>E : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} E<VAR>F : D ⥤ E<VAR>G : E ⥤ D<VAR>inst✝ : HasWeakSheafify J D<VAR>adj : G ⊣ F<VAR>P Q : Cᵒᵖ ⥤ E<VAR>f : P ⟶ Q<VAR>hf : J.W f<VAR>this : F.IsRightAdjoint<VAR>R : Cᵒᵖ ⥤ D<VAR>hR : Presheaf.IsSheaf J R<GOAL>Function.Bijective fun g => whiskerRight f G ≫ g
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>J : GrothendieckTopology C<VAR>D : Type u₂<VAR>inst✝² : Category.{v₂, u₂} D<VAR>E : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} E<VAR>F : D ⥤ E<VAR>G : E ⥤ D<VAR>inst✝ : HasWeakSheafify J D<VAR>adj : G ⊣ F<VAR>P Q : Cᵒᵖ ⥤ E<VAR>f : P ⟶ Q<VAR>hf : J.W f<VAR>this : F.IsRightAdjoint<VAR>R : Cᵒᵖ ⥤ D<VAR>hR : Presheaf.IsSheaf J R<GOAL>Function.Bijective (⇑((Adjunction.whiskerRight Cᵒᵖ adj).homEquiv P R) ∘ fun g => whiskerRight f G ≫ g)
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>J : GrothendieckTopology C<VAR>D : Type u₂<VAR>inst✝² : Category.{v₂, u₂} D<VAR>E : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} E<VAR>F : D ⥤ E<VAR>G : E ⥤ D<VAR>inst✝ : HasWeakSheafify J D<VAR>adj : G ⊣ F<VAR>P Q : Cᵒᵖ ⥤ E<VAR>f : P ⟶ Q<VAR>hf : J.W f<VAR>this : F.IsRightAdjoint<VAR>R : Cᵒᵖ ⥤ D<VAR>hR : Presheaf.IsSheaf J R<VAR>e_1✝ : (Q ⋙ G ⟶ R) = (((whiskeringRight Cᵒᵖ E D).obj G).obj Q ⟶ R)<VAR>e_2✝ : (P ⟶ ((whiskeringRight Cᵒᵖ D E).obj F).obj R) = (P ⟶ R ⋙ F)<GOAL>(⇑((Adjunction.whiskerRight Cᵒᵖ adj).homEquiv P R) ∘ fun g => whiskerRight f G ≫ g) = ⇑(((Adjunction.whiskerRight Cᵒᵖ adj).homEquiv Q R).trans (Localization.LeftBousfield.W.homEquiv hf (R ⋙ F) ⋯))
<VAR>R : Type u<VAR>A : Type v<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>M : Submonoid R<VAR>B : Type w<VAR>inst✝¹ : CommRing B<VAR>inst✝ : Algebra R B<VAR>f : A →ₐ[R] B<GOAL>algebraMapSubmonoid A M ≤ Submonoid.comap f.toRingHom (algebraMapSubmonoid B M)
<VAR>R : Type u<VAR>A : Type v<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>M : Submonoid R<VAR>B : Type w<VAR>inst✝¹ : CommRing B<VAR>inst✝ : Algebra R B<VAR>f : A →ₐ[R] B<GOAL>algebraMapSubmonoid A M ≤ Submonoid.comap f.toRingHom (Submonoid.map f (algebraMapSubmonoid A M))
<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 H : Subgroup G<VAR>inst✝ : Nontrivial ↥H<GOAL>∃ x ∈ H, x ≠ 1
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>M : R[T;T⁻¹] → Prop<VAR>p : R[T;T⁻¹]<VAR>h_C : ∀ (a : R), M (C a)<VAR>h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)<VAR>h_C_mul_T : ∀ (n : ℕ) (a : R), M (C a * T ↑n) → M (C a * T (↑n + 1))<VAR>h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (C a * T (-↑n)) → M (C a * T (-↑n - 1))<VAR>A : ∀ {n : ℤ} {a : R}, M (C a * T n)<VAR>B : ∀ (s : Finset ℤ), M (∑ n ∈ s, C (p.toFun n) * T n)<VAR>a : ℤ<GOAL>p a = (∑ n ∈ p.support, C (p.toFun n) * T n) a
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>M : R[T;T⁻¹] → Prop<VAR>p : R[T;T⁻¹]<VAR>h_C : ∀ (a : R), M (C a)<VAR>h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)<VAR>h_C_mul_T : ∀ (n : ℕ) (a : R), M (C a * T ↑n) → M (C a * T (↑n + 1))<VAR>h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (C a * T (-↑n)) → M (C a * T (-↑n - 1))<VAR>A : ∀ {n : ℤ} {a : R}, M (C a * T n)<VAR>B : ∀ (s : Finset ℤ), M (∑ n ∈ s, C (p.toFun n) * T n)<VAR>a : ℤ<GOAL>p a = (∑ x ∈ p.support, Finsupp.single x (p.toFun x)) a
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>M : R[T;T⁻¹] → Prop<VAR>p : R[T;T⁻¹]<VAR>h_C : ∀ (a : R), M (C a)<VAR>h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)<VAR>h_C_mul_T : ∀ (n : ℕ) (a : R), M (C a * T ↑n) → M (C a * T (↑n + 1))<VAR>h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (C a * T (-↑n)) → M (C a * T (-↑n - 1))<VAR>A : ∀ {n : ℤ} {a : R}, M (C a * T n)<VAR>B : ∀ (s : Finset ℤ), M (∑ n ∈ s, C (p.toFun n) * T n)<VAR>a : ℤ<GOAL>p a = ∑ k ∈ p.support, (Finsupp.single k (p.toFun k)) a
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>M : R[T;T⁻¹] → Prop<VAR>p : R[T;T⁻¹]<VAR>h_C : ∀ (a : R), M (C a)<VAR>h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)<VAR>h_C_mul_T : ∀ (n : ℕ) (a : R), M (C a * T ↑n) → M (C a * T (↑n + 1))<VAR>h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (C a * T (-↑n)) → M (C a * T (-↑n - 1))<VAR>A : ∀ {n : ℤ} {a : R}, M (C a * T n)<VAR>B : ∀ (s : Finset ℤ), M (∑ n ∈ s, C (p.toFun n) * T n)<VAR>a : ℤ<GOAL>p a = if a ∈ p.support then p.toFun a else 0
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : Measure α<VAR>E : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace 𝕜 E<VAR>f : α → E<VAR>hf : Integrable f μ<VAR>c : E<GOAL>Integrable (fun x => ⟪f x, c⟫_𝕜) μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : Measure α<VAR>E : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace 𝕜 E<VAR>f : α → E<VAR>hf : Memℒp f 1 μ<VAR>c : E<GOAL>Memℒp (fun x => ⟪f x, c⟫_𝕜) 1 μ
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M : Bimod A B<VAR>inst✝ : HasCoequalizers C<VAR>R S : Mon_ C<VAR>P : Bimod R S<GOAL>((λ_ P.X).inv ≫ R.one ▷ P.X ≫ coequalizer.π (R.mul ▷ P.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft)) ≫ coequalizer.desc P.actLeft ⋯ = 𝟙 P.X
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M : Bimod A B<VAR>inst✝ : HasCoequalizers C<VAR>R S : Mon_ C<VAR>P : Bimod R S<GOAL>(λ_ P.X).inv ≫ R.one ▷ P.X ≫ P.actLeft = 𝟙 P.X
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝¹ : (i : α) → NormedAddCommGroup (E i)<VAR>ι : Type u_3<VAR>l : Filter ι<VAR>inst✝ : l.NeBot<VAR>_i : Fact (1 ≤ p)<VAR>F : ℕ → ↥(lp E p)<VAR>hF : CauchySeq F<VAR>f : ↥(lp E p)<VAR>hf : Tendsto (id fun i => ↑(F i)) atTop (𝓝 ↑f)<GOAL>Tendsto F atTop (𝓝 f)
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝¹ : (i : α) → NormedAddCommGroup (E i)<VAR>ι : Type u_3<VAR>l : Filter ι<VAR>inst✝ : l.NeBot<VAR>_i : Fact (1 ≤ p)<VAR>F : ℕ → ↥(lp E p)<VAR>hF : CauchySeq F<VAR>f : ↥(lp E p)<VAR>hf : Tendsto (id fun i => ↑(F i)) atTop (𝓝 ↑f)<GOAL>∀ (i : ℝ), 0 < i → ∀ᶠ (x : ℕ) in atTop, F x ∈ Metric.closedBall f i
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝¹ : (i : α) → NormedAddCommGroup (E i)<VAR>ι : Type u_3<VAR>l : Filter ι<VAR>inst✝ : l.NeBot<VAR>_i : Fact (1 ≤ p)<VAR>F : ℕ → ↥(lp E p)<VAR>hF : CauchySeq F<VAR>f : ↥(lp E p)<VAR>hf : Tendsto (id fun i => ↑(F i)) atTop (𝓝 ↑f)<VAR>ε : ℝ<VAR>hε : 0 < ε<GOAL>∀ᶠ (x : ℕ) in atTop, F x ∈ Metric.closedBall f ε
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝¹ : (i : α) → NormedAddCommGroup (E i)<VAR>ι : Type u_3<VAR>l : Filter ι<VAR>inst✝ : l.NeBot<VAR>_i : Fact (1 ≤ p)<VAR>F : ℕ → ↥(lp E p)<VAR>hF : CauchySeq F<VAR>f : ↥(lp E p)<VAR>hf : Tendsto (id fun i => ↑(F i)) atTop (𝓝 ↑f)<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hε' : {p_1 | ‖p_1.1 - p_1.2‖ < ε} ∈ uniformity ↥(lp E p)<GOAL>∀ᶠ (x : ℕ) in atTop, F x ∈ Metric.closedBall f ε
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝¹ : (i : α) → NormedAddCommGroup (E i)<VAR>ι : Type u_3<VAR>l : Filter ι<VAR>inst✝ : l.NeBot<VAR>_i : Fact (1 ≤ p)<VAR>F : ℕ → ↥(lp E p)<VAR>hF : CauchySeq F<VAR>f : ↥(lp E p)<VAR>hf : Tendsto (id fun i => ↑(F i)) atTop (𝓝 ↑f)<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hε' : {p_1 | ‖p_1.1 - p_1.2‖ < ε} ∈ uniformity ↥(lp E p)<GOAL>∀ (x : ℕ), (∀ᶠ (l : ℕ) in atTop, (F x, F l) ∈ {p_1 | ‖p_1.1 - p_1.2‖ < ε}) → F x ∈ Metric.closedBall f ε
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝¹ : (i : α) → NormedAddCommGroup (E i)<VAR>ι : Type u_3<VAR>l : Filter ι<VAR>inst✝ : l.NeBot<VAR>_i : Fact (1 ≤ p)<VAR>F : ℕ → ↥(lp E p)<VAR>hF : CauchySeq F<VAR>f : ↥(lp E p)<VAR>hf : Tendsto (id fun i => ↑(F i)) atTop (𝓝 ↑f)<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hε' : {p_1 | ‖p_1.1 - p_1.2‖ < ε} ∈ uniformity ↥(lp E p)<VAR>n : ℕ<VAR>hn : ∀ᶠ (l : ℕ) in atTop, ‖(fun f => F n - f) (F l)‖ < ε<GOAL>F n ∈ Metric.closedBall f ε
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝¹ : (i : α) → NormedAddCommGroup (E i)<VAR>ι : Type u_3<VAR>l : Filter ι<VAR>inst✝ : l.NeBot<VAR>_i : Fact (1 ≤ p)<VAR>F : ℕ → ↥(lp E p)<VAR>hF : CauchySeq F<VAR>f : ↥(lp E p)<VAR>hf : Tendsto (id fun i => ↑(F i)) atTop (𝓝 ↑f)<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hε' : {p_1 | ‖p_1.1 - p_1.2‖ < ε} ∈ uniformity ↥(lp E p)<VAR>n : ℕ<VAR>hn : ∀ᶠ (l : ℕ) in atTop, ‖(fun f => F n - f) (F l)‖ < ε<GOAL>Tendsto (id fun i => ↑((fun f => F n - f) (F i))) atTop (𝓝 ↑(F n - f))
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝¹ : (i : α) → NormedAddCommGroup (E i)<VAR>ι : Type u_3<VAR>l : Filter ι<VAR>inst✝ : l.NeBot<VAR>_i : Fact (1 ≤ p)<VAR>F : ℕ → ↥(lp E p)<VAR>hF : CauchySeq F<VAR>f : ↥(lp E p)<VAR>hf : Tendsto (id fun i => ↑(F i)) atTop (𝓝 ↑f)<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hε' : {p_1 | ‖p_1.1 - p_1.2‖ < ε} ∈ uniformity ↥(lp E p)<VAR>n : ℕ<VAR>hn : ∀ᶠ (l : ℕ) in atTop, ‖(fun f => F n - f) (F l)‖ < ε<GOAL>∀ (x : α), Tendsto (fun i => id (fun i => ↑((fun f => F n - f) (F i))) i x) atTop (𝓝 (↑(F n - f) x))
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝¹ : (i : α) → NormedAddCommGroup (E i)<VAR>ι : Type u_3<VAR>l : Filter ι<VAR>inst✝ : l.NeBot<VAR>_i : Fact (1 ≤ p)<VAR>F : ℕ → ↥(lp E p)<VAR>hF : CauchySeq F<VAR>f : ↥(lp E p)<VAR>hf : Tendsto (id fun i => ↑(F i)) atTop (𝓝 ↑f)<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hε' : {p_1 | ‖p_1.1 - p_1.2‖ < ε} ∈ uniformity ↥(lp E p)<VAR>n : ℕ<VAR>hn : ∀ᶠ (l : ℕ) in atTop, ‖(fun f => F n - f) (F l)‖ < ε<VAR>a : α<GOAL>Tendsto (fun i => id (fun i => ↑((fun f => F n - f) (F i))) i a) atTop (𝓝 (↑(F n - f) a))
<VAR>𝓕 : Type u_1<VAR>α : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹ : SeminormedCommGroup E<VAR>inst✝ : SeminormedCommGroup F<VAR>a✝ a₁ a₂ b✝ b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>a b : E<GOAL>dist a (a / b) = ‖b‖
<VAR>R✝ : Type u<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>ι : Type w<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✝⁸ : Nontrivial R✝<VAR>inst✝⁷ : NoZeroSMulDivisors R✝ M<VAR>inst✝⁶ : StrongRankCondition R✝<VAR>inst✝⁵ : Module.Finite R✝ M<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : StrongRankCondition R<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module.Finite R M<GOAL>finrank R M = 0 ↔ Module.IsTorsion R M
<VAR>R✝ : Type u<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>ι : Type w<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✝⁸ : Nontrivial R✝<VAR>inst✝⁷ : NoZeroSMulDivisors R✝ M<VAR>inst✝⁶ : StrongRankCondition R✝<VAR>inst✝⁵ : Module.Finite R✝ M<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : StrongRankCondition R<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module.Finite R M<GOAL>finrank R M = 0 ↔ ↑(finrank R M) = 0
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>f : CauSeq ℚ (padicNorm p)<VAR>hf : ¬f ≈ 0<VAR>this : ∃ ε > 0, ∃ N1, ∀ j ≥ N1, ε ≤ padicNorm p (↑f j)<VAR>ε : ℚ<VAR>hε : ε > 0<VAR>N1 : ℕ<VAR>hN1 : ∀ j ≥ N1, ε ≤ padicNorm p (↑f j)<VAR>N2 : ℕ<VAR>hN2 : ∀ j ≥ N2, ∀ k ≥ N2, padicNorm p (↑f j - ↑f k) < ε<VAR>n m : ℕ<VAR>hn : max N1 N2 ≤ n<VAR>hm : max N1 N2 ≤ m<GOAL>padicNorm p (↑f m) = padicNorm p (↑f n)
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>f : CauSeq ℚ (padicNorm p)<VAR>hf : ¬f ≈ 0<VAR>this✝ : ∃ ε > 0, ∃ N1, ∀ j ≥ N1, ε ≤ padicNorm p (↑f j)<VAR>ε : ℚ<VAR>hε : ε > 0<VAR>N1 : ℕ<VAR>hN1 : ∀ j ≥ N1, ε ≤ padicNorm p (↑f j)<VAR>N2 : ℕ<VAR>hN2 : ∀ j ≥ N2, ∀ k ≥ N2, padicNorm p (↑f j - ↑f k) < ε<VAR>n m : ℕ<VAR>hn : max N1 N2 ≤ n<VAR>hm : max N1 N2 ≤ m<VAR>this : padicNorm p (↑f n - ↑f m) < ε<GOAL>padicNorm p (↑f m) = padicNorm p (↑f n)
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>f : CauSeq ℚ (padicNorm p)<VAR>hf : ¬f ≈ 0<VAR>this✝¹ : ∃ ε > 0, ∃ N1, ∀ j ≥ N1, ε ≤ padicNorm p (↑f j)<VAR>ε : ℚ<VAR>hε : ε > 0<VAR>N1 : ℕ<VAR>hN1 : ∀ j ≥ N1, ε ≤ padicNorm p (↑f j)<VAR>N2 : ℕ<VAR>hN2 : ∀ j ≥ N2, ∀ k ≥ N2, padicNorm p (↑f j - ↑f k) < ε<VAR>n m : ℕ<VAR>hn : max N1 N2 ≤ n<VAR>hm : max N1 N2 ≤ m<VAR>this✝ : padicNorm p (↑f n - ↑f m) < ε<VAR>this : padicNorm p (↑f n - ↑f m) < padicNorm p (↑f n)<GOAL>padicNorm p (↑f m) = padicNorm p (↑f n)
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>f : CauSeq ℚ (padicNorm p)<VAR>hf : ¬f ≈ 0<VAR>this✝² : ∃ ε > 0, ∃ N1, ∀ j ≥ N1, ε ≤ padicNorm p (↑f j)<VAR>ε : ℚ<VAR>hε : ε > 0<VAR>N1 : ℕ<VAR>hN1 : ∀ j ≥ N1, ε ≤ padicNorm p (↑f j)<VAR>N2 : ℕ<VAR>hN2 : ∀ j ≥ N2, ∀ k ≥ N2, padicNorm p (↑f j - ↑f k) < ε<VAR>n m : ℕ<VAR>hn : max N1 N2 ≤ n<VAR>hm : max N1 N2 ≤ m<VAR>this✝¹ : padicNorm p (↑f n - ↑f m) < ε<VAR>this✝ : padicNorm p (↑f n - ↑f m) < padicNorm p (↑f n)<VAR>this : padicNorm p (↑f n - ↑f m) < max (padicNorm p (↑f n)) (padicNorm p (↑f m))<GOAL>padicNorm p (↑f m) = padicNorm p (↑f n)
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>f : CauSeq ℚ (padicNorm p)<VAR>hf : ¬f ≈ 0<VAR>this✝² : ∃ ε > 0, ∃ N1, ∀ j ≥ N1, ε ≤ padicNorm p (↑f j)<VAR>ε : ℚ<VAR>hε : ε > 0<VAR>N1 : ℕ<VAR>hN1 : ∀ j ≥ N1, ε ≤ padicNorm p (↑f j)<VAR>N2 : ℕ<VAR>hN2 : ∀ j ≥ N2, ∀ k ≥ N2, padicNorm p (↑f j - ↑f k) < ε<VAR>n m : ℕ<VAR>hn : max N1 N2 ≤ n<VAR>hm : max N1 N2 ≤ m<VAR>this✝¹ : padicNorm p (↑f n - ↑f m) < ε<VAR>this✝ : padicNorm p (↑f n - ↑f m) < padicNorm p (↑f n)<VAR>this : padicNorm p (↑f n - ↑f m) < max (padicNorm p (↑f n)) (padicNorm p (↑f m))<VAR>hne : ¬padicNorm p (↑f m) = padicNorm p (↑f n)<GOAL>False
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>f : CauSeq ℚ (padicNorm p)<VAR>hf : ¬f ≈ 0<VAR>this✝² : ∃ ε > 0, ∃ N1, ∀ j ≥ N1, ε ≤ padicNorm p (↑f j)<VAR>ε : ℚ<VAR>hε : ε > 0<VAR>N1 : ℕ<VAR>hN1 : ∀ j ≥ N1, ε ≤ padicNorm p (↑f j)<VAR>N2 : ℕ<VAR>hN2 : ∀ j ≥ N2, ∀ k ≥ N2, padicNorm p (↑f j - ↑f k) < ε<VAR>n m : ℕ<VAR>hn : max N1 N2 ≤ n<VAR>hm : max N1 N2 ≤ m<VAR>this✝¹ : padicNorm p (↑f n - ↑f m) < ε<VAR>this✝ : padicNorm p (↑f n - ↑f m) < padicNorm p (↑f n)<VAR>this : padicNorm p (↑f n - ↑f m) < max (padicNorm p (↑f n)) (padicNorm p (↑f m))<VAR>hne : ¬padicNorm p (-↑f m) = padicNorm p (↑f n)<GOAL>False
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>f : CauSeq ℚ (padicNorm p)<VAR>hf : ¬f ≈ 0<VAR>this✝² : ∃ ε > 0, ∃ N1, ∀ j ≥ N1, ε ≤ padicNorm p (↑f j)<VAR>ε : ℚ<VAR>hε : ε > 0<VAR>N1 : ℕ<VAR>hN1 : ∀ j ≥ N1, ε ≤ padicNorm p (↑f j)<VAR>N2 : ℕ<VAR>hN2 : ∀ j ≥ N2, ∀ k ≥ N2, padicNorm p (↑f j - ↑f k) < ε<VAR>n m : ℕ<VAR>hn : max N1 N2 ≤ n<VAR>hm : max N1 N2 ≤ m<VAR>this✝¹ : padicNorm p (↑f n - ↑f m) < ε<VAR>this✝ : padicNorm p (↑f n - ↑f m) < padicNorm p (↑f n)<VAR>this : padicNorm p (↑f n - ↑f m) < max (padicNorm p (↑f n)) (padicNorm p (↑f m))<VAR>hne : ¬padicNorm p (-↑f m) = padicNorm p (↑f n)<VAR>hnam : padicNorm p (-↑f m + ↑f n) = max (padicNorm p (-↑f m)) (padicNorm p (↑f n))<GOAL>False
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>f : CauSeq ℚ (padicNorm p)<VAR>hf : ¬f ≈ 0<VAR>this✝² : ∃ ε > 0, ∃ N1, ∀ j ≥ N1, ε ≤ padicNorm p (↑f j)<VAR>ε : ℚ<VAR>hε : ε > 0<VAR>N1 : ℕ<VAR>hN1 : ∀ j ≥ N1, ε ≤ padicNorm p (↑f j)<VAR>N2 : ℕ<VAR>hN2 : ∀ j ≥ N2, ∀ k ≥ N2, padicNorm p (↑f j - ↑f k) < ε<VAR>n m : ℕ<VAR>hn : max N1 N2 ≤ n<VAR>hm : max N1 N2 ≤ m<VAR>this✝¹ : padicNorm p (↑f n - ↑f m) < ε<VAR>this✝ : padicNorm p (↑f n - ↑f m) < padicNorm p (↑f n)<VAR>this : padicNorm p (↑f n - ↑f m) < max (padicNorm p (↑f n)) (padicNorm p (↑f m))<VAR>hne : ¬padicNorm p (-↑f m) = padicNorm p (↑f n)<VAR>hnam : padicNorm p (-↑f m + ↑f n) = max (padicNorm p (↑f n)) (padicNorm p (↑f m))<GOAL>False
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>f : CauSeq ℚ (padicNorm p)<VAR>hf : ¬f ≈ 0<VAR>this✝² : ∃ ε > 0, ∃ N1, ∀ j ≥ N1, ε ≤ padicNorm p (↑f j)<VAR>ε : ℚ<VAR>hε : ε > 0<VAR>N1 : ℕ<VAR>hN1 : ∀ j ≥ N1, ε ≤ padicNorm p (↑f j)<VAR>N2 : ℕ<VAR>hN2 : ∀ j ≥ N2, ∀ k ≥ N2, padicNorm p (↑f j - ↑f k) < ε<VAR>n m : ℕ<VAR>hn : max N1 N2 ≤ n<VAR>hm : max N1 N2 ≤ m<VAR>this✝¹ : padicNorm p (↑f n - ↑f m) < ε<VAR>this✝ : padicNorm p (↑f n - ↑f m) < padicNorm p (↑f n)<VAR>this : padicNorm p (-↑f m + ↑f n) < padicNorm p (-↑f m + ↑f n)<VAR>hne : ¬padicNorm p (-↑f m) = padicNorm p (↑f n)<VAR>hnam : padicNorm p (-↑f m + ↑f n) = max (padicNorm p (↑f n)) (padicNorm p (↑f m))<GOAL>False
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>inst✝¹ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : Solution hζ<VAR>S' : Solution' hζ<VAR>inst✝ : DecidableRel fun a b => a ∣ b<GOAL>λ ∣ S.a + ↑η ^ 2 * S.b
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>inst✝¹ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : Solution hζ<VAR>S' : Solution' hζ<VAR>inst✝ : DecidableRel fun a b => a ∣ b<GOAL>λ ∣ S.a + S.b + λ ^ 2 * S.b + 2 * λ * S.b
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>r : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝ : CommSemiring R<VAR>p✝ q✝ p q : MvPolynomial σ R<VAR>h : q.totalDegree < p.totalDegree<GOAL>(q + p).totalDegree = p.totalDegree
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>ι : Type u_4<VAR>p : ι → P<VAR>s : Set ι<VAR>i : ι<VAR>hi : i ∈ s<GOAL>vectorSpan k (p '' s) = Submodule.span k ((fun x => p i -ᵥ x) '' (p '' (s \ {i})))
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>ι : Type u_4<VAR>p : ι → P<VAR>s : Set ι<VAR>i : ι<VAR>hi : i ∈ s<GOAL>Submodule.span k (insert (p i -ᵥ p i) ((fun x => p i -ᵥ x) '' (p '' (s \ {i})))) = Submodule.span k ((fun x => p i -ᵥ x) '' (p '' (s \ {i})))
<VAR>ι : Type u_1<VAR>inst✝⁴ : DecidableEq ι<VAR>A : ι → Type u_2<VAR>R : Type u_3<VAR>inst✝³ : (i : ι) → AddCommMonoid (A i)<VAR>inst✝² : AddMonoid ι<VAR>inst✝¹ : GSemiring A<VAR>inst✝ : Semiring R<VAR>F : (⨁ (i : ι), A i) →+* R<GOAL>((↑F).comp (of A 0)) GradedMonoid.GOne.one = 1
<VAR>ι : Type u_1<VAR>inst✝⁴ : DecidableEq ι<VAR>A : ι → Type u_2<VAR>R : Type u_3<VAR>inst✝³ : (i : ι) → AddCommMonoid (A i)<VAR>inst✝² : AddMonoid ι<VAR>inst✝¹ : GSemiring A<VAR>inst✝ : Semiring R<VAR>F : (⨁ (i : ι), A i) →+* R<GOAL>↑F ((of A 0) GradedMonoid.GOne.one) = 1
<VAR>ι : Type u_1<VAR>inst✝⁴ : DecidableEq ι<VAR>A : ι → Type u_2<VAR>R : Type u_3<VAR>inst✝³ : (i : ι) → AddCommMonoid (A i)<VAR>inst✝² : AddMonoid ι<VAR>inst✝¹ : GSemiring A<VAR>inst✝ : Semiring R<VAR>F : (⨁ (i : ι), A i) →+* R<GOAL>↑F ((of A 0) GradedMonoid.GOne.one) = F 1
<VAR>ι : Type u_1<VAR>inst✝⁴ : DecidableEq ι<VAR>A : ι → Type u_2<VAR>R : Type u_3<VAR>inst✝³ : (i : ι) → AddCommMonoid (A i)<VAR>inst✝² : AddMonoid ι<VAR>inst✝¹ : GSemiring A<VAR>inst✝ : Semiring R<VAR>F : (⨁ (i : ι), A i) →+* R<VAR>i j : ι<VAR>ai : A i<VAR>aj : A j<GOAL>((↑F).comp (of A (i + j))) (GradedMonoid.GMul.mul ai aj) = ((↑F).comp (of A i)) ai * ((↑F).comp (of A j)) aj
<VAR>ι : Type u_1<VAR>inst✝⁴ : DecidableEq ι<VAR>A : ι → Type u_2<VAR>R : Type u_3<VAR>inst✝³ : (i : ι) → AddCommMonoid (A i)<VAR>inst✝² : AddMonoid ι<VAR>inst✝¹ : GSemiring A<VAR>inst✝ : Semiring R<VAR>F : (⨁ (i : ι), A i) →+* R<VAR>i j : ι<VAR>ai : A i<VAR>aj : A j<GOAL>F ((of A (i + j)) (GradedMonoid.GMul.mul ai aj)) = F ((of A i) ai) * F ((of A j) aj)
<VAR>ι : Type u_1<VAR>inst✝⁴ : DecidableEq ι<VAR>A : ι → Type u_2<VAR>R : Type u_3<VAR>inst✝³ : (i : ι) → AddCommMonoid (A i)<VAR>inst✝² : AddMonoid ι<VAR>inst✝¹ : GSemiring A<VAR>inst✝ : Semiring R<VAR>f : { f // f GradedMonoid.GOne.one = 1 ∧ ∀ {i j : ι} (ai : A i) (aj : A j), f (GradedMonoid.GMul.mul ai aj) = f ai * f aj }<VAR>xi : ι<VAR>xv : A xi<GOAL>↑((fun F => ⟨fun {i} => (↑F).comp (of A i), ⋯⟩) ((fun f => toSemiring (fun x => ↑f) ⋯ ⋯) f)) xv = ↑f xv