ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹⁵ : CommRing R<VAR>inst✝¹⁴ : CommRing S<VAR>inst✝¹³ : Algebra R S<VAR>M : Type u_1<VAR>inst✝¹² : AddCommGroup M<VAR>inst✝¹¹ : Module R M<VAR>inst✝¹⁰ : Module S M<VAR>inst✝⁹ : IsScalarTower R S M<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝⁸ : CommRing A<VAR>inst✝⁷ : CommRing B<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : Algebra R B<VAR>inst✝⁴ : Algebra A B<VAR>inst✝³ : Algebra S B<VAR>inst✝² : IsScalarTower R A B<VAR>inst✝¹ : IsScalarTower R S B<VAR>inst✝ : SMulCommClass S A B<VAR>h : Function.Surjective ⇑(algebraMap A B)<GOAL>Submodule.span A (Set.range fun x => (Finsupp.mapRange.linearMap (Algebra.linearMap A B) ∘ₗ Finsupp.lmapDomain A A ⇑(algebraMap A B)) (Finsupp.single x.1 1) + (Finsupp.mapRange.linearMap (Algebra.linearMap A B) ∘ₗ Finsupp.lmapDomain A A ⇑(algebraMap A B)) (Finsupp.single x.2 1) - (Finsupp.mapRange.linearMap (Algebra.linearMap A B) ∘ₗ Finsupp.lmapDomain A A ⇑(algebraMap A B)) (Finsupp.single (x.1 + x.2) 1)) ⊔ Submodule.span A (Set.range fun x => (Finsupp.mapRange.linearMap (Algebra.linearMap A B) ∘ₗ Finsupp.lmapDomain A A ⇑(algebraMap A B)) (Finsupp.single x.2 x.1) + (Finsupp.mapRange.linearMap (Algebra.linearMap A B) ∘ₗ Finsupp.lmapDomain A A ⇑(algebraMap A B)) (Finsupp.single x.1 x.2) - (Finsupp.mapRange.linearMap (Algebra.linearMap A B) ∘ₗ Finsupp.lmapDomain A A ⇑(algebraMap A B)) (Finsupp.single (x.1 * x.2) 1)) ⊔ Submodule.span A (Set.range fun x => (Finsupp.mapRange.linearMap (Algebra.linearMap A B) ∘ₗ Finsupp.lmapDomain A A ⇑(algebraMap A B)) (Finsupp.single ((algebraMap R A) x) 1)) ⊔ Submodule.span A (Set.range fun x => Finsupp.single ((algebraMap S B) x) 1) = Submodule.span A (Set.range fun x => Finsupp.single x.1 1 + Finsupp.single x.2 1 - Finsupp.single (x.1 + x.2) 1) ⊔ Submodule.span A (Set.range fun x => Finsupp.single x.2 x.1 + Finsupp.single x.1 x.2 - Finsupp.single (x.1 * x.2) 1) ⊔ Submodule.span A (Set.range fun x => Finsupp.single ((algebraMap S B) x) 1)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹⁵ : CommRing R<VAR>inst✝¹⁴ : CommRing S<VAR>inst✝¹³ : Algebra R S<VAR>M : Type u_1<VAR>inst✝¹² : AddCommGroup M<VAR>inst✝¹¹ : Module R M<VAR>inst✝¹⁰ : Module S M<VAR>inst✝⁹ : IsScalarTower R S M<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝⁸ : CommRing A<VAR>inst✝⁷ : CommRing B<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : Algebra R B<VAR>inst✝⁴ : Algebra A B<VAR>inst✝³ : Algebra S B<VAR>inst✝² : IsScalarTower R A B<VAR>inst✝¹ : IsScalarTower R S B<VAR>inst✝ : SMulCommClass S A B<VAR>h : Function.Surjective ⇑(algebraMap A B)<GOAL>Submodule.span A (Set.range fun x => Finsupp.single ((algebraMap A B) x.1) 1 + Finsupp.single ((algebraMap A B) x.2) 1 - Finsupp.single ((algebraMap A B) x.1 + (algebraMap A B) x.2) 1) ⊔ Submodule.span A (Set.range fun x => Finsupp.single ((algebraMap A B) x.2) ((algebraMap A B) x.1) + Finsupp.single ((algebraMap A B) x.1) ((algebraMap A B) x.2) - Finsupp.single ((algebraMap A B) x.1 * (algebraMap A B) x.2) 1) ⊔ Submodule.span A (Set.range fun x => Finsupp.single ((algebraMap A B) ((algebraMap R A) x)) 1) ⊔ Submodule.span A (Set.range fun x => Finsupp.single ((algebraMap S B) x) 1) = Submodule.span A (Set.range fun x => Finsupp.single x.1 1 + Finsupp.single x.2 1 - Finsupp.single (x.1 + x.2) 1) ⊔ Submodule.span A (Set.range fun x => Finsupp.single x.2 x.1 + Finsupp.single x.1 x.2 - Finsupp.single (x.1 * x.2) 1) ⊔ Submodule.span A (Set.range fun x => Finsupp.single ((algebraMap S B) x) 1)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹⁵ : CommRing R<VAR>inst✝¹⁴ : CommRing S<VAR>inst✝¹³ : Algebra R S<VAR>M : Type u_1<VAR>inst✝¹² : AddCommGroup M<VAR>inst✝¹¹ : Module R M<VAR>inst✝¹⁰ : Module S M<VAR>inst✝⁹ : IsScalarTower R S M<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝⁸ : CommRing A<VAR>inst✝⁷ : CommRing B<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : Algebra R B<VAR>inst✝⁴ : Algebra A B<VAR>inst✝³ : Algebra S B<VAR>inst✝² : IsScalarTower R A B<VAR>inst✝¹ : IsScalarTower R S B<VAR>inst✝ : SMulCommClass S A B<VAR>h : Function.Surjective ⇑(algebraMap A B)<GOAL>Submodule.span A (Set.range fun x => Finsupp.single ((algebraMap A B) x.1) 1 + Finsupp.single ((algebraMap A B) x.2) 1 - Finsupp.single ((algebraMap A B) x.1 + (algebraMap A B) x.2) 1) ⊔ (Submodule.span A (Set.range fun x => Finsupp.single ((algebraMap A B) x.2) ((algebraMap A B) x.1) + Finsupp.single ((algebraMap A B) x.1) ((algebraMap A B) x.2) - Finsupp.single ((algebraMap A B) x.1 * (algebraMap A B) x.2) 1) ⊔ (Submodule.span A (Set.range fun x => Finsupp.single ((algebraMap A B) ((algebraMap R A) x)) 1) ⊔ Submodule.span A (Set.range fun x => Finsupp.single ((algebraMap S B) x) 1))) = Submodule.span A (Set.range ((fun x => Finsupp.single x.1 1 + Finsupp.single x.2 1 - Finsupp.single (x.1 + x.2) 1) ∘ Prod.map ⇑(algebraMap A B) ⇑(algebraMap A B))) ⊔ (Submodule.span A (Set.range ((fun x => Finsupp.single x.2 x.1 + Finsupp.single x.1 x.2 - Finsupp.single (x.1 * x.2) 1) ∘ Prod.map ⇑(algebraMap A B) ⇑(algebraMap A B))) ⊔ Submodule.span A (Set.range fun x => Finsupp.single ((algebraMap S B) x) 1))
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹⁵ : CommRing R<VAR>inst✝¹⁴ : CommRing S<VAR>inst✝¹³ : Algebra R S<VAR>M : Type u_1<VAR>inst✝¹² : AddCommGroup M<VAR>inst✝¹¹ : Module R M<VAR>inst✝¹⁰ : Module S M<VAR>inst✝⁹ : IsScalarTower R S M<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝⁸ : CommRing A<VAR>inst✝⁷ : CommRing B<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : Algebra R B<VAR>inst✝⁴ : Algebra A B<VAR>inst✝³ : Algebra S B<VAR>inst✝² : IsScalarTower R A B<VAR>inst✝¹ : IsScalarTower R S B<VAR>inst✝ : SMulCommClass S A B<VAR>h : Function.Surjective ⇑(algebraMap A B)<GOAL>Submodule.span A (Set.range fun x => Finsupp.single ((algebraMap A B) ((algebraMap R A) x)) 1) ⊔ Submodule.span A (Set.range fun x => Finsupp.single ((algebraMap S B) x) 1) = Submodule.span A (Set.range fun x => Finsupp.single ((algebraMap S B) x) 1)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹⁵ : CommRing R<VAR>inst✝¹⁴ : CommRing S<VAR>inst✝¹³ : Algebra R S<VAR>M : Type u_1<VAR>inst✝¹² : AddCommGroup M<VAR>inst✝¹¹ : Module R M<VAR>inst✝¹⁰ : Module S M<VAR>inst✝⁹ : IsScalarTower R S M<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝⁸ : CommRing A<VAR>inst✝⁷ : CommRing B<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : Algebra R B<VAR>inst✝⁴ : Algebra A B<VAR>inst✝³ : Algebra S B<VAR>inst✝² : IsScalarTower R A B<VAR>inst✝¹ : IsScalarTower R S B<VAR>inst✝ : SMulCommClass S A B<VAR>h : Function.Surjective ⇑(algebraMap A B)<GOAL>Submodule.span A (Set.range fun x => Finsupp.single ((algebraMap R B) x) 1) ⊔ Submodule.span A (Set.range fun x => Finsupp.single ((algebraMap S B) x) 1) = Submodule.span A (Set.range fun x => Finsupp.single ((algebraMap S B) x) 1)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹⁵ : CommRing R<VAR>inst✝¹⁴ : CommRing S<VAR>inst✝¹³ : Algebra R S<VAR>M : Type u_1<VAR>inst✝¹² : AddCommGroup M<VAR>inst✝¹¹ : Module R M<VAR>inst✝¹⁰ : Module S M<VAR>inst✝⁹ : IsScalarTower R S M<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝⁸ : CommRing A<VAR>inst✝⁷ : CommRing B<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : Algebra R B<VAR>inst✝⁴ : Algebra A B<VAR>inst✝³ : Algebra S B<VAR>inst✝² : IsScalarTower R A B<VAR>inst✝¹ : IsScalarTower R S B<VAR>inst✝ : SMulCommClass S A B<VAR>h : Function.Surjective ⇑(algebraMap A B)<GOAL>Submodule.span A (Set.range fun x => Finsupp.single ((algebraMap R B) x) 1) ≤ Submodule.span A (Set.range fun x => Finsupp.single ((algebraMap S B) x) 1)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹⁵ : CommRing R<VAR>inst✝¹⁴ : CommRing S<VAR>inst✝¹³ : Algebra R S<VAR>M : Type u_1<VAR>inst✝¹² : AddCommGroup M<VAR>inst✝¹¹ : Module R M<VAR>inst✝¹⁰ : Module S M<VAR>inst✝⁹ : IsScalarTower R S M<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝⁸ : CommRing A<VAR>inst✝⁷ : CommRing B<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : Algebra R B<VAR>inst✝⁴ : Algebra A B<VAR>inst✝³ : Algebra S B<VAR>inst✝² : IsScalarTower R A B<VAR>inst✝¹ : IsScalarTower R S B<VAR>inst✝ : SMulCommClass S A B<VAR>h : Function.Surjective ⇑(algebraMap A B)<GOAL>(Set.range fun x => Finsupp.single ((algebraMap R B) x) 1) ⊆ Set.range fun x => Finsupp.single ((algebraMap S B) x) 1
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹⁵ : CommRing R<VAR>inst✝¹⁴ : CommRing S<VAR>inst✝¹³ : Algebra R S<VAR>M : Type u_1<VAR>inst✝¹² : AddCommGroup M<VAR>inst✝¹¹ : Module R M<VAR>inst✝¹⁰ : Module S M<VAR>inst✝⁹ : IsScalarTower R S M<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝⁸ : CommRing A<VAR>inst✝⁷ : CommRing B<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : Algebra R B<VAR>inst✝⁴ : Algebra A B<VAR>inst✝³ : Algebra S B<VAR>inst✝² : IsScalarTower R A B<VAR>inst✝¹ : IsScalarTower R S B<VAR>inst✝ : SMulCommClass S A B<VAR>h : Function.Surjective ⇑(algebraMap A B)<GOAL>(Set.range fun x => Finsupp.single ((algebraMap S B) ((algebraMap R S) x)) 1) ⊆ Set.range fun x => Finsupp.single ((algebraMap S B) x) 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : NonAssocSemiring α<VAR>n : ℕ<VAR>x : α<GOAL>Commute (↑n) x
<VAR>p n k : ℕ<VAR>n_big : 2 < n<VAR>p_le_n : p ≤ n<VAR>big : 2 * n < 3 * p<GOAL>n.centralBinom.factorization p = 0
<VAR>p n k : ℕ<VAR>n_big : 2 < n<VAR>p_le_n : p ≤ n<VAR>big : 2 * n < 3 * p<GOAL>p ≠ 2
<VAR>p n k : ℕ<VAR>n_big : 2 < n<VAR>p_le_n : p ≤ n<VAR>big : 2 * n < 3 * p<GOAL>n ≤ 2 * n - n
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>t : Measure α := μ.withDensity (ρ.rnDeriv μ)<GOAL>∀ᵐ (x : α) ∂μ, Tendsto (fun a => ρ a / μ a) (v.filterAt x) (𝓝 (ρ.rnDeriv μ x))
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>t : Measure α := μ.withDensity (ρ.rnDeriv μ)<VAR>eq_add : ρ = ρ.singularPart μ + t<GOAL>∀ᵐ (x : α) ∂μ, Tendsto (fun a => ρ a / μ a) (v.filterAt x) (𝓝 (ρ.rnDeriv μ x))
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>t : Measure α := μ.withDensity (ρ.rnDeriv μ)<VAR>eq_add : ρ = ρ.singularPart μ + t<VAR>A : ∀ᵐ (x : α) ∂μ, Tendsto (fun a => (ρ.singularPart μ) a / μ a) (v.filterAt x) (𝓝 0)<GOAL>∀ᵐ (x : α) ∂μ, Tendsto (fun a => ρ a / μ a) (v.filterAt x) (𝓝 (ρ.rnDeriv μ x))
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>t : Measure α := μ.withDensity (ρ.rnDeriv μ)<VAR>eq_add : ρ = ρ.singularPart μ + t<VAR>A : ∀ᵐ (x : α) ∂μ, Tendsto (fun a => (ρ.singularPart μ) a / μ a) (v.filterAt x) (𝓝 0)<VAR>B : ∀ᵐ (x : α) ∂μ, t.rnDeriv μ x = ρ.rnDeriv μ x<GOAL>∀ᵐ (x : α) ∂μ, Tendsto (fun a => ρ a / μ a) (v.filterAt x) (𝓝 (ρ.rnDeriv μ x))
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>t : Measure α := μ.withDensity (ρ.rnDeriv μ)<VAR>eq_add : ρ = ρ.singularPart μ + t<VAR>A : ∀ᵐ (x : α) ∂μ, Tendsto (fun a => (ρ.singularPart μ) a / μ a) (v.filterAt x) (𝓝 0)<VAR>B : ∀ᵐ (x : α) ∂μ, t.rnDeriv μ x = ρ.rnDeriv μ x<VAR>C : ∀ᵐ (x : α) ∂μ, Tendsto (fun a => t a / μ a) (v.filterAt x) (𝓝 (t.rnDeriv μ x))<GOAL>∀ᵐ (x : α) ∂μ, Tendsto (fun a => ρ a / μ a) (v.filterAt x) (𝓝 (ρ.rnDeriv μ x))
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>t : Measure α := μ.withDensity (ρ.rnDeriv μ)<VAR>eq_add : ρ = ρ.singularPart μ + t<VAR>A : ∀ᵐ (x : α) ∂μ, Tendsto (fun a => (ρ.singularPart μ) a / μ a) (v.filterAt x) (𝓝 0)<VAR>B : ∀ᵐ (x : α) ∂μ, t.rnDeriv μ x = ρ.rnDeriv μ x<VAR>C : ∀ᵐ (x : α) ∂μ, Tendsto (fun a => t a / μ a) (v.filterAt x) (𝓝 (t.rnDeriv μ x))<VAR>a✝ : α<VAR>Ax : Tendsto (fun a => (ρ.singularPart μ) a / μ a) (v.filterAt a✝) (𝓝 0)<VAR>Bx : t.rnDeriv μ a✝ = ρ.rnDeriv μ a✝<VAR>Cx : Tendsto (fun a => t a / μ a) (v.filterAt a✝) (𝓝 (t.rnDeriv μ a✝))<GOAL>Tendsto (fun a => ρ a / μ a) (v.filterAt a✝) (𝓝 (ρ.rnDeriv μ a✝))
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>t : Measure α := μ.withDensity (ρ.rnDeriv μ)<VAR>eq_add : ρ = ρ.singularPart μ + t<VAR>A : ∀ᵐ (x : α) ∂μ, Tendsto (fun a => (ρ.singularPart μ) a / μ a) (v.filterAt x) (𝓝 0)<VAR>B : ∀ᵐ (x : α) ∂μ, t.rnDeriv μ x = ρ.rnDeriv μ x<VAR>C : ∀ᵐ (x : α) ∂μ, Tendsto (fun a => t a / μ a) (v.filterAt x) (𝓝 (t.rnDeriv μ x))<VAR>a✝ : α<VAR>Ax : Tendsto (fun a => (ρ.singularPart μ) a / μ a) (v.filterAt a✝) (𝓝 0)<VAR>Bx : t.rnDeriv μ a✝ = ρ.rnDeriv μ a✝<VAR>Cx : Tendsto (fun a => t a / μ a) (v.filterAt a✝) (𝓝 (t.rnDeriv μ a✝))<GOAL>(fun a => ρ a / μ a) = fun x => (ρ.singularPart μ) x / μ x + t x / μ x
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>t : Measure α := μ.withDensity (ρ.rnDeriv μ)<VAR>eq_add : ρ = ρ.singularPart μ + t<VAR>A : ∀ᵐ (x : α) ∂μ, Tendsto (fun a => (ρ.singularPart μ) a / μ a) (v.filterAt x) (𝓝 0)<VAR>B : ∀ᵐ (x : α) ∂μ, t.rnDeriv μ x = ρ.rnDeriv μ x<VAR>C : ∀ᵐ (x : α) ∂μ, Tendsto (fun a => t a / μ a) (v.filterAt x) (𝓝 (t.rnDeriv μ x))<VAR>a✝ : α<VAR>Ax : Tendsto (fun a => (ρ.singularPart μ) a / μ a) (v.filterAt a✝) (𝓝 0)<VAR>Bx : t.rnDeriv μ a✝ = ρ.rnDeriv μ a✝<VAR>Cx : Tendsto (fun a => t a / μ a) (v.filterAt a✝) (𝓝 (t.rnDeriv μ a✝))<GOAL>𝓝 (ρ.rnDeriv μ a✝) = 𝓝 (0 + t.rnDeriv μ a✝)
<VAR>f g : CircleDeg1Lift<VAR>x : ℝ<VAR>m : ℤ<VAR>n : ℕ<VAR>hn : 0 < n<GOAL>(⇑f)^[n] x < x + ↑n * ↑m ↔ f x < x + ↑m
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>P : WeakFEPair E<VAR>x : ℝ<VAR>hx : 0 < x<GOAL>(fun x => P.f_modif x - P.f x + P.f₀) x = (((Ioo 0 1).indicator fun x => P.f₀ - (P.ε * ↑(x ^ (-P.k))) • P.g₀) + {1}.indicator fun x => P.f₀ - P.f 1) x
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>P : WeakFEPair E<VAR>x : ℝ<VAR>hx : 0 < x<GOAL>(Ioi 1).indicator (fun x => P.f x - P.f₀) x + (Ioo 0 1).indicator (fun x => P.f x - (P.ε * ↑(x ^ (-P.k))) • P.g₀) x - P.f x + P.f₀ = (Ioo 0 1).indicator (fun x => P.f₀ - (P.ε * ↑(x ^ (-P.k))) • P.g₀) x + {1}.indicator (fun x => P.f₀ - P.f 1) x
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>P : WeakFEPair E<VAR>x : ℝ<VAR>hx : 0 < x<VAR>hx' : x < 1<GOAL>(Ioi 1).indicator (fun x => P.f x - P.f₀) x + (Ioo 0 1).indicator (fun x => P.f x - (P.ε * ↑(x ^ (-P.k))) • P.g₀) x - P.f x + P.f₀ = (Ioo 0 1).indicator (fun x => P.f₀ - (P.ε * ↑(x ^ (-P.k))) • P.g₀) x + {1}.indicator (fun x => P.f₀ - P.f 1) x
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>P : WeakFEPair E<VAR>hx : 0 < 1<GOAL>(Ioi 1).indicator (fun x => P.f x - P.f₀) 1 + (Ioo 0 1).indicator (fun x => P.f x - (P.ε * ↑(x ^ (-P.k))) • P.g₀) 1 - P.f 1 + P.f₀ = (Ioo 0 1).indicator (fun x => P.f₀ - (P.ε * ↑(x ^ (-P.k))) • P.g₀) 1 + {1}.indicator (fun x => P.f₀ - P.f 1) 1
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>P : WeakFEPair E<VAR>x : ℝ<VAR>hx : 0 < x<VAR>hx' : 1 < x<GOAL>(Ioi 1).indicator (fun x => P.f x - P.f₀) x + (Ioo 0 1).indicator (fun x => P.f x - (P.ε * ↑(x ^ (-P.k))) • P.g₀) x - P.f x + P.f₀ = (Ioo 0 1).indicator (fun x => P.f₀ - (P.ε * ↑(x ^ (-P.k))) • P.g₀) x + {1}.indicator (fun x => P.f₀ - P.f 1) x
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : LieRing L<VAR>inst✝⁹ : LieAlgebra R L<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : LieRingModule L M<VAR>inst✝⁵ : LieModule R L M<VAR>k : ℕ<VAR>N : LieSubmodule R L M<VAR>M₂ : Type w₁<VAR>inst✝⁴ : AddCommGroup M₂<VAR>inst✝³ : Module R M₂<VAR>inst✝² : LieRingModule L M₂<VAR>inst✝¹ : LieModule R L M₂<VAR>inst✝ : IsNilpotent R L M<VAR>x y : L<GOAL>_root_.IsNilpotent ((toEnd R L M) x ∘ₗ (toEnd R L M) y)
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : LieRing L<VAR>inst✝⁹ : LieAlgebra R L<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : LieRingModule L M<VAR>inst✝⁵ : LieModule R L M<VAR>k✝ : ℕ<VAR>N : LieSubmodule R L M<VAR>M₂ : Type w₁<VAR>inst✝⁴ : AddCommGroup M₂<VAR>inst✝³ : Module R M₂<VAR>inst✝² : LieRingModule L M₂<VAR>inst✝¹ : LieModule R L M₂<VAR>inst✝ : IsNilpotent R L M<VAR>x y : L<VAR>k : ℕ<VAR>hM : lowerCentralSeries R L M k = ⊥<GOAL>_root_.IsNilpotent ((toEnd R L M) x ∘ₗ (toEnd R L M) y)
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : LieRing L<VAR>inst✝⁹ : LieAlgebra R L<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : LieRingModule L M<VAR>inst✝⁵ : LieModule R L M<VAR>k✝ : ℕ<VAR>N : LieSubmodule R L M<VAR>M₂ : Type w₁<VAR>inst✝⁴ : AddCommGroup M₂<VAR>inst✝³ : Module R M₂<VAR>inst✝² : LieRingModule L M₂<VAR>inst✝¹ : LieModule R L M₂<VAR>inst✝ : IsNilpotent R L M<VAR>x y : L<VAR>k : ℕ<VAR>hM : lowerCentralSeries R L M (2 * k) = ⊥<GOAL>_root_.IsNilpotent ((toEnd R L M) x ∘ₗ (toEnd R L M) y)
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : LieRing L<VAR>inst✝⁹ : LieAlgebra R L<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : LieRingModule L M<VAR>inst✝⁵ : LieModule R L M<VAR>k✝ : ℕ<VAR>N : LieSubmodule R L M<VAR>M₂ : Type w₁<VAR>inst✝⁴ : AddCommGroup M₂<VAR>inst✝³ : Module R M₂<VAR>inst✝² : LieRingModule L M₂<VAR>inst✝¹ : LieModule R L M₂<VAR>inst✝ : IsNilpotent R L M<VAR>x y : L<VAR>k : ℕ<VAR>hM : lowerCentralSeries R L M (2 * k) = ⊥<GOAL>((toEnd R L M) x ∘ₗ (toEnd R L M) y) ^ k = 0
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : LieRing L<VAR>inst✝⁹ : LieAlgebra R L<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : LieRingModule L M<VAR>inst✝⁵ : LieModule R L M<VAR>k✝ : ℕ<VAR>N : LieSubmodule R L M<VAR>M₂ : Type w₁<VAR>inst✝⁴ : AddCommGroup M₂<VAR>inst✝³ : Module R M₂<VAR>inst✝² : LieRingModule L M₂<VAR>inst✝¹ : LieModule R L M₂<VAR>inst✝ : IsNilpotent R L M<VAR>x y : L<VAR>k : ℕ<VAR>hM : lowerCentralSeries R L M (2 * k) = ⊥<VAR>m : M<GOAL>(((toEnd R L M) x ∘ₗ (toEnd R L M) y) ^ k) m = 0 m
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : LieRing L<VAR>inst✝⁹ : LieAlgebra R L<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : LieRingModule L M<VAR>inst✝⁵ : LieModule R L M<VAR>k✝ : ℕ<VAR>N : LieSubmodule R L M<VAR>M₂ : Type w₁<VAR>inst✝⁴ : AddCommGroup M₂<VAR>inst✝³ : Module R M₂<VAR>inst✝² : LieRingModule L M₂<VAR>inst✝¹ : LieModule R L M₂<VAR>inst✝ : IsNilpotent R L M<VAR>x y : L<VAR>k : ℕ<VAR>hM : lowerCentralSeries R L M (2 * k) = ⊥<VAR>m : M<GOAL>(⇑((toEnd R L M) x ∘ₗ (toEnd R L M) y))^[k] m ∈ lowerCentralSeries R L M (2 * k)
<VAR>α : Type u_1<VAR>inst✝ : OrderedAddCommGroup α<VAR>a b c : α<GOAL>(fun x => x - a) ⁻¹' Iio b = Iio (b + a)
<VAR>Fq : Type u_1<VAR>inst✝¹ : Fintype Fq<VAR>inst✝ : Ring Fq<VAR>d m : ℕ<VAR>hm : Fintype.card Fq ^ d ≤ m<VAR>b : Fq[X]<VAR>A : Fin m.succ → Fq[X]<VAR>hA : ∀ (i : Fin m.succ), (A i).degree < b.degree<GOAL>∃ i₀ i₁, i₀ ≠ i₁ ∧ (A i₁ - A i₀).degree < ↑(b.natDegree - d)
<VAR>Fq : Type u_1<VAR>inst✝¹ : Fintype Fq<VAR>inst✝ : Ring Fq<VAR>d m : ℕ<VAR>hm : Fintype.card Fq ^ d ≤ m<VAR>b : Fq[X]<VAR>A : Fin m.succ → Fq[X]<VAR>hA : ∀ (i : Fin m.succ), (A i).degree < b.degree<VAR>hb : b ≠ 0<GOAL>∃ i₀ i₁, i₀ ≠ i₁ ∧ (A i₁ - A i₀).degree < ↑(b.natDegree - d)
<VAR>Fq : Type u_1<VAR>inst✝¹ : Fintype Fq<VAR>inst✝ : Ring Fq<VAR>d m : ℕ<VAR>hm : Fintype.card Fq ^ d ≤ m<VAR>b : Fq[X]<VAR>A : Fin m.succ → Fq[X]<VAR>hA : ∀ (i : Fin m.succ), (A i).degree < b.degree<VAR>hb : b ≠ 0<VAR>f : Fin m.succ → Fin d → Fq := fun i j => (A i).coeff (b.natDegree - ↑j.succ)<GOAL>∃ i₀ i₁, i₀ ≠ i₁ ∧ (A i₁ - A i₀).degree < ↑(b.natDegree - d)
<VAR>Fq : Type u_1<VAR>inst✝¹ : Fintype Fq<VAR>inst✝ : Ring Fq<VAR>d m : ℕ<VAR>hm : Fintype.card Fq ^ d ≤ m<VAR>b : Fq[X]<VAR>A : Fin m.succ → Fq[X]<VAR>hA : ∀ (i : Fin m.succ), (A i).degree < b.degree<VAR>hb : b ≠ 0<VAR>f : Fin m.succ → Fin d → Fq := fun i j => (A i).coeff (b.natDegree - ↑j.succ)<VAR>this : Fintype.card (Fin d → Fq) < Fintype.card (Fin m.succ)<GOAL>∃ i₀ i₁, i₀ ≠ i₁ ∧ (A i₁ - A i₀).degree < ↑(b.natDegree - d)
<VAR>Fq : Type u_1<VAR>inst✝¹ : Fintype Fq<VAR>inst✝ : Ring Fq<VAR>d m : ℕ<VAR>hm : Fintype.card Fq ^ d ≤ m<VAR>b : Fq[X]<VAR>A : Fin m.succ → Fq[X]<VAR>hA : ∀ (i : Fin m.succ), (A i).degree < b.degree<VAR>hb : b ≠ 0<VAR>f : Fin m.succ → Fin d → Fq := fun i j => (A i).coeff (b.natDegree - ↑j.succ)<VAR>this : Fintype.card (Fin d → Fq) < Fintype.card (Fin m.succ)<VAR>i₀ i₁ : Fin m.succ<VAR>i_ne : i₀ ≠ i₁<VAR>i_eq : f i₀ = f i₁<GOAL>∃ i₀ i₁, i₀ ≠ i₁ ∧ (A i₁ - A i₀).degree < ↑(b.natDegree - d)
<VAR>Fq : Type u_1<VAR>inst✝¹ : Fintype Fq<VAR>inst✝ : Ring Fq<VAR>d m : ℕ<VAR>hm : Fintype.card Fq ^ d ≤ m<VAR>b : Fq[X]<VAR>A : Fin m.succ → Fq[X]<VAR>hA : ∀ (i : Fin m.succ), (A i).degree < b.degree<VAR>hb : b ≠ 0<VAR>f : Fin m.succ → Fin d → Fq := fun i j => (A i).coeff (b.natDegree - ↑j.succ)<VAR>this : Fintype.card (Fin d → Fq) < Fintype.card (Fin m.succ)<VAR>i₀ i₁ : Fin m.succ<VAR>i_ne : i₀ ≠ i₁<VAR>i_eq : f i₀ = f i₁<GOAL>(A i₁ - A i₀).degree < ↑(b.natDegree - d)
<VAR>Fq : Type u_1<VAR>inst✝¹ : Fintype Fq<VAR>inst✝ : Ring Fq<VAR>d m : ℕ<VAR>hm : Fintype.card Fq ^ d ≤ m<VAR>b : Fq[X]<VAR>A : Fin m.succ → Fq[X]<VAR>hA : ∀ (i : Fin m.succ), (A i).degree < b.degree<VAR>hb : b ≠ 0<VAR>f : Fin m.succ → Fin d → Fq := fun i j => (A i).coeff (b.natDegree - ↑j.succ)<VAR>this : Fintype.card (Fin d → Fq) < Fintype.card (Fin m.succ)<VAR>i₀ i₁ : Fin m.succ<VAR>i_ne : i₀ ≠ i₁<VAR>i_eq : f i₀ = f i₁<VAR>j : ℕ<VAR>hj : b.natDegree - d ≤ j<GOAL>(A i₁ - A i₀).coeff j = 0
<VAR>Fq : Type u_1<VAR>inst✝¹ : Fintype Fq<VAR>inst✝ : Ring Fq<VAR>d m : ℕ<VAR>hm : Fintype.card Fq ^ d ≤ m<VAR>b : Fq[X]<VAR>A : Fin m.succ → Fq[X]<VAR>hA : ∀ (i : Fin m.succ), (A i).degree < b.degree<VAR>hb : b ≠ 0<VAR>f : Fin m.succ → Fin d → Fq := fun i j => (A i).coeff (b.natDegree - ↑j.succ)<VAR>this : Fintype.card (Fin d → Fq) < Fintype.card (Fin m.succ)<VAR>i₀ i₁ : Fin m.succ<VAR>i_ne : i₀ ≠ i₁<VAR>i_eq : f i₀ = f i₁<VAR>j : ℕ<VAR>hj : b.natDegree - d ≤ j<VAR>hbj : ¬b.degree ≤ ↑j<GOAL>(A i₁ - A i₀).coeff j = 0
<VAR>Fq : Type u_1<VAR>inst✝¹ : Fintype Fq<VAR>inst✝ : Ring Fq<VAR>d m : ℕ<VAR>hm : Fintype.card Fq ^ d ≤ m<VAR>b : Fq[X]<VAR>A : Fin m.succ → Fq[X]<VAR>hA : ∀ (i : Fin m.succ), (A i).degree < b.degree<VAR>hb : b ≠ 0<VAR>f : Fin m.succ → Fin d → Fq := fun i j => (A i).coeff (b.natDegree - ↑j.succ)<VAR>this : Fintype.card (Fin d → Fq) < Fintype.card (Fin m.succ)<VAR>i₀ i₁ : Fin m.succ<VAR>i_ne : i₀ ≠ i₁<VAR>i_eq : f i₀ = f i₁<VAR>j : ℕ<VAR>hj : b.natDegree - d ≤ j<VAR>hbj : ¬b.degree ≤ ↑j<GOAL>(A i₁).coeff j = (A i₀).coeff j