ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type x<VAR>k : Type y<VAR>A : Type z<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : CommRing R<VAR>f : R[X]<VAR>x y : R<GOAL>eval₂ (RingHom.id R) (x + y) f = f.sum fun e a => a * (x ^ e + ↑e * x ^ (e - 1) * y + ↑(Polynomial.polyBinomAux1 x y e a) * y ^ 2)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type x<VAR>k : Type y<VAR>A : Type z<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : CommRing R<VAR>f : R[X]<VAR>x y : R<GOAL>(f.sum fun e a => (RingHom.id R) a * (x + y) ^ e) = f.sum fun e a => a * (x ^ e + ↑e * x ^ (e - 1) * y + ↑(Polynomial.polyBinomAux1 x y e a) * y ^ 2)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type x<VAR>k : Type y<VAR>A : Type z<VAR>a b : R<VAR>m n✝ : ℕ<VAR>inst✝ : CommRing R<VAR>f : R[X]<VAR>x y : R<VAR>n : ℕ<VAR>z : R<GOAL>(RingHom.id R) z * (x + y) ^ n = z * (x ^ n + ↑n * x ^ (n - 1) * y + ↑(Polynomial.polyBinomAux1 x y n z) * y ^ 2)
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>n : ℕ<GOAL>card ↑(derangements (Fin (n + 2))) = (n + 1) * card ↑(derangements (Fin n)) + (n + 1) * card ↑(derangements (Fin (n + 1)))
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>n : ℕ<VAR>h1 : ∀ (a : Fin (n + 1)), card ↑{a}ᶜ = card (Fin n)<GOAL>card ↑(derangements (Fin (n + 2))) = (n + 1) * card ↑(derangements (Fin n)) + (n + 1) * card ↑(derangements (Fin (n + 1)))
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>n : ℕ<VAR>h1 : ∀ (a : Fin (n + 1)), card ↑{a}ᶜ = card (Fin n)<VAR>h2 : card (Fin (n + 2)) = card (Option (Fin (n + 1)))<GOAL>card ↑(derangements (Fin (n + 2))) = (n + 1) * card ↑(derangements (Fin n)) + (n + 1) * card ↑(derangements (Fin (n + 1)))
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>r r' : α → α → Prop<VAR>f : β → α<VAR>s✝ t : Set α<VAR>x y : α<VAR>s : Set β<GOAL>(f '' s).WellFoundedOn r ↔ s.WellFoundedOn (r on f)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>r r' : α → α → Prop<VAR>f : β → α<VAR>s✝ t : Set α<VAR>x y : α<VAR>s : Set β<GOAL>(range fun x => f ↑x).WellFoundedOn r ↔ s.WellFoundedOn (r on f)
<VAR>α : Type u_1<VAR>inst✝ : MetricSpace α<VAR>C : Set α<VAR>hC : Perfect C<VAR>ε : ℝ≥0∞<VAR>ε_pos : 0 < ε<VAR>x : α<VAR>xC : x ∈ C<GOAL>let D := closure (EMetric.ball x (ε / 2) ∩ C); Perfect D ∧ D.Nonempty ∧ D ⊆ C ∧ EMetric.diam D ≤ ε
<VAR>α : Type u_1<VAR>inst✝ : MetricSpace α<VAR>C : Set α<VAR>hC : Perfect C<VAR>ε : ℝ≥0∞<VAR>ε_pos : 0 < ε<VAR>x : α<VAR>xC : x ∈ C<VAR>this : x ∈ EMetric.ball x (ε / 2)<GOAL>let D := closure (EMetric.ball x (ε / 2) ∩ C); Perfect D ∧ D.Nonempty ∧ D ⊆ C ∧ EMetric.diam D ≤ ε
<VAR>α : Type u_1<VAR>inst✝ : MetricSpace α<VAR>C : Set α<VAR>hC : Perfect C<VAR>ε : ℝ≥0∞<VAR>ε_pos : 0 < ε<VAR>x : α<VAR>xC : x ∈ C<VAR>this✝ : x ∈ EMetric.ball x (ε / 2)<VAR>this : Perfect (closure (EMetric.ball x (ε / 2) ∩ C)) ∧ (closure (EMetric.ball x (ε / 2) ∩ C)).Nonempty<GOAL>let D := closure (EMetric.ball x (ε / 2) ∩ C); Perfect D ∧ D.Nonempty ∧ D ⊆ C ∧ EMetric.diam D ≤ ε
<VAR>α : Type u_1<VAR>inst✝ : MetricSpace α<VAR>C : Set α<VAR>hC : Perfect C<VAR>ε : ℝ≥0∞<VAR>ε_pos : 0 < ε<VAR>x : α<VAR>xC : x ∈ C<VAR>this✝ : x ∈ EMetric.ball x (ε / 2)<VAR>this : Perfect (closure (EMetric.ball x (ε / 2) ∩ C)) ∧ (closure (EMetric.ball x (ε / 2) ∩ C)).Nonempty<GOAL>closure (EMetric.ball x (ε / 2) ∩ C) ⊆ C
<VAR>α : Type u_1<VAR>inst✝ : MetricSpace α<VAR>C : Set α<VAR>hC : Perfect C<VAR>ε : ℝ≥0∞<VAR>ε_pos : 0 < ε<VAR>x : α<VAR>xC : x ∈ C<VAR>this✝ : x ∈ EMetric.ball x (ε / 2)<VAR>this : Perfect (closure (EMetric.ball x (ε / 2) ∩ C)) ∧ (closure (EMetric.ball x (ε / 2) ∩ C)).Nonempty<GOAL>EMetric.diam (closure (EMetric.ball x (ε / 2) ∩ C)) ≤ ε
<VAR>α : Type u_1<VAR>inst✝ : MetricSpace α<VAR>C : Set α<VAR>hC : Perfect C<VAR>ε : ℝ≥0∞<VAR>ε_pos : 0 < ε<VAR>x : α<VAR>xC : x ∈ C<VAR>this✝ : x ∈ EMetric.ball x (ε / 2)<VAR>this : Perfect (closure (EMetric.ball x (ε / 2) ∩ C)) ∧ (closure (EMetric.ball x (ε / 2) ∩ C)).Nonempty<GOAL>EMetric.diam (EMetric.ball x (ε / 2) ∩ C) ≤ ε
<VAR>α : Type u_1<VAR>inst✝ : MetricSpace α<VAR>C : Set α<VAR>hC : Perfect C<VAR>ε : ℝ≥0∞<VAR>ε_pos : 0 < ε<VAR>x : α<VAR>xC : x ∈ C<VAR>this✝ : x ∈ EMetric.ball x (ε / 2)<VAR>this : Perfect (closure (EMetric.ball x (ε / 2) ∩ C)) ∧ (closure (EMetric.ball x (ε / 2) ∩ C)).Nonempty<GOAL>EMetric.diam (EMetric.ball x (ε / 2)) ≤ ε
<VAR>α : Type u_1<VAR>inst✝ : MetricSpace α<VAR>C : Set α<VAR>hC : Perfect C<VAR>ε : ℝ≥0∞<VAR>ε_pos : 0 < ε<VAR>x : α<VAR>xC : x ∈ C<VAR>this✝ : x ∈ EMetric.ball x (ε / 2)<VAR>this : Perfect (closure (EMetric.ball x (ε / 2) ∩ C)) ∧ (closure (EMetric.ball x (ε / 2) ∩ C)).Nonempty<GOAL>ε = 2 * (ε / 2)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : OrderClosedTopology α<VAR>f g : β → α<VAR>l : Filter β<VAR>a : α<VAR>h : Tendsto f l (𝓝[>] a)<GOAL>Tendsto (fun i => max (f i) a) l (𝓝[>] a)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : Preorder α<VAR>inst✝¹ : OrderBot α<VAR>inst✝ : OrderTopology α<GOAL>𝓝 ⊥ = ⨅ l, ⨅ (_ : ⊥ < l), 𝓟 (Iio l)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : LinearOrder α<VAR>a b : α<GOAL>max a b = if b ≤ a then a else b
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : LinearOrder α<VAR>a b : α<GOAL>(if a ≤ b then b else a) = if b ≤ a then a else b
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : LinearOrder α<VAR>a b : α<VAR>lt : a < b<GOAL>(if a ≤ b then b else a) = if b ≤ a then a else b
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : LinearOrder α<VAR>a b : α<VAR>eq : a = b<GOAL>(if a ≤ b then b else a) = if b ≤ a then a else b
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : LinearOrder α<VAR>a b : α<VAR>gt : b < a<GOAL>(if a ≤ b then b else a) = if b ≤ a then a else b
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : HasKernels C<VAR>inst✝ : HasCokernels C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>kernel.lift (cokernel.π f) f ⋯ ≫ equalizer.ι (cokernel.π f) 0 = (cokernel.π (kernel.ι f) ≫ coimageImageComparison f) ≫ equalizer.ι (cokernel.π f) 0
<VAR>X✝ : Type u_1<VAR>Y✝ : Type u_2<VAR>inst✝⁴ : TopologicalSpace X✝<VAR>inst✝³ : FirstCountableTopology X✝<VAR>X : Type u_3<VAR>Y : Type u_4<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : T2Space Y<VAR>f : X → Y<VAR>hf : Continuous f<VAR>g : t2Quotient X → Y<VAR>hfg : g ∘ mk = f<GOAL>g = lift hf
<VAR>X✝ : Type u_1<VAR>Y✝ : Type u_2<VAR>inst✝⁴ : TopologicalSpace X✝<VAR>inst✝³ : FirstCountableTopology X✝<VAR>X : Type u_3<VAR>Y : Type u_4<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : T2Space Y<VAR>f : X → Y<VAR>hf : Continuous f<VAR>g : t2Quotient X → Y<VAR>hfg : g ∘ mk = f<GOAL>∀ (x : X), (g ∘ mk) x = (lift hf ∘ mk) x
<VAR>δ : Type u_1<VAR>δ' : Type u_2<VAR>π : δ → Type u_3<VAR>inst✝² : (x : δ) → MeasurableSpace (π x)<VAR>μ : (i : δ) → Measure (π i)<VAR>inst✝¹ : ∀ (i : δ), SigmaFinite (μ i)<VAR>inst✝ : DecidableEq δ<VAR>s t : Finset δ<VAR>f✝ g : ((i : δ) → π i) → ℝ≥0∞<VAR>x✝ y : (i : δ) → π i<VAR>i : δ<VAR>f : ((i : δ) → π i) → ℝ≥0∞<VAR>hf : Measurable f<VAR>hst : Disjoint s t<VAR>x : (i : δ) → π i<VAR>e : ((i : { x // x ∈ s }) → π ↑i) × ((i : { x // x ∈ t }) → π ↑i) ≃ᵐ ((i : { x // x ∈ s ∪ t }) → π ↑i) := MeasurableEquiv.piFinsetUnion π hst<GOAL>(∫⋯∫⁻_s ∪ t, f ∂μ) x = (∫⋯∫⁻_s, ∫⋯∫⁻_t, f ∂μ ∂μ) x
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : Semiring R<VAR>inst✝ : CharP R 2<VAR>x : R<GOAL>x + x = 0
<VAR>u : Lean.Level<VAR>α : Type u_1<VAR>inst✝¹ : DivisionRing α<VAR>inst✝ : CharZero α<VAR>n d : ℕ<VAR>inv✝ : Invertible ↑d<GOAL>IsRat (↑(Int.negOfNat n.succ) * ⅟↑d)⁻¹ (Int.negOfNat d) n.succ
<VAR>u : Lean.Level<VAR>α : Type u_1<VAR>inst✝¹ : DivisionRing α<VAR>inst✝ : CharZero α<VAR>n d : ℕ<VAR>inv✝ : Invertible ↑d<GOAL>IsRat (↑(-Int.ofNat n.succ) * ⅟↑d)⁻¹ (-Int.ofNat d) n.succ
<VAR>u : Lean.Level<VAR>α : Type u_1<VAR>inst✝¹ : DivisionRing α<VAR>inst✝ : CharZero α<VAR>n d : ℕ<VAR>inv✝ : Invertible ↑d<VAR>this : Invertible ↑n.succ<GOAL>IsRat (↑(-Int.ofNat n.succ) * ⅟↑d)⁻¹ (-Int.ofNat d) n.succ
<VAR>u : Lean.Level<VAR>α : Type u_1<VAR>inst✝¹ : DivisionRing α<VAR>inst✝ : CharZero α<VAR>n✝ d : ℕ<VAR>inv✝ : Invertible ↑d<VAR>n : ℕ<VAR>this : Invertible ↑n<GOAL>IsRat (↑(-Int.ofNat n) * ⅟↑d)⁻¹ (-Int.ofNat d) n
<VAR>u : Lean.Level<VAR>α : Type u_1<VAR>inst✝¹ : DivisionRing α<VAR>inst✝ : CharZero α<VAR>n✝ d : ℕ<VAR>inv✝ : Invertible ↑d<VAR>n : ℕ<VAR>this : Invertible ↑n<GOAL>(↑(-Int.ofNat n) * ⅟↑d)⁻¹ = ↑(-Int.ofNat d) * ⅟↑n
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>S : Set E<VAR>α x : E<GOAL>x ∈ adjoin F {α} ↔ ∃ r s, x = (aeval α) r / (aeval α) s
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>S : Set E<VAR>α x : E<GOAL>(∃ a a_1, (aeval α) a / (aeval α) a_1 = x) ↔ ∃ r s, x = (aeval α) r / (aeval α) s
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>f✝ f₀ f₁ g : 𝕜 → F<VAR>f'✝ f₀' f₁' g' : F<VAR>x✝ : 𝕜<VAR>s✝ t✝ : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>𝕜' : Type u_1<VAR>inst✝³ : NontriviallyNormedField 𝕜'<VAR>inst✝² : NormedAlgebra 𝕜 𝕜'<VAR>inst✝¹ : NormedSpace 𝕜' F<VAR>inst✝ : IsScalarTower 𝕜 𝕜' F<VAR>s' t' : Set 𝕜'<VAR>h : 𝕜 → 𝕜'<VAR>h₁ : 𝕜 → 𝕜<VAR>h₂ : 𝕜' → 𝕜'<VAR>h' h₂' : 𝕜'<VAR>h₁' : 𝕜<VAR>g₁ : 𝕜' → F<VAR>g₁' : F<VAR>L' : Filter 𝕜'<VAR>y : 𝕜'<VAR>f : E → 𝕜'<VAR>f' : E →L[𝕜] 𝕜'<VAR>s : Set E<VAR>t : Set 𝕜'<VAR>x : E<VAR>hh : HasDerivWithinAt h₂ h₂' t (f x)<VAR>hf : HasFDerivWithinAt f f' s x<VAR>hst : MapsTo f s t<VAR>hy : y = f x<GOAL>HasFDerivWithinAt (h₂ ∘ f) (h₂' • f') s x
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>m n : ℤ<GOAL>T (m - n) = T m * T (-n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s✝ t✝ u v : Finset α<VAR>a✝ b : α<VAR>s t : Finset α<VAR>a : α<GOAL>s.erase a ∩ t = s ∩ t.erase a
<VAR>𝕜 : Type u_1<VAR>S : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>inst✝¹⁸ : Field 𝕜<VAR>inst✝¹⁷ : CharZero 𝕜<VAR>inst✝¹⁶ : Ring R<VAR>inst✝¹⁵ : AddCommGroup M<VAR>inst✝¹⁴ : Algebra 𝕜 R<VAR>inst✝¹³ : Module 𝕜 M<VAR>inst✝¹² : Module R M<VAR>inst✝¹¹ : Module Rᵐᵒᵖ M<VAR>inst✝¹⁰ : SMulCommClass R Rᵐᵒᵖ M<VAR>inst✝⁹ : IsScalarTower 𝕜 R M<VAR>inst✝⁸ : IsScalarTower 𝕜 Rᵐᵒᵖ M<VAR>inst✝⁷ : TopologicalSpace R<VAR>inst✝⁶ : TopologicalSpace M<VAR>inst✝⁵ : TopologicalRing R<VAR>inst✝⁴ : TopologicalAddGroup M<VAR>inst✝³ : ContinuousSMul R M<VAR>inst✝² : ContinuousSMul Rᵐᵒᵖ M<VAR>inst✝¹ : T2Space R<VAR>inst✝ : T2Space M<VAR>m : M<GOAL>exp 𝕜 (inr m) = 1 + inr m
<VAR>𝕜 : Type u_1<VAR>S : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>inst✝¹⁸ : Field 𝕜<VAR>inst✝¹⁷ : CharZero 𝕜<VAR>inst✝¹⁶ : Ring R<VAR>inst✝¹⁵ : AddCommGroup M<VAR>inst✝¹⁴ : Algebra 𝕜 R<VAR>inst✝¹³ : Module 𝕜 M<VAR>inst✝¹² : Module R M<VAR>inst✝¹¹ : Module Rᵐᵒᵖ M<VAR>inst✝¹⁰ : SMulCommClass R Rᵐᵒᵖ M<VAR>inst✝⁹ : IsScalarTower 𝕜 R M<VAR>inst✝⁸ : IsScalarTower 𝕜 Rᵐᵒᵖ M<VAR>inst✝⁷ : TopologicalSpace R<VAR>inst✝⁶ : TopologicalSpace M<VAR>inst✝⁵ : TopologicalRing R<VAR>inst✝⁴ : TopologicalAddGroup M<VAR>inst✝³ : ContinuousSMul R M<VAR>inst✝² : ContinuousSMul Rᵐᵒᵖ M<VAR>inst✝¹ : T2Space R<VAR>inst✝ : T2Space M<VAR>m : M<GOAL>MulOpposite.op (inr m).fst • (inr m).snd = (inr m).fst • (inr m).snd
<VAR>R : Type u<VAR>inst✝⁴ : CommRing R<VAR>S : Type v<VAR>inst✝³ : CommRing S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>P : Ideal S<VAR>hfp : NeZero e<VAR>inst✝² : IsDedekindDomain S<VAR>inst✝¹ : p.IsMaximal<VAR>inst✝ : P.IsPrime<VAR>hP0 : P ≠ ⊥<VAR>i : ℕ<VAR>hi : i < e<VAR>this : Field (R ⧸ p) := Quotient.field p<GOAL>Module.rank (R ⧸ p) ↥(map (Quotient.mk (P ^ e)) (P ^ i)) = Module.rank (R ⧸ p) (S ⧸ P) + Module.rank (R ⧸ p) ↥(map (Quotient.mk (P ^ e)) (P ^ (i + 1)))
<VAR>R : Type u<VAR>inst✝⁴ : CommRing R<VAR>S : Type v<VAR>inst✝³ : CommRing S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>P : Ideal S<VAR>hfp : NeZero e<VAR>inst✝² : IsDedekindDomain S<VAR>inst✝¹ : p.IsMaximal<VAR>inst✝ : P.IsPrime<VAR>hP0 : P ≠ ⊥<VAR>i : ℕ<VAR>hi : i < e<VAR>this : Field (R ⧸ p) := Quotient.field p<GOAL>Module.rank (R ⧸ p) ↥(map (Quotient.mk (P ^ e)) (P ^ i)) = Module.rank (R ⧸ p) (↥(map (Quotient.mk (P ^ e)) (P ^ i)) ⧸ LinearMap.range (powQuotSuccInclusion f p P i)) + Module.rank (R ⧸ p) ↥(LinearMap.range (powQuotSuccInclusion f p P i))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>G : Type u_5<VAR>inst✝¹⁶ : TopologicalSpace α<VAR>inst✝¹⁵ : AddCommGroup α<VAR>inst✝¹⁴ : TopologicalAddGroup α<VAR>inst✝¹³ : TopologicalSpace β<VAR>inst✝¹² : AddCommGroup β<VAR>inst✝¹¹ : TopologicalAddGroup β<VAR>inst✝¹⁰ : TopologicalSpace γ<VAR>inst✝⁹ : AddCommGroup γ<VAR>inst✝⁸ : TopologicalAddGroup γ<VAR>inst✝⁷ : TopologicalSpace δ<VAR>inst✝⁶ : AddCommGroup δ<VAR>inst✝⁵ : TopologicalAddGroup δ<VAR>inst✝⁴ : UniformSpace G<VAR>inst✝³ : AddCommGroup G<VAR>inst✝² : UniformAddGroup G<VAR>inst✝¹ : T0Space G<VAR>inst✝ : CompleteSpace G<VAR>e : β →+ α<VAR>de : DenseInducing ⇑e<VAR>f : δ →+ γ<VAR>df : DenseInducing ⇑f<VAR>φ : β →+ δ →+ G<VAR>hφ : Continuous fun p => (φ p.1) p.2<VAR>W' : Set G<VAR>W'_nhd : W' ∈ 𝓝 0<VAR>x₀ : α<VAR>y₀ : γ<VAR>ee : β × β → α × α := fun u => (e u.1, e u.2)<VAR>ff : δ × δ → γ × γ := fun u => (f u.1, f u.2)<GOAL>∃ U ∈ comap (⇑e) (𝓝 x₀), ∃ V ∈ comap (⇑f) (𝓝 y₀), ∀ x ∈ U, ∀ x' ∈ U, ∀ y ∈ V, ∀ y' ∈ V, (fun p => (φ p.1) p.2) (x', y') - (fun p => (φ p.1) p.2) (x, y) ∈ W'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>G : Type u_5<VAR>inst✝¹⁶ : TopologicalSpace α<VAR>inst✝¹⁵ : AddCommGroup α<VAR>inst✝¹⁴ : TopologicalAddGroup α<VAR>inst✝¹³ : TopologicalSpace β<VAR>inst✝¹² : AddCommGroup β<VAR>inst✝¹¹ : TopologicalAddGroup β<VAR>inst✝¹⁰ : TopologicalSpace γ<VAR>inst✝⁹ : AddCommGroup γ<VAR>inst✝⁸ : TopologicalAddGroup γ<VAR>inst✝⁷ : TopologicalSpace δ<VAR>inst✝⁶ : AddCommGroup δ<VAR>inst✝⁵ : TopologicalAddGroup δ<VAR>inst✝⁴ : UniformSpace G<VAR>inst✝³ : AddCommGroup G<VAR>inst✝² : UniformAddGroup G<VAR>inst✝¹ : T0Space G<VAR>inst✝ : CompleteSpace G<VAR>e : β →+ α<VAR>de : DenseInducing ⇑e<VAR>f : δ →+ γ<VAR>df : DenseInducing ⇑f<VAR>φ : β →+ δ →+ G<VAR>hφ : Continuous fun p => (φ p.1) p.2<VAR>W' : Set G<VAR>W'_nhd : W' ∈ 𝓝 0<VAR>x₀ : α<VAR>y₀ : γ<VAR>ee : β × β → α × α := fun u => (e u.1, e u.2)<VAR>ff : δ × δ → γ × γ := fun u => (f u.1, f u.2)<VAR>lim_φ : Tendsto (fun p => (φ p.1) p.2) (𝓝 (0, 0)) (𝓝 0)<GOAL>∃ U ∈ comap (⇑e) (𝓝 x₀), ∃ V ∈ comap (⇑f) (𝓝 y₀), ∀ x ∈ U, ∀ x' ∈ U, ∀ y ∈ V, ∀ y' ∈ V, (fun p => (φ p.1) p.2) (x', y') - (fun p => (φ p.1) p.2) (x, y) ∈ W'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>G : Type u_5<VAR>inst✝¹⁶ : TopologicalSpace α<VAR>inst✝¹⁵ : AddCommGroup α<VAR>inst✝¹⁴ : TopologicalAddGroup α<VAR>inst✝¹³ : TopologicalSpace β<VAR>inst✝¹² : AddCommGroup β<VAR>inst✝¹¹ : TopologicalAddGroup β<VAR>inst✝¹⁰ : TopologicalSpace γ<VAR>inst✝⁹ : AddCommGroup γ<VAR>inst✝⁸ : TopologicalAddGroup γ<VAR>inst✝⁷ : TopologicalSpace δ<VAR>inst✝⁶ : AddCommGroup δ<VAR>inst✝⁵ : TopologicalAddGroup δ<VAR>inst✝⁴ : UniformSpace G<VAR>inst✝³ : AddCommGroup G<VAR>inst✝² : UniformAddGroup G<VAR>inst✝¹ : T0Space G<VAR>inst✝ : CompleteSpace G<VAR>e : β →+ α<VAR>de : DenseInducing ⇑e<VAR>f : δ →+ γ<VAR>df : DenseInducing ⇑f<VAR>φ : β →+ δ →+ G<VAR>hφ : Continuous fun p => (φ p.1) p.2<VAR>W' : Set G<VAR>W'_nhd : W' ∈ 𝓝 0<VAR>x₀ : α<VAR>y₀ : γ<VAR>ee : β × β → α × α := fun u => (e u.1, e u.2)<VAR>ff : δ × δ → γ × γ := fun u => (f u.1, f u.2)<VAR>lim_φ : Tendsto (fun p => (φ p.1) p.2) (𝓝 (0, 0)) (𝓝 0)<VAR>lim_φ_sub_sub : Tendsto (fun p => (fun p => (φ p.1) p.2) (p.1.2 - p.1.1, p.2.2 - p.2.1)) (comap ee (𝓝 (x₀, x₀)) ×ˢ comap ff (𝓝 (y₀, y₀))) (𝓝 0)<GOAL>∃ U ∈ comap (⇑e) (𝓝 x₀), ∃ V ∈ comap (⇑f) (𝓝 y₀), ∀ x ∈ U, ∀ x' ∈ U, ∀ y ∈ V, ∀ y' ∈ V, (fun p => (φ p.1) p.2) (x', y') - (fun p => (φ p.1) p.2) (x, y) ∈ W'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>G : Type u_5<VAR>inst✝¹⁶ : TopologicalSpace α<VAR>inst✝¹⁵ : AddCommGroup α<VAR>inst✝¹⁴ : TopologicalAddGroup α<VAR>inst✝¹³ : TopologicalSpace β<VAR>inst✝¹² : AddCommGroup β<VAR>inst✝¹¹ : TopologicalAddGroup β<VAR>inst✝¹⁰ : TopologicalSpace γ<VAR>inst✝⁹ : AddCommGroup γ<VAR>inst✝⁸ : TopologicalAddGroup γ<VAR>inst✝⁷ : TopologicalSpace δ<VAR>inst✝⁶ : AddCommGroup δ<VAR>inst✝⁵ : TopologicalAddGroup δ<VAR>inst✝⁴ : UniformSpace G<VAR>inst✝³ : AddCommGroup G<VAR>inst✝² : UniformAddGroup G<VAR>inst✝¹ : T0Space G<VAR>inst✝ : CompleteSpace G<VAR>e : β →+ α<VAR>de : DenseInducing ⇑e<VAR>f : δ →+ γ<VAR>df : DenseInducing ⇑f<VAR>φ : β →+ δ →+ G<VAR>hφ : Continuous fun p => (φ p.1) p.2<VAR>W' : Set G<VAR>W'_nhd : W' ∈ 𝓝 0<VAR>x₀ : α<VAR>y₀ : γ<VAR>ee : β × β → α × α := fun u => (e u.1, e u.2)<VAR>ff : δ × δ → γ × γ := fun u => (f u.1, f u.2)<VAR>lim_φ : Tendsto (fun p => (φ p.1) p.2) (𝓝 (0, 0)) (𝓝 0)<VAR>lim_φ_sub_sub : Tendsto (fun p => (fun p => (φ p.1) p.2) (p.1.2 - p.1.1, p.2.2 - p.2.1)) (comap ee (𝓝 (x₀, x₀)) ×ˢ comap ff (𝓝 (y₀, y₀))) (𝓝 0)<VAR>W : Set G<VAR>W_nhd : W ∈ 𝓝 0<VAR>W4 : ∀ {v w s t : G}, v ∈ W → w ∈ W → s ∈ W → t ∈ W → v + w + s + t ∈ W'<GOAL>∃ U ∈ comap (⇑e) (𝓝 x₀), ∃ V ∈ comap (⇑f) (𝓝 y₀), ∀ x ∈ U, ∀ x' ∈ U, ∀ y ∈ V, ∀ y' ∈ V, (fun p => (φ p.1) p.2) (x', y') - (fun p => (φ p.1) p.2) (x, y) ∈ W'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>G : Type u_5<VAR>inst✝¹⁶ : TopologicalSpace α<VAR>inst✝¹⁵ : AddCommGroup α<VAR>inst✝¹⁴ : TopologicalAddGroup α<VAR>inst✝¹³ : TopologicalSpace β<VAR>inst✝¹² : AddCommGroup β<VAR>inst✝¹¹ : TopologicalAddGroup β<VAR>inst✝¹⁰ : TopologicalSpace γ<VAR>inst✝⁹ : AddCommGroup γ<VAR>inst✝⁸ : TopologicalAddGroup γ<VAR>inst✝⁷ : TopologicalSpace δ<VAR>inst✝⁶ : AddCommGroup δ<VAR>inst✝⁵ : TopologicalAddGroup δ<VAR>inst✝⁴ : UniformSpace G<VAR>inst✝³ : AddCommGroup G<VAR>inst✝² : UniformAddGroup G<VAR>inst✝¹ : T0Space G<VAR>inst✝ : CompleteSpace G<VAR>e : β →+ α<VAR>de : DenseInducing ⇑e<VAR>f : δ →+ γ<VAR>df : DenseInducing ⇑f<VAR>φ : β →+ δ →+ G<VAR>hφ : Continuous fun p => (φ p.1) p.2<VAR>W' : Set G<VAR>W'_nhd : W' ∈ 𝓝 0<VAR>x₀ : α<VAR>y₀ : γ<VAR>ee : β × β → α × α := fun u => (e u.1, e u.2)<VAR>ff : δ × δ → γ × γ := fun u => (f u.1, f u.2)<VAR>lim_φ : Tendsto (fun p => (φ p.1) p.2) (𝓝 (0, 0)) (𝓝 0)<VAR>lim_φ_sub_sub : Tendsto (fun p => (fun p => (φ p.1) p.2) (p.1.2 - p.1.1, p.2.2 - p.2.1)) (comap ee (𝓝 (x₀, x₀)) ×ˢ comap ff (𝓝 (y₀, y₀))) (𝓝 0)<VAR>W : Set G<VAR>W_nhd : W ∈ 𝓝 0<VAR>W4 : ∀ {v w s t : G}, v ∈ W → w ∈ W → s ∈ W → t ∈ W → v + w + s + t ∈ W'<VAR>this : ∃ U₁ ∈ comap (⇑e) (𝓝 x₀), ∃ V₁ ∈ comap (⇑f) (𝓝 y₀), ∀ x ∈ U₁, ∀ x' ∈ U₁, ∀ y ∈ V₁, ∀ y' ∈ V₁, (fun p => (φ p.1) p.2) (x' - x, y' - y) ∈ W<GOAL>∃ U ∈ comap (⇑e) (𝓝 x₀), ∃ V ∈ comap (⇑f) (𝓝 y₀), ∀ x ∈ U, ∀ x' ∈ U, ∀ y ∈ V, ∀ y' ∈ V, (fun p => (φ p.1) p.2) (x', y') - (fun p => (φ p.1) p.2) (x, y) ∈ W'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>G : Type u_5<VAR>inst✝¹⁶ : TopologicalSpace α<VAR>inst✝¹⁵ : AddCommGroup α<VAR>inst✝¹⁴ : TopologicalAddGroup α<VAR>inst✝¹³ : TopologicalSpace β<VAR>inst✝¹² : AddCommGroup β<VAR>inst✝¹¹ : TopologicalAddGroup β<VAR>inst✝¹⁰ : TopologicalSpace γ<VAR>inst✝⁹ : AddCommGroup γ<VAR>inst✝⁸ : TopologicalAddGroup γ<VAR>inst✝⁷ : TopologicalSpace δ<VAR>inst✝⁶ : AddCommGroup δ<VAR>inst✝⁵ : TopologicalAddGroup δ<VAR>inst✝⁴ : UniformSpace G<VAR>inst✝³ : AddCommGroup G<VAR>inst✝² : UniformAddGroup G<VAR>inst✝¹ : T0Space G<VAR>inst✝ : CompleteSpace G<VAR>e : β →+ α<VAR>de : DenseInducing ⇑e<VAR>f : δ →+ γ<VAR>df : DenseInducing ⇑f<VAR>φ : β →+ δ →+ G<VAR>hφ : Continuous fun p => (φ p.1) p.2<VAR>W' : Set G<VAR>W'_nhd : W' ∈ 𝓝 0<VAR>x₀ : α<VAR>y₀ : γ<VAR>ee : β × β → α × α := fun u => (e u.1, e u.2)<VAR>ff : δ × δ → γ × γ := fun u => (f u.1, f u.2)<VAR>lim_φ : Tendsto (fun p => (φ p.1) p.2) (𝓝 (0, 0)) (𝓝 0)<VAR>lim_φ_sub_sub : Tendsto (fun p => (fun p => (φ p.1) p.2) (p.1.2 - p.1.1, p.2.2 - p.2.1)) (comap ee (𝓝 (x₀, x₀)) ×ˢ comap ff (𝓝 (y₀, y₀))) (𝓝 0)<VAR>W : Set G<VAR>W_nhd : W ∈ 𝓝 0<VAR>W4 : ∀ {v w s t : G}, v ∈ W → w ∈ W → s ∈ W → t ∈ W → v + w + s + t ∈ W'<VAR>U₁ : Set β<VAR>U₁_nhd : U₁ ∈ comap (⇑e) (𝓝 x₀)<VAR>V₁ : Set δ<VAR>V₁_nhd : V₁ ∈ comap (⇑f) (𝓝 y₀)<VAR>H : ∀ x ∈ U₁, ∀ x' ∈ U₁, ∀ y ∈ V₁, ∀ y' ∈ V₁, (fun p => (φ p.1) p.2) (x' - x, y' - y) ∈ W<GOAL>∃ U ∈ comap (⇑e) (𝓝 x₀), ∃ V ∈ comap (⇑f) (𝓝 y₀), ∀ x ∈ U, ∀ x' ∈ U, ∀ y ∈ V, ∀ y' ∈ V, (fun p => (φ p.1) p.2) (x', y') - (fun p => (φ p.1) p.2) (x, y) ∈ W'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>G : Type u_5<VAR>inst✝¹⁶ : TopologicalSpace α<VAR>inst✝¹⁵ : AddCommGroup α<VAR>inst✝¹⁴ : TopologicalAddGroup α<VAR>inst✝¹³ : TopologicalSpace β<VAR>inst✝¹² : AddCommGroup β<VAR>inst✝¹¹ : TopologicalAddGroup β<VAR>inst✝¹⁰ : TopologicalSpace γ<VAR>inst✝⁹ : AddCommGroup γ<VAR>inst✝⁸ : TopologicalAddGroup γ<VAR>inst✝⁷ : TopologicalSpace δ<VAR>inst✝⁶ : AddCommGroup δ<VAR>inst✝⁵ : TopologicalAddGroup δ<VAR>inst✝⁴ : UniformSpace G<VAR>inst✝³ : AddCommGroup G<VAR>inst✝² : UniformAddGroup G<VAR>inst✝¹ : T0Space G<VAR>inst✝ : CompleteSpace G<VAR>e : β →+ α<VAR>de : DenseInducing ⇑e<VAR>f : δ →+ γ<VAR>df : DenseInducing ⇑f<VAR>φ : β →+ δ →+ G<VAR>hφ : Continuous fun p => (φ p.1) p.2<VAR>W' : Set G<VAR>W'_nhd : W' ∈ 𝓝 0<VAR>x₀ : α<VAR>y₀ : γ<VAR>ee : β × β → α × α := fun u => (e u.1, e u.2)<VAR>ff : δ × δ → γ × γ := fun u => (f u.1, f u.2)<VAR>lim_φ : Tendsto (fun p => (φ p.1) p.2) (𝓝 (0, 0)) (𝓝 0)<VAR>lim_φ_sub_sub : Tendsto (fun p => (fun p => (φ p.1) p.2) (p.1.2 - p.1.1, p.2.2 - p.2.1)) (comap ee (𝓝 (x₀, x₀)) ×ˢ comap ff (𝓝 (y₀, y₀))) (𝓝 0)<VAR>W : Set G<VAR>W_nhd : W ∈ 𝓝 0<VAR>W4 : ∀ {v w s t : G}, v ∈ W → w ∈ W → s ∈ W → t ∈ W → v + w + s + t ∈ W'<VAR>U₁ : Set β<VAR>U₁_nhd : U₁ ∈ comap (⇑e) (𝓝 x₀)<VAR>V₁ : Set δ<VAR>V₁_nhd : V₁ ∈ comap (⇑f) (𝓝 y₀)<VAR>H : ∀ x ∈ U₁, ∀ x' ∈ U₁, ∀ y ∈ V₁, ∀ y' ∈ V₁, (fun p => (φ p.1) p.2) (x' - x, y' - y) ∈ W<VAR>x₁ : β<VAR>x₁_in : x₁ ∈ U₁<GOAL>∃ U ∈ comap (⇑e) (𝓝 x₀), ∃ V ∈ comap (⇑f) (𝓝 y₀), ∀ x ∈ U, ∀ x' ∈ U, ∀ y ∈ V, ∀ y' ∈ V, (fun p => (φ p.1) p.2) (x', y') - (fun p => (φ p.1) p.2) (x, y) ∈ W'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>G : Type u_5<VAR>inst✝¹⁶ : TopologicalSpace α<VAR>inst✝¹⁵ : AddCommGroup α<VAR>inst✝¹⁴ : TopologicalAddGroup α<VAR>inst✝¹³ : TopologicalSpace β<VAR>inst✝¹² : AddCommGroup β<VAR>inst✝¹¹ : TopologicalAddGroup β<VAR>inst✝¹⁰ : TopologicalSpace γ<VAR>inst✝⁹ : AddCommGroup γ<VAR>inst✝⁸ : TopologicalAddGroup γ<VAR>inst✝⁷ : TopologicalSpace δ<VAR>inst✝⁶ : AddCommGroup δ<VAR>inst✝⁵ : TopologicalAddGroup δ<VAR>inst✝⁴ : UniformSpace G<VAR>inst✝³ : AddCommGroup G<VAR>inst✝² : UniformAddGroup G<VAR>inst✝¹ : T0Space G<VAR>inst✝ : CompleteSpace G<VAR>e : β →+ α<VAR>de : DenseInducing ⇑e<VAR>f : δ →+ γ<VAR>df : DenseInducing ⇑f<VAR>φ : β →+ δ →+ G<VAR>hφ : Continuous fun p => (φ p.1) p.2<VAR>W' : Set G<VAR>W'_nhd : W' ∈ 𝓝 0<VAR>x₀ : α<VAR>y₀ : γ<VAR>ee : β × β → α × α := fun u => (e u.1, e u.2)<VAR>ff : δ × δ → γ × γ := fun u => (f u.1, f u.2)<VAR>lim_φ : Tendsto (fun p => (φ p.1) p.2) (𝓝 (0, 0)) (𝓝 0)<VAR>lim_φ_sub_sub : Tendsto (fun p => (fun p => (φ p.1) p.2) (p.1.2 - p.1.1, p.2.2 - p.2.1)) (comap ee (𝓝 (x₀, x₀)) ×ˢ comap ff (𝓝 (y₀, y₀))) (𝓝 0)<VAR>W : Set G<VAR>W_nhd : W ∈ 𝓝 0<VAR>W4 : ∀ {v w s t : G}, v ∈ W → w ∈ W → s ∈ W → t ∈ W → v + w + s + t ∈ W'<VAR>U₁ : Set β<VAR>U₁_nhd : U₁ ∈ comap (⇑e) (𝓝 x₀)<VAR>V₁ : Set δ<VAR>V₁_nhd : V₁ ∈ comap (⇑f) (𝓝 y₀)<VAR>H : ∀ x ∈ U₁, ∀ x' ∈ U₁, ∀ y ∈ V₁, ∀ y' ∈ V₁, (fun p => (φ p.1) p.2) (x' - x, y' - y) ∈ W<VAR>x₁ : β<VAR>x₁_in : x₁ ∈ U₁<VAR>y₁ : δ<VAR>y₁_in : y₁ ∈ V₁<GOAL>∃ U ∈ comap (⇑e) (𝓝 x₀), ∃ V ∈ comap (⇑f) (𝓝 y₀), ∀ x ∈ U, ∀ x' ∈ U, ∀ y ∈ V, ∀ y' ∈ V, (fun p => (φ p.1) p.2) (x', y') - (fun p => (φ p.1) p.2) (x, y) ∈ W'