ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>inst✝¹ : Semiring R<VAR>S : Type v<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>s : S<VAR>n : ℕ<VAR>hzero : ¬s = 0<VAR>q : R[X]<VAR>hq : (map f q).coeff n = ((monomial n) s).coeff n<VAR>hcoeff : f (q.coeff n) = s<VAR>hqzero : q.coeff n ≠ 0<GOAL>(C (q.coeff n) * X ^ n).degree = (C s * X ^ n).degree
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>f₁ f₂ : α → R<VAR>g₁ g₂ : α → 𝕜<VAR>h₁ : f₁ =O[l] g₁<VAR>h₂ : f₂ =o[l] g₂<GOAL>(fun x => f₁ x * f₂ x) =o[l] fun x => g₁ x * g₂ x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>f₁ f₂ : α → R<VAR>g₁ g₂ : α → 𝕜<VAR>h₁ : f₁ =O[l] g₁<VAR>h₂ : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f₂ g₂<GOAL>∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l (fun x => f₁ x * f₂ x) fun x => g₁ x * g₂ x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c✝ c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>f₁ f₂ : α → R<VAR>g₁ g₂ : α → 𝕜<VAR>h₁ : f₁ =O[l] g₁<VAR>h₂ : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f₂ g₂<VAR>c : ℝ<VAR>cpos : 0 < c<GOAL>IsBigOWith c l (fun x => f₁ x * f₂ x) fun x => g₁ x * g₂ x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c✝ c'✝ c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>f₁ f₂ : α → R<VAR>g₁ g₂ : α → 𝕜<VAR>h₁ : f₁ =O[l] g₁<VAR>h₂ : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f₂ g₂<VAR>c : ℝ<VAR>cpos : 0 < c<VAR>c' : ℝ<VAR>c'pos : c' > 0<VAR>hc' : IsBigOWith c' l f₁ g₁<GOAL>IsBigOWith c l (fun x => f₁ x * f₂ x) fun x => g₁ x * g₂ x
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>r : R<VAR>f✝ f : R[X]<GOAL>(taylor 0) f = f
<VAR>M : Type u_1<VAR>R : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝⁵ : UniformSpace α<VAR>inst✝⁴ : AddGroup α<VAR>inst✝³ : UniformAddGroup α<VAR>inst✝² : UniformSpace β<VAR>inst✝¹ : AddGroup β<VAR>inst✝ : UniformAddGroup β<VAR>x : Completion α<GOAL>(completion 0 ⋯) x = 0 x
<VAR>M : Type u_1<VAR>R : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝⁵ : UniformSpace α<VAR>inst✝⁴ : AddGroup α<VAR>inst✝³ : UniformAddGroup α<VAR>inst✝² : UniformSpace β<VAR>inst✝¹ : AddGroup β<VAR>inst✝ : UniformAddGroup β<VAR>x : Completion α<GOAL>IsClosed {a | (completion 0 ⋯) a = 0 a}
<VAR>M : Type u_1<VAR>R : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝⁵ : UniformSpace α<VAR>inst✝⁴ : AddGroup α<VAR>inst✝³ : UniformAddGroup α<VAR>inst✝² : UniformSpace β<VAR>inst✝¹ : AddGroup β<VAR>inst✝ : UniformAddGroup β<VAR>x : Completion α<GOAL>∀ (a : α), (completion 0 ⋯) (↑α a) = 0 (↑α a)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : CompleteSpace E<VAR>f : ℕ → α → E<VAR>hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ<VAR>hp : 1 ≤ p<VAR>B : ℕ → ℝ≥0∞<VAR>hB : ∑' (i : ℕ), B i ≠ ⊤<VAR>h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm (f n - f m) p μ < B N<VAR>hp_top : ¬p = ⊤<GOAL>∀ᵐ (x : α) ∂μ, ∃ l, Tendsto (fun n => f n x) atTop (𝓝 l)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : CompleteSpace E<VAR>f : ℕ → α → E<VAR>hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ<VAR>hp : 1 ≤ p<VAR>B : ℕ → ℝ≥0∞<VAR>hB : ∑' (i : ℕ), B i ≠ ⊤<VAR>h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm (f n - f m) p μ < B N<VAR>hp_top : ¬p = ⊤<VAR>hp1 : 1 ≤ p.toReal<GOAL>∀ᵐ (x : α) ∂μ, ∃ l, Tendsto (fun n => f n x) atTop (𝓝 l)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : CompleteSpace E<VAR>f : ℕ → α → E<VAR>hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ<VAR>hp : 1 ≤ p<VAR>B : ℕ → ℝ≥0∞<VAR>hB : ∑' (i : ℕ), B i ≠ ⊤<VAR>h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm (f n - f m) p μ < B N<VAR>hp_top : ¬p = ⊤<VAR>hp1 : 1 ≤ p.toReal<VAR>h_cau' : ∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm' (f n - f m) p.toReal μ < B N<GOAL>∀ᵐ (x : α) ∂μ, ∃ l, Tendsto (fun n => f n x) atTop (𝓝 l)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : SecondCountableTopology α<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure μ<GOAL>Nonempty (μ.FiniteSpanningSetsIn {K | IsOpen K})
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : SecondCountableTopology α<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>h✝ : IsEmpty α<GOAL>Nonempty (μ.FiniteSpanningSetsIn {K | IsOpen K})
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : SecondCountableTopology α<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>h✝ : Nonempty α<GOAL>Nonempty (μ.FiniteSpanningSetsIn {K | IsOpen K})
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : SecondCountableTopology α<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>h✝ : Nonempty α<VAR>inhabited_h : Inhabited α<VAR>S : Set (Set α) := {s | IsOpen s ∧ μ s < ⊤}<GOAL>Nonempty (μ.FiniteSpanningSetsIn {K | IsOpen K})
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : SecondCountableTopology α<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>h✝ : Nonempty α<VAR>inhabited_h : Inhabited α<VAR>S : Set (Set α) := {s | IsOpen s ∧ μ s < ⊤}<VAR>T : Set (Set α)<VAR>T_count : T.Countable<VAR>TS : T ⊆ S<VAR>hT : ⋃₀ T = ⋃₀ S<GOAL>Nonempty (μ.FiniteSpanningSetsIn {K | IsOpen K})
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : SecondCountableTopology α<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>h✝ : Nonempty α<VAR>inhabited_h : Inhabited α<VAR>S : Set (Set α) := {s | IsOpen s ∧ μ s < ⊤}<VAR>T : Set (Set α)<VAR>T_count : T.Countable<VAR>TS : T ⊆ S<VAR>hT : ⋃₀ T = univ<GOAL>Nonempty (μ.FiniteSpanningSetsIn {K | IsOpen K})
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : SecondCountableTopology α<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>h✝ : Nonempty α<VAR>inhabited_h : Inhabited α<VAR>S : Set (Set α) := {s | IsOpen s ∧ μ s < ⊤}<VAR>T : Set (Set α)<VAR>T_count : T.Countable<VAR>TS : T ⊆ S<VAR>hT : ⋃₀ T = univ<VAR>T_ne : T.Nonempty<GOAL>Nonempty (μ.FiniteSpanningSetsIn {K | IsOpen K})
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : SecondCountableTopology α<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>h✝ : Nonempty α<VAR>inhabited_h : Inhabited α<VAR>S : Set (Set α) := {s | IsOpen s ∧ μ s < ⊤}<VAR>T : Set (Set α)<VAR>T_count : T.Countable<VAR>TS : T ⊆ S<VAR>hT : ⋃₀ T = univ<VAR>T_ne : T.Nonempty<VAR>f : ℕ → Set α<VAR>hf : T = range f<GOAL>Nonempty (μ.FiniteSpanningSetsIn {K | IsOpen K})
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : SecondCountableTopology α<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>h✝ : Nonempty α<VAR>inhabited_h : Inhabited α<VAR>S : Set (Set α) := {s | IsOpen s ∧ μ s < ⊤}<VAR>T : Set (Set α)<VAR>T_count : T.Countable<VAR>TS : T ⊆ S<VAR>hT : ⋃₀ T = univ<VAR>T_ne : T.Nonempty<VAR>f : ℕ → Set α<VAR>hf : T = range f<VAR>fS : ∀ (n : ℕ), f n ∈ S<GOAL>Nonempty (μ.FiniteSpanningSetsIn {K | IsOpen K})
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : SecondCountableTopology α<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>h✝ : Nonempty α<VAR>inhabited_h : Inhabited α<VAR>S : Set (Set α) := {s | IsOpen s ∧ μ s < ⊤}<VAR>T : Set (Set α)<VAR>T_count : T.Countable<VAR>TS : T ⊆ S<VAR>hT : ⋃₀ T = univ<VAR>T_ne : T.Nonempty<VAR>f : ℕ → Set α<VAR>hf : T = range f<VAR>fS : ∀ (n : ℕ), f n ∈ S<GOAL>⋃ i, f i = univ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : SecondCountableTopology α<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>h✝ : Nonempty α<VAR>inhabited_h : Inhabited α<VAR>S : Set (Set α) := {s | IsOpen s ∧ μ s < ⊤}<VAR>T : Set (Set α)<VAR>T_count : T.Countable<VAR>TS : T ⊆ S<VAR>hT : ⋃₀ T = univ<VAR>T_ne : T.Nonempty<VAR>f : ℕ → Set α<VAR>hf : T = range f<VAR>fS : ∀ (n : ℕ), f n ∈ S<VAR>x : α<GOAL>x ∈ ⋃ i, f i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : SecondCountableTopology α<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>h✝ : Nonempty α<VAR>inhabited_h : Inhabited α<VAR>S : Set (Set α) := {s | IsOpen s ∧ μ s < ⊤}<VAR>T : Set (Set α)<VAR>T_count : T.Countable<VAR>TS : T ⊆ S<VAR>hT : ⋃₀ T = univ<VAR>T_ne : T.Nonempty<VAR>f : ℕ → Set α<VAR>hf : T = range f<VAR>fS : ∀ (n : ℕ), f n ∈ S<VAR>x : α<VAR>t : Set α<VAR>tT : t ∈ range f<VAR>xt : x ∈ t<GOAL>x ∈ ⋃ i, f i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : SecondCountableTopology α<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>h✝ : Nonempty α<VAR>inhabited_h : Inhabited α<VAR>S : Set (Set α) := {s | IsOpen s ∧ μ s < ⊤}<VAR>T : Set (Set α)<VAR>T_count : T.Countable<VAR>TS : T ⊆ S<VAR>hT : ⋃₀ T = univ<VAR>T_ne : T.Nonempty<VAR>f : ℕ → Set α<VAR>hf : T = range f<VAR>fS : ∀ (n : ℕ), f n ∈ S<VAR>x : α<VAR>n : ℕ<VAR>tT : f n ∈ range f<VAR>xt : x ∈ f n<GOAL>x ∈ ⋃ i, f i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝ : AddCommMonoid M<VAR>k l m n : α<VAR>u v : M<VAR>hu : u ≠ 0<VAR>hv : v ≠ 0<GOAL>single k u + single l v = single m u + single n v ↔ k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u + v = 0 ∧ k = l ∧ m = n
<VAR>R : Type u<VAR>inst✝¹ : Semifield R<VAR>inst✝ : StarRing R<VAR>x y : R<GOAL>star (x / y) = star x / star y
<VAR>R : Type u<VAR>inst✝¹ : Semifield R<VAR>inst✝ : StarRing R<VAR>x y : R<GOAL>op (star (x / y)) = op (star x / star y)
<VAR>α : Type u_1<VAR>inst✝ : EMetricSpace α<VAR>cs : CompleteSpace α<VAR>K : ℝ≥0<VAR>f : α → α<VAR>hf : ContractingWith K f<VAR>x y : α<VAR>h : edist x y ≠ ⊤<VAR>hy : IsFixedPt f y<GOAL>edist x y ≤ edist x (f x) / (1 - ↑K)
<VAR>K : Type u_1<VAR>v : K<VAR>inst✝² : LinearOrderedField K<VAR>inst✝¹ : FloorRing K<VAR>inst✝ : Archimedean K<VAR>ε : K<VAR>ε_pos : ε > 0<GOAL>∃ N, ∀ n ≥ N, |v - (of v).convs n| < ε
<VAR>K : Type u_1<VAR>v : K<VAR>inst✝² : LinearOrderedField K<VAR>inst✝¹ : FloorRing K<VAR>inst✝ : Archimedean K<VAR>ε : K<VAR>ε_pos : ε > 0<VAR>N' : ℕ<VAR>one_div_ε_lt_N' : 1 / ε < ↑N'<GOAL>∃ N, ∀ n ≥ N, |v - (of v).convs n| < ε
<VAR>K : Type u_1<VAR>v : K<VAR>inst✝² : LinearOrderedField K<VAR>inst✝¹ : FloorRing K<VAR>inst✝ : Archimedean K<VAR>ε : K<VAR>ε_pos : ε > 0<VAR>N' : ℕ<VAR>one_div_ε_lt_N' : 1 / ε < ↑N'<VAR>N : ℕ := max N' 5<VAR>n : ℕ<VAR>n_ge_N : n ≥ N<VAR>g : GenContFract K := of v<GOAL>|v - (of v).convs n| < ε
<VAR>K : Type u_1<VAR>v : K<VAR>inst✝² : LinearOrderedField K<VAR>inst✝¹ : FloorRing K<VAR>inst✝ : Archimedean K<VAR>ε : K<VAR>ε_pos : ε > 0<VAR>N' : ℕ<VAR>one_div_ε_lt_N' : 1 / ε < ↑N'<VAR>N : ℕ := max N' 5<VAR>n : ℕ<VAR>n_ge_N : n ≥ N<VAR>g : GenContFract K := of v<VAR>terminatedAt_n : g.TerminatedAt n<GOAL>|v - (of v).convs n| < ε
<VAR>K : Type u_1<VAR>v : K<VAR>inst✝² : LinearOrderedField K<VAR>inst✝¹ : FloorRing K<VAR>inst✝ : Archimedean K<VAR>ε : K<VAR>ε_pos : ε > 0<VAR>N' : ℕ<VAR>one_div_ε_lt_N' : 1 / ε < ↑N'<VAR>N : ℕ := max N' 5<VAR>n : ℕ<VAR>n_ge_N : n ≥ N<VAR>g : GenContFract K := of v<VAR>not_terminatedAt_n : ¬g.TerminatedAt n<GOAL>|v - (of v).convs n| < ε
<VAR>a b m n p : ℕ<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<GOAL>a.factorizationLCMLeft b * a.factorizationLCMRight b = a.lcm b
<VAR>a b m n p : ℕ<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<GOAL>((a.lcm b).factorization.prod fun a_1 b_1 => (if b.factorization a_1 ≤ a.factorization a_1 then a_1 ^ b_1 else 1) * if b.factorization a_1 ≤ a.factorization a_1 then 1 else a_1 ^ b_1) = (a.lcm b).factorization.prod fun x x_1 => x ^ x_1
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>z : K<GOAL>(starRingEnd K) (↑(re z) + ↑(im z) * I) = ↑(re z) - ↑(im z) * I
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Field K<VAR>inst✝ : IsDedekindDomain R<VAR>I : Ideal R<VAR>hI : I.IsPrime<VAR>a b : R<VAR>n : ℕ<VAR>h : a * b ∈ I ^ n<GOAL>a ∈ I ^ n ∨ b ∈ I
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Field K<VAR>inst✝ : IsDedekindDomain R<VAR>I : Ideal R<VAR>hI : I.IsPrime<VAR>a b : R<VAR>n : ℕ<VAR>h : b * a ∈ I ^ n<GOAL>a ∈ I ^ n ∨ b ∈ I
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Field K<VAR>inst✝ : IsDedekindDomain R<VAR>I : Ideal R<VAR>hI : I.IsPrime<VAR>a b : R<VAR>n : ℕ<VAR>h : b * a ∈ I ^ n<GOAL>b ∈ I ∨ a ∈ I ^ n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : CancelCommMonoidWithZero α<VAR>p m : Associates α<VAR>hp : Prime p<VAR>hle : m ≤ p<GOAL>m = 1 ∨ m = p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : CancelCommMonoidWithZero α<VAR>m : Associates α<VAR>p : α<VAR>hp : Prime (Associates.mk p)<VAR>hle : m ≤ Associates.mk p<GOAL>m = 1 ∨ m = Associates.mk p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : CancelCommMonoidWithZero α<VAR>p : α<VAR>hp : Prime (Associates.mk p)<VAR>m : α<VAR>hle : Associates.mk m ≤ Associates.mk p<GOAL>Associates.mk m = 1 ∨ Associates.mk m = Associates.mk p
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝¹ : (i : α) → NormedAddCommGroup (E i)<VAR>ι : Type u_3<VAR>inst✝ : PseudoMetricSpace α<VAR>f : α → ↥(lp (fun i => ℝ) ⊤)<VAR>K : ℝ≥0<GOAL>LipschitzWith K f ↔ ∀ (i : ι), LipschitzWith K fun a => ↑(f a) i
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝¹ : (i : α) → NormedAddCommGroup (E i)<VAR>ι : Type u_3<VAR>inst✝ : PseudoMetricSpace α<VAR>f : α → ↥(lp (fun i => ℝ) ⊤)<VAR>K : ℝ≥0<GOAL>LipschitzOnWith K f Set.univ ↔ ∀ (i : ι), LipschitzOnWith K (fun a => ↑(f a) i) Set.univ
<VAR>C : Type u<VAR>A : Type u_1<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : AddGroup A<VAR>inst✝ : HasShift C A<VAR>X✝ Y : C<VAR>f : X✝ ⟶ Y<VAR>n : A<VAR>X : C<GOAL>(shiftFunctor C (-n)).map ((shiftFunctorCompIsoId C (-n) n ⋯).inv.app X) = (shiftFunctorCompIsoId C n (-n) ⋯).inv.app ((shiftFunctor C (-n)).obj X)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>f g : PadicSeq p<VAR>hfg : ¬f + g ≈ 0<VAR>hf : ¬f ≈ 0<VAR>hg : ¬g ≈ 0<GOAL>padicNorm p (↑(f + g) (stationaryPoint hfg)) ≤ max (padicNorm p (↑f (stationaryPoint hf))) (padicNorm p (↑g (stationaryPoint hg)))
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>f g : PadicSeq p<VAR>hfg : ¬f + g ≈ 0<VAR>hf : ¬f ≈ 0<VAR>hg : ¬g ≈ 0<GOAL>padicNorm p (↑(f + g) (max (stationaryPoint hfg) (max ?v2 ?v3))) ≤ max (padicNorm p (↑f (max ?v1 (max (stationaryPoint hf) ?v3)))) (padicNorm p (↑g (max ?v1 (max ?v2 (stationaryPoint hg)))))
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>f g : PadicSeq p<VAR>hfg : ¬f + g ≈ 0<VAR>hf : ¬f ≈ 0<VAR>hg : ¬g ≈ 0<GOAL>ℕ
<VAR>G : Type u<VAR>inst✝² : Group G<VAR>N : Subgroup G<VAR>nN : N.Normal<VAR>H : Type v<VAR>inst✝¹ : Group H<VAR>M : Type x<VAR>inst✝ : Monoid M<VAR>φ : G →* H<VAR>g : G<GOAL>∃ a, (rangeKerLift φ) a = ⟨φ g, ⋯⟩
<VAR>G : Type u<VAR>inst✝² : Group G<VAR>N : Subgroup G<VAR>nN : N.Normal<VAR>H : Type v<VAR>inst✝¹ : Group H<VAR>M : Type x<VAR>inst✝ : Monoid M<VAR>φ : G →* H<VAR>g : G<GOAL>(rangeKerLift φ) ↑g = ⟨φ g, ⋯⟩
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝¹ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x✝ : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g : ι → α<VAR>inst✝ : TopologicalSpace α<VAR>h : TendstoLocallyUniformlyOn F f p s<VAR>h' : s' ⊆ s<VAR>u : Set (β × β)<VAR>hu : u ∈ 𝓤 β<VAR>x : α<VAR>hx : x ∈ s'<VAR>t : Set α<VAR>ht : t ∈ 𝓝[s] x<VAR>H : ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u<GOAL>∃ t ∈ 𝓝[s'] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u
<VAR>m n b : ℕ<VAR>hm : m ≠ 1<VAR>hn : 0 < n<VAR>hb : log m n < b<VAR>i : ℕ<GOAL>i ∈ Ico 1 ((multiplicity m n).get ⋯ + 1) ↔ i ∈ filter (fun i => m ^ i ∣ n) (Ico 1 b)
<VAR>m n b : ℕ<VAR>hm : m ≠ 1<VAR>hn : 0 < n<VAR>hb : log m n < b<VAR>i : ℕ<GOAL>1 ≤ i ∧ m ^ i ∣ n ↔ (1 ≤ i ∧ m ^ i ∣ n) ∧ i < b
<VAR>m n b : ℕ<VAR>hm : m ≠ 1<VAR>hn : 0 < n<VAR>hb : log m n < b<VAR>i : ℕ<VAR>h : 1 ≤ i ∧ m ^ i ∣ n<GOAL>i ≤ log m n
<VAR>n b : ℕ<VAR>hn : 0 < n<VAR>i m : ℕ<VAR>hm : m + 1 ≠ 1<VAR>hb : log (m + 1) n < b<VAR>h : 1 ≤ i ∧ (m + 1) ^ i ∣ n<GOAL>i ≤ log (m + 1) n
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>a b : α<VAR>s s₁ s₂ t t₁ t₂ u : Set α<VAR>inst✝ : Nontrivial α<VAR>x : α<GOAL>{x}ᶜ.Nonempty
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>a b : α<VAR>s s₁ s₂ t t₁ t₂ u : Set α<VAR>inst✝ : Nontrivial α<VAR>x y : α<VAR>hy : y ≠ x<GOAL>{x}ᶜ.Nonempty
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>inst✝¹⁵ : CommRing R<VAR>inst✝¹⁴ : Nontrivial R<VAR>inst✝¹³ : AddCommGroup M<VAR>inst✝¹² : Module R M<VAR>inst✝¹¹ : Module.Free R M<VAR>inst✝¹⁰ : Module.Finite R M<VAR>inst✝⁹ : AddCommGroup M₁<VAR>inst✝⁸ : Module R M₁<VAR>inst✝⁷ : Module.Finite R M₁<VAR>inst✝⁶ : Module.Free R M₁<VAR>inst✝⁵ : AddCommGroup M₂<VAR>inst✝⁴ : Module R M₂<VAR>inst✝³ : Module.Finite R M₂<VAR>inst✝² : Module.Free R M₂<VAR>f : M →ₗ[R] M<VAR>ι : Type w<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<VAR>b : Basis ι R M<VAR>A : Matrix ι ι R := (toMatrix b b) f<VAR>b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M<VAR>ι' : Type u_2 := ChooseBasisIndex R M<VAR>A' : Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R := (toMatrix b' b') f<VAR>e : ι ≃ ChooseBasisIndex R M := b.indexEquiv b'<VAR>φ : Matrix ι ι R ≃ₗ[R] Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R := reindexLinearEquiv R R e e<VAR>φ₁ : Matrix ι ι' R ≃ₗ[R] Matrix (ChooseBasisIndex R M) ι' R := reindexLinearEquiv R R e (Equiv.refl ι')<VAR>φ₂ : Matrix ι' ι' R ≃ₗ[R] Matrix ι' ι' R := reindexLinearEquiv R R (Equiv.refl ι') (Equiv.refl ι')<VAR>φ₃ : Matrix ι' ι R ≃ₗ[R] Matrix ι' (ChooseBasisIndex R M) R := reindexLinearEquiv R R (Equiv.refl ι') e<VAR>P : Matrix ι (ChooseBasisIndex R M) R := b.toMatrix ⇑b'<VAR>Q : Matrix (ChooseBasisIndex R M) ι R := b'.toMatrix ⇑b<GOAL>((toMatrix b b) f).charpoly = f.charpoly
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>inst✝¹⁵ : CommRing R<VAR>inst✝¹⁴ : Nontrivial R<VAR>inst✝¹³ : AddCommGroup M<VAR>inst✝¹² : Module R M<VAR>inst✝¹¹ : Module.Free R M<VAR>inst✝¹⁰ : Module.Finite R M<VAR>inst✝⁹ : AddCommGroup M₁<VAR>inst✝⁸ : Module R M₁<VAR>inst✝⁷ : Module.Finite R M₁<VAR>inst✝⁶ : Module.Free R M₁<VAR>inst✝⁵ : AddCommGroup M₂<VAR>inst✝⁴ : Module R M₂<VAR>inst✝³ : Module.Finite R M₂<VAR>inst✝² : Module.Free R M₂<VAR>f : M →ₗ[R] M<VAR>ι : Type w<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<VAR>b : Basis ι R M<VAR>A : Matrix ι ι R := (toMatrix b b) f<VAR>b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M<VAR>ι' : Type u_2 := ChooseBasisIndex R M<VAR>A' : Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R := (toMatrix b' b') f<VAR>e : ι ≃ ChooseBasisIndex R M := b.indexEquiv b'<VAR>φ : Matrix ι ι R ≃ₗ[R] Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R := reindexLinearEquiv R R e e<VAR>φ₁ : Matrix ι ι' R ≃ₗ[R] Matrix (ChooseBasisIndex R M) ι' R := reindexLinearEquiv R R e (Equiv.refl ι')<VAR>φ₂ : Matrix ι' ι' R ≃ₗ[R] Matrix ι' ι' R := reindexLinearEquiv R R (Equiv.refl ι') (Equiv.refl ι')<VAR>φ₃ : Matrix ι' ι R ≃ₗ[R] Matrix ι' (ChooseBasisIndex R M) R := reindexLinearEquiv R R (Equiv.refl ι') e<VAR>P : Matrix ι (ChooseBasisIndex R M) R := b.toMatrix ⇑b'<VAR>Q : Matrix (ChooseBasisIndex R M) ι R := b'.toMatrix ⇑b<VAR>hPQ : C.mapMatrix (φ₁ P) * C.mapMatrix (φ₃ Q) = 1<GOAL>((toMatrix b b) f).charpoly = f.charpoly
<VAR>c : Cardinal.{u}<GOAL>𝔠 < lift.{v, u} c ↔ 𝔠 < c
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : DistribLattice α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a✝ a₁ a₂ b✝ b₁ b₂ c✝ x a b c : α<VAR>h : (fun b => [[b, a]]) b = (fun b => [[b, a]]) c<GOAL>b = c