ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>l l' : Filter α<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>t✝ : Set α<VAR>i : ι<VAR>p' : ι' → Prop<VAR>s' : ι' → Set α<VAR>i' : ι'<VAR>hl : l.HasBasis p s<VAR>hl' : l'.HasBasis p' s'<VAR>t : Set α<GOAL>(∃ x x_1, (p x ∧ s x ⊆ t) ∧ p' x_1 ∧ s' x_1 ⊆ t) ↔ ∃ a b, (p a ∧ p' b) ∧ s a ⊆ t ∧ s' b ⊆ t
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t K : Set X<VAR>hK : IsCompact K<VAR>l : Filter X<VAR>this : ∀ (f : Filter X), f ⊓ l = comap (fun x => (x, x)) (f ×ˢ l)<GOAL>𝓝ˢ K ⊓ l = ⨆ x ∈ K, 𝓝 x ⊓ l
<VAR>x✝ y✝ z : ℝ<VAR>n : ℕ<VAR>x : ℝ<VAR>hx : x ≠ 0<VAR>y : ℝ<GOAL>x ^ (y + 1) = x ^ y * x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁸ : AddCommGroup E<VAR>inst✝⁷ : Module ℝ E<VAR>s✝ t : Set E<VAR>x : E<VAR>a✝ : ℝ<VAR>α : Type u_4<VAR>inst✝⁶ : LinearOrderedField α<VAR>inst✝⁵ : MulActionWithZero α ℝ<VAR>inst✝⁴ : OrderedSMul α ℝ<VAR>inst✝³ : Module α E<VAR>inst✝² : SMulCommClass α ℝ ℝ<VAR>inst✝¹ : IsScalarTower α ℝ ℝ<VAR>inst✝ : IsScalarTower α ℝ E<VAR>s : Set E<VAR>symmetric : ∀ x ∈ s, -x ∈ s<VAR>a : α<GOAL>gauge (a • s) = |a|⁻¹ • gauge s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁸ : AddCommGroup E<VAR>inst✝⁷ : Module ℝ E<VAR>s✝ t : Set E<VAR>x : E<VAR>a✝ : ℝ<VAR>α : Type u_4<VAR>inst✝⁶ : LinearOrderedField α<VAR>inst✝⁵ : MulActionWithZero α ℝ<VAR>inst✝⁴ : OrderedSMul α ℝ<VAR>inst✝³ : Module α E<VAR>inst✝² : SMulCommClass α ℝ ℝ<VAR>inst✝¹ : IsScalarTower α ℝ ℝ<VAR>inst✝ : IsScalarTower α ℝ E<VAR>s : Set E<VAR>symmetric : ∀ x ∈ s, -x ∈ s<VAR>a : α<GOAL>gauge (a • s) = gauge (|a| • s)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁸ : AddCommGroup E<VAR>inst✝⁷ : Module ℝ E<VAR>s✝ t : Set E<VAR>x : E<VAR>a✝ : ℝ<VAR>α : Type u_4<VAR>inst✝⁶ : LinearOrderedField α<VAR>inst✝⁵ : MulActionWithZero α ℝ<VAR>inst✝⁴ : OrderedSMul α ℝ<VAR>inst✝³ : Module α E<VAR>inst✝² : SMulCommClass α ℝ ℝ<VAR>inst✝¹ : IsScalarTower α ℝ ℝ<VAR>inst✝ : IsScalarTower α ℝ E<VAR>s : Set E<VAR>symmetric : ∀ x ∈ s, -x ∈ s<VAR>a : α<VAR>h : |a| = a<GOAL>gauge (a • s) = gauge (|a| • s)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁸ : AddCommGroup E<VAR>inst✝⁷ : Module ℝ E<VAR>s✝ t : Set E<VAR>x : E<VAR>a✝ : ℝ<VAR>α : Type u_4<VAR>inst✝⁶ : LinearOrderedField α<VAR>inst✝⁵ : MulActionWithZero α ℝ<VAR>inst✝⁴ : OrderedSMul α ℝ<VAR>inst✝³ : Module α E<VAR>inst✝² : SMulCommClass α ℝ ℝ<VAR>inst✝¹ : IsScalarTower α ℝ ℝ<VAR>inst✝ : IsScalarTower α ℝ E<VAR>s : Set E<VAR>symmetric : ∀ x ∈ s, -x ∈ s<VAR>a : α<VAR>h : |a| = -a<GOAL>gauge (a • s) = gauge (|a| • s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t✝ : Set α<VAR>f : α → β<VAR>s : Set ι<VAR>μ : ι → Measure α<VAR>t : Set α<VAR>ht : MeasurableSet t<GOAL>((sum fun i => μ ↑i) + sum fun i => μ ↑i) t = (sum μ) t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t✝ : Set α<VAR>f : α → β<VAR>s : Set ι<VAR>μ : ι → Measure α<VAR>t : Set α<VAR>ht : MeasurableSet t<GOAL>∑' (i : ↑s), (μ ↑i) t + ∑' (i : ↑sᶜ), (μ ↑i) t = ∑' (i : ι), (μ i) t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : CommMonoid N<VAR>f✝ g✝ : α → M<VAR>a b : α<VAR>s✝ t : Set α<VAR>inst✝ : DecidableEq β<VAR>s : Finset α<VAR>f : α → M<VAR>g : α → β<GOAL>(mulSupport fun b => (filter (fun a => g a = b) s).prod f) ⊆ ↑(image g s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : CommMonoid N<VAR>f✝ g✝ : α → M<VAR>a b : α<VAR>s✝ t : Set α<VAR>inst✝ : DecidableEq β<VAR>s : Finset α<VAR>f : α → M<VAR>g : α → β<GOAL>(mulSupport fun b => (filter (fun a => g a = b) s).prod f) ⊆ g '' ↑s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : CommMonoid N<VAR>f✝ g✝ : α → M<VAR>a b✝ : α<VAR>s✝ t : Set α<VAR>inst✝ : DecidableEq β<VAR>s : Finset α<VAR>f : α → M<VAR>g : α → β<VAR>b : β<VAR>h : b ∈ mulSupport fun b => (filter (fun a => g a = b) s).prod f<GOAL>b ∈ g '' ↑s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : CommMonoid N<VAR>f✝ g✝ : α → M<VAR>a b✝ : α<VAR>s✝ t : Set α<VAR>inst✝ : DecidableEq β<VAR>s : Finset α<VAR>f : α → M<VAR>g : α → β<VAR>b : β<VAR>h : b ∈ mulSupport fun b => (filter (fun a => g a = b) s).prod f<GOAL>(filter (fun a => g a = b) s).Nonempty
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : Ring A<VAR>inst✝² : Ring B<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>c₁ c₂ : R<VAR>q : Basis A c₁ c₂<GOAL>q.k * q.k = -((c₁ * c₂) • 1)
<VAR>X✝ Y : Scheme<VAR>f✝ : X✝ ⟶ Y<VAR>Z X : Scheme<VAR>U : X.Opens<VAR>hU : IsCompact U.carrier<VAR>x f : ↑Γ(X, U)<VAR>H : (x |_ X.basicOpen f) ⋯ = 0<GOAL>∃ n, f ^ n * x = 0
<VAR>X✝ Y : Scheme<VAR>f✝ : X✝ ⟶ Y<VAR>Z X : Scheme<VAR>U : X.Opens<VAR>hU : IsCompact U.carrier<VAR>x f : ↑Γ(X, U)<VAR>H : (x |_ X.basicOpen f) ⋯ = 0<VAR>s : Set ↑X.affineOpens<VAR>hs : s.Finite<VAR>e : U.carrier = ⋃ i ∈ s, ↑↑i<GOAL>∃ n, f ^ n * x = 0
<VAR>X✝ Y : Scheme<VAR>f✝ : X✝ ⟶ Y<VAR>Z X : Scheme<VAR>U : X.Opens<VAR>hU : IsCompact U.carrier<VAR>x f : ↑Γ(X, U)<VAR>H : (x |_ X.basicOpen f) ⋯ = 0<VAR>s : Set ↑X.affineOpens<VAR>hs : s.Finite<VAR>e : U = ⨆ i, ↑↑i<GOAL>∃ n, f ^ n * x = 0
<VAR>X✝ Y : Scheme<VAR>f✝ : X✝ ⟶ Y<VAR>Z X : Scheme<VAR>U : X.Opens<VAR>hU : IsCompact U.carrier<VAR>x f : ↑Γ(X, U)<VAR>H : (x |_ X.basicOpen f) ⋯ = 0<VAR>s : Set ↑X.affineOpens<VAR>hs : s.Finite<VAR>e : U = ⨆ i, ↑↑i<VAR>h₁ : ∀ (i : ↑s), ↑↑i ≤ U<GOAL>∃ n, f ^ n * x = 0
<VAR>X✝ Y : Scheme<VAR>f✝ : X✝ ⟶ Y<VAR>Z X : Scheme<VAR>U : X.Opens<VAR>hU : IsCompact U.carrier<VAR>x f : ↑Γ(X, U)<VAR>H : (x |_ X.basicOpen f) ⋯ = 0<VAR>s : Set ↑X.affineOpens<VAR>hs : s.Finite<VAR>e : U = ⨆ i, ↑↑i<VAR>h₁ : ∀ (i : ↑s), ↑↑i ≤ U<VAR>H' : ∀ (i : ↑s), ∃ n, (X.presheaf.map (homOfLE ⋯).op) f ^ n * (X.presheaf.map (homOfLE ⋯).op) x = 0<GOAL>∃ n, f ^ n * x = 0
<VAR>X✝ Y : Scheme<VAR>f✝ : X✝ ⟶ Y<VAR>Z X : Scheme<VAR>U : X.Opens<VAR>hU : IsCompact U.carrier<VAR>x f : ↑Γ(X, U)<VAR>H : (x |_ X.basicOpen f) ⋯ = 0<VAR>s : Set ↑X.affineOpens<VAR>hs : s.Finite<VAR>e : U = ⨆ i, ↑↑i<VAR>h₁ : ∀ (i : ↑s), ↑↑i ≤ U<VAR>i : ↑s<GOAL>((X.presheaf.map (homOfLE ⋯).op) x |_ X.basicOpen ((X.presheaf.map (homOfLE ⋯).op) f)) ⋯ = 0
<VAR>X✝ Y : Scheme<VAR>f✝ : X✝ ⟶ Y<VAR>Z X : Scheme<VAR>U : X.Opens<VAR>hU : IsCompact U.carrier<VAR>x f : ↑Γ(X, U)<VAR>H : (x |_ X.basicOpen f) ⋯ = 0<VAR>s : Set ↑X.affineOpens<VAR>hs : s.Finite<VAR>e : U = ⨆ i, ↑↑i<VAR>h₁ : ∀ (i : ↑s), ↑↑i ≤ U<VAR>n : ↑s → ℕ<VAR>hn : ∀ (i : ↑s), (X.presheaf.map (homOfLE ⋯).op) f ^ n i * (X.presheaf.map (homOfLE ⋯).op) x = 0<GOAL>∃ n, f ^ n * x = 0
<VAR>X✝ Y : Scheme<VAR>f✝ : X✝ ⟶ Y<VAR>Z X : Scheme<VAR>U : X.Opens<VAR>hU : IsCompact U.carrier<VAR>x f : ↑Γ(X, U)<VAR>H : (x |_ X.basicOpen f) ⋯ = 0<VAR>s : Set ↑X.affineOpens<VAR>hs : s.Finite<VAR>e : U = ⨆ i, ↑↑i<VAR>h₁ : ∀ (i : ↑s), ↑↑i ≤ U<VAR>n : ↑s → ℕ<VAR>hn : ∀ (i : ↑s), (X.presheaf.map (homOfLE ⋯).op) f ^ n i * (X.presheaf.map (homOfLE ⋯).op) x = 0<VAR>this : Finite ↑s<GOAL>∃ n, f ^ n * x = 0
<VAR>X✝ Y : Scheme<VAR>f✝ : X✝ ⟶ Y<VAR>Z X : Scheme<VAR>U : X.Opens<VAR>hU : IsCompact U.carrier<VAR>x f : ↑Γ(X, U)<VAR>H : (x |_ X.basicOpen f) ⋯ = 0<VAR>s : Set ↑X.affineOpens<VAR>hs : s.Finite<VAR>e : U = ⨆ i, ↑↑i<VAR>h₁ : ∀ (i : ↑s), ↑↑i ≤ U<VAR>n : ↑s → ℕ<VAR>hn : ∀ (i : ↑s), (X.presheaf.map (homOfLE ⋯).op) f ^ n i * (X.presheaf.map (homOfLE ⋯).op) x = 0<VAR>this : Finite ↑s<VAR>val✝ : Fintype ↑s<GOAL>∃ n, f ^ n * x = 0
<VAR>X✝ Y : Scheme<VAR>f✝ : X✝ ⟶ Y<VAR>Z X : Scheme<VAR>U : X.Opens<VAR>hU : IsCompact U.carrier<VAR>x f : ↑Γ(X, U)<VAR>H : (x |_ X.basicOpen f) ⋯ = 0<VAR>s : Set ↑X.affineOpens<VAR>hs : s.Finite<VAR>e : U = ⨆ i, ↑↑i<VAR>h₁ : ∀ (i : ↑s), ↑↑i ≤ U<VAR>n : ↑s → ℕ<VAR>hn : ∀ (i : ↑s), (X.presheaf.map (homOfLE ⋯).op) f ^ n i * (X.presheaf.map (homOfLE ⋯).op) x = 0<VAR>this : Finite ↑s<VAR>val✝ : Fintype ↑s<GOAL>f ^ Finset.univ.sup n * x = 0
<VAR>X✝ Y : Scheme<VAR>f✝ : X✝ ⟶ Y<VAR>Z X : Scheme<VAR>U : X.Opens<VAR>hU : IsCompact U.carrier<VAR>x f : ↑Γ(X, U)<VAR>H : (x |_ X.basicOpen f) ⋯ = 0<VAR>s : Set ↑X.affineOpens<VAR>hs : s.Finite<VAR>e : U = ⨆ i, ↑↑i<VAR>h₁ : ∀ (i : ↑s), ↑↑i ≤ U<VAR>n : ↑s → ℕ<VAR>hn : ∀ (i : ↑s), (X.presheaf.map (homOfLE ⋯).op) f ^ n i * (X.presheaf.map (homOfLE ⋯).op) x = 0<VAR>this : Finite ↑s<VAR>val✝ : Fintype ↑s<GOAL>∀ (i : ↑s), (X.presheaf.map (homOfLE ⋯).op) (f ^ Finset.univ.sup n * x) = 0
<VAR>X✝ Y : Scheme<VAR>f✝ : X✝ ⟶ Y<VAR>Z X : Scheme<VAR>U : X.Opens<VAR>hU : IsCompact U.carrier<VAR>x f : ↑Γ(X, U)<VAR>H : (x |_ X.basicOpen f) ⋯ = 0<VAR>s : Set ↑X.affineOpens<VAR>hs : s.Finite<VAR>e : U = ⨆ i, ↑↑i<VAR>h₁ : ∀ (i : ↑s), ↑↑i ≤ U<VAR>n : ↑s → ℕ<VAR>this : Finite ↑s<VAR>val✝ : Fintype ↑s<VAR>i : ↑s<VAR>hn : (X.presheaf.map (homOfLE ⋯).op) (f ^ (Finset.univ.sup n - n i)) * ((X.presheaf.map (homOfLE ⋯).op) f ^ n i * (X.presheaf.map (homOfLE ⋯).op) x) = (X.presheaf.map (homOfLE ⋯).op) (f ^ (Finset.univ.sup n - n i)) * 0<GOAL>(X.presheaf.map (homOfLE ⋯).op) (f ^ Finset.univ.sup n * x) = 0
<VAR>X✝ Y : Scheme<VAR>f✝ : X✝ ⟶ Y<VAR>Z X : Scheme<VAR>U : X.Opens<VAR>hU : IsCompact U.carrier<VAR>x f : ↑Γ(X, U)<VAR>H : (x |_ X.basicOpen f) ⋯ = 0<VAR>s : Set ↑X.affineOpens<VAR>hs : s.Finite<VAR>e : U = ⨆ i, ↑↑i<VAR>h₁ : ∀ (i : ↑s), ↑↑i ≤ U<VAR>n : ↑s → ℕ<VAR>this : Finite ↑s<VAR>val✝ : Fintype ↑s<VAR>i : ↑s<VAR>hn : (X.presheaf.map (homOfLE ⋯).op) (f ^ (Finset.univ.sup n - n i) * (f ^ n i * x)) = (X.presheaf.map (homOfLE ⋯).op) (f ^ (Finset.univ.sup n - n i)) * 0<GOAL>(X.presheaf.map (homOfLE ⋯).op) (f ^ Finset.univ.sup n * x) = 0
<VAR>X✝ Y : Scheme<VAR>f✝ : X✝ ⟶ Y<VAR>Z X : Scheme<VAR>U : X.Opens<VAR>hU : IsCompact U.carrier<VAR>x f : ↑Γ(X, U)<VAR>H : (x |_ X.basicOpen f) ⋯ = 0<VAR>s : Set ↑X.affineOpens<VAR>hs : s.Finite<VAR>e : U = ⨆ i, ↑↑i<VAR>h₁ : ∀ (i : ↑s), ↑↑i ≤ U<VAR>n : ↑s → ℕ<VAR>this : Finite ↑s<VAR>val✝ : Fintype ↑s<VAR>i : ↑s<VAR>hn : (X.presheaf.map (homOfLE ⋯).op) (f ^ (Finset.univ.sup n - n i + n i) * x) = 0<GOAL>n i ≤ Finset.univ.sup n
<VAR>x y : ℤ[i]<VAR>hy : y ≠ 0<GOAL>toComplex y ≠ 0
<VAR>x y : ℤ[i]<VAR>hy : y ≠ 0<VAR>this : toComplex y ≠ 0<GOAL>↑(norm (x % y)) = normSq (toComplex x - toComplex y * toComplex (x / y))
<VAR>x y : ℤ[i]<VAR>hy : y ≠ 0<VAR>this : toComplex y ≠ 0<GOAL>normSq (toComplex x - toComplex y * toComplex (x / y)) = normSq (toComplex y) * normSq (toComplex x / toComplex y - toComplex (x / y))
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>s✝ t : Set α<VAR>inst✝¹ : Nonempty α<VAR>inst✝ : LinearOrder β<VAR>s : Set α<VAR>f : α → β<VAR>h : s.Finite<GOAL>∃ a, ∀ b ∈ s, f a ≤ f b
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>s t : Set α<VAR>inst✝¹ : Nonempty α<VAR>inst✝ : LinearOrder β<VAR>f : α → β<VAR>h : ∅.Finite<GOAL>∃ a, ∀ b ∈ ∅, f a ≤ f b
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>s✝ t : Set α<VAR>inst✝¹ : Nonempty α<VAR>inst✝ : LinearOrder β<VAR>s : Set α<VAR>f : α → β<VAR>h : s.Finite<VAR>hs : s.Nonempty<GOAL>∃ a, ∀ b ∈ s, f a ≤ f b
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedSemifield α<VAR>a b c d e : α<VAR>m n : ℤ<VAR>h : 0 < b<GOAL>a * b⁻¹ < c ↔ a < c * b
<VAR>c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>a b : ℕ<VAR>h : n * a < n * b + n<GOAL>n * a ≤ n * b
<VAR>c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>a b : ℕ<VAR>h : n * a < n * b.succ<GOAL>n * a ≤ n * b
<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>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>s : Set H<VAR>x : H<VAR>u : Set H<VAR>f : H → H'<VAR>u_open : IsOpen u<VAR>xu : x ∈ u<GOAL>DifferentiableWithinAtProp I I' f s x ↔ DifferentiableWithinAtProp I I' f (s ∩ u) x
<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>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>s : Set H<VAR>x : H<VAR>u : Set H<VAR>f : H → H'<VAR>u_open : IsOpen u<VAR>xu : x ∈ u<VAR>this : ↑I.symm ⁻¹' (s ∩ u) ∩ range ↑I = ↑I.symm ⁻¹' s ∩ range ↑I ∩ ↑I.symm ⁻¹' u<GOAL>DifferentiableWithinAtProp I I' f s x ↔ DifferentiableWithinAtProp I I' f (s ∩ u) x
<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>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>s : Set H<VAR>x : H<VAR>u : Set H<VAR>f : H → H'<VAR>u_open : IsOpen u<VAR>xu : x ∈ u<VAR>this : ↑I.symm ⁻¹' (s ∩ u) ∩ range ↑I = ↑I.symm ⁻¹' s ∩ range ↑I ∩ ↑I.symm ⁻¹' u<GOAL>DifferentiableWithinAt 𝕜 (↑I' ∘ f ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ range ↑I ∩ ↑I.symm ⁻¹' u) (↑I x) ↔ DifferentiableWithinAt 𝕜 (↑I' ∘ f ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ range ↑I) (↑I x)
<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>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>s : Set H<VAR>x : H<VAR>u : Set H<VAR>f : H → H'<VAR>u_open : IsOpen u<VAR>xu : x ∈ u<VAR>this : ↑I.symm ⁻¹' (s ∩ u) ∩ range ↑I = ↑I.symm ⁻¹' s ∩ range ↑I ∩ ↑I.symm ⁻¹' u<GOAL>↑I.symm ⁻¹' u ∈ 𝓝 (↑I x)
<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>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>s : Set H<VAR>x : H<VAR>u : Set H<VAR>f : H → H'<VAR>u_open : IsOpen u<VAR>xu : x ∈ u<VAR>this✝ : ↑I.symm ⁻¹' (s ∩ u) ∩ range ↑I = ↑I.symm ⁻¹' s ∩ range ↑I ∩ ↑I.symm ⁻¹' u<VAR>this : u ∈ 𝓝 (↑I.symm (↑I x))<GOAL>↑I.symm ⁻¹' u ∈ 𝓝 (↑I x)
<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>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>s : Set H<VAR>x : H<VAR>f : H → H'<VAR>e : PartialHomeomorph H H<VAR>he : e ∈ contDiffGroupoid ⊤ I<VAR>hx : x ∈ e.source<VAR>h : DifferentiableWithinAt 𝕜 (↑I' ∘ f ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ range ↑I) ((↑I ∘ ↑e.symm ∘ ↑I.symm) (↑I (↑e x)))<VAR>this✝ : ↑I x = (↑I ∘ ↑e.symm ∘ ↑I.symm) (↑I (↑e x))<VAR>this : ↑I (↑e x) ∈ ↑I.symm ⁻¹' e.target ∩ range ↑I<GOAL>DifferentiableWithinAt 𝕜 (↑I' ∘ (f ∘ ↑e.symm) ∘ ↑I.symm) (↑I.symm ⁻¹' (↑e.symm ⁻¹' s) ∩ range ↑I) (↑I (↑e x))
<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>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>s : Set H<VAR>x : H<VAR>f : H → H'<VAR>e : PartialHomeomorph H H<VAR>he : e ∈ contDiffGroupoid ⊤ I<VAR>hx : x ∈ e.source<VAR>h : DifferentiableWithinAt 𝕜 (↑I' ∘ f ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ range ↑I) ((↑I ∘ ↑e.symm ∘ ↑I.symm) (↑I (↑e x)))<VAR>this✝¹ : ↑I x = (↑I ∘ ↑e.symm ∘ ↑I.symm) (↑I (↑e x))<VAR>this✝ : ↑I (↑e x) ∈ ↑I.symm ⁻¹' e.target ∩ range ↑I<VAR>this : ContDiffWithinAt 𝕜 ⊤ (↑I ∘ ↑e.symm ∘ ↑I.symm) (↑I.symm ⁻¹' e.target ∩ range ↑I) (↑I (↑e x))<GOAL>DifferentiableWithinAt 𝕜 (↑I' ∘ (f ∘ ↑e.symm) ∘ ↑I.symm) (↑I.symm ⁻¹' (↑e.symm ⁻¹' s) ∩ range ↑I) (↑I (↑e x))
<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>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>s : Set H<VAR>x : H<VAR>f : H → H'<VAR>e : PartialHomeomorph H H<VAR>he : e ∈ contDiffGroupoid ⊤ I<VAR>hx : x ∈ e.source<VAR>h : DifferentiableWithinAt 𝕜 (↑I' ∘ f ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ range ↑I) ((↑I ∘ ↑e.symm ∘ ↑I.symm) (↑I (↑e x)))<VAR>this✝¹ : ↑I x = (↑I ∘ ↑e.symm ∘ ↑I.symm) (↑I (↑e x))<VAR>this✝ : ↑I (↑e x) ∈ ↑I.symm ⁻¹' e.target ∩ range ↑I<VAR>this : ContDiffWithinAt 𝕜 ⊤ (↑I ∘ ↑e.symm ∘ ↑I.symm) (↑I.symm ⁻¹' e.target ∩ range ↑I) (↑I (↑e x))<GOAL>↑I' ∘ (f ∘ ↑e.symm) ∘ ↑I.symm = (↑I' ∘ f ∘ ↑I.symm) ∘ ↑I ∘ ↑e.symm ∘ ↑I.symm
<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>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>s : Set H<VAR>x : H<VAR>f : H → H'<VAR>e : PartialHomeomorph H H<VAR>he : e ∈ contDiffGroupoid ⊤ I<VAR>hx : x ∈ e.source<VAR>h : DifferentiableWithinAt 𝕜 (↑I' ∘ f ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ range ↑I) ((↑I ∘ ↑e.symm ∘ ↑I.symm) (↑I (↑e x)))<VAR>this✝¹ : ↑I x = (↑I ∘ ↑e.symm ∘ ↑I.symm) (↑I (↑e x))<VAR>this✝ : ↑I (↑e x) ∈ ↑I.symm ⁻¹' e.target ∩ range ↑I<VAR>this : ContDiffWithinAt 𝕜 ⊤ (↑I ∘ ↑e.symm ∘ ↑I.symm) (↑I.symm ⁻¹' e.target ∩ range ↑I) (↑I (↑e x))<GOAL>↑I.symm ⁻¹' e.target ∩ range ↑I ∩ ↑I ∘ ↑e.symm ∘ ↑I.symm ⁻¹' (↑I.symm ⁻¹' s ∩ range ↑I) ∈ 𝓝[↑I.symm ⁻¹' (↑e.symm ⁻¹' s) ∩ range ↑I] ↑I (↑e x)
<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>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>s : Set H<VAR>x : H<VAR>f : H → H'<VAR>e : PartialHomeomorph H H<VAR>he : e ∈ contDiffGroupoid ⊤ I<VAR>hx : x ∈ e.source<VAR>h : DifferentiableWithinAt 𝕜 (↑I' ∘ f ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ range ↑I) ((↑I ∘ ↑e.symm ∘ ↑I.symm) (↑I (↑e x)))<VAR>this✝¹ : ↑I x = (↑I ∘ ↑e.symm ∘ ↑I.symm) (↑I (↑e x))<VAR>this✝ : ↑I (↑e x) ∈ ↑I.symm ⁻¹' e.target ∩ range ↑I<VAR>this : ContDiffWithinAt 𝕜 ⊤ (↑I ∘ ↑e.symm ∘ ↑I.symm) (↑I.symm ⁻¹' e.target ∩ range ↑I) (↑I (↑e x))<GOAL>↑I.symm ⁻¹' e.target ∩ (↑I.symm ⁻¹' (↑e.symm ⁻¹' s) ∩ range ↑I) ⊆ ↑I.symm ⁻¹' e.target ∩ range ↑I ∩ ↑I ∘ ↑e.symm ∘ ↑I.symm ⁻¹' (↑I.symm ⁻¹' s ∩ range ↑I)
<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>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>s : Set H<VAR>x : H<VAR>f g : H → H'<VAR>h : ∀ y ∈ s, f y = g y<VAR>hx : f x = g x<VAR>hf : DifferentiableWithinAtProp I I' f s x<GOAL>DifferentiableWithinAtProp I I' g s x
<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>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>s : Set H<VAR>x : H<VAR>f g : H → H'<VAR>h : ∀ y ∈ s, f y = g y<VAR>hx : f x = g x<VAR>hf : DifferentiableWithinAtProp I I' f s x<GOAL>∀ x ∈ ↑I.symm ⁻¹' s ∩ range ↑I, (↑I' ∘ g ∘ ↑I.symm) x = (↑I' ∘ f ∘ ↑I.symm) x
<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>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>s : Set H<VAR>x : H<VAR>f g : H → H'<VAR>h : ∀ y ∈ s, f y = g y<VAR>hx : f x = g x<VAR>hf : DifferentiableWithinAtProp I I' f s x<GOAL>(↑I' ∘ g ∘ ↑I.symm) (↑I x) = (↑I' ∘ f ∘ ↑I.symm) (↑I x)