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>f : ι → α<VAR>s t : Set α<VAR>h : Unique ι<VAR>x : α<GOAL>x ∈ range f ↔ x ∈ {f default}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>f : ι → α<VAR>s t : Set α<VAR>h : Unique ι<VAR>x : α<GOAL>(∃ y, f y = x) ↔ x ∈ {f default}
<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>f g : Filter α<GOAL>(f ⊓ g).NeBot ↔ ∀ {p : α → Prop}, (∀ᶠ (x : α) in f, p x) → ∃ᶠ (x : α) in g, p x
<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>f g : Filter α<GOAL>(∀ ⦃s : Set α⦄, s ∈ f → ∀ ⦃s' : Set α⦄, s' ∈ g → (s ∩ s').Nonempty) ↔ ∀ {p : α → Prop}, (∀ᶠ (x : α) in f, p x) → ∀ {U : Set α}, U ∈ g → ∃ x, p x ∧ x ∈ U
<VAR>X : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : NormedField 𝕜<VAR>inst✝³ : NormedDivisionRing R<VAR>inst✝² : Algebra 𝕜 R<VAR>inst✝¹ : CompleteSpace R<VAR>inst✝ : CompleteSpace 𝕜<VAR>f : C(X, 𝕜)<GOAL>spectrum 𝕜 f = Set.range ⇑f
<VAR>X : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : NormedField 𝕜<VAR>inst✝³ : NormedDivisionRing R<VAR>inst✝² : Algebra 𝕜 R<VAR>inst✝¹ : CompleteSpace R<VAR>inst✝ : CompleteSpace 𝕜<VAR>f : C(X, 𝕜)<GOAL>⇑(RingHom.id 𝕜) ⁻¹' Set.range ⇑f = Set.range ⇑f
<VAR>E : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>H : Type u_2<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>γ γ' : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>s s' : Set ℝ<VAR>t₀ : ℝ<VAR>hγ : IsIntegralCurveOn γ v s<VAR>t : ℝ<VAR>ht : t ∈ s<VAR>hsrc : γ t ∈ (extChartAt I (γ t₀)).source<GOAL>HasDerivAt (↑(extChartAt I (γ t₀)) ∘ γ) ((tangentCoordChange I (γ t) (γ t₀) (γ t)) (v (γ t))) t
<VAR>E : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>H : Type u_2<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>γ γ' : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>s s' : Set ℝ<VAR>t₀ : ℝ<VAR>hγ : IsIntegralCurveOn γ v s<VAR>t : ℝ<VAR>ht : t ∈ s<VAR>hsrc✝ : γ t ∈ (extChartAt I (γ t₀)).source<VAR>hsrc : γ t ∈ (chartAt H (γ t₀)).source<GOAL>HasDerivAt (↑(extChartAt I (γ t₀)) ∘ γ) ((tangentCoordChange I (γ t) (γ t₀) (γ t)) (v (γ t))) t
<VAR>E : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>H : Type u_2<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>γ γ' : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>s s' : Set ℝ<VAR>t₀ : ℝ<VAR>hγ : IsIntegralCurveOn γ v s<VAR>t : ℝ<VAR>ht : t ∈ s<VAR>hsrc✝ : γ t ∈ (extChartAt I (γ t₀)).source<VAR>hsrc : γ t ∈ (chartAt H (γ t₀)).source<GOAL>HasMFDerivAt 𝓘(ℝ, ℝ) 𝓘(ℝ, E) (↑(extChartAt I (γ t₀)) ∘ γ) t (ContinuousLinearMap.smulRight 1 ((tangentCoordChange I (γ t) (γ t₀) (γ t)) (v (γ t))))
<VAR>E : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>H : Type u_2<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>γ γ' : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>s s' : Set ℝ<VAR>t₀ : ℝ<VAR>hγ : IsIntegralCurveOn γ v s<VAR>t : ℝ<VAR>ht : t ∈ s<VAR>hsrc✝ : γ t ∈ (extChartAt I (γ t₀)).source<VAR>hsrc : γ t ∈ (chartAt H (γ t₀)).source<GOAL>(mfderiv I I (↑(chartAt H (γ t₀))) (γ t)).comp (ContinuousLinearMap.smulRight 1 (v (γ t))) = ContinuousLinearMap.smulRight 1 ((tangentCoordChange I (γ t) (γ t₀) (γ t)) (v (γ t)))
<VAR>E : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>H : Type u_2<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>γ γ' : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>s s' : Set ℝ<VAR>t₀ : ℝ<VAR>hγ : IsIntegralCurveOn γ v s<VAR>t : ℝ<VAR>ht : t ∈ s<VAR>hsrc✝ : γ t ∈ (extChartAt I (γ t₀)).source<VAR>hsrc : γ t ∈ (chartAt H (γ t₀)).source<GOAL>∀ (x : TangentSpace 𝓘(ℝ, ℝ) t), ((mfderiv I I (↑(chartAt H (γ t₀))) (γ t)).comp (ContinuousLinearMap.smulRight 1 (v (γ t)))) x = (ContinuousLinearMap.smulRight 1 ((tangentCoordChange I (γ t) (γ t₀) (γ t)) (v (γ t)))) x
<VAR>E : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>H : Type u_2<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>γ γ' : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>s s' : Set ℝ<VAR>t₀ : ℝ<VAR>hγ : IsIntegralCurveOn γ v s<VAR>t : ℝ<VAR>ht : t ∈ s<VAR>hsrc✝ : γ t ∈ (extChartAt I (γ t₀)).source<VAR>hsrc : γ t ∈ (chartAt H (γ t₀)).source<VAR>a : TangentSpace 𝓘(ℝ, ℝ) t<GOAL>((mfderiv I I (↑(chartAt H (γ t₀))) (γ t)).comp (ContinuousLinearMap.smulRight 1 (v (γ t)))) a = (ContinuousLinearMap.smulRight 1 ((tangentCoordChange I (γ t) (γ t₀) (γ t)) (v (γ t)))) a
<VAR>E : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>H : Type u_2<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>γ γ' : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>s s' : Set ℝ<VAR>t₀ : ℝ<VAR>hγ : IsIntegralCurveOn γ v s<VAR>t : ℝ<VAR>ht : t ∈ s<VAR>hsrc✝ : γ t ∈ (extChartAt I (γ t₀)).source<VAR>hsrc : γ t ∈ (chartAt H (γ t₀)).source<VAR>a : TangentSpace 𝓘(ℝ, ℝ) t<GOAL>(ContinuousLinearMap.smulRight 1 ((tangentCoordChange I (γ t) (γ t₀) (γ t)) (v (γ t)))) (1 a) = (ContinuousLinearMap.smulRight 1 ((tangentCoordChange I (γ t) (γ t₀) (γ t)) (v (γ t)))) (1 a)
<VAR>𝕜 : Type u_1<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝² : NormedAddCommGroup G'<VAR>inst✝¹ : NormedSpace 𝕜 G'<VAR>ε : ℝ<VAR>inst✝ : CompleteSpace E<VAR>f : E → F<VAR>f' : E ≃L[𝕜] F<VAR>s : Set E<VAR>c : ℝ≥0<VAR>hf : ApproximatesLinearOn f (↑f') s c<VAR>hc : c < ‖↑f'.symm‖₊⁻¹<GOAL>AntilipschitzWith (‖↑f'.symm‖₊⁻¹ - c)⁻¹ (s.restrict f)
<VAR>𝕜 : Type u_1<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝² : NormedAddCommGroup G'<VAR>inst✝¹ : NormedSpace 𝕜 G'<VAR>ε : ℝ<VAR>inst✝ : CompleteSpace E<VAR>f : E → F<VAR>f' : E ≃L[𝕜] F<VAR>s : Set E<VAR>c : ℝ≥0<VAR>hf : ApproximatesLinearOn f (↑f') s c<VAR>hc : c < ‖↑f'.symm‖₊⁻¹<VAR>x✝ : ↑s<GOAL>s.restrict f x✝ = s.restrict (⇑f') x✝ + (f ↑x✝ - ↑f' ↑x✝)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>N N₁ N₂ P P₁ P₂ : Submodule R M<GOAL>⊥.colon N = N.annihilator
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : NormedSpace ℝ E<VAR>x y z : E<VAR>δ ε : ℝ<VAR>hδ : 0 ≤ δ<VAR>hε : 0 ≤ ε<VAR>h : dist x z ≤ ε + δ<VAR>hε' : 0 < ε<VAR>hεδ : 0 < ε + δ<GOAL>∃ y, dist x y ≤ δ ∧ dist y z ≤ ε
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : NormedSpace ℝ E<VAR>x y✝ z : E<VAR>δ ε : ℝ<VAR>hδ : 0 ≤ δ<VAR>hε : 0 ≤ ε<VAR>h : dist x z ≤ ε + δ<VAR>hε' : 0 < ε<VAR>hεδ : 0 < ε + δ<VAR>y : E<VAR>hy : dist x y = δ / (ε + δ) * dist x z ∧ dist y z = ε / (ε + δ) * dist x z<GOAL>dist x y ≤ δ ∧ dist y z ≤ ε
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : NormedSpace ℝ E<VAR>x y✝ z : E<VAR>δ ε : ℝ<VAR>hδ : 0 ≤ δ<VAR>hε : 0 ≤ ε<VAR>h : dist x z ≤ ε + δ<VAR>hε' : 0 < ε<VAR>hεδ : 0 < ε + δ<VAR>y : E<VAR>hy : dist x y = δ / (ε + δ) * dist x z ∧ dist y z = ε / (ε + δ) * dist x z<GOAL>dist x z / (ε + δ) * δ ≤ δ ∧ dist x z / (ε + δ) * ε ≤ ε
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : NormedSpace ℝ E<VAR>x y✝ z : E<VAR>δ ε : ℝ<VAR>hδ : 0 ≤ δ<VAR>hε : 0 ≤ ε<VAR>h : dist x z / (ε + δ) ≤ 1<VAR>hε' : 0 < ε<VAR>hεδ : 0 < ε + δ<VAR>y : E<VAR>hy : dist x y = δ / (ε + δ) * dist x z ∧ dist y z = ε / (ε + δ) * dist x z<GOAL>dist x z / (ε + δ) * δ ≤ δ ∧ dist x z / (ε + δ) * ε ≤ ε
<VAR>Δ Δ' Δ'' : SimplexCategory<VAR>φ : Δ ⟶ Δ''<VAR>e : Δ ⟶ Δ'<VAR>inst✝¹ : Epi e<VAR>i : Δ' ⟶ Δ''<VAR>inst✝ : Mono i<VAR>fac : e ≫ i = φ<GOAL>image φ = Δ'
<VAR>Δ Δ' Δ'' : SimplexCategory<VAR>φ : Δ ⟶ Δ''<VAR>e : Δ ⟶ Δ'<VAR>inst✝¹ : Epi e<VAR>i : Δ' ⟶ Δ''<VAR>inst✝ : Mono i<VAR>fac : e ≫ i = φ<VAR>this : StrongEpi e<GOAL>image φ = Δ'
<VAR>Δ Δ' Δ'' : SimplexCategory<VAR>φ : Δ ⟶ Δ''<VAR>e✝ : Δ ⟶ Δ'<VAR>inst✝¹ : Epi e✝<VAR>i : Δ' ⟶ Δ''<VAR>inst✝ : Mono i<VAR>fac : e✝ ≫ i = φ<VAR>this : StrongEpi e✝<VAR>e : Δ' ≅ image φ := image.isoStrongEpiMono e✝ i fac<GOAL>(image φ).len = Δ'.len
<VAR>m n : ℕ<VAR>h : m ≤ n<GOAL>(n - m).gcd n = m.gcd n
<VAR>m n : ℕ<VAR>h : m ≤ n<VAR>this : n - m + m = n<GOAL>(n - m).gcd n = m.gcd n
<VAR>m n : ℕ<VAR>h : m ≤ n<VAR>this : n - m + m = n<GOAL>(n - m + m - m).gcd (n - m + m) = (n - m).gcd m
<VAR>m n : ℕ<VAR>h : m ≤ n<VAR>this✝ : n - m + m = n<VAR>this : (n - m).gcd n = (n - m).gcd m<GOAL>(n - m + m - m).gcd (n - m + m) = (n - m).gcd m
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>inst✝⁴ : DivisionRing K<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module K V<VAR>inst✝ : Module K V'<VAR>v : ι → V<VAR>s t : Set V<VAR>x✝ y z : V<VAR>hs : LinearIndependent (ι := { x // x ∈ s }) K Subtype.val<VAR>hst : s ⊆ t<VAR>b : Set V<VAR>bt : b ⊆ t<VAR>bi : LinearIndependent (ι := { x // x ∈ b }) K Subtype.val<VAR>sb : s ⊆ b<VAR>h : ∀ a ∈ {b | b ⊆ t ∧ LinearIndependent (ι := { x // x ∈ b }) K Subtype.val}, b ⊆ a → a = b<VAR>x : V<VAR>xt : x ∈ t<GOAL>x ∈ ↑(span K b)
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>inst✝⁴ : DivisionRing K<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module K V<VAR>inst✝ : Module K V'<VAR>v : ι → V<VAR>s t : Set V<VAR>x✝ y z : V<VAR>hs : LinearIndependent (ι := { x // x ∈ s }) K Subtype.val<VAR>hst : s ⊆ t<VAR>b : Set V<VAR>bt : b ⊆ t<VAR>bi : LinearIndependent (ι := { x // x ∈ b }) K Subtype.val<VAR>sb : s ⊆ b<VAR>h : ∀ a ∈ {b | b ⊆ t ∧ LinearIndependent (ι := { x // x ∈ b }) K Subtype.val}, b ⊆ a → a = b<VAR>x : V<VAR>xt : x ∈ t<VAR>hn : x ∉ ↑(span K b)<GOAL>False
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>inst✝⁴ : DivisionRing K<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module K V<VAR>inst✝ : Module K V'<VAR>v : ι → V<VAR>s t : Set V<VAR>x✝ y z : V<VAR>hs : LinearIndependent (ι := { x // x ∈ s }) K Subtype.val<VAR>hst : s ⊆ t<VAR>b : Set V<VAR>bt : b ⊆ t<VAR>bi : LinearIndependent (ι := { x // x ∈ b }) K Subtype.val<VAR>sb : s ⊆ b<VAR>h : ∀ a ∈ {b | b ⊆ t ∧ LinearIndependent (ι := { x // x ∈ b }) K Subtype.val}, b ⊆ a → a = b<VAR>x : V<VAR>xt : x ∈ t<VAR>hn : x ∉ ↑(span K b)<GOAL>x ∈ ↑(span K b)
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>inst✝⁴ : DivisionRing K<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module K V<VAR>inst✝ : Module K V'<VAR>v : ι → V<VAR>s t : Set V<VAR>x✝ y z : V<VAR>hs : LinearIndependent (ι := { x // x ∈ s }) K Subtype.val<VAR>hst : s ⊆ t<VAR>b : Set V<VAR>bt : b ⊆ t<VAR>bi : LinearIndependent (ι := { x // x ∈ b }) K Subtype.val<VAR>sb : s ⊆ b<VAR>h : ∀ a ∈ {b | b ⊆ t ∧ LinearIndependent (ι := { x // x ∈ b }) K Subtype.val}, b ⊆ a → a = b<VAR>x : V<VAR>xt : x ∈ t<VAR>hn : x ∉ ↑(span K b)<GOAL>x ∈ ↑(span K (insert x b))
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : CanonicallyOrderedAddCommMonoid α<VAR>f✝ g✝ f g : ι →₀ α<GOAL>f + g = 0 ↔ f = 0 ∧ g = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁴ : LinearOrderedField α<VAR>inst✝³ : Ring β<VAR>abv : β → α<VAR>inst✝² : IsAbsoluteValue abv<VAR>f g : ℕ → β<VAR>a : ℕ → α<VAR>inst✝¹ : Archimedean α<VAR>inst✝ : Nontrivial β<VAR>x : β<VAR>hx1 : abv x < 1<GOAL>IsCauSeq abv fun n => ∑ m ∈ range n, x ^ m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁴ : LinearOrderedField α<VAR>inst✝³ : Ring β<VAR>abv : β → α<VAR>inst✝² : IsAbsoluteValue abv<VAR>f g : ℕ → β<VAR>a : ℕ → α<VAR>inst✝¹ : Archimedean α<VAR>inst✝ : Nontrivial β<VAR>x : β<VAR>hx1 : abv x < 1<VAR>hx1' : abv x ≠ 1<GOAL>IsCauSeq abv fun n => ∑ m ∈ range n, x ^ m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁴ : LinearOrderedField α<VAR>inst✝³ : Ring β<VAR>abv : β → α<VAR>inst✝² : IsAbsoluteValue abv<VAR>f g : ℕ → β<VAR>a : ℕ → α<VAR>inst✝¹ : Archimedean α<VAR>inst✝ : Nontrivial β<VAR>x : β<VAR>hx1 : abv x < 1<VAR>hx1' : abv x ≠ 1<GOAL>IsCauSeq abs fun m => ∑ n ∈ range m, abv (x ^ n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁴ : LinearOrderedField α<VAR>inst✝³ : Ring β<VAR>abv : β → α<VAR>inst✝² : IsAbsoluteValue abv<VAR>f g : ℕ → β<VAR>a : ℕ → α<VAR>inst✝¹ : Archimedean α<VAR>inst✝ : Nontrivial β<VAR>x : β<VAR>hx1 : abv x < 1<VAR>hx1' : abv x ≠ 1<GOAL>IsCauSeq abs fun m => (abv x ^ m - 1) / (abv x - 1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁴ : LinearOrderedField α<VAR>inst✝³ : Ring β<VAR>abv : β → α<VAR>inst✝² : IsAbsoluteValue abv<VAR>f g : ℕ → β<VAR>a : ℕ → α<VAR>inst✝¹ : Archimedean α<VAR>inst✝ : Nontrivial β<VAR>x : β<VAR>hx1 : abv x < 1<VAR>hx1' : abv x ≠ 1<GOAL>IsCauSeq abs fun m => (1 - abv x ^ m) / (1 - abv x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁴ : LinearOrderedField α<VAR>inst✝³ : Ring β<VAR>abv : β → α<VAR>inst✝² : IsAbsoluteValue abv<VAR>f g : ℕ → β<VAR>a : ℕ → α<VAR>inst✝¹ : Archimedean α<VAR>inst✝ : Nontrivial β<VAR>x : β<VAR>hx1 : abv x < 1<VAR>hx1' : abv x ≠ 1<VAR>this : 0 < 1 - abv x<GOAL>IsCauSeq abs fun m => (1 - abv x ^ m) / (1 - abv x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁴ : LinearOrderedField α<VAR>inst✝³ : Ring β<VAR>abv : β → α<VAR>inst✝² : IsAbsoluteValue abv<VAR>f g : ℕ → β<VAR>a : ℕ → α<VAR>inst✝¹ : Archimedean α<VAR>inst✝ : Nontrivial β<VAR>x : β<VAR>hx1 : abv x < 1<VAR>hx1' : abv x ≠ 1<VAR>this : 0 < 1 - abv x<GOAL>∀ n ≥ 0, |(1 - abv x ^ n) / (1 - abv x)| ≤ 1 / (1 - abv x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁴ : LinearOrderedField α<VAR>inst✝³ : Ring β<VAR>abv : β → α<VAR>inst✝² : IsAbsoluteValue abv<VAR>f g : ℕ → β<VAR>a : ℕ → α<VAR>inst✝¹ : Archimedean α<VAR>inst✝ : Nontrivial β<VAR>x : β<VAR>hx1 : abv x < 1<VAR>hx1' : abv x ≠ 1<VAR>this : 0 < 1 - abv x<GOAL>∀ n ≥ 0, (1 - abv x ^ n) / (1 - abv x) ≤ (1 - abv x ^ n.succ) / (1 - abv x)
<VAR>C : Type u_1<VAR>inst✝ : Category.{?u.17202, u_1} C<VAR>F G : ℕ ⥤ C<VAR>app : (n : ℕ) → F.obj n ⟶ G.obj n<VAR>naturality : ∀ (n : ℕ), F.map (homOfLE ⋯) ≫ app (n + 1) = app n ≫ G.map (homOfLE ⋯)<VAR>i j : ℕ<VAR>φ : i ⟶ j<GOAL>F.map φ ≫ app j = app i ≫ G.map φ
<VAR>C : Type u_1<VAR>inst✝ : Category.{?u.17202, u_1} C<VAR>F G : ℕ ⥤ C<VAR>app : (n : ℕ) → F.obj n ⟶ G.obj n<VAR>naturality : ∀ (n : ℕ), F.map (homOfLE ⋯) ≫ app (n + 1) = app n ≫ G.map (homOfLE ⋯)<VAR>i j : ℕ<VAR>φ : i ⟶ j<VAR>k : ℕ<VAR>hk : j = i + k<GOAL>F.map φ ≫ app j = app i ≫ G.map φ
<VAR>C : Type u_1<VAR>inst✝ : Category.{?u.17202, u_1} C<VAR>F G : ℕ ⥤ C<VAR>app : (n : ℕ) → F.obj n ⟶ G.obj n<VAR>naturality : ∀ (n : ℕ), F.map (homOfLE ⋯) ≫ app (n + 1) = app n ≫ G.map (homOfLE ⋯)<VAR>i j k : ℕ<VAR>hk : j = i + k<GOAL>F.map (homOfLE ⋯) ≫ app j = app i ≫ G.map (homOfLE ⋯)
<VAR>C : Type u_1<VAR>inst✝ : Category.{?u.17202, u_1} C<VAR>F G : ℕ ⥤ C<VAR>app : (n : ℕ) → F.obj n ⟶ G.obj n<VAR>naturality : ∀ (n : ℕ), F.map (homOfLE ⋯) ≫ app (n + 1) = app n ≫ G.map (homOfLE ⋯)<VAR>k : ℕ<GOAL>∀ ⦃i j : ℕ⦄ (hk : j = i + k), F.map (homOfLE ⋯) ≫ app j = app i ≫ G.map (homOfLE ⋯)
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>R : Type u_5<VAR>S : Type u_6<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : Semiring S<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : AddCommMonoid N<VAR>inst✝² : Module R N<VAR>inst✝¹ : AddCommMonoid P<VAR>inst✝ : Module R P<VAR>α' : Type u_7<VAR>α'' : Type u_8<VAR>f : α → α'<VAR>s : Set α<VAR>H : ∀ a ∈ s, ∀ b ∈ s, f a = f b → a = b<GOAL>Disjoint (supported M R s) (ker (lmapDomain M R f))
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>R : Type u_5<VAR>S : Type u_6<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : Semiring S<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : AddCommMonoid N<VAR>inst✝² : Module R N<VAR>inst✝¹ : AddCommMonoid P<VAR>inst✝ : Module R P<VAR>α' : Type u_7<VAR>α'' : Type u_8<VAR>f : α → α'<VAR>s : Set α<VAR>H : ∀ a ∈ s, ∀ b ∈ s, f a = f b → a = b<GOAL>supported M R s ⊓ ker (lmapDomain M R f) ≤ ⊥
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>R : Type u_5<VAR>S : Type u_6<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : Semiring S<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : AddCommMonoid N<VAR>inst✝² : Module R N<VAR>inst✝¹ : AddCommMonoid P<VAR>inst✝ : Module R P<VAR>α' : Type u_7<VAR>α'' : Type u_8<VAR>f : α → α'<VAR>s : Set α<VAR>H : ∀ a ∈ s, ∀ b ∈ s, f a = f b → a = b<VAR>l : α →₀ M<VAR>h₁ : l ∈ ↑(supported M R s)<VAR>h₂ : l ∈ ↑(ker (lmapDomain M R f))<GOAL>l ∈ ⊥
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>R : Type u_5<VAR>S : Type u_6<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : Semiring S<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : AddCommMonoid N<VAR>inst✝² : Module R N<VAR>inst✝¹ : AddCommMonoid P<VAR>inst✝ : Module R P<VAR>α' : Type u_7<VAR>α'' : Type u_8<VAR>f : α → α'<VAR>s : Set α<VAR>H : ∀ a ∈ s, ∀ b ∈ s, f a = f b → a = b<VAR>l : α →₀ M<VAR>h₁ : l ∈ ↑(supported M R s)<VAR>h₂ : (l.sum fun a => single (f a)) = 0<GOAL>l ∈ ⊥
<VAR>α : Type u_1<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : CompleteSpace α<VAR>inst✝ : T0Space α<VAR>f g : CauchyFilter α<GOAL>lim ↑f = lim ↑g ↔ Inseparable f g
<VAR>R : Type u_1<VAR>a b : R<VAR>inst✝ : Monoid R<VAR>n : ℕ<VAR>rla : IsLeftRegular a<GOAL>IsLeftRegular (a ^ n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>u : ℕ → ℝ<VAR>c : ℝ<VAR>hc : 0 ≤ c<VAR>n : ℕ<VAR>h : ∀ k < n, c * u k ≤ u (k + 1)<GOAL>c ^ n * u 0 ≤ u n
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<GOAL>⟪x, y⟫_ℝ = 0 ↔ x = 0 ∨ ∃ r, r • (o.rotation ↑(π / 2)) x = y
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<GOAL>x = 0 ∨ y = 0 ∨ o.oangle x y = ↑(π / 2) ∨ o.oangle x y = ↑(-π / 2) ↔ x = 0 ∨ ∃ r, r • (o.rotation ↑(π / 2)) x = y
<VAR>p q x y : ℝ<VAR>r : ℚ<VAR>m : ℤ<VAR>n : ℕ<VAR>hr : r ≠ 0<VAR>h : LiouvilleWith p (x * ↑r)<GOAL>LiouvilleWith p x
<VAR>J : Type u<VAR>inst✝ : Category.{u_1, u} J<VAR>F : J ⥤ Type v<VAR>i j✝ k✝ : J<VAR>s : Set (F.obj i)<VAR>h : ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective (F.map f)<VAR>j k : J<VAR>g : k ⟶ j<GOAL>range (F.map (𝟙 j)) ⊆ range (F.map g)
<VAR>R : Type u<VAR>S : Type v<VAR>k : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Field R<VAR>p q : R[X]<VAR>hq0 : q ≠ 0<VAR>hpq : q.degree ≤ p.degree<GOAL>q.degree + (p / q).degree = p.degree
<VAR>R : Type u<VAR>S : Type v<VAR>k : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Field R<VAR>p q : R[X]<VAR>hq0 : q ≠ 0<VAR>hpq : q.degree ≤ p.degree<VAR>this : (p % q).degree < (q * (p / q)).degree<GOAL>q.degree + (p / q).degree = p.degree
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>inst✝⁴ : Fintype ι<VAR>m : (i : ι) → OuterMeasure (α i)<VAR>inst✝³ : (i : ι) → MeasurableSpace (α i)<VAR>μ✝ : (i : ι) → Measure (α i)<VAR>inst✝² : ∀ (i : ι), SigmaFinite (μ✝ i)<VAR>β : Option ι → Type u_4<VAR>inst✝¹ : (i : Option ι) → MeasurableSpace (β i)<VAR>μ : (i : Option ι) → Measure (β i)<VAR>inst✝ : ∀ (i : Option ι), SigmaFinite (μ i)<GOAL>map (⇑(MeasurableEquiv.piOptionEquivProd β).symm) ((Measure.pi fun i => μ (some i)).prod (μ none)) = Measure.pi μ
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>inst✝⁴ : Fintype ι<VAR>m : (i : ι) → OuterMeasure (α i)<VAR>inst✝³ : (i : ι) → MeasurableSpace (α i)<VAR>μ✝ : (i : ι) → Measure (α i)<VAR>inst✝² : ∀ (i : ι), SigmaFinite (μ✝ i)<VAR>β : Option ι → Type u_4<VAR>inst✝¹ : (i : Option ι) → MeasurableSpace (β i)<VAR>μ : (i : Option ι) → Measure (β i)<VAR>inst✝ : ∀ (i : Option ι), SigmaFinite (μ i)<VAR>s : (i : Option ι) → Set (β i)<VAR>x✝ : ∀ (i : Option ι), MeasurableSet (s i)<GOAL>(map (⇑(MeasurableEquiv.piOptionEquivProd β).symm) ((Measure.pi fun i => μ (some i)).prod (μ none))) (univ.pi s) = ∏ i : Option ι, (μ i) (s i)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>inst✝⁴ : Fintype ι<VAR>m : (i : ι) → OuterMeasure (α i)<VAR>inst✝³ : (i : ι) → MeasurableSpace (α i)<VAR>μ✝ : (i : ι) → Measure (α i)<VAR>inst✝² : ∀ (i : ι), SigmaFinite (μ✝ i)<VAR>β : Option ι → Type u_4<VAR>inst✝¹ : (i : Option ι) → MeasurableSpace (β i)<VAR>μ : (i : Option ι) → Measure (β i)<VAR>inst✝ : ∀ (i : Option ι), SigmaFinite (μ i)<VAR>s : (i : Option ι) → Set (β i)<VAR>x✝ : ∀ (i : Option ι), MeasurableSet (s i)<VAR>e_meas : ((i : ι) → β (some i)) × β none ≃ᵐ ((i : Option ι) → β i) := (MeasurableEquiv.piOptionEquivProd β).symm<GOAL>(map (⇑(MeasurableEquiv.piOptionEquivProd β).symm) ((Measure.pi fun i => μ (some i)).prod (μ none))) (univ.pi s) = ∏ i : Option ι, (μ i) (s i)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>inst✝⁴ : Fintype ι<VAR>m : (i : ι) → OuterMeasure (α i)<VAR>inst✝³ : (i : ι) → MeasurableSpace (α i)<VAR>μ✝ : (i : ι) → Measure (α i)<VAR>inst✝² : ∀ (i : ι), SigmaFinite (μ✝ i)<VAR>β : Option ι → Type u_4<VAR>inst✝¹ : (i : Option ι) → MeasurableSpace (β i)<VAR>μ : (i : Option ι) → Measure (β i)<VAR>inst✝ : ∀ (i : Option ι), SigmaFinite (μ i)<VAR>s : (i : Option ι) → Set (β i)<VAR>x✝ : ∀ (i : Option ι), MeasurableSet (s i)<VAR>e_meas : ((i : ι) → β (some i)) × β none ≃ᵐ ((i : Option ι) → β i) := (MeasurableEquiv.piOptionEquivProd β).symm<VAR>me : MeasurableEmbedding ⇑e_meas<GOAL>(map (⇑(MeasurableEquiv.piOptionEquivProd β).symm) ((Measure.pi fun i => μ (some i)).prod (μ none))) (univ.pi s) = ∏ i : Option ι, (μ i) (s i)