ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>μ : YoungDiagram<VAR>j1 j2 : ℕ<VAR>hj : j1 ≤ j2<GOAL>μ.colLen j2 ≤ μ.colLen j1
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝¹ : SemilatticeInf α<VAR>inst✝ : Nonempty α<VAR>p : α × α → Prop<GOAL>(∀ᶠ (x : α × α) in atBot, p x) ↔ ∃ a, ∀ (k l : α), k ≤ a → l ≤ a → p (k, l)
<VAR>G : Type u<VAR>α : Type v<VAR>β : Type w<VAR>inst✝ : Group G<VAR>n p : ℕ<VAR>hp : Nat.Prime p<VAR>h : IsPGroup p G<VAR>hn : p ^ n ≤ Nat.card G<VAR>this : Fact (Nat.Prime p)<GOAL>∃ H, Nat.card ↥H = p ^ n
<VAR>G : Type u<VAR>α : Type v<VAR>β : Type w<VAR>inst✝ : Group G<VAR>n p : ℕ<VAR>hp : Nat.Prime p<VAR>h : IsPGroup p G<VAR>hn : p ^ n ≤ Nat.card G<VAR>this✝ : Fact (Nat.Prime p)<VAR>this : Finite G<GOAL>∃ H, Nat.card ↥H = p ^ n
<VAR>G : Type u<VAR>α : Type v<VAR>β : Type w<VAR>inst✝ : Group G<VAR>n p : ℕ<VAR>hp : Nat.Prime p<VAR>h : IsPGroup p G<VAR>hn : p ^ n ≤ Nat.card G<VAR>this✝ : Fact (Nat.Prime p)<VAR>this : Finite G<VAR>m : ℕ<VAR>hm : Nat.card G = p ^ m<GOAL>∃ H, Nat.card ↥H = p ^ n
<VAR>G : Type u<VAR>α : Type v<VAR>β : Type w<VAR>inst✝ : Group G<VAR>n p : ℕ<VAR>hp : Nat.Prime p<VAR>h : IsPGroup p G<VAR>hn : p ^ n ≤ Nat.card G<VAR>this✝ : Fact (Nat.Prime p)<VAR>this : Finite G<VAR>m : ℕ<VAR>hm : Nat.card G = p ^ m<GOAL>p ^ n ∣ Nat.card G
<VAR>G : Type u<VAR>α : Type v<VAR>β : Type w<VAR>inst✝ : Group G<VAR>n p : ℕ<VAR>hp : Nat.Prime p<VAR>h : IsPGroup p G<VAR>this✝ : Fact (Nat.Prime p)<VAR>this : Finite G<VAR>m : ℕ<VAR>hn : p ^ n ≤ p ^ m<VAR>hm : Nat.card G = p ^ m<GOAL>p ^ n ∣ p ^ m
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁷ : MeasurableSpace α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>f : α → E<VAR>g : α → F<VAR>a b : α<VAR>μ : Measure α<VAR>l : Filter α<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : CompactIccSpace α<VAR>g' : α → F<VAR>inst✝ : atTop.IsMeasurablyGenerated<VAR>hf : LocallyIntegrableOn f (Ici a) μ<VAR>ho : f =O[atTop] g<VAR>hg : IntegrableAtFilter g atTop μ<GOAL>IntegrableOn f (Ici a) μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁷ : MeasurableSpace α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>f : α → E<VAR>g : α → F<VAR>a b : α<VAR>μ : Measure α<VAR>l : Filter α<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : CompactIccSpace α<VAR>g' : α → F<VAR>inst✝ : atTop.IsMeasurablyGenerated<VAR>hf : LocallyIntegrableOn f (Ici a) μ<VAR>ho : f =O[atTop] g<VAR>hg : IntegrableAtFilter g atTop μ<GOAL>StronglyMeasurableAtFilter f atTop μ
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>𝕜 : Type u_4<VAR>E : Type u_5<VAR>inst✝³ : DecidableEq α<VAR>inst✝² : CommMonoid α<VAR>inst✝¹ : CommMonoid β<VAR>inst✝ : DecidableEq β<VAR>A : Finset α<VAR>B : Finset β<VAR>f : α → β<VAR>hf : IsMulFreimanHom 2 (↑A) (↑B) f<VAR>hf' : Set.BijOn f ↑A ↑B<GOAL>mulRothNumber B ≤ mulRothNumber A
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>𝕜 : Type u_4<VAR>E : Type u_5<VAR>inst✝³ : DecidableEq α<VAR>inst✝² : CommMonoid α<VAR>inst✝¹ : CommMonoid β<VAR>inst✝ : DecidableEq β<VAR>A : Finset α<VAR>B : Finset β<VAR>f : α → β<VAR>hf : IsMulFreimanHom 2 (↑A) (↑B) f<VAR>hf' : Set.BijOn f ↑A ↑B<VAR>s : Finset β<VAR>hsB : s ⊆ B<VAR>hcard : s.card = mulRothNumber B<VAR>hs : ThreeGPFree ↑s<GOAL>mulRothNumber B ≤ mulRothNumber A
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>𝕜 : Type u_4<VAR>E : Type u_5<VAR>inst✝³ : DecidableEq α<VAR>inst✝² : CommMonoid α<VAR>inst✝¹ : CommMonoid β<VAR>inst✝ : DecidableEq β<VAR>A : Finset α<VAR>B : Finset β<VAR>f : α → β<VAR>hf : IsMulFreimanHom 2 (↑A) (↑B) f<VAR>hf' : Set.BijOn f ↑A ↑B<VAR>s : Finset β<VAR>hsB : s ⊆ B<VAR>hcard : s.card = mulRothNumber B<VAR>hs : ThreeGPFree ↑s<VAR>hsA : invFunOn f ↑A '' ↑s ⊆ ↑A<GOAL>mulRothNumber B ≤ mulRothNumber A
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>𝕜 : Type u_4<VAR>E : Type u_5<VAR>inst✝³ : DecidableEq α<VAR>inst✝² : CommMonoid α<VAR>inst✝¹ : CommMonoid β<VAR>inst✝ : DecidableEq β<VAR>A : Finset α<VAR>B : Finset β<VAR>f : α → β<VAR>hf : IsMulFreimanHom 2 (↑A) (↑B) f<VAR>hf' : Set.BijOn f ↑A ↑B<VAR>s : Finset β<VAR>hsB : s ⊆ B<VAR>hcard : s.card = mulRothNumber B<VAR>hs : ThreeGPFree ↑s<VAR>hsA : invFunOn f ↑A '' ↑s ⊆ ↑A<VAR>hfsA : Set.SurjOn f ↑A ↑s<GOAL>mulRothNumber B ≤ mulRothNumber A
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>𝕜 : Type u_4<VAR>E : Type u_5<VAR>inst✝³ : DecidableEq α<VAR>inst✝² : CommMonoid α<VAR>inst✝¹ : CommMonoid β<VAR>inst✝ : DecidableEq β<VAR>A : Finset α<VAR>B : Finset β<VAR>f : α → β<VAR>hf : IsMulFreimanHom 2 (↑A) (↑B) f<VAR>hf' : Set.BijOn f ↑A ↑B<VAR>s : Finset β<VAR>hsB : s ⊆ B<VAR>hcard : s.card = mulRothNumber B<VAR>hs : ThreeGPFree ↑s<VAR>hsA : invFunOn f ↑A '' ↑s ⊆ ↑A<VAR>hfsA : Set.SurjOn f ↑A ↑s<GOAL>(image (invFunOn f ↑A) s).card ≤ mulRothNumber A
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>𝕜 : Type u_4<VAR>E : Type u_5<VAR>inst✝³ : DecidableEq α<VAR>inst✝² : CommMonoid α<VAR>inst✝¹ : CommMonoid β<VAR>inst✝ : DecidableEq β<VAR>A : Finset α<VAR>B : Finset β<VAR>f : α → β<VAR>hf : IsMulFreimanHom 2 (↑A) (↑B) f<VAR>hf' : Set.BijOn f ↑A ↑B<VAR>s : Finset β<VAR>hsB : s ⊆ B<VAR>hcard : s.card = mulRothNumber B<VAR>hs : ThreeGPFree ↑s<VAR>hsA : invFunOn f ↑A '' ↑s ⊆ ↑A<VAR>hfsA : Set.SurjOn f ↑A ↑s<GOAL>ThreeGPFree ↑(image (invFunOn f ↑A) s)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>𝕜 : Type u_4<VAR>E : Type u_5<VAR>inst✝³ : DecidableEq α<VAR>inst✝² : CommMonoid α<VAR>inst✝¹ : CommMonoid β<VAR>inst✝ : DecidableEq β<VAR>A : Finset α<VAR>B : Finset β<VAR>f : α → β<VAR>hf : IsMulFreimanHom 2 (↑A) (↑B) f<VAR>hf' : Set.BijOn f ↑A ↑B<VAR>s : Finset β<VAR>hsB : s ⊆ B<VAR>hcard : s.card = mulRothNumber B<VAR>hs : ThreeGPFree ↑s<VAR>hsA : invFunOn f ↑A '' ↑s ⊆ ↑A<VAR>hfsA : Set.SurjOn f ↑A ↑s<GOAL>ThreeGPFree (invFunOn f ↑A '' ↑s)
<VAR>m n : ℕ<GOAL>↑(m * (n + 1)) = ↑m * ↑(n + 1)
<VAR>E : Type u_1<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace ℂ E<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℂ F<VAR>H : Type u_3<VAR>inst✝⁵ : TopologicalSpace H<VAR>I : ModelWithCorners ℂ E H<VAR>inst✝⁴ : I.Boundaryless<VAR>M : Type u_4<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : CompactSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>f : M → F<VAR>c : M<VAR>hd : ∀ᶠ (z : M) in 𝓝 c, MDifferentiableAt I 𝓘(ℂ, F) f z<VAR>hc : IsLocalMax (norm ∘ f) c<VAR>e : PartialEquiv M E := extChartAt I c<GOAL>∀ᶠ (y : M) in 𝓝 c, ‖f y‖ = ‖f c‖
<VAR>E : Type u_1<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace ℂ E<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℂ F<VAR>H : Type u_3<VAR>inst✝⁵ : TopologicalSpace H<VAR>I : ModelWithCorners ℂ E H<VAR>inst✝⁴ : I.Boundaryless<VAR>M : Type u_4<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : CompactSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>f : M → F<VAR>c : M<VAR>hd : ∀ᶠ (z : M) in 𝓝 c, MDifferentiableAt I 𝓘(ℂ, F) f z<VAR>hc : IsLocalMax (norm ∘ f) c<VAR>e : PartialEquiv M E := extChartAt I c<VAR>hI : range ↑I = univ<GOAL>∀ᶠ (y : M) in 𝓝 c, ‖f y‖ = ‖f c‖
<VAR>E : Type u_1<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace ℂ E<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℂ F<VAR>H : Type u_3<VAR>inst✝⁵ : TopologicalSpace H<VAR>I : ModelWithCorners ℂ E H<VAR>inst✝⁴ : I.Boundaryless<VAR>M : Type u_4<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : CompactSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>f : M → F<VAR>c : M<VAR>hd : ∀ᶠ (z : M) in 𝓝 c, MDifferentiableAt I 𝓘(ℂ, F) f z<VAR>hc : IsLocalMax (norm ∘ f) c<VAR>e : PartialEquiv M E := extChartAt I c<VAR>hI : range ↑I = univ<VAR>H₁ : 𝓝[range ↑I] ↑e c = 𝓝 (↑e c)<GOAL>∀ᶠ (y : M) in 𝓝 c, ‖f y‖ = ‖f c‖
<VAR>E : Type u_1<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace ℂ E<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℂ F<VAR>H : Type u_3<VAR>inst✝⁵ : TopologicalSpace H<VAR>I : ModelWithCorners ℂ E H<VAR>inst✝⁴ : I.Boundaryless<VAR>M : Type u_4<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : CompactSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>f : M → F<VAR>c : M<VAR>hd : ∀ᶠ (z : M) in 𝓝 c, MDifferentiableAt I 𝓘(ℂ, F) f z<VAR>hc : IsLocalMax (norm ∘ f) c<VAR>e : PartialEquiv M E := extChartAt I c<VAR>hI : range ↑I = univ<VAR>H₁ : 𝓝[range ↑I] ↑e c = 𝓝 (↑e c)<VAR>H₂ : map (↑e.symm) (𝓝 (↑e c)) = 𝓝 c<GOAL>∀ᶠ (y : M) in 𝓝 c, ‖f y‖ = ‖f c‖
<VAR>E : Type u_1<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace ℂ E<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℂ F<VAR>H : Type u_3<VAR>inst✝⁵ : TopologicalSpace H<VAR>I : ModelWithCorners ℂ E H<VAR>inst✝⁴ : I.Boundaryless<VAR>M : Type u_4<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : CompactSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>f : M → F<VAR>c : M<VAR>hd : ∀ᶠ (z : M) in 𝓝 c, MDifferentiableAt I 𝓘(ℂ, F) f z<VAR>hc : IsLocalMax (norm ∘ f) c<VAR>e : PartialEquiv M E := extChartAt I c<VAR>hI : range ↑I = univ<VAR>H₁ : 𝓝[range ↑I] ↑e c = 𝓝 (↑e c)<VAR>H₂ : map (↑e.symm) (𝓝 (↑e c)) = 𝓝 c<GOAL>∀ᶠ (a : E) in 𝓝 (↑e c), ‖f (↑e.symm a)‖ = ‖f c‖
<VAR>E : Type u_1<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace ℂ E<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℂ F<VAR>H : Type u_3<VAR>inst✝⁵ : TopologicalSpace H<VAR>I : ModelWithCorners ℂ E H<VAR>inst✝⁴ : I.Boundaryless<VAR>M : Type u_4<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : CompactSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>f : M → F<VAR>c : M<VAR>hc : IsLocalMax (norm ∘ f) c<VAR>e : PartialEquiv M E := extChartAt I c<VAR>hI : range ↑I = univ<VAR>H₁ : 𝓝[range ↑I] ↑e c = 𝓝 (↑e c)<VAR>H₂ : map (↑e.symm) (𝓝 (↑e c)) = 𝓝 c<VAR>hd : ∀ᶠ (y : E) in 𝓝 (↑e c), DifferentiableAt ℂ (f ∘ ↑e.symm) y<GOAL>∀ᶠ (a : E) in 𝓝 (↑e c), ‖f (↑e.symm a)‖ = ‖f c‖
<VAR>E : Type u_1<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace ℂ E<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℂ F<VAR>H : Type u_3<VAR>inst✝⁵ : TopologicalSpace H<VAR>I : ModelWithCorners ℂ E H<VAR>inst✝⁴ : I.Boundaryless<VAR>M : Type u_4<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : CompactSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>f : M → F<VAR>c : M<VAR>hc : IsLocalMax (norm ∘ f) c<VAR>e : PartialEquiv M E := extChartAt I c<VAR>hI : range ↑I = univ<VAR>H₁ : 𝓝[range ↑I] ↑e c = 𝓝 (↑e c)<VAR>H₂ : map (↑e.symm) (𝓝 (↑e c)) = 𝓝 c<VAR>hd : ∀ᶠ (y : E) in 𝓝 (↑e c), DifferentiableAt ℂ (f ∘ ↑e.symm) y<VAR>x✝ : E<GOAL>f c = (f ∘ ↑e.symm) (↑e c)
<VAR>E : Type u_1<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace ℂ E<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℂ F<VAR>H : Type u_3<VAR>inst✝⁵ : TopologicalSpace H<VAR>I : ModelWithCorners ℂ E H<VAR>inst✝⁴ : I.Boundaryless<VAR>M : Type u_4<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : CompactSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>f : M → F<VAR>c : M<VAR>hc : IsLocalMax (norm ∘ f) c<VAR>e : PartialEquiv M E := extChartAt I c<VAR>hI : range ↑I = univ<VAR>H₁ : 𝓝[range ↑I] ↑e c = 𝓝 (↑e c)<VAR>H₂ : map (↑e.symm) (𝓝 (↑e c)) = 𝓝 c<VAR>hd : ∀ᶠ (y : E) in 𝓝 (↑e c), DifferentiableAt ℂ (f ∘ ↑e.symm) y<GOAL>IsLocalMax (norm ∘ f ∘ ↑e.symm) (↑e c)
<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 Q : Fin 3 → F<VAR>hQz : Q z = 0<GOAL>addU P Q = 0
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>γ' : Type u_6<VAR>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>ζ : Type u_11<VAR>ζ' : Type u_12<VAR>ν : Type u_13<VAR>f f' : α → β → γ<VAR>g g' : α → β → γ → δ<VAR>s s' : Set α<VAR>t t' : Set β<VAR>u u' : Set γ<VAR>v : Set δ<VAR>a a' : α<VAR>b b' : β<VAR>c c' : γ<VAR>d d' : δ<GOAL>image2 f s t ⊆ u ↔ ∀ a ∈ s, (fun b => f a b) '' t ⊆ u
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹⁴ : CommRing R<VAR>inst✝¹³ : CommRing S<VAR>inst✝¹² : Algebra R S<VAR>Rₘ : Type u_3<VAR>Sₘ : Type u_4<VAR>inst✝¹¹ : CommRing Rₘ<VAR>inst✝¹⁰ : Algebra R Rₘ<VAR>inst✝⁹ : CommRing Sₘ<VAR>inst✝⁸ : Algebra S Sₘ<VAR>M : Submonoid R<VAR>inst✝⁷ : IsLocalization M Rₘ<VAR>inst✝⁶ : IsLocalization (algebraMapSubmonoid S M) Sₘ<VAR>inst✝⁵ : Algebra Rₘ Sₘ<VAR>inst✝⁴ : Algebra R Sₘ<VAR>inst✝³ : IsScalarTower R Rₘ Sₘ<VAR>inst✝² : IsScalarTower R S Sₘ<VAR>ι : Type u_5<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>b : Basis ι R S<VAR>a : S<VAR>i j : ι<GOAL>(algebraMap R Rₘ).mapMatrix ((leftMulMatrix b) a) i j = (leftMulMatrix (Basis.localizationLocalization Rₘ M Sₘ b)) ((algebraMap S Sₘ) a) i j
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>X : Type u_5<VAR>inst✝⁸ : TopologicalSpace X<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : Mul M<VAR>inst✝⁵ : ContinuousMul M<VAR>inst✝⁴ : TopologicalSpace N<VAR>inst✝³ : Monoid N<VAR>inst✝² : ContinuousMul N<VAR>inst✝¹ : T2Space N<VAR>f : ι → Nˣ<VAR>r₁ r₂ : N<VAR>l : Filter ι<VAR>inst✝ : l.NeBot<VAR>h₁ : Tendsto (fun x => ↑(f x)) l (𝓝 r₁)<VAR>h₂ : Tendsto (fun x => ↑(f x)⁻¹) l (𝓝 r₂)<GOAL>1 = r₁ * r₂
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>X : Type u_5<VAR>inst✝⁸ : TopologicalSpace X<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : Mul M<VAR>inst✝⁵ : ContinuousMul M<VAR>inst✝⁴ : TopologicalSpace N<VAR>inst✝³ : Monoid N<VAR>inst✝² : ContinuousMul N<VAR>inst✝¹ : T2Space N<VAR>f : ι → Nˣ<VAR>r₁ r₂ : N<VAR>l : Filter ι<VAR>inst✝ : l.NeBot<VAR>h₁ : Tendsto (fun x => ↑(f x)) l (𝓝 r₁)<VAR>h₂ : Tendsto (fun x => ↑(f x)⁻¹) l (𝓝 r₂)<GOAL>1 = r₂ * r₁
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>t : α → Set β<VAR>s₁ s₂ : Set α<GOAL>(⋃ x ∈ s₁, t x) \ ⋃ x ∈ s₂, t x ⊆ ⋃ x ∈ s₁ \ s₂, t x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>t : α → Set β<VAR>s₁ s₂ : Set α<GOAL>⋃ x ∈ s₁, t x ⊆ ⋃ x ∈ s₂ ∪ s₁ \ s₂, t x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>t : α → Set β<VAR>s₁ s₂ : Set α<GOAL>s₁ ⊆ s₂ ∪ s₁ \ s₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>t : α → Set β<VAR>s₁ s₂ : Set α<GOAL>s₁ ⊆ s₂ ∪ s₁
<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>κ : ι → Sort u_7<VAR>κ' : ι' → Sort u_8<VAR>inst✝ : CompleteLattice α<VAR>f✝ g s✝ t : ι → α<VAR>a b : α<VAR>s : Set β<VAR>f : β → α<GOAL>sSup (f '' s) = ⨆ a ∈ s, f a
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : WeierstrassCurve R<VAR>n : ℕ<GOAL>(W.Φ ↑n).natDegree ≤ n ^ 2 ∧ (W.Φ ↑n).coeff (n ^ 2) = 1
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : WeierstrassCurve R<VAR>n : ℕ<VAR>dm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).natDegree ≤ m + n := fun {m n} {p q} => natDegree_mul_le_of_le<GOAL>(W.Φ ↑n).natDegree ≤ n ^ 2 ∧ (W.Φ ↑n).coeff (n ^ 2) = 1
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : WeierstrassCurve R<VAR>n : ℕ<VAR>dm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).natDegree ≤ m + n := fun {m n} {p q} => natDegree_mul_le_of_le<VAR>dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := fun {m n} {p} => natDegree_pow_le_of_le n<GOAL>(W.Φ ↑n).natDegree ≤ n ^ 2 ∧ (W.Φ ↑n).coeff (n ^ 2) = 1
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : WeierstrassCurve R<VAR>n : ℕ<VAR>dm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).natDegree ≤ m + n := fun {m n} {p q} => natDegree_mul_le_of_le<VAR>dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := fun {m n} {p} => natDegree_pow_le_of_le n<VAR>cm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).coeff (m + n) = p.coeff m * q.coeff n := fun {m n} {p q} => coeff_mul_of_natDegree_le<GOAL>(W.Φ ↑n).natDegree ≤ n ^ 2 ∧ (W.Φ ↑n).coeff (n ^ 2) = 1
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : WeierstrassCurve R<VAR>n : ℕ<VAR>dm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).natDegree ≤ m + n := fun {m n} {p q} => natDegree_mul_le_of_le<VAR>dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := fun {m n} {p} => natDegree_pow_le_of_le n<VAR>cm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).coeff (m + n) = p.coeff m * q.coeff n := fun {m n} {p q} => coeff_mul_of_natDegree_le<VAR>h : ∀ {n : ℕ}, (W.preΨ' n).natDegree ≤ WeierstrassCurve.expDegree n ∧ (W.preΨ' n).coeff (WeierstrassCurve.expDegree n) = ↑(WeierstrassCurve.expCoeff n) := fun {n} => WeierstrassCurve.natDegree_coeff_preΨ' W n<GOAL>(W.Φ ↑n).natDegree ≤ n ^ 2 ∧ (W.Φ ↑n).coeff (n ^ 2) = 1
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : WeierstrassCurve R<VAR>dm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).natDegree ≤ m + n := fun {m n} {p q} => natDegree_mul_le_of_le<VAR>dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := fun {m n} {p} => natDegree_pow_le_of_le n<VAR>cm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).coeff (m + n) = p.coeff m * q.coeff n := fun {m n} {p q} => coeff_mul_of_natDegree_le<VAR>h : ∀ {n : ℕ}, (W.preΨ' n).natDegree ≤ WeierstrassCurve.expDegree n ∧ (W.preΨ' n).coeff (WeierstrassCurve.expDegree n) = ↑(WeierstrassCurve.expCoeff n) := fun {n} => WeierstrassCurve.natDegree_coeff_preΨ' W n<VAR>n : ℕ<GOAL>(W.Φ ↑(n + 1 + 1)).natDegree ≤ (n + 1 + 1) ^ 2 ∧ (W.Φ ↑(n + 1 + 1)).coeff ((n + 1 + 1) ^ 2) = 1
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : WeierstrassCurve R<VAR>dm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).natDegree ≤ m + n := fun {m n} {p q} => natDegree_mul_le_of_le<VAR>dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := fun {m n} {p} => natDegree_pow_le_of_le n<VAR>cm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).coeff (m + n) = p.coeff m * q.coeff n := fun {m n} {p q} => coeff_mul_of_natDegree_le<VAR>h : ∀ {n : ℕ}, (W.preΨ' n).natDegree ≤ WeierstrassCurve.expDegree n ∧ (W.preΨ' n).coeff (WeierstrassCurve.expDegree n) = ↑(WeierstrassCurve.expCoeff n) := fun {n} => WeierstrassCurve.natDegree_coeff_preΨ' W n<VAR>n : ℕ<VAR>hd : (n + 1 + 1) ^ 2 = 1 + 2 * WeierstrassCurve.expDegree (n + 2) + if Even (n + 1) then 0 else 3<GOAL>(W.Φ ↑(n + 1 + 1)).natDegree ≤ (n + 1 + 1) ^ 2 ∧ (W.Φ ↑(n + 1 + 1)).coeff ((n + 1 + 1) ^ 2) = 1
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : WeierstrassCurve R<VAR>dm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).natDegree ≤ m + n := fun {m n} {p q} => natDegree_mul_le_of_le<VAR>dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := fun {m n} {p} => natDegree_pow_le_of_le n<VAR>cm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).coeff (m + n) = p.coeff m * q.coeff n := fun {m n} {p q} => coeff_mul_of_natDegree_le<VAR>h : ∀ {n : ℕ}, (W.preΨ' n).natDegree ≤ WeierstrassCurve.expDegree n ∧ (W.preΨ' n).coeff (WeierstrassCurve.expDegree n) = ↑(WeierstrassCurve.expCoeff n) := fun {n} => WeierstrassCurve.natDegree_coeff_preΨ' W n<VAR>n : ℕ<VAR>hd : (n + 1 + 1) ^ 2 = 1 + 2 * WeierstrassCurve.expDegree (n + 2) + if Even (n + 1) then 0 else 3<VAR>hd' : (n + 1 + 1) ^ 2 = WeierstrassCurve.expDegree (n + 3) + WeierstrassCurve.expDegree (n + 1) + if Even (n + 1) then 3 else 0<GOAL>(W.Φ ↑(n + 1 + 1)).natDegree ≤ (n + 1 + 1) ^ 2 ∧ (W.Φ ↑(n + 1 + 1)).coeff ((n + 1 + 1) ^ 2) = 1
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : WeierstrassCurve R<VAR>dm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).natDegree ≤ m + n := fun {m n} {p q} => natDegree_mul_le_of_le<VAR>dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := fun {m n} {p} => natDegree_pow_le_of_le n<VAR>cm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).coeff (m + n) = p.coeff m * q.coeff n := fun {m n} {p q} => coeff_mul_of_natDegree_le<VAR>h : ∀ {n : ℕ}, (W.preΨ' n).natDegree ≤ WeierstrassCurve.expDegree n ∧ (W.preΨ' n).coeff (WeierstrassCurve.expDegree n) = ↑(WeierstrassCurve.expCoeff n) := fun {n} => WeierstrassCurve.natDegree_coeff_preΨ' W n<VAR>n : ℕ<VAR>hd : (n + 1 + 1) ^ 2 = 1 + 2 * WeierstrassCurve.expDegree (n + 2) + if Even (n + 1) then 0 else 3<VAR>hd' : (n + 1 + 1) ^ 2 = WeierstrassCurve.expDegree (n + 3) + WeierstrassCurve.expDegree (n + 1) + if Even (n + 1) then 3 else 0<VAR>hc : 1 = (1 * WeierstrassCurve.expCoeff (n + 2) ^ 2 * if Even (n + 1) then 1 else 4) - WeierstrassCurve.expCoeff (n + 3) * WeierstrassCurve.expCoeff (n + 1) * if Even (n + 1) then 4 else 1<GOAL>(W.Φ ↑(n + 1 + 1)).natDegree ≤ (n + 1 + 1) ^ 2 ∧ (W.Φ ↑(n + 1 + 1)).coeff ((n + 1 + 1) ^ 2) = 1
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : WeierstrassCurve R<VAR>dm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).natDegree ≤ m + n := fun {m n} {p q} => natDegree_mul_le_of_le<VAR>dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := fun {m n} {p} => natDegree_pow_le_of_le n<VAR>cm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).coeff (m + n) = p.coeff m * q.coeff n := fun {m n} {p q} => coeff_mul_of_natDegree_le<VAR>h : ∀ {n : ℕ}, (W.preΨ' n).natDegree ≤ WeierstrassCurve.expDegree n ∧ (W.preΨ' n).coeff (WeierstrassCurve.expDegree n) = ↑(WeierstrassCurve.expCoeff n) := fun {n} => WeierstrassCurve.natDegree_coeff_preΨ' W n<VAR>n : ℕ<VAR>hd : (n + 1 + 1) ^ 2 = 1 + 2 * WeierstrassCurve.expDegree (n + 2) + if Even (n + 1) then 0 else 3<VAR>hd' : (n + 1 + 1) ^ 2 = WeierstrassCurve.expDegree (n + 3) + WeierstrassCurve.expDegree (n + 1) + if Even (n + 1) then 3 else 0<VAR>hc : 1 = (1 * WeierstrassCurve.expCoeff (n + 2) ^ 2 * if Even (n + 1) then 1 else 4) - WeierstrassCurve.expCoeff (n + 3) * WeierstrassCurve.expCoeff (n + 1) * if Even (n + 1) then 4 else 1<GOAL>((X * W.preΨ' (n + 1 + 1) ^ 2 * if Even (n + 1) then 1 else W.Ψ₂Sq) - W.preΨ' (n + 1 + 2) * W.preΨ' (n + 1) * if Even (n + 1) then W.Ψ₂Sq else 1).natDegree ≤ (n + 1 + 1) ^ 2 ∧ ((X * W.preΨ' (n + 1 + 1) ^ 2 * if Even (n + 1) then 1 else W.Ψ₂Sq) - W.preΨ' (n + 1 + 2) * W.preΨ' (n + 1) * if Even (n + 1) then W.Ψ₂Sq else 1).coeff ((n + 1 + 1) ^ 2) = 1
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : OrderTop α<VAR>h : IsAtomic αᵒᵈ<VAR>b : α<GOAL>b = ⊤ ∨ ∃ a, IsCoatom a ∧ b ≤ a
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : OrderTop α<VAR>h : IsCoatomic α<VAR>b : αᵒᵈ<GOAL>b = ⊥ ∨ ∃ a, IsAtom a ∧ a ≤ b
<VAR>T a b : ℝ<VAR>hab : a < b<VAR>f f' : ℝ → ℂ<VAR>n : ℤ<VAR>hn : n ≠ 0<VAR>hf : ContinuousOn f [[a, b]]<VAR>hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Ioi x) x<VAR>hf' : IntervalIntegrable f' volume a b<GOAL>fourierCoeffOn hab f n = 1 / (-2 * ↑π * I * ↑n) * ((fourier (-n)) ↑a * (f b - f a) - (↑b - ↑a) * fourierCoeffOn hab f' n)
<VAR>T a b : ℝ<VAR>hab : a < b<VAR>f f' : ℝ → ℂ<VAR>n : ℤ<VAR>hn : n ≠ 0<VAR>hf : ContinuousOn f [[a, b]]<VAR>hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Ioi x) x<VAR>hf' : IntervalIntegrable f' volume a b<GOAL>fourierCoeffOn hab f n = 1 / (-2 * ↑π * I * ↑n) * ((fourier (-n)) ↑a * (f b - f a) - ↑(b - a) * fourierCoeffOn hab f' n)
<VAR>T a b : ℝ<VAR>hab : a < b<VAR>f f' : ℝ → ℂ<VAR>n : ℤ<VAR>hn : n ≠ 0<VAR>hf : ContinuousOn f [[a, b]]<VAR>hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Ioi x) x<VAR>hf' : IntervalIntegrable f' volume a b<VAR>hT : Fact (0 < b - a)<GOAL>fourierCoeffOn hab f n = 1 / (-2 * ↑π * I * ↑n) * ((fourier (-n)) ↑a * (f b - f a) - ↑(b - a) * fourierCoeffOn hab f' n)