ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>m : Type u_1<VAR>n✝ : Type u_2<VAR>inst✝⁴ : DecidableEq n✝<VAR>inst✝³ : Fintype n✝<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>R : Type v<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>A : Matrix (Fin n.succ) (Fin n.succ) R<VAR>j i : Fin n.succ<VAR>x✝ : i ∈ univ<GOAL>(-1) ^ (↑j + ↑i) * Aᵀ j i * (Aᵀ.submatrix j.succAbove i.succAbove).det = (-1) ^ (↑i + ↑j) * A i j * (A.submatrix i.succAbove j.succAbove).det
<VAR>R : Type r<VAR>S : Type s<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : CommRing S<VAR>W : WeierstrassCurve R<VAR>inst✝⁸ : Algebra R S<VAR>A : Type u<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : Algebra S A<VAR>inst✝⁴ : IsScalarTower R S A<VAR>B : Type v<VAR>inst✝³ : CommRing B<VAR>inst✝² : Algebra R B<VAR>inst✝¹ : Algebra S B<VAR>inst✝ : IsScalarTower R S B<VAR>f : A →ₐ[S] B<VAR>n : ℤ<GOAL>(W.baseChange B).Ψ n = Polynomial.map (mapRingHom ↑f) ((W.baseChange A).Ψ n)
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace W<VAR>u : Set Y<VAR>hu : IsOpen u<GOAL>IsOpen (inr '' u)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝² : Countable ι<VAR>f✝ g : α → β<VAR>m : MeasurableSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : Zero β<VAR>s : Set α<VAR>f : α → β<VAR>hs : MeasurableSet s<VAR>hf : StronglyMeasurable f<VAR>hf_zero : ∀ x ∉ s, f x = 0<VAR>g_seq_s : ℕ → α →ₛ β := fun n => (hf.approx n).restrict s<GOAL>∃ fs, (∀ (x : α), Tendsto (fun n => ↑(fs n) x) atTop (𝓝 (f x))) ∧ ∀ x ∉ s, ∀ (n : ℕ), ↑(fs n) x = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝² : Countable ι<VAR>f✝ g : α → β<VAR>m : MeasurableSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : Zero β<VAR>s : Set α<VAR>f : α → β<VAR>hs : MeasurableSet s<VAR>hf : StronglyMeasurable f<VAR>hf_zero : ∀ x ∉ s, f x = 0<VAR>g_seq_s : ℕ → α →ₛ β := fun n => (hf.approx n).restrict s<VAR>hg_eq : ∀ x ∈ s, ∀ (n : ℕ), ↑(g_seq_s n) x = ↑(hf.approx n) x<GOAL>∃ fs, (∀ (x : α), Tendsto (fun n => ↑(fs n) x) atTop (𝓝 (f x))) ∧ ∀ x ∉ s, ∀ (n : ℕ), ↑(fs n) x = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝² : Countable ι<VAR>f✝ g : α → β<VAR>m : MeasurableSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : Zero β<VAR>s : Set α<VAR>f : α → β<VAR>hs : MeasurableSet s<VAR>hf : StronglyMeasurable f<VAR>hf_zero : ∀ x ∉ s, f x = 0<VAR>g_seq_s : ℕ → α →ₛ β := fun n => (hf.approx n).restrict s<VAR>hg_eq : ∀ x ∈ s, ∀ (n : ℕ), ↑(g_seq_s n) x = ↑(hf.approx n) x<VAR>hg_zero : ∀ x ∉ s, ∀ (n : ℕ), ↑(g_seq_s n) x = 0<GOAL>∃ fs, (∀ (x : α), Tendsto (fun n => ↑(fs n) x) atTop (𝓝 (f x))) ∧ ∀ x ∉ s, ∀ (n : ℕ), ↑(fs n) x = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>x y : E<GOAL>⟪x, y⟫_𝕜 = ↑‖x‖ * ↑‖y‖ ↔ ↑‖y‖ • x = ↑‖x‖ • y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>y : E<GOAL>⟪0, y⟫_𝕜 = ↑‖0‖ * ↑‖y‖ ↔ ↑‖y‖ • 0 = ↑‖0‖ • y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>x y : E<VAR>h₀ : x ≠ 0<GOAL>⟪x, y⟫_𝕜 = ↑‖x‖ * ↑‖y‖ ↔ ↑‖y‖ • x = ↑‖x‖ • y
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : InnerProductSpace ℝ E<VAR>inst✝ : InnerProductSpace ℝ F<VAR>f : E → F<VAR>x : E<GOAL>ConformalAt f x ↔ ∃ c, 0 < c ∧ ∀ (u v : E), ⟪(fderiv ℝ f x) u, (fderiv ℝ f x) v⟫_ℝ = c * ⟪u, v⟫_ℝ
<VAR>f : ℕ → ℂ<VAR>c s : ℂ<VAR>n : ℕ<GOAL>term (c • f) s n = c * term f s n
<VAR>n : Type u_1<VAR>p : Type u_2<VAR>R : Type u₂<VAR>𝕜 : Type u_3<VAR>inst✝⁴ : Field 𝕜<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : DecidableEq p<VAR>inst✝¹ : CommRing R<VAR>i j : n<VAR>inst✝ : Fintype n<VAR>M : Matrix n n R<VAR>hM : ∀ (t : TransvectionStruct n R), Commute t.toMatrix M<GOAL>M ∈ Set.range ⇑(scalar n)
<VAR>n : Type u_1<VAR>p : Type u_2<VAR>R : Type u₂<VAR>𝕜 : Type u_3<VAR>inst✝⁴ : Field 𝕜<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : DecidableEq p<VAR>inst✝¹ : CommRing R<VAR>i j : n<VAR>inst✝ : Fintype n<VAR>M : Matrix n n R<VAR>hM : ∀ (t : TransvectionStruct n R), Commute t.toMatrix M<GOAL>Pairwise fun i j => Commute (stdBasisMatrix i j 1) M
<VAR>n : Type u_1<VAR>p : Type u_2<VAR>R : Type u₂<VAR>𝕜 : Type u_3<VAR>inst✝⁴ : Field 𝕜<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : DecidableEq p<VAR>inst✝¹ : CommRing R<VAR>i✝ j✝ : n<VAR>inst✝ : Fintype n<VAR>M : Matrix n n R<VAR>hM : ∀ (t : TransvectionStruct n R), Commute t.toMatrix M<VAR>i j : n<VAR>hij : i ≠ j<GOAL>Commute (stdBasisMatrix i j 1) M
<VAR>R : Type u<VAR>S : Type v<VAR>k : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : NormalizationMonoid R<VAR>p : R[X]<GOAL>(normalize p).roots = p.roots
<VAR>α : Type u<VAR>β : Type v<VAR>R : Type u<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : Nontrivial R<VAR>M : Ideal R<VAR>hm : M.IsMaximal<VAR>non_field : ¬IsField R<GOAL>⊥ < M
<VAR>α : Type u<VAR>β : Type v<VAR>R : Type u<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : Nontrivial R<VAR>M : Ideal R<VAR>hm : M.IsMaximal<VAR>non_field : ¬IsField R<VAR>I : Ideal R<VAR>Ibot : ⊥ < I<VAR>Itop : I < ⊤<GOAL>⊥ < M
<VAR>α : Type u<VAR>β : Type v<VAR>R : Type u<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : Nontrivial R<VAR>M : Ideal R<VAR>hm : M.IsMaximal<VAR>non_field : ¬IsField R<VAR>I : Ideal R<VAR>Ibot : ⊥ < I<VAR>Itop : I < ⊤<VAR>mle : ↑M ⊆ ↑⊥<GOAL>False
<VAR>α : Type u<VAR>β : Type v<VAR>R : Type u<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : Nontrivial R<VAR>M : Ideal R<VAR>hm : M.IsMaximal<VAR>non_field : ¬IsField R<VAR>I : Ideal R<VAR>Ibot : ⊥ < I<VAR>Itop : I < ⊤<VAR>mle : ↑M ⊆ ↑⊥<GOAL>⊤ < ⊤
<VAR>α : Type u<VAR>β : Type v<VAR>R : Type u<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : Nontrivial R<VAR>M : Ideal R<VAR>hm : M.IsMaximal<VAR>non_field : ¬IsField R<VAR>I : Ideal R<VAR>Ibot : ⊥ < I<VAR>Itop : I < ⊤<VAR>mle : ↑M ⊆ ↑⊥<VAR>this : M = ⊥<GOAL>⊤ < ⊤
<VAR>α : Type u<VAR>β : Type v<VAR>R : Type u<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : Nontrivial R<VAR>M : Ideal R<VAR>hm : M.IsMaximal<VAR>non_field : ¬IsField R<VAR>I : Ideal R<VAR>Ibot : M < I<VAR>Itop : I < ⊤<VAR>mle : ↑M ⊆ ↑⊥<VAR>this : M = ⊥<GOAL>⊤ < ⊤
<VAR>m n a b c d : ℕ<VAR>h₁ : a ≡ b [MOD n]<VAR>h₂ : a + c ≡ b + d [MOD n]<GOAL>c ≡ d [MOD n]
<VAR>m n a b c d : ℕ<VAR>h₁ : ↑n ∣ ↑b - ↑a<VAR>h₂ : ↑n ∣ ↑b + ↑d - (↑a + ↑c)<GOAL>↑n ∣ ↑d - ↑c
<VAR>m n a b c d : ℕ<VAR>h₁ : ↑n ∣ ↑b - ↑a<VAR>h₂ : ↑n ∣ ↑b - ↑a + (↑d - ↑c)<GOAL>↑n ∣ ↑d - ↑c
<VAR>m n a b c d : ℕ<VAR>h₁ : ↑n ∣ ↑b - ↑a<VAR>h₂ : ↑n ∣ ↑b - ↑a + (↑d - ↑c)<GOAL>↑d - ↑c = ↑b - ↑a + (↑d - ↑c) - (↑b - ↑a)
<VAR>o : Ordinal.{u_1}<GOAL>ℵ₀ ≤ aleph o
<VAR>o : Ordinal.{u_1}<GOAL>ω ≤ ω + o
<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.j * q.k = -c₂ • q.i
<VAR>ι : Type u_1<VAR>α✝ : Type u_2<VAR>β : Type u_3<VAR>α : Type u_4<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : OrderBot α<VAR>l : Multiset α<VAR>n : α<VAR>h : ∀ x ∈ l, x ≤ n<GOAL>fold max ⊥ l ≤ n
<VAR>ι : Type u_1<VAR>α✝ : Type u_2<VAR>β : Type u_3<VAR>α : Type u_4<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : OrderBot α<VAR>n : α<VAR>a✝ : List α<VAR>h : ∀ x ∈ ⟦a✝⟧, x ≤ n<GOAL>fold max ⊥ ⟦a✝⟧ ≤ n
<VAR>R : Type u<VAR>inst✝⁴ : Ring R<VAR>ι : Type v<VAR>inst✝³ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝² : Nonempty ι<VAR>inst✝¹ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>inst✝ : (i : ι) → Field (G i)<VAR>f : (i j : ι) → i ≤ j → G i → G j<VAR>f' : (i j : ι) → i ≤ j → G i →+* G j<VAR>p : Ring.DirectLimit G f<VAR>i : ι<VAR>x : G i<VAR>H : (Ring.DirectLimit.of G f i) x ≠ 0<GOAL>(Ring.DirectLimit.of G f i) x * (Ring.DirectLimit.of G f i) x⁻¹ = 1
<VAR>ι : Type uι<VAR>E : Type uE<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : FiniteDimensional ℝ E<VAR>F : Type uF<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>H : Type uH<VAR>inst✝⁵ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝⁴ : TopologicalSpace M<VAR>inst✝³ : ChartedSpace H M<VAR>inst✝² : SmoothManifoldWithCorners I M<VAR>inst✝¹ : T2Space M<VAR>inst✝ : SigmaCompactSpace M<VAR>s t : Set M<VAR>hs : IsClosed s<VAR>ht : IsClosed t<VAR>hd : Disjoint s t<GOAL>∃ f, EqOn (⇑f) 0 s ∧ EqOn (⇑f) 1 t ∧ ∀ (x : M), f x ∈ Icc 0 1
<VAR>ι : Type uι<VAR>E : Type uE<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : FiniteDimensional ℝ E<VAR>F : Type uF<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>H : Type uH<VAR>inst✝⁵ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝⁴ : TopologicalSpace M<VAR>inst✝³ : ChartedSpace H M<VAR>inst✝² : SmoothManifoldWithCorners I M<VAR>inst✝¹ : T2Space M<VAR>inst✝ : SigmaCompactSpace M<VAR>s t : Set M<VAR>hs : IsClosed s<VAR>ht : IsClosed t<VAR>hd : Disjoint s t<VAR>this : ∀ x ∈ t, sᶜ ∈ 𝓝 x<GOAL>∃ f, EqOn (⇑f) 0 s ∧ EqOn (⇑f) 1 t ∧ ∀ (x : M), f x ∈ Icc 0 1
<VAR>ι✝ : Type uι<VAR>E : Type uE<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : FiniteDimensional ℝ E<VAR>F : Type uF<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>H : Type uH<VAR>inst✝⁵ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝⁴ : TopologicalSpace M<VAR>inst✝³ : ChartedSpace H M<VAR>inst✝² : SmoothManifoldWithCorners I M<VAR>inst✝¹ : T2Space M<VAR>inst✝ : SigmaCompactSpace M<VAR>s t : Set M<VAR>hs : IsClosed s<VAR>ht : IsClosed t<VAR>hd : Disjoint s t<VAR>this : ∀ x ∈ t, sᶜ ∈ 𝓝 x<VAR>ι : Type uM<VAR>f : SmoothBumpCovering ι I M t<VAR>hf : f.IsSubordinate fun x => sᶜ<GOAL>∃ f, EqOn (⇑f) 0 s ∧ EqOn (⇑f) 1 t ∧ ∀ (x : M), f x ∈ Icc 0 1
<VAR>ι✝ : Type uι<VAR>E : Type uE<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : FiniteDimensional ℝ E<VAR>F : Type uF<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>H : Type uH<VAR>inst✝⁵ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝⁴ : TopologicalSpace M<VAR>inst✝³ : ChartedSpace H M<VAR>inst✝² : SmoothManifoldWithCorners I M<VAR>inst✝¹ : T2Space M<VAR>inst✝ : SigmaCompactSpace M<VAR>s t : Set M<VAR>hs : IsClosed s<VAR>ht : IsClosed t<VAR>hd : Disjoint s t<VAR>this : ∀ x ∈ t, sᶜ ∈ 𝓝 x<VAR>ι : Type uM<VAR>f : SmoothBumpCovering ι I M t<VAR>hf : f.IsSubordinate fun x => sᶜ<VAR>g : SmoothPartitionOfUnity ι I M t := f.toSmoothPartitionOfUnity<GOAL>∃ f, EqOn (⇑f) 0 s ∧ EqOn (⇑f) 1 t ∧ ∀ (x : M), f x ∈ Icc 0 1
<VAR>ι✝ : Type uι<VAR>E : Type uE<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : FiniteDimensional ℝ E<VAR>F : Type uF<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>H : Type uH<VAR>inst✝⁵ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝⁴ : TopologicalSpace M<VAR>inst✝³ : ChartedSpace H M<VAR>inst✝² : SmoothManifoldWithCorners I M<VAR>inst✝¹ : T2Space M<VAR>inst✝ : SigmaCompactSpace M<VAR>s t : Set M<VAR>hs : IsClosed s<VAR>ht : IsClosed t<VAR>hd : Disjoint s t<VAR>this : ∀ x ∈ t, sᶜ ∈ 𝓝 x<VAR>ι : Type uM<VAR>f : SmoothBumpCovering ι I M t<VAR>hf : f.IsSubordinate fun x => sᶜ<VAR>g : SmoothPartitionOfUnity ι I M t := f.toSmoothPartitionOfUnity<VAR>x : M<VAR>hx : x ∈ s<GOAL>⟨fun x => ∑ᶠ (i : ι), (g i) x, ⋯⟩ x = 0 x
<VAR>ι✝ : Type uι<VAR>E : Type uE<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : FiniteDimensional ℝ E<VAR>F : Type uF<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>H : Type uH<VAR>inst✝⁵ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝⁴ : TopologicalSpace M<VAR>inst✝³ : ChartedSpace H M<VAR>inst✝² : SmoothManifoldWithCorners I M<VAR>inst✝¹ : T2Space M<VAR>inst✝ : SigmaCompactSpace M<VAR>s t : Set M<VAR>hs : IsClosed s<VAR>ht : IsClosed t<VAR>hd : Disjoint s t<VAR>this : ∀ x ∈ t, sᶜ ∈ 𝓝 x<VAR>ι : Type uM<VAR>f : SmoothBumpCovering ι I M t<VAR>hf : f.IsSubordinate fun x => sᶜ<VAR>g : SmoothPartitionOfUnity ι I M t := f.toSmoothPartitionOfUnity<VAR>x : M<VAR>hx : x ∈ s<GOAL>∀ (i : ι), (g i) x = 0
<VAR>ι✝ : Type uι<VAR>E : Type uE<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : FiniteDimensional ℝ E<VAR>F : Type uF<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>H : Type uH<VAR>inst✝⁵ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝⁴ : TopologicalSpace M<VAR>inst✝³ : ChartedSpace H M<VAR>inst✝² : SmoothManifoldWithCorners I M<VAR>inst✝¹ : T2Space M<VAR>inst✝ : SigmaCompactSpace M<VAR>s t : Set M<VAR>hs : IsClosed s<VAR>ht : IsClosed t<VAR>hd : Disjoint s t<VAR>this : ∀ x ∈ t, sᶜ ∈ 𝓝 x<VAR>ι : Type uM<VAR>f : SmoothBumpCovering ι I M t<VAR>hf : f.IsSubordinate fun x => sᶜ<VAR>g : SmoothPartitionOfUnity ι I M t := f.toSmoothPartitionOfUnity<VAR>x : M<VAR>hx : x ∈ s<VAR>i : ι<GOAL>↑(f.toFun i) x = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>s s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>p✝ : Set γ<VAR>f f₁ f₂ f₃ : α → β<VAR>g g₁ g₂ : β → γ<VAR>f' f₁' f₂' : β → α<VAR>g' : γ → β<VAR>a : α<VAR>b✝ : β<VAR>p : β → Prop<VAR>hf : BijOn f s t<VAR>b : β<VAR>hb : b ∈ t<VAR>h : p b<GOAL>∃ a ∈ s, p (f a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>s s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>p✝ : Set γ<VAR>f f₁ f₂ f₃ : α → β<VAR>g g₁ g₂ : β → γ<VAR>f' f₁' f₂' : β → α<VAR>g' : γ → β<VAR>a✝ : α<VAR>b : β<VAR>p : β → Prop<VAR>hf : BijOn f s t<VAR>a : α<VAR>ha : a ∈ s<VAR>hb : f a ∈ t<VAR>h : p (f a)<GOAL>∃ a ∈ s, p (f a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>s s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>p✝ : Set γ<VAR>f f₁ f₂ f₃ : α → β<VAR>g g₁ g₂ : β → γ<VAR>f' f₁' f₂' : β → α<VAR>g' : γ → β<VAR>a✝ : α<VAR>b : β<VAR>p : β → Prop<VAR>hf : BijOn f s t<VAR>a : α<VAR>ha : a ∈ s<VAR>h : p (f a)<GOAL>∃ b ∈ t, p b
<VAR>R✝ : Type u_1<VAR>inst✝¹¹ : CommRing R✝<VAR>S : Submonoid R✝<VAR>P : Type u_2<VAR>inst✝¹⁰ : CommRing P<VAR>inst✝⁹ : Algebra R✝ P<VAR>loc : IsLocalization S P<VAR>R₁ : Type u_3<VAR>inst✝⁸ : CommRing R₁<VAR>K✝ : Type u_4<VAR>inst✝⁷ : Field K✝<VAR>inst✝⁶ : Algebra R₁ K✝<VAR>inst✝⁵ : IsFractionRing R₁ K✝<VAR>inst✝⁴ : IsDomain R₁<VAR>R : Type u_6<VAR>inst✝³ : CommRing R<VAR>K : Type u_5<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>I : FractionalIdeal R⁰ K<VAR>hI : I ≠ 0<VAR>a : R<VAR>J : Ideal R<VAR>haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J<VAR>h : J = 0<GOAL>False
<VAR>R✝ : Type u_1<VAR>inst✝¹¹ : CommRing R✝<VAR>S : Submonoid R✝<VAR>P : Type u_2<VAR>inst✝¹⁰ : CommRing P<VAR>inst✝⁹ : Algebra R✝ P<VAR>loc : IsLocalization S P<VAR>R₁ : Type u_3<VAR>inst✝⁸ : CommRing R₁<VAR>K✝ : Type u_4<VAR>inst✝⁷ : Field K✝<VAR>inst✝⁶ : Algebra R₁ K✝<VAR>inst✝⁵ : IsFractionRing R₁ K✝<VAR>inst✝⁴ : IsDomain R₁<VAR>R : Type u_6<VAR>inst✝³ : CommRing R<VAR>K : Type u_5<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>I : FractionalIdeal R⁰ K<VAR>hI : I ≠ 0<VAR>a : R<VAR>J : Ideal R<VAR>haJ : I = 0<VAR>h : J = 0<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_4<VAR>inst✝³ : Primcodable α<VAR>inst✝² : Primcodable β<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Primcodable σ<VAR>f : α → ℕ<VAR>g : α → σ<VAR>h : α → ℕ →. σ<VAR>hf : Computable f<VAR>hg : Computable g<VAR>hh : Partrec₂ h<VAR>a : α<GOAL>Nat.rec (↑g a) (fun y IH => IH.bind fun i => h (a, y, i).1 (f (a, y, i).1).pred) (f a) = Nat.casesOn (f a) (Part.some (g a)) (h a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_4<VAR>inst✝³ : Primcodable α<VAR>inst✝² : Primcodable β<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Primcodable σ<VAR>f : α → ℕ<VAR>g : α → σ<VAR>h : α → ℕ →. σ<VAR>hf : Computable f<VAR>hg : Computable g<VAR>hh : Partrec₂ h<VAR>a : α<GOAL>Nat.rec (Part.some (g a)) (fun y IH => IH.bind fun i => h a (f a - 1)) (f a) = Nat.rec (Part.some (g a)) (fun n n_ih => h a n) (f a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_4<VAR>inst✝³ : Primcodable α<VAR>inst✝² : Primcodable β<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Primcodable σ<VAR>f : α → ℕ<VAR>g : α → σ<VAR>h : α → ℕ →. σ<VAR>hf : Computable f<VAR>hg : Computable g<VAR>hh : Partrec₂ h<VAR>a : α<VAR>n : ℕ<GOAL>((Nat.rec (Part.some (g a)) (fun y IH => IH.bind fun i => h a n) n).bind fun i => h a n) = h a n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_4<VAR>inst✝³ : Primcodable α<VAR>inst✝² : Primcodable β<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Primcodable σ<VAR>f : α → ℕ<VAR>g : α → σ<VAR>h : α → ℕ →. σ<VAR>hf : Computable f<VAR>hg : Computable g<VAR>hh : Partrec₂ h<VAR>a : α<VAR>n : ℕ<VAR>b : σ<VAR>H : b ∈ (Nat.rec (Part.some (g a)) (fun y IH => IH.bind fun i => h a n) n).bind fun i => h a n<GOAL>b ∈ h a n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_4<VAR>inst✝³ : Primcodable α<VAR>inst✝² : Primcodable β<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Primcodable σ<VAR>f : α → ℕ<VAR>g : α → σ<VAR>h : α → ℕ →. σ<VAR>hf : Computable f<VAR>hg : Computable g<VAR>hh : Partrec₂ h<VAR>a : α<VAR>n : ℕ<VAR>b : σ<VAR>H : b ∈ h a n<GOAL>b ∈ (Nat.rec (Part.some (g a)) (fun y IH => IH.bind fun i => h a n) n).bind fun i => h a n
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>F : Type u_3<VAR>K : Type u_4<VAR>P : Cubic F<VAR>inst✝² : Field F<VAR>inst✝¹ : Field K<VAR>φ : F →+* K<VAR>x y z : K<VAR>inst✝ : DecidableEq K<VAR>ha : P.a ≠ 0<VAR>h3 : (map φ P).roots = {x, y, z}<VAR>hd : P.disc ≠ 0<GOAL>(map φ P).roots.toFinset.card = 3
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>F : Type u_3<VAR>K : Type u_4<VAR>P : Cubic F<VAR>inst✝² : Field F<VAR>inst✝¹ : Field K<VAR>φ : F →+* K<VAR>x y z : K<VAR>inst✝ : DecidableEq K<VAR>ha : P.a ≠ 0<VAR>h3 : (map φ P).roots = {x, y, z}<VAR>hd : P.disc ≠ 0<GOAL>∃ x y z, (map φ P).roots = {x, y, z}
<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>m : MeasurableSpace α<VAR>μ μ₁ μ₂ : Measure α<VAR>s✝ s₁ s₂ t✝ : Set α<VAR>s : ι → Set α<VAR>t : Set ι<VAR>ht : t.Countable<VAR>hd : DirectedOn ((fun x x_1 => x ⊆ x_1) on s) t<VAR>this : Encodable ↑t<GOAL>μ (⋃ i ∈ t, s i) = ⨆ i ∈ t, μ (s i)
<VAR>k : Type u<VAR>inst✝¹ : Field k<VAR>G : Type u<VAR>inst✝ : Monoid G<VAR>V : FDRep k G<GOAL>V.character 1 = ↑(finrank k (CoeSort.coe V))
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>a : Ordinal.{u_3}<GOAL>a ≤ 1 ↔ a = 0 ∨ a = 1
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : Field F<VAR>inst✝² : Field E<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : Finite (IntermediateField F E)<VAR>IF : Type u_2 := { K // ∃ x, K = F⟮x⟯ }<GOAL>FiniteDimensional F E
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : Field F<VAR>inst✝² : Field E<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : Finite (IntermediateField F E)<VAR>IF : Type u_2 := { K // ∃ x, K = F⟮x⟯ }<VAR>this : Algebra.IsAlgebraic F E<GOAL>FiniteDimensional F E
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : Field F<VAR>inst✝² : Field E<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : Finite (IntermediateField F E)<VAR>IF : Type u_2 := { K // ∃ x, K = F⟮x⟯ }<VAR>this✝ : Algebra.IsAlgebraic F E<VAR>this : ∀ (K : IF), FiniteDimensional F ↥↑K<GOAL>FiniteDimensional F E
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : Field F<VAR>inst✝² : Field E<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : Finite (IntermediateField F E)<VAR>IF : Type u_2 := { K // ∃ x, K = F⟮x⟯ }<VAR>this✝ : Algebra.IsAlgebraic F E<VAR>this : ∀ (K : IF), FiniteDimensional F ↥↑K<VAR>hfin : FiniteDimensional F ↥(⨆ i, ↑i)<GOAL>FiniteDimensional F E
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : Field F<VAR>inst✝² : Field E<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : Finite (IntermediateField F E)<VAR>IF : Type u_2 := { K // ∃ x, K = F⟮x⟯ }<VAR>this✝ : Algebra.IsAlgebraic F E<VAR>this : ∀ (K : IF), FiniteDimensional F ↥↑K<VAR>hfin : FiniteDimensional F ↥(⨆ i, ↑i)<VAR>htop : ⨆ K, ↑K = ⊤<GOAL>FiniteDimensional F E
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : Field F<VAR>inst✝² : Field E<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : Finite (IntermediateField F E)<VAR>IF : Type u_2 := { K // ∃ x, K = F⟮x⟯ }<VAR>this✝ : Algebra.IsAlgebraic F E<VAR>this : ∀ (K : IF), FiniteDimensional F ↥↑K<VAR>hfin : FiniteDimensional F ↥⊤<VAR>htop : ⨆ K, ↑K = ⊤<GOAL>FiniteDimensional F E
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q : QuadraticForm R M<VAR>m : M<GOAL>(ofEven Q) ((toEven Q) ((ι Q) m)) = (ofEven Q) ⟨↑((toEven Q) ((ι Q) m)), ⋯⟩
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q : QuadraticForm R M<VAR>m : M<GOAL>(ofEven Q) ⟨↑((toEven Q) ((ι Q) m)), ⋯⟩ = ((ι Q) 0 + (algebraMap R (CliffordAlgebra Q)) 1) * ((ι Q) m - (algebraMap R (CliffordAlgebra Q)) 0)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q : QuadraticForm R M<VAR>m : M<GOAL>(ofEven Q) ⟨e0 Q * (v Q) m, ⋯⟩ = ((ι Q) 0 + (algebraMap R (CliffordAlgebra Q)) 1) * ((ι Q) m - (algebraMap R (CliffordAlgebra Q)) 0)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q : QuadraticForm R M<VAR>m : M<GOAL>((ι Q) 0 + (algebraMap R (CliffordAlgebra Q)) 1) * ((ι Q) m - (algebraMap R (CliffordAlgebra Q)) 0) = (ι Q) m
<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>f : ℝ → E<VAR>a b C : ℝ<VAR>hf : DifferentiableOn ℝ f (Icc a b)<VAR>bound : ∀ x ∈ Ico a b, ‖derivWithin f (Icc a b) x‖ ≤ C<GOAL>∀ x ∈ Icc a b, ‖f x - f a‖ ≤ C * (x - a)
<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>f : ℝ → E<VAR>a b C : ℝ<VAR>hf : DifferentiableOn ℝ f (Icc a b)<VAR>bound : ∀ x ∈ Ico a b, ‖derivWithin f (Icc a b) x‖ ≤ C<GOAL>∀ x ∈ Icc a b, HasDerivWithinAt f (derivWithin f (Icc a b) x) (Icc a b) x
<VAR>α β : SemilatInfCat<VAR>e : α.X ≃o β.X<VAR>x✝ : (forget SemilatInfCat).obj α<GOAL>({ toFun := ⇑e, map_inf' := ⋯, map_top' := ⋯ } ≫ { toFun := ⇑e.symm, map_inf' := ⋯, map_top' := ⋯ }) x✝ = (𝟙 α) x✝
<VAR>α β : SemilatInfCat<VAR>e : α.X ≃o β.X<VAR>x✝ : (forget SemilatInfCat).obj β<GOAL>({ toFun := ⇑e.symm, map_inf' := ⋯, map_top' := ⋯ } ≫ { toFun := ⇑e, map_inf' := ⋯, map_top' := ⋯ }) x✝ = (𝟙 β) x✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort u_5<VAR>s : Set α<VAR>t : Set β<VAR>f : Filter α<VAR>g : Filter β<VAR>p : α × β → Prop<GOAL>(∀ᶠ (x : α × β) in f ×ˢ g, p x) ↔ ∃ pa, (∀ᶠ (x : α) in f, pa x) ∧ ∃ pb, (∀ᶠ (y : β) in g, pb y) ∧ ∀ {x : α}, pa x → ∀ {y : β}, pb y → p (x, y)
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N n m : ℕ<VAR>ω✝ : Ω<VAR>ℱ : Filtration ℕ m0<VAR>ω : Ω<GOAL>upcrossingsBefore a b f 0 ω = 0 ω
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Fintype α<VAR>inst✝² : Fintype β<VAR>A : Matrix α β ℤ<VAR>v✝ : β → ℤ<VAR>hn : m < n<VAR>hm : 0 < m<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>v : β → ℤ<VAR>hv : v ∈ T<GOAL>A *ᵥ v ∈ S
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Fintype α<VAR>inst✝² : Fintype β<VAR>A : Matrix α β ℤ<VAR>v✝ : β → ℤ<VAR>hn : m < n<VAR>hm : 0 < m<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>v : β → ℤ<VAR>hv : 0 ≤ v ∧ v ≤ B'<GOAL>N ≤ A *ᵥ v ∧ A *ᵥ v ≤ P
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Fintype α<VAR>inst✝² : Fintype β<VAR>A : Matrix α β ℤ<VAR>v✝ : β → ℤ<VAR>hn : m < n<VAR>hm : 0 < m<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>v : β → ℤ<VAR>hv : 0 ≤ v ∧ v ≤ B'<VAR>mulVec_def : A *ᵥ v = fun i => ∑ j : β, A i j * v j<VAR>i : α<GOAL>N i ≤ (fun i => ∑ j : β, A i j * v j) i