ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝¹³ : CommRing R<VAR>inst✝¹² : Field K<VAR>inst✝¹¹ : Field L<VAR>inst✝¹⁰ : DecidableEq L<VAR>inst✝⁹ : Algebra R K<VAR>inst✝⁸ : IsFractionRing R K<VAR>inst✝⁷ : Algebra K L<VAR>inst✝⁶ : FiniteDimensional K L<VAR>inst✝⁵ : Algebra R L<VAR>inst✝⁴ : IsScalarTower R K L<VAR>inst✝³ : IsDomain R<VAR>K' : Type u_4<VAR>inst✝² : Field K'<VAR>inst✝¹ : Algebra R K'<VAR>inst✝ : IsFractionRing R K'<VAR>I : (FractionalIdeal R⁰ K)ˣ<GOAL>mk ((Units.map ↑(canonicalEquiv R⁰ K K')) I) = mk I
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝¹³ : CommRing R<VAR>inst✝¹² : Field K<VAR>inst✝¹¹ : Field L<VAR>inst✝¹⁰ : DecidableEq L<VAR>inst✝⁹ : Algebra R K<VAR>inst✝⁸ : IsFractionRing R K<VAR>inst✝⁷ : Algebra K L<VAR>inst✝⁶ : FiniteDimensional K L<VAR>inst✝⁵ : Algebra R L<VAR>inst✝⁴ : IsScalarTower R K L<VAR>inst✝³ : IsDomain R<VAR>K' : Type u_4<VAR>inst✝² : Field K'<VAR>inst✝¹ : Algebra R K'<VAR>inst✝ : IsFractionRing R K'<VAR>I : (FractionalIdeal R⁰ K)ˣ<GOAL>(QuotientGroup.mk' (toPrincipalIdeal R (FractionRing R)).range) ((Units.map ↑(canonicalEquiv R⁰ K (FractionRing R))) I) = mk I
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>inst✝¹ : HasCoequalizer f g<VAR>X' Y' Z : C<VAR>f' g' : X' ⟶ Y'<VAR>inst✝ : HasCoequalizer f' g'<VAR>p : X ⟶ X'<VAR>q : Y ⟶ Y'<VAR>wf : f ≫ q = p ≫ f'<VAR>wg : g ≫ q = p ≫ g'<VAR>h : Y' ⟶ Z<VAR>wh : f' ≫ h = g' ≫ h<GOAL>π f g ≫ colimMap (parallelPairHom f g f' g' p q wf wg) ≫ desc h wh = q ≫ h
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>κ : Kernel α β<VAR>η : Kernel (α × β) γ<VAR>a : α<VAR>E : Type u_4<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>inst✝ : IsSFiniteKernel η<VAR>f : γ × β → E<VAR>hf : StronglyMeasurable f<GOAL>StronglyMeasurable ((fun y => ∫ (x : γ), (fun u => f (u.1, u.2.2)) (x, y) ∂η y) ∘ fun x => (a, x))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>κ : Kernel α β<VAR>η : Kernel (α × β) γ<VAR>a : α<VAR>E : Type u_4<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>inst✝ : IsSFiniteKernel η<VAR>f : γ × β → E<VAR>hf : StronglyMeasurable f<GOAL>StronglyMeasurable fun y => ∫ (x : γ), (fun u => f (u.1, u.2.2)) (x, y) ∂η y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁵ : OrderedSemiring 𝕜<VAR>inst✝⁴ : AddCommMonoid E<VAR>inst✝³ : AddCommMonoid F<VAR>inst✝² : OrderedAddCommGroup β<VAR>inst✝¹ : SMul 𝕜 E<VAR>inst✝ : Module 𝕜 β<VAR>s : Set E<VAR>f g : E → β<GOAL>StrictConcaveOn 𝕜 s (-f) ↔ StrictConvexOn 𝕜 s f
<VAR>v : PrimeMultiset<VAR>p : ℕ<VAR>h : p ∈ v.toNatMultiset<GOAL>Nat.Prime p
<VAR>v : PrimeMultiset<VAR>p : ℕ<VAR>h : p ∈ v.toNatMultiset<VAR>val✝ : ℕ<VAR>hp' : Nat.Prime val✝<VAR>left✝ : ⟨val✝, hp'⟩ ∈ v<VAR>h_eq : Coe.coe ⟨val✝, hp'⟩ = p<GOAL>Nat.Prime p
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasZeroMorphisms C<VAR>inst✝¹ : HasZeroObject C<VAR>ι : Type u_1<VAR>inst✝ : DecidableEq ι<VAR>c : ComplexShape ι<VAR>j : ι<VAR>A B : C<VAR>f : A ⟶ B<GOAL>(singleObjOpcyclesSelfIso c j A).hom ≫ opcyclesMap ((single C c j).map f) j = f ≫ (singleObjOpcyclesSelfIso c j B).hom
<VAR>u v a b c d : ℤ<VAR>ha : IsUnit a<VAR>hb : IsUnit b<VAR>hc : IsUnit c<VAR>hd : IsUnit d<GOAL>a + b = c + d ↔ a = c ∧ b = d ∨ a = d ∧ b = c
<VAR>u v a b c d : ℤ<VAR>ha : a = 1 ∨ a = -1<VAR>hb : b = 1 ∨ b = -1<VAR>hc : c = 1 ∨ c = -1<VAR>hd : d = 1 ∨ d = -1<GOAL>a + b = c + d ↔ a = c ∧ b = d ∨ a = d ∧ b = c
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ✝ μ : Measure α<VAR>inst✝ : SFinite μ<VAR>n : ℕ<GOAL>sFiniteSeq μ n ≪ μ.toFiniteAux
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ✝ μ : Measure α<VAR>inst✝ : SFinite μ<VAR>n : ℕ<GOAL>(2 ^ (n + 1) * (sFiniteSeq μ n) Set.univ)⁻¹ ≠ 0
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ✝ μ : Measure α<VAR>inst✝ : SFinite μ<VAR>n : ℕ<GOAL>¬2 ^ (n + 1) * (sFiniteSeq μ n) Set.univ = ⊤
<VAR>α : Type u_1<VAR>E' : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>𝕜 : Type u_5<VAR>p : ℝ≥0∞<VAR>inst✝¹¹ : RCLike 𝕜<VAR>inst✝¹⁰ : NormedAddCommGroup E'<VAR>inst✝⁹ : InnerProductSpace 𝕜 E'<VAR>inst✝⁸ : CompleteSpace E'<VAR>inst✝⁷ : NormedSpace ℝ E'<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>inst✝⁴ : NormedAddCommGroup F'<VAR>inst✝³ : NormedSpace 𝕜 F'<VAR>inst✝² : NormedSpace ℝ F'<VAR>inst✝¹ : CompleteSpace F'<VAR>ι : Type u_6<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hp : Fact (1 ≤ p)<VAR>inst✝ : CompleteSpace F<VAR>hm : m ≤ m0<GOAL>IsComplete {f | AEStronglyMeasurable' m (↑↑f) μ}
<VAR>α : Type u_1<VAR>E' : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>𝕜 : Type u_5<VAR>p : ℝ≥0∞<VAR>inst✝¹¹ : RCLike 𝕜<VAR>inst✝¹⁰ : NormedAddCommGroup E'<VAR>inst✝⁹ : InnerProductSpace 𝕜 E'<VAR>inst✝⁸ : CompleteSpace E'<VAR>inst✝⁷ : NormedSpace ℝ E'<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>inst✝⁴ : NormedAddCommGroup F'<VAR>inst✝³ : NormedSpace 𝕜 F'<VAR>inst✝² : NormedSpace ℝ F'<VAR>inst✝¹ : CompleteSpace F'<VAR>ι : Type u_6<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hp : Fact (1 ≤ p)<VAR>inst✝ : CompleteSpace F<VAR>hm : m ≤ m0<GOAL>CompleteSpace ↑{f | AEStronglyMeasurable' m (↑↑f) μ}
<VAR>R : Type u_1<VAR>inst✝ : CommMonoidWithZero R<VAR>n✝ p : R<VAR>k n : ℕ<GOAL>IsPrimePow n ↔ ∃! p, Nat.Prime p ∧ p ∣ n
<VAR>R : Type u_1<VAR>inst✝ : CommMonoidWithZero R<VAR>n✝ p : R<VAR>k n : ℕ<GOAL>(∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n) ↔ ∃! p, Nat.Prime p ∧ p ∣ n
<VAR>R : Type u_1<VAR>inst✝ : CommMonoidWithZero R<VAR>n✝ p✝ : R<VAR>k n p : ℕ<VAR>hq : ∀ (y : ℕ), (fun p => Nat.Prime p ∧ p ∣ n) y → y = p<VAR>hp : Nat.Prime p<VAR>hn : p ∣ n<GOAL>∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
<VAR>R : Type u_1<VAR>inst✝ : CommMonoidWithZero R<VAR>n p✝ : R<VAR>k p : ℕ<VAR>hp : Nat.Prime p<VAR>hq : ∀ (y : ℕ), (fun p => Nat.Prime p ∧ p ∣ 0) y → y = p<VAR>hn : p ∣ 0<GOAL>∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = 0
<VAR>R : Type u_1<VAR>inst✝ : CommMonoidWithZero R<VAR>n✝ p✝ : R<VAR>k n p : ℕ<VAR>hq : ∀ (y : ℕ), (fun p => Nat.Prime p ∧ p ∣ n) y → y = p<VAR>hp : Nat.Prime p<VAR>hn : p ∣ n<VAR>hn₀ : n ≠ 0<GOAL>∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
<VAR>R : Type u_1<VAR>inst✝ : CommMonoidWithZero R<VAR>n✝ p✝ : R<VAR>k n p : ℕ<VAR>hq : ∀ (y : ℕ), (fun p => Nat.Prime p ∧ p ∣ n) y → y = p<VAR>hp : Nat.Prime p<VAR>hn : p ∣ n<VAR>hn₀ : n ≠ 0<GOAL>p ^ n.factorization p = n
<VAR>R : Type u_1<VAR>inst✝ : CommMonoidWithZero R<VAR>n✝ p✝ : R<VAR>k n p : ℕ<VAR>hp : Nat.Prime p<VAR>hn : p ∣ n<VAR>hn₀ : n ≠ 0<VAR>hq : ∀ (y : ℕ), Nat.Prime y → y ∣ n → y = p<GOAL>p ^ n.factorization p = n
<VAR>R : Type u_1<VAR>inst✝ : CommMonoidWithZero R<VAR>n✝ p✝ : R<VAR>k n p : ℕ<VAR>hp : Nat.Prime p<VAR>hn : p ∣ n<VAR>hn₀ : n ≠ 0<VAR>hq : ∀ (y : ℕ), Nat.Prime y → y ∣ n → y = p<GOAL>n ∣ p ^ n.factorization p
<VAR>R : Type u_1<VAR>inst✝ : CommMonoidWithZero R<VAR>n✝ p✝ : R<VAR>k n p : ℕ<VAR>hp : Nat.Prime p<VAR>hn : p ∣ n<VAR>hn₀ : n ≠ 0<VAR>hq : ∀ (y : ℕ), Nat.Prime y → y ∣ n → y = p<GOAL>n.primeFactorsList.Subperm (p ^ n.factorization p).primeFactorsList
<VAR>R : Type u_1<VAR>inst✝ : CommMonoidWithZero R<VAR>n✝ p✝ : R<VAR>k n p : ℕ<VAR>hp : Nat.Prime p<VAR>hn : p ∣ n<VAR>hn₀ : n ≠ 0<VAR>hq : ∀ (y : ℕ), Nat.Prime y → y ∣ n → y = p<GOAL>∀ x ∈ n.primeFactorsList, List.count x n.primeFactorsList ≤ List.count x (List.replicate (n.factorization p) p)
<VAR>R : Type u_1<VAR>inst✝ : CommMonoidWithZero R<VAR>n✝ p✝ : R<VAR>k n p : ℕ<VAR>hp : Nat.Prime p<VAR>hn : p ∣ n<VAR>hn₀ : n ≠ 0<VAR>hq : ∀ (y : ℕ), Nat.Prime y → y ∣ n → y = p<VAR>q : ℕ<VAR>hq' : q ∈ n.primeFactorsList<GOAL>List.count q n.primeFactorsList ≤ List.count q (List.replicate (n.factorization p) p)
<VAR>R : Type u_1<VAR>inst✝ : CommMonoidWithZero R<VAR>n✝ p✝ : R<VAR>k n p : ℕ<VAR>hp : Nat.Prime p<VAR>hn : p ∣ n<VAR>hn₀ : n ≠ 0<VAR>hq : ∀ (y : ℕ), Nat.Prime y → y ∣ n → y = p<VAR>q : ℕ<VAR>hq' : Nat.Prime q ∧ q ∣ n<GOAL>List.count q n.primeFactorsList ≤ List.count q (List.replicate (n.factorization p) p)
<VAR>R : Type u_1<VAR>inst✝ : CommMonoidWithZero R<VAR>n✝ p✝ : R<VAR>k n p : ℕ<VAR>hp : Nat.Prime p<VAR>hn : p ∣ n<VAR>hn₀ : n ≠ 0<VAR>hq : ∀ (y : ℕ), Nat.Prime y → y ∣ n → y = p<VAR>hq' : Nat.Prime p ∧ p ∣ n<GOAL>List.count p n.primeFactorsList ≤ List.count p (List.replicate (n.factorization p) p)
<VAR>G : Type u_1<VAR>inst✝⁷ : CommGroup G<VAR>inst✝⁶ : TopologicalSpace G<VAR>inst✝⁵ : TopologicalGroup G<VAR>inst✝⁴ : MeasurableSpace G<VAR>inst✝³ : BorelSpace G<VAR>μ : Measure G<VAR>inst✝² : μ.IsHaarMeasure<VAR>inst✝¹ : CompactSpace G<VAR>inst✝ : RootableBy G ℤ<VAR>n : ℤ<VAR>hn : n ≠ 0<VAR>f : G →* G := zpowGroupHom n<GOAL>map (fun g => g ^ n) μ = μ
<VAR>G : Type u_1<VAR>inst✝⁷ : CommGroup G<VAR>inst✝⁶ : TopologicalSpace G<VAR>inst✝⁵ : TopologicalGroup G<VAR>inst✝⁴ : MeasurableSpace G<VAR>inst✝³ : BorelSpace G<VAR>μ : Measure G<VAR>inst✝² : μ.IsHaarMeasure<VAR>inst✝¹ : CompactSpace G<VAR>inst✝ : RootableBy G ℤ<VAR>n : ℤ<VAR>hn : n ≠ 0<VAR>f : G →* G := zpowGroupHom n<VAR>hf : Continuous ⇑f<GOAL>map (fun g => g ^ n) μ = μ
<VAR>G : Type u_1<VAR>inst✝⁷ : CommGroup G<VAR>inst✝⁶ : TopologicalSpace G<VAR>inst✝⁵ : TopologicalGroup G<VAR>inst✝⁴ : MeasurableSpace G<VAR>inst✝³ : BorelSpace G<VAR>μ : Measure G<VAR>inst✝² : μ.IsHaarMeasure<VAR>inst✝¹ : CompactSpace G<VAR>inst✝ : RootableBy G ℤ<VAR>n : ℤ<VAR>hn : n ≠ 0<VAR>f : G →* G := zpowGroupHom n<VAR>hf : Continuous ⇑f<VAR>this : (map (⇑f) μ).IsHaarMeasure<GOAL>map (fun g => g ^ n) μ = μ
<VAR>G : Type u_1<VAR>inst✝⁷ : CommGroup G<VAR>inst✝⁶ : TopologicalSpace G<VAR>inst✝⁵ : TopologicalGroup G<VAR>inst✝⁴ : MeasurableSpace G<VAR>inst✝³ : BorelSpace G<VAR>μ : Measure G<VAR>inst✝² : μ.IsHaarMeasure<VAR>inst✝¹ : CompactSpace G<VAR>inst✝ : RootableBy G ℤ<VAR>n : ℤ<VAR>hn : n ≠ 0<VAR>f : G →* G := zpowGroupHom n<VAR>hf : Continuous ⇑f<VAR>this : (map (⇑f) μ).IsHaarMeasure<VAR>C : ℝ≥0∞ := ↑((map (⇑f) μ).haarScalarFactor μ)<GOAL>map (fun g => g ^ n) μ = μ
<VAR>G : Type u_1<VAR>inst✝⁷ : CommGroup G<VAR>inst✝⁶ : TopologicalSpace G<VAR>inst✝⁵ : TopologicalGroup G<VAR>inst✝⁴ : MeasurableSpace G<VAR>inst✝³ : BorelSpace G<VAR>μ : Measure G<VAR>inst✝² : μ.IsHaarMeasure<VAR>inst✝¹ : CompactSpace G<VAR>inst✝ : RootableBy G ℤ<VAR>n : ℤ<VAR>hn : n ≠ 0<VAR>f : G →* G := zpowGroupHom n<VAR>hf : Continuous ⇑f<VAR>this : (map (⇑f) μ).IsHaarMeasure<VAR>C : ℝ≥0∞ := ↑((map (⇑f) μ).haarScalarFactor μ)<VAR>hC : map (⇑f) μ = C • μ<GOAL>map (fun g => g ^ n) μ = μ
<VAR>G : Type u_1<VAR>inst✝⁷ : CommGroup G<VAR>inst✝⁶ : TopologicalSpace G<VAR>inst✝⁵ : TopologicalGroup G<VAR>inst✝⁴ : MeasurableSpace G<VAR>inst✝³ : BorelSpace G<VAR>μ : Measure G<VAR>inst✝² : μ.IsHaarMeasure<VAR>inst✝¹ : CompactSpace G<VAR>inst✝ : RootableBy G ℤ<VAR>n : ℤ<VAR>hn : n ≠ 0<VAR>f : G →* G := zpowGroupHom n<VAR>hf : Continuous ⇑f<VAR>this : (map (⇑f) μ).IsHaarMeasure<VAR>C : ℝ≥0∞ := ↑((map (⇑f) μ).haarScalarFactor μ)<VAR>hC : map (⇑f) μ = C • μ<GOAL>C = 1
<VAR>G : Type u_1<VAR>inst✝⁷ : CommGroup G<VAR>inst✝⁶ : TopologicalSpace G<VAR>inst✝⁵ : TopologicalGroup G<VAR>inst✝⁴ : MeasurableSpace G<VAR>inst✝³ : BorelSpace G<VAR>μ : Measure G<VAR>inst✝² : μ.IsHaarMeasure<VAR>inst✝¹ : CompactSpace G<VAR>inst✝ : RootableBy G ℤ<VAR>n : ℤ<VAR>hn : n ≠ 0<VAR>f : G →* G := zpowGroupHom n<VAR>hf : Continuous ⇑f<VAR>this : (map (⇑f) μ).IsHaarMeasure<VAR>C : ℝ≥0∞ := ↑((map (⇑f) μ).haarScalarFactor μ)<VAR>hC : map (⇑f) μ = C • μ<VAR>h_univ : (map (⇑f) μ) univ = μ univ<GOAL>C = 1
<VAR>G : Type u_1<VAR>inst✝⁷ : CommGroup G<VAR>inst✝⁶ : TopologicalSpace G<VAR>inst✝⁵ : TopologicalGroup G<VAR>inst✝⁴ : MeasurableSpace G<VAR>inst✝³ : BorelSpace G<VAR>μ : Measure G<VAR>inst✝² : μ.IsHaarMeasure<VAR>inst✝¹ : CompactSpace G<VAR>inst✝ : RootableBy G ℤ<VAR>n : ℤ<VAR>hn : n ≠ 0<VAR>f : G →* G := zpowGroupHom n<VAR>hf : Continuous ⇑f<VAR>this : (map (⇑f) μ).IsHaarMeasure<VAR>C : ℝ≥0∞ := ↑((map (⇑f) μ).haarScalarFactor μ)<VAR>hC : map (⇑f) μ = C • μ<VAR>h_univ : (map (⇑f) μ) univ = μ univ<VAR>hμ₀ : μ univ ≠ 0<GOAL>C = 1
<VAR>G : Type u_1<VAR>inst✝⁷ : CommGroup G<VAR>inst✝⁶ : TopologicalSpace G<VAR>inst✝⁵ : TopologicalGroup G<VAR>inst✝⁴ : MeasurableSpace G<VAR>inst✝³ : BorelSpace G<VAR>μ : Measure G<VAR>inst✝² : μ.IsHaarMeasure<VAR>inst✝¹ : CompactSpace G<VAR>inst✝ : RootableBy G ℤ<VAR>n : ℤ<VAR>hn : n ≠ 0<VAR>f : G →* G := zpowGroupHom n<VAR>hf : Continuous ⇑f<VAR>this : (map (⇑f) μ).IsHaarMeasure<VAR>C : ℝ≥0∞ := ↑((map (⇑f) μ).haarScalarFactor μ)<VAR>hC : map (⇑f) μ = C • μ<VAR>h_univ : (map (⇑f) μ) univ = μ univ<VAR>hμ₀ : μ univ ≠ 0<VAR>hμ₁ : μ univ ≠ ⊤<GOAL>C = 1
<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✝ : Zero M<VAR>a a' : α<VAR>b : M<GOAL>⇑(single a b) = {a}.indicator fun x => b
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s t u : Multiset α<VAR>a b : α<VAR>x✝ : a ∈ s ∧ a ∈ t<VAR>h₁ : a ∈ s<VAR>h₂ : a ∈ t<GOAL>a ∈ s ∩ t
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s t u : Multiset α<VAR>a b : α<VAR>x✝ : a ∈ s ∧ a ∈ t<VAR>h₁ : a ∈ s<VAR>h₂ : a ∈ t<GOAL>a ∈ a ::ₘ s.erase a ∩ t.erase a
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝⁴ : CancelCommMonoidWithZero R<VAR>inst✝³ : UniqueFactorizationMonoid R<VAR>inst✝² : NormalizationMonoid R<VAR>inst✝¹ : DecidableRel Dvd.dvd<VAR>inst✝ : DecidableEq R<VAR>a b : R<VAR>ha : Irreducible a<VAR>hb : b ≠ 0<GOAL>multiplicity a b = ↑(count (normalize a) (normalizedFactors b))
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝⁴ : CancelCommMonoidWithZero R<VAR>inst✝³ : UniqueFactorizationMonoid R<VAR>inst✝² : NormalizationMonoid R<VAR>inst✝¹ : DecidableRel Dvd.dvd<VAR>inst✝ : DecidableEq R<VAR>a b : R<VAR>ha : Irreducible a<VAR>hb : b ≠ 0<GOAL>multiplicity a b ≤ ↑(count (normalize a) (normalizedFactors b))
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝⁴ : CancelCommMonoidWithZero R<VAR>inst✝³ : UniqueFactorizationMonoid R<VAR>inst✝² : NormalizationMonoid R<VAR>inst✝¹ : DecidableRel Dvd.dvd<VAR>inst✝ : DecidableEq R<VAR>a b : R<VAR>ha : Irreducible a<VAR>hb : b ≠ 0<GOAL>↑(count (normalize a) (normalizedFactors b)) ≤ multiplicity a b
<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>s : Set ℝ<VAR>e : E<VAR>a : ℝ<VAR>f : ℝ → E<VAR>f_diff : DifferentiableOn ℝ f s<VAR>f_lim : ContinuousWithinAt f s a<VAR>hs : s ∈ 𝓝[>] a<VAR>f_lim' : Tendsto (fun x => deriv f x) (𝓝[>] a) (𝓝 e)<GOAL>HasDerivWithinAt f e (Ici a) 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>s : Set ℝ<VAR>e : E<VAR>a : ℝ<VAR>f : ℝ → E<VAR>f_diff : DifferentiableOn ℝ f s<VAR>f_lim : ContinuousWithinAt f s a<VAR>hs : s ∈ 𝓝[>] a<VAR>f_lim' : Tendsto (fun x => deriv f x) (𝓝[>] a) (𝓝 e)<VAR>b : ℝ<VAR>ab : a < b<VAR>sab : Ioc a b ⊆ s<GOAL>HasDerivWithinAt f e (Ici a) 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>s : Set ℝ<VAR>e : E<VAR>a : ℝ<VAR>f : ℝ → E<VAR>f_diff : DifferentiableOn ℝ f s<VAR>f_lim : ContinuousWithinAt f s a<VAR>hs : s ∈ 𝓝[>] a<VAR>f_lim' : Tendsto (fun x => deriv f x) (𝓝[>] a) (𝓝 e)<VAR>b : ℝ<VAR>ab : a < b<VAR>sab : Ioc a b ⊆ s<VAR>t : Set ℝ := Ioo a b<GOAL>HasDerivWithinAt f e (Ici a) 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>s : Set ℝ<VAR>e : E<VAR>a : ℝ<VAR>f : ℝ → E<VAR>f_diff : DifferentiableOn ℝ f s<VAR>f_lim : ContinuousWithinAt f s a<VAR>hs : s ∈ 𝓝[>] a<VAR>f_lim' : Tendsto (fun x => deriv f x) (𝓝[>] a) (𝓝 e)<VAR>b : ℝ<VAR>ab : a < b<VAR>sab : Ioc a b ⊆ s<VAR>t : Set ℝ := Ioo a b<VAR>ts : t ⊆ s<GOAL>HasDerivWithinAt f e (Ici a) 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>s : Set ℝ<VAR>e : E<VAR>a : ℝ<VAR>f : ℝ → E<VAR>f_diff : DifferentiableOn ℝ f s<VAR>f_lim : ContinuousWithinAt f s a<VAR>hs : s ∈ 𝓝[>] a<VAR>f_lim' : Tendsto (fun x => deriv f x) (𝓝[>] a) (𝓝 e)<VAR>b : ℝ<VAR>ab : a < b<VAR>sab : Ioc a b ⊆ s<VAR>t : Set ℝ := Ioo a b<VAR>ts : t ⊆ s<VAR>t_diff : DifferentiableOn ℝ f t<GOAL>HasDerivWithinAt f e (Ici a) 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>s : Set ℝ<VAR>e : E<VAR>a : ℝ<VAR>f : ℝ → E<VAR>f_diff : DifferentiableOn ℝ f s<VAR>f_lim : ContinuousWithinAt f s a<VAR>hs : s ∈ 𝓝[>] a<VAR>f_lim' : Tendsto (fun x => deriv f x) (𝓝[>] a) (𝓝 e)<VAR>b : ℝ<VAR>ab : a < b<VAR>sab : Ioc a b ⊆ s<VAR>t : Set ℝ := Ioo a b<VAR>ts : t ⊆ s<VAR>t_diff : DifferentiableOn ℝ f t<VAR>t_conv : Convex ℝ t<GOAL>HasDerivWithinAt f e (Ici a) 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>s : Set ℝ<VAR>e : E<VAR>a : ℝ<VAR>f : ℝ → E<VAR>f_diff : DifferentiableOn ℝ f s<VAR>f_lim : ContinuousWithinAt f s a<VAR>hs : s ∈ 𝓝[>] a<VAR>f_lim' : Tendsto (fun x => deriv f x) (𝓝[>] a) (𝓝 e)<VAR>b : ℝ<VAR>ab : a < b<VAR>sab : Ioc a b ⊆ s<VAR>t : Set ℝ := Ioo a b<VAR>ts : t ⊆ s<VAR>t_diff : DifferentiableOn ℝ f t<VAR>t_conv : Convex ℝ t<VAR>t_open : IsOpen t<GOAL>HasDerivWithinAt f e (Ici a) 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>s : Set ℝ<VAR>e : E<VAR>a : ℝ<VAR>f : ℝ → E<VAR>f_diff : DifferentiableOn ℝ f s<VAR>f_lim : ContinuousWithinAt f s a<VAR>hs : s ∈ 𝓝[>] a<VAR>f_lim' : Tendsto (fun x => deriv f x) (𝓝[>] a) (𝓝 e)<VAR>b : ℝ<VAR>ab : a < b<VAR>sab : Ioc a b ⊆ s<VAR>t : Set ℝ := Ioo a b<VAR>ts : t ⊆ s<VAR>t_diff : DifferentiableOn ℝ f t<VAR>t_conv : Convex ℝ t<VAR>t_open : IsOpen t<VAR>t_closure : closure t = Icc a b<GOAL>HasDerivWithinAt f e (Ici a) 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>s : Set ℝ<VAR>e : E<VAR>a : ℝ<VAR>f : ℝ → E<VAR>f_diff : DifferentiableOn ℝ f s<VAR>f_lim : ContinuousWithinAt f s a<VAR>hs : s ∈ 𝓝[>] a<VAR>f_lim' : Tendsto (fun x => deriv f x) (𝓝[>] a) (𝓝 e)<VAR>b : ℝ<VAR>ab : a < b<VAR>sab : Ioc a b ⊆ s<VAR>t : Set ℝ := Ioo a b<VAR>ts : t ⊆ s<VAR>t_diff : DifferentiableOn ℝ f t<VAR>t_conv : Convex ℝ t<VAR>t_open : IsOpen t<VAR>t_closure : closure t = Icc a b<VAR>t_cont : ∀ y ∈ closure t, ContinuousWithinAt f t y<GOAL>HasDerivWithinAt f e (Ici a) 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>s : Set ℝ<VAR>e : E<VAR>a : ℝ<VAR>f : ℝ → E<VAR>f_diff : DifferentiableOn ℝ f s<VAR>f_lim : ContinuousWithinAt f s a<VAR>hs : s ∈ 𝓝[>] a<VAR>f_lim' : Tendsto (fun x => deriv f x) (𝓝[>] a) (𝓝 e)<VAR>b : ℝ<VAR>ab : a < b<VAR>sab : Ioc a b ⊆ s<VAR>t : Set ℝ := Ioo a b<VAR>ts : t ⊆ s<VAR>t_diff : DifferentiableOn ℝ f t<VAR>t_conv : Convex ℝ t<VAR>t_open : IsOpen t<VAR>t_closure : closure t = Icc a b<VAR>t_cont : ∀ y ∈ closure t, ContinuousWithinAt f t y<VAR>t_diff' : Tendsto (fun x => fderiv ℝ f x) (𝓝[t] a) (𝓝 (smulRight 1 e))<GOAL>HasDerivWithinAt f e (Ici a) 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>s : Set ℝ<VAR>e : E<VAR>a : ℝ<VAR>f : ℝ → E<VAR>f_diff : DifferentiableOn ℝ f s<VAR>f_lim : ContinuousWithinAt f s a<VAR>hs : s ∈ 𝓝[>] a<VAR>f_lim' : Tendsto (fun x => deriv f x) (𝓝[>] a) (𝓝 e)<VAR>b : ℝ<VAR>ab : a < b<VAR>sab : Ioc a b ⊆ s<VAR>t : Set ℝ := Ioo a b<VAR>ts : t ⊆ s<VAR>t_diff : DifferentiableOn ℝ f t<VAR>t_conv : Convex ℝ t<VAR>t_open : IsOpen t<VAR>t_closure : closure t = Icc a b<VAR>t_cont : ∀ y ∈ closure t, ContinuousWithinAt f t y<VAR>t_diff' : Tendsto (fun x => fderiv ℝ f x) (𝓝[t] a) (𝓝 (smulRight 1 e))<VAR>this : HasDerivWithinAt f e (Icc a b) a<GOAL>HasDerivWithinAt f e (Ici a) a
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g : E → F<VAR>p pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x✝ : E<VAR>r r' : ℝ≥0∞<VAR>hf : HasFPowerSeriesOnBall f p x✝ r<VAR>u : Set (F × F)<VAR>hu : u ∈ uniformity F<VAR>x : E<VAR>hx : x ∈ EMetric.ball 0 r<GOAL>∃ t ∈ 𝓝[EMetric.ball 0 r] x, ∀ᶠ (n : ℕ) in atTop, ∀ y ∈ t, ((fun y => f (x✝ + y)) y, (fun n y => p.partialSum n y) n y) ∈ u
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g : E → F<VAR>p pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x✝ : E<VAR>r r'✝ : ℝ≥0∞<VAR>hf : HasFPowerSeriesOnBall f p x✝ r<VAR>u : Set (F × F)<VAR>hu : u ∈ uniformity F<VAR>x : E<VAR>hx : x ∈ EMetric.ball 0 r<VAR>r' : ℝ≥0<VAR>xr' : edist x 0 < ↑r'<VAR>hr' : ↑r' < r<GOAL>∃ t ∈ 𝓝[EMetric.ball 0 r] x, ∀ᶠ (n : ℕ) in atTop, ∀ y ∈ t, ((fun y => f (x✝ + y)) y, (fun n y => p.partialSum n y) n y) ∈ u
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g : E → F<VAR>p pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x✝ : E<VAR>r r'✝ : ℝ≥0∞<VAR>hf : HasFPowerSeriesOnBall f p x✝ r<VAR>u : Set (F × F)<VAR>hu : u ∈ uniformity F<VAR>x : E<VAR>hx : x ∈ EMetric.ball 0 r<VAR>r' : ℝ≥0<VAR>xr' : edist x 0 < ↑r'<VAR>hr' : ↑r' < r<VAR>this : EMetric.ball 0 ↑r' ∈ 𝓝 x<GOAL>∃ t ∈ 𝓝[EMetric.ball 0 r] x, ∀ᶠ (n : ℕ) in atTop, ∀ y ∈ t, ((fun y => f (x✝ + y)) y, (fun n y => p.partialSum n y) n y) ∈ u
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g : E → F<VAR>p pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x✝ : E<VAR>r r'✝ : ℝ≥0∞<VAR>hf : HasFPowerSeriesOnBall f p x✝ r<VAR>u : Set (F × F)<VAR>hu : u ∈ uniformity F<VAR>x : E<VAR>hx : x ∈ EMetric.ball 0 r<VAR>r' : ℝ≥0<VAR>xr' : edist x 0 < ↑r'<VAR>hr' : ↑r' < r<VAR>this : EMetric.ball 0 ↑r' ∈ 𝓝 x<GOAL>∀ᶠ (n : ℕ) in atTop, ∀ y ∈ EMetric.ball 0 ↑r', ((fun y => f (x✝ + y)) y, (fun n y => p.partialSum n y) n y) ∈ u
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝¹ : (i : ι) → Zero (β i)<VAR>p : ι → Prop<VAR>inst✝ : DecidablePred p<VAR>f : Π₀ (i : ι), β i<VAR>i : ι<VAR>h : p i<GOAL>(filter p f) i = f i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : Group G<VAR>a✝ b✝ c d : G<VAR>n : ℤ<VAR>a b : G<GOAL>a / b * b = a
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : AddCommMonoid N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>M₁ M₂ : Submodule R M<VAR>N₁ N₂ : Submodule R N<VAR>s : Set (↥M₁ ⊗[R] ↥N₁)<VAR>hs : s.Finite<GOAL>∃ M', ∃ (hM : M' ≤ M₁), Module.Finite R ↥M' ∧ s ⊆ ↑(LinearMap.range (LinearMap.rTensor (↥N₁) (inclusion hM)))