ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝⁴ : CancelCommMonoidWithZero R<VAR>inst✝³ : UniqueFactorizationMonoid R<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : UniqueFactorizationMonoid α<VAR>β : Type u_3<VAR>inst✝ : CancelCommMonoidWithZero β<VAR>f : α → β<VAR>i j : α → ℕ<VAR>h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y<VAR>hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i<VAR>hcp : ∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y<VAR>this : DecidableEq α := Classical.decEq α<VAR>p : α<VAR>s : Finset α<VAR>hps : p ∉ s<VAR>ih : (∀ p ∈ s, Prime p) → (∀ p ∈ s, ∀ q ∈ s, p ∣ q → p = q) → f (∏ p ∈ s, p ^ (i p + j p)) = f (∏ p ∈ s, p ^ i p) * f (∏ p ∈ s, p ^ j p)<VAR>is_prime : ∀ p_1 ∈ insert p s, Prime p_1<VAR>is_coprime : ∀ p_1 ∈ insert p s, ∀ q ∈ insert p s, p_1 ∣ q → p_1 = q<VAR>hpr_p : Prime p<VAR>hpr_s : ∀ p ∈ s, Prime p<VAR>hcp_p : ∀ (i : α → ℕ), IsRelPrime (p ^ i p) (∏ p' ∈ s, p' ^ i p')<GOAL>f (∏ p ∈ insert p s, p ^ (i p + j p)) = f (∏ p ∈ insert p s, p ^ i p) * f (∏ p ∈ insert p s, p ^ j p)
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝⁴ : CancelCommMonoidWithZero R<VAR>inst✝³ : UniqueFactorizationMonoid R<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : UniqueFactorizationMonoid α<VAR>β : Type u_3<VAR>inst✝ : CancelCommMonoidWithZero β<VAR>f : α → β<VAR>i j : α → ℕ<VAR>h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y<VAR>hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i<VAR>hcp : ∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y<VAR>this : DecidableEq α := Classical.decEq α<VAR>p : α<VAR>s : Finset α<VAR>hps : p ∉ s<VAR>ih : (∀ p ∈ s, Prime p) → (∀ p ∈ s, ∀ q ∈ s, p ∣ q → p = q) → f (∏ p ∈ s, p ^ (i p + j p)) = f (∏ p ∈ s, p ^ i p) * f (∏ p ∈ s, p ^ j p)<VAR>is_prime : ∀ p_1 ∈ insert p s, Prime p_1<VAR>is_coprime : ∀ p_1 ∈ insert p s, ∀ q ∈ insert p s, p_1 ∣ q → p_1 = q<VAR>hpr_p : Prime p<VAR>hpr_s : ∀ p ∈ s, Prime p<VAR>hcp_p : ∀ (i : α → ℕ), IsRelPrime (p ^ i p) (∏ p' ∈ s, p' ^ i p')<VAR>hcp_s : ∀ p ∈ s, ∀ q ∈ s, p ∣ q → p = q<GOAL>f (∏ p ∈ insert p s, p ^ (i p + j p)) = f (∏ p ∈ insert p s, p ^ i p) * f (∏ p ∈ insert p s, p ^ j p)
<VAR>α : Type u<VAR>α' : Type w<VAR>β : Type v<VAR>β' : Type x<VAR>γ : Type u_1<VAR>δ : Type u_2<VAR>x y : α ⊕ β<VAR>h₁ : x.isRight = true<VAR>h₂ : x.getRight?.isSome = true<GOAL>x.getRight h₁ = x.getRight?.get h₂
<VAR>X : Type u<VAR>inst✝¹ : Lattice X<VAR>inst✝ : JordanHolderLattice X<VAR>s : CompositionSeries X<GOAL>(eraseLast s).last ≤ last s
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝ : CommRing R<VAR>n : ℕ<GOAL>constantCoeff (wittNeg p n) = 0
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝ : CommRing R<VAR>n : ℕ<GOAL>constantCoeff (-X 0) = 0
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>a✝ a₁ a₂ b✝ c : G<VAR>inst✝¹ : Group G<VAR>inst✝ : Group H<VAR>f : G → H<VAR>hf : IsGroupHom f<VAR>a b : G<VAR>h : f (a * b⁻¹) = 1<GOAL>f a = f b
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>a✝ a₁ a₂ b✝ c : G<VAR>inst✝¹ : Group G<VAR>inst✝ : Group H<VAR>f : G → H<VAR>hf : IsGroupHom f<VAR>a b : G<VAR>h : f a * (f b)⁻¹ = 1<GOAL>f a = f b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝³ : AddCommMonoid α<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : StarAddMonoid α<VAR>inst✝ : ContinuousStar α<VAR>f : β → α<VAR>a : α<VAR>hf : Summable fun b => Star.star (f b)<GOAL>Summable f
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring S<VAR>inst✝ : Algebra R S<VAR>M N : Submodule R S<GOAL>TensorProduct.comm R ↥M ↥⊥ ≪≫ₗ M.lTensorOne = M.rTensorOne
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring S<VAR>inst✝ : Algebra R S<VAR>M N : Submodule R S<VAR>m : ↥M<VAR>r : ↥⊥<GOAL>↑(TensorProduct.comm R ↥M ↥⊥ ≪≫ₗ M.lTensorOne) (m ⊗ₜ[R] r) = ↑M.rTensorOne (m ⊗ₜ[R] r)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring S<VAR>inst✝ : Algebra R S<VAR>M N : Submodule R S<VAR>m : ↥M<VAR>r : ↥⊥<VAR>x : R<VAR>h : (algebraMap R S) x = ↑r<GOAL>↑(TensorProduct.comm R ↥M ↥⊥ ≪≫ₗ M.lTensorOne) (m ⊗ₜ[R] r) = ↑M.rTensorOne (m ⊗ₜ[R] r)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring S<VAR>inst✝ : Algebra R S<VAR>M N : Submodule R S<VAR>m : ↥M<VAR>r : ↥⊥<VAR>x : R<VAR>h : (algebraMap R ↥⊥) x = r<GOAL>↑(TensorProduct.comm R ↥M ↥⊥ ≪≫ₗ M.lTensorOne) (m ⊗ₜ[R] r) = ↑M.rTensorOne (m ⊗ₜ[R] r)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : GeneralizedHeytingAlgebra α<VAR>a b c d : α<VAR>h : Codisjoint a b<GOAL>b ⇨ a = a
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : GeneralizedHeytingAlgebra α<VAR>a b c d : α<VAR>h : Codisjoint a b<GOAL>b ⇨ a = ⊤ ⇨ a
<VAR>α : Type u<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝ : DivisionCommMonoid α<VAR>a b c d : α<VAR>h : IsUnit a<GOAL>a / (a / b) = b
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ✝ : Type u_3<VAR>δ : Type u_4<VAR>p : α✝ → Prop<VAR>f✝ : (a : α✝) → p a → β✝<VAR>x✝ : Option α✝<VAR>α β γ : Type u_5<VAR>f : β → γ<VAR>x : Option α<VAR>g : α → Option β<GOAL>Option.map f (x >>= g) = do let a ← x Option.map f (g a)
<VAR>C : Type u₁<VAR>inst✝² : Category.{u₂, u₁} C<VAR>inst✝¹ : GaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝ : FiberFunctor F<VAR>X : C<VAR>t : ↑(F.obj X)<GOAL>F.map (Pi.π (fun x => X) t) (CategoryTheory.PreGaloisCategory.mkSelfProdFib F X) = t
<VAR>C : Type u₁<VAR>inst✝² : Category.{u₂, u₁} C<VAR>inst✝¹ : GaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝ : FiberFunctor F<VAR>X : C<VAR>t : ↑(F.obj X)<GOAL>Pi.π (fun b => F.obj X) t ((PreservesProduct.iso F fun x => X).hom (CategoryTheory.PreGaloisCategory.mkSelfProdFib F X)) = t
<VAR>C : Type u₁<VAR>inst✝² : Category.{u₂, u₁} C<VAR>inst✝¹ : GaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝ : FiberFunctor F<VAR>X : C<VAR>t : ↑(F.obj X)<GOAL>Pi.π (fun b => F.obj X) t ((Concrete.productEquiv fun x => F.obj X).symm id) = t
<VAR>α : Type u<VAR>head✝ : α<VAR>tail✝ : List α<GOAL>(ofList (head✝ :: tail✝)).toList = head✝ :: tail✝
<VAR>p n k : ℕ<VAR>hp : Prime p<VAR>hk : k ≠ 0<VAR>hkp : k ≠ p ^ n<GOAL>p ∣ (p ^ n).choose k
<VAR>p n k : ℕ<VAR>hp : Prime p<VAR>hk : k ≠ 0<VAR>hkp✝ : k ≠ p ^ n<VAR>hkp : p ^ n < k<GOAL>p ∣ (p ^ n).choose k
<VAR>p n k : ℕ<VAR>hp : Prime p<VAR>hk : k ≠ 0<VAR>hkp✝ : k ≠ p ^ n<VAR>hkp : k < p ^ n<GOAL>p ∣ (p ^ n).choose k
<VAR>p n k : ℕ<VAR>hp : Prime p<VAR>hk : k ≠ 0<VAR>hkp✝ : k ≠ p ^ n<VAR>hkp : k < p ^ n<VAR>h : multiplicity p ((p ^ n).choose k) = 0<GOAL>p ^ n ∣ k
<VAR>p n k : ℕ<VAR>hp : Prime p<VAR>hk : k ≠ 0<VAR>hkp✝ : k ≠ p ^ n<VAR>hkp : k < p ^ n<VAR>h : multiplicity p ((p ^ n).choose k) = 0<VAR>H : multiplicity p ((p ^ n).choose k) + multiplicity p k = ↑n<GOAL>p ^ n ∣ k
<VAR>p n k : ℕ<VAR>hp : Prime p<VAR>hk : k ≠ 0<VAR>hkp✝ : k ≠ p ^ n<VAR>hkp : k < p ^ n<VAR>h : multiplicity p ((p ^ n).choose k) = 0<VAR>H : p ^ n ∣ k ∧ ¬p ^ (n + 1) ∣ k<GOAL>p ^ n ∣ k
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>γ' : Type u_6<VAR>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>ζ : Type u_11<VAR>ζ' : Type u_12<VAR>ν : Type u_13<VAR>inst✝⁸ : DecidableEq α'<VAR>inst✝⁷ : DecidableEq β'<VAR>inst✝⁶ : DecidableEq γ<VAR>inst✝⁵ : DecidableEq γ'<VAR>inst✝⁴ : DecidableEq δ<VAR>inst✝³ : DecidableEq δ'<VAR>inst✝² : DecidableEq ε<VAR>inst✝¹ : DecidableEq ε'<VAR>f f' : α → β → γ<VAR>g g' : α → β → γ → δ<VAR>s s' : Finset α<VAR>t t' : Finset β<VAR>u u' : Finset γ<VAR>a a' : α<VAR>b b' : β<VAR>c : γ<VAR>inst✝ : DecidableEq β<VAR>hf : Injective2 f<GOAL>image2 f (↑s) (↑t ∩ ↑t') = image2 f ↑s ↑t ∩ image2 f ↑s ↑t'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>inst✝² : One M<VAR>inst✝¹ : One N<VAR>s✝ t : Set α<VAR>f✝ g : α → M<VAR>a : α<VAR>h : M → β<VAR>f : α → M<VAR>s : Set α<VAR>x : α<VAR>inst✝ : DecidablePred fun x => x ∈ s<VAR>this : DecidablePred fun x => x ∈ s := Classical.decPred fun x => x ∈ s<GOAL>h (s.mulIndicator f x) = s.piecewise (h ∘ f) (const α (h 1)) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a a₁ a₂ b b₁ b₂ c d : α<GOAL>Iio b \ Iic a = Ioo a b
<VAR>α : Type u<VAR>inst✝ : Monoid α<VAR>a✝ b✝ c u : αˣ<VAR>a : α<VAR>b : αˣ<GOAL>a * ↑b⁻¹ * ↑b = a
<VAR>R : Type u<VAR>inst✝² : Ring R<VAR>X Y : ModuleCat R<VAR>f : X ⟶ Y<VAR>M : Type v<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>hf : LinearMap.ker f = ⊥<GOAL>Function.Injective ⇑f
<VAR>s : Set ℕ<VAR>m : ℕ<VAR>hm : m < sInf s<GOAL>m ∉ s
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E✝ : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : NormedAddCommGroup E✝<VAR>p : ℝ≥0∞<VAR>f✝ : ι → α → E✝<VAR>g✝ : α → E✝<VAR>E : Type u_4<VAR>inst✝ : NormedAddCommGroup E<VAR>f : ι → α → E<VAR>g : α → E<VAR>l : Filter ι<VAR>hfg : Tendsto (fun n => eLpNorm (f n - g) ⊤ μ) l (𝓝 0)<VAR>δ : ℝ<VAR>hδ : 0 < δ<GOAL>Tendsto (fun i => μ {x | δ ≤ dist (f i x) (g x)}) l (𝓝 0)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E✝ : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : NormedAddCommGroup E✝<VAR>p : ℝ≥0∞<VAR>f✝ : ι → α → E✝<VAR>g✝ : α → E✝<VAR>E : Type u_4<VAR>inst✝ : NormedAddCommGroup E<VAR>f : ι → α → E<VAR>g : α → E<VAR>l : Filter ι<VAR>δ : ℝ<VAR>hδ : 0 < δ<VAR>hfg : Tendsto (fun n => essSup (fun x => ↑‖(f n - g) x‖₊) μ) l (𝓝 0)<GOAL>Tendsto (fun i => μ {x | δ ≤ dist (f i x) (g x)}) l (𝓝 0)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E✝ : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : NormedAddCommGroup E✝<VAR>p : ℝ≥0∞<VAR>f✝ : ι → α → E✝<VAR>g✝ : α → E✝<VAR>E : Type u_4<VAR>inst✝ : NormedAddCommGroup E<VAR>f : ι → α → E<VAR>g : α → E<VAR>l : Filter ι<VAR>δ : ℝ<VAR>hδ : 0 < δ<VAR>hfg : ∀ ε > 0, ∀ᶠ (x : ι) in l, essSup (fun x_1 => ↑‖(f x - g) x_1‖₊) μ ≤ ε<GOAL>∀ ε > 0, ∀ᶠ (x : ι) in l, μ {x_1 | δ ≤ dist (f x x_1) (g x_1)} ≤ ε
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E✝ : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : NormedAddCommGroup E✝<VAR>p : ℝ≥0∞<VAR>f✝ : ι → α → E✝<VAR>g✝ : α → E✝<VAR>E : Type u_4<VAR>inst✝ : NormedAddCommGroup E<VAR>f : ι → α → E<VAR>g : α → E<VAR>l : Filter ι<VAR>δ : ℝ<VAR>hδ : 0 < δ<VAR>hfg : ∀ ε > 0, ∀ᶠ (x : ι) in l, essSup (fun x_1 => ↑‖(f x - g) x_1‖₊) μ ≤ ε<VAR>ε : ℝ≥0∞<VAR>hε : ε > 0<GOAL>∀ᶠ (x : ι) in l, μ {x_1 | δ ≤ dist (f x x_1) (g x_1)} ≤ ε
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E✝ : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : NormedAddCommGroup E✝<VAR>p : ℝ≥0∞<VAR>f✝ : ι → α → E✝<VAR>g✝ : α → E✝<VAR>E : Type u_4<VAR>inst✝ : NormedAddCommGroup E<VAR>f : ι → α → E<VAR>g : α → E<VAR>l : Filter ι<VAR>δ : ℝ<VAR>hδ : 0 < δ<VAR>ε : ℝ≥0∞<VAR>hε : ε > 0<VAR>hfg : ∀ᶠ (x : ι) in l, essSup (fun x_1 => ↑‖(f x - g) x_1‖₊) μ ≤ ENNReal.ofReal δ / 2<GOAL>∀ᶠ (x : ι) in l, μ {x_1 | δ ≤ dist (f x x_1) (g x_1)} ≤ ε
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E✝ : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : NormedAddCommGroup E✝<VAR>p : ℝ≥0∞<VAR>f✝ : ι → α → E✝<VAR>g✝ : α → E✝<VAR>E : Type u_4<VAR>inst✝ : NormedAddCommGroup E<VAR>f : ι → α → E<VAR>g : α → E<VAR>l : Filter ι<VAR>δ : ℝ<VAR>hδ : 0 < δ<VAR>ε : ℝ≥0∞<VAR>hε : ε > 0<VAR>hfg : ∀ᶠ (x : ι) in l, essSup (fun x_1 => ↑‖(f x - g) x_1‖₊) μ ≤ ENNReal.ofReal δ / 2<VAR>n : ι<VAR>hn : essSup (fun x => ↑‖(f n - g) x‖₊) μ ≤ ENNReal.ofReal δ / 2<GOAL>μ {x | δ ≤ dist (f n x) (g x)} ≤ ε
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E✝ : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : NormedAddCommGroup E✝<VAR>p : ℝ≥0∞<VAR>f✝ : ι → α → E✝<VAR>g✝ : α → E✝<VAR>E : Type u_4<VAR>inst✝ : NormedAddCommGroup E<VAR>f : ι → α → E<VAR>g : α → E<VAR>l : Filter ι<VAR>δ : ℝ<VAR>hδ : 0 < δ<VAR>ε : ℝ≥0∞<VAR>hfg : ∀ᶠ (x : ι) in l, essSup (fun x_1 => ↑‖f x x_1 - g x_1‖₊) μ ≤ ENNReal.ofReal δ / 2<VAR>n : ι<VAR>hn : essSup (fun x => ↑‖f n x - g x‖₊) μ ≤ ENNReal.ofReal δ / 2<VAR>hε : 0 < ε<GOAL>μ {x | δ ≤ dist (f n x) (g x)} ≤ ε
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E✝ : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : NormedAddCommGroup E✝<VAR>p : ℝ≥0∞<VAR>f✝ : ι → α → E✝<VAR>g✝ : α → E✝<VAR>E : Type u_4<VAR>inst✝ : NormedAddCommGroup E<VAR>f : ι → α → E<VAR>g : α → E<VAR>l : Filter ι<VAR>δ : ℝ<VAR>hδ : 0 < δ<VAR>ε : ℝ≥0∞<VAR>hfg : ∀ᶠ (x : ι) in l, essSup (fun x_1 => ↑‖f x x_1 - g x_1‖₊) μ ≤ ENNReal.ofReal δ / 2<VAR>n : ι<VAR>hn : essSup (fun x => ↑‖f n x - g x‖₊) μ ≤ ENNReal.ofReal δ / 2<VAR>hε : 0 < ε<VAR>this : essSup (fun x => ↑‖f n x - g x‖₊) μ < ENNReal.ofReal δ<GOAL>μ {x | δ ≤ dist (f n x) (g x)} ≤ ε
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E✝ : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : NormedAddCommGroup E✝<VAR>p : ℝ≥0∞<VAR>f✝ : ι → α → E✝<VAR>g✝ : α → E✝<VAR>E : Type u_4<VAR>inst✝ : NormedAddCommGroup E<VAR>f : ι → α → E<VAR>g : α → E<VAR>l : Filter ι<VAR>δ : ℝ<VAR>hδ : 0 < δ<VAR>ε : ℝ≥0∞<VAR>hfg : ∀ᶠ (x : ι) in l, essSup (fun x_1 => ↑‖f x x_1 - g x_1‖₊) μ ≤ ENNReal.ofReal δ / 2<VAR>n : ι<VAR>hn : essSup (fun x => ↑‖f n x - g x‖₊) μ ≤ ENNReal.ofReal δ / 2<VAR>hε : 0 < ε<VAR>this : essSup (fun x => ↑‖f n x - g x‖₊) μ < ENNReal.ofReal δ<GOAL>μ {x | δ ≤ dist (f n x) (g x)} = μ {x | (fun y => ↑‖f n y - g y‖₊ < ENNReal.ofReal δ) x}ᶜ
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E✝ : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : NormedAddCommGroup E✝<VAR>p : ℝ≥0∞<VAR>f✝ : ι → α → E✝<VAR>g✝ : α → E✝<VAR>E : Type u_4<VAR>inst✝ : NormedAddCommGroup E<VAR>f : ι → α → E<VAR>g : α → E<VAR>l : Filter ι<VAR>δ : ℝ<VAR>hδ : 0 < δ<VAR>ε : ℝ≥0∞<VAR>hfg : ∀ᶠ (x : ι) in l, essSup (fun x_1 => ↑‖f x x_1 - g x_1‖₊) μ ≤ ENNReal.ofReal δ / 2<VAR>n : ι<VAR>hn : essSup (fun x => ↑‖f n x - g x‖₊) μ ≤ ENNReal.ofReal δ / 2<VAR>hε : 0 < ε<VAR>this : essSup (fun x => ↑‖f n x - g x‖₊) μ < ENNReal.ofReal δ<VAR>x : α<GOAL>x ∈ {x | δ ≤ dist (f n x) (g x)} ↔ x ∈ {x | (fun y => ↑‖f n y - g y‖₊ < ENNReal.ofReal δ) x}ᶜ
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E✝ : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : NormedAddCommGroup E✝<VAR>p : ℝ≥0∞<VAR>f✝ : ι → α → E✝<VAR>g✝ : α → E✝<VAR>E : Type u_4<VAR>inst✝ : NormedAddCommGroup E<VAR>f : ι → α → E<VAR>g : α → E<VAR>l : Filter ι<VAR>δ : ℝ<VAR>hδ : 0 < δ<VAR>ε : ℝ≥0∞<VAR>hfg : ∀ᶠ (x : ι) in l, essSup (fun x_1 => ↑‖f x x_1 - g x_1‖₊) μ ≤ ENNReal.ofReal δ / 2<VAR>n : ι<VAR>hn : essSup (fun x => ↑‖f n x - g x‖₊) μ ≤ ENNReal.ofReal δ / 2<VAR>hε : 0 < ε<VAR>this : essSup (fun x => ↑‖f n x - g x‖₊) μ < ENNReal.ofReal δ<VAR>x : α<GOAL>δ ≤ dist (f n x) (g x) ↔ δ ≤ ‖f n x - g x‖
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedSemifield α<VAR>inst✝ : LinearOrderedSemifield β<VAR>s : Set ι<VAR>f f₁ f₂ : ι → α<VAR>g g₁ g₂ : ι → β<VAR>hg : StrongLT 0 g<VAR>i j : ι<GOAL>g⁻¹ j < g⁻¹ i → f j ≤ f i ↔ g i < g j → f j ≤ f i
<VAR>B : Type u<VAR>inst✝ : Bicategory B<VAR>a b c : B<VAR>f : a ⟶ b<VAR>g : b ⟶ a<VAR>f₁ : a ⟶ b<VAR>g₁ : b ⟶ a<VAR>f₂ : b ⟶ c<VAR>g₂ : c ⟶ b<VAR>adj₁ : f₁ ⊣ g₁<VAR>adj₂ : f₂ ⊣ g₂<GOAL>leftZigzag (adj₁.compUnit adj₂) (adj₁.compCounit adj₂) = (λ_ (f₁ ≫ f₂)).hom ≫ (ρ_ (f₁ ≫ f₂)).inv
<VAR>α : Type u_1<VAR>inst✝⁴ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝³ : PseudoEMetricSpace E<VAR>V : Type u_3<VAR>inst✝² : NormedAddCommGroup V<VAR>inst✝¹ : NormedSpace ℝ V<VAR>inst✝ : FiniteDimensional ℝ V<VAR>f : ℝ → V<VAR>s : Set ℝ<VAR>h : LocallyBoundedVariationOn f s<VAR>A : V ≃L[ℝ] ↑(Basis.ofVectorSpaceIndex ℝ V) → ℝ := (Basis.ofVectorSpace ℝ V).equivFun.toContinuousLinearEquiv<GOAL>∀ᵐ (x : ℝ), x ∈ s → DifferentiableWithinAt ℝ f s x
<VAR>α : Type u_1<VAR>inst✝⁴ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝³ : PseudoEMetricSpace E<VAR>V : Type u_3<VAR>inst✝² : NormedAddCommGroup V<VAR>inst✝¹ : NormedSpace ℝ V<VAR>inst✝ : FiniteDimensional ℝ V<VAR>f : ℝ → V<VAR>s : Set ℝ<VAR>h : LocallyBoundedVariationOn f s<VAR>A : V ≃L[ℝ] ↑(Basis.ofVectorSpaceIndex ℝ V) → ℝ := (Basis.ofVectorSpace ℝ V).equivFun.toContinuousLinearEquiv<GOAL>∀ᵐ (x : ℝ), x ∈ s → DifferentiableWithinAt ℝ (⇑A ∘ f) s x
<VAR>α : Type u_1<VAR>inst✝⁴ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝³ : PseudoEMetricSpace E<VAR>V : Type u_3<VAR>inst✝² : NormedAddCommGroup V<VAR>inst✝¹ : NormedSpace ℝ V<VAR>inst✝ : FiniteDimensional ℝ V<VAR>f : ℝ → V<VAR>s : Set ℝ<VAR>h : LocallyBoundedVariationOn f s<VAR>A : V ≃L[ℝ] ↑(Basis.ofVectorSpaceIndex ℝ V) → ℝ := (Basis.ofVectorSpace ℝ V).equivFun.toContinuousLinearEquiv<GOAL>LocallyBoundedVariationOn (⇑A ∘ f) s
<VAR>V : Type u_1<VAR>R : Type u_2<VAR>inst✝³ : Fintype V<VAR>inst✝² : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝¹ : DecidableRel G.Adj<VAR>inst✝ : AddCommMonoidWithOne R<VAR>i : V<GOAL>↑{w | G.Adj i w}.toFinset.card = ∑ j : V, if G.Adj i j then 1 else 0
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : C<VAR>𝒯 : LimitCone (Functor.empty C)<VAR>ℬ : (X Y : C) → LimitCone (pair X Y)<VAR>X₁ X₂ : C<GOAL>tensorHom ℬ (𝟙 X₁) (𝟙 X₂) = 𝟙 (tensorObj ℬ X₁ X₂)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : C<VAR>𝒯 : LimitCone (Functor.empty C)<VAR>ℬ : (X Y : C) → LimitCone (pair X Y)<VAR>X₁ X₂ : C<GOAL>∀ (j : Discrete WalkingPair), tensorHom ℬ (𝟙 X₁) (𝟙 X₂) ≫ (ℬ X₁ X₂).cone.π.app j = 𝟙 (tensorObj ℬ X₁ X₂) ≫ (ℬ X₁ X₂).cone.π.app j
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s s₁ s₂ : Finset α<VAR>a : α<VAR>f✝ g : α → β<VAR>inst✝¹ : CommMonoid β<VAR>M : Type u_6<VAR>inst✝ : CommGroup M<VAR>f : ℕ → M<VAR>n : ℕ<GOAL>∏ i ∈ range n, f i / f (i + 1) = f 0 / f n
<VAR>X₁ X₂ Y : TopCat<VAR>f : C(↑X₁, ↑Y)<VAR>g : C(↑X₂, ↑Y)<VAR>x₀ x₁ : ↑X₁<VAR>x₂ x₃ : ↑X₂<VAR>p : Path x₀ x₁<VAR>q : Path x₂ x₃<VAR>hfg : ∀ (t : ↑I), f (p t) = g (q t)<GOAL>HEq ⟦p.map ⋯⟧ ⟦q.map ⋯⟧
<VAR>X₁ X₂ Y : TopCat<VAR>f : C(↑X₁, ↑Y)<VAR>g : C(↑X₂, ↑Y)<VAR>x₀ x₁ : ↑X₁<VAR>x₂ x₃ : ↑X₂<VAR>p : Path x₀ x₁<VAR>q : Path x₂ x₃<VAR>hfg : ∀ (t : ↑I), f (p t) = g (q t)<GOAL>∀ (t : ↑I), (p.map ⋯) t = (q.map ⋯) t
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝⁶ : SeminormedRing 𝕜<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module 𝕜 E<VAR>inst✝³ : SeminormedRing 𝕜₂<VAR>inst✝² : AddCommGroup E₂<VAR>inst✝¹ : Module 𝕜₂ E₂<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝ : RingHomIsometric σ₁₂<VAR>p✝ : Seminorm 𝕜 E<VAR>p : ι → Seminorm 𝕜 E<VAR>s : Finset ι<VAR>x : E<VAR>r : ℝ<VAR>hr : 0 < r<GOAL>(s.sup p).ball x r = s.inf fun i => (p i).ball x r
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝⁶ : SeminormedRing 𝕜<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module 𝕜 E<VAR>inst✝³ : SeminormedRing 𝕜₂<VAR>inst✝² : AddCommGroup E₂<VAR>inst✝¹ : Module 𝕜₂ E₂<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝ : RingHomIsometric σ₁₂<VAR>p✝ : Seminorm 𝕜 E<VAR>p : ι → Seminorm 𝕜 E<VAR>s : Finset ι<VAR>x : E<VAR>r : ℝ<VAR>hr : 0 < r<GOAL>(s.sup p).ball x r = ⨅ a ∈ s, (p a).ball x r
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>B : BilinForm R M<VAR>f g : Module.End R M<VAR>hf : f ∈ skewAdjointSubmodule B<VAR>hg : g ∈ skewAdjointSubmodule B<GOAL>⁅f, g⁆ ∈ skewAdjointSubmodule B
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>B : BilinForm R M<VAR>f g : Module.End R M<VAR>hf : IsSkewAdjoint B f<VAR>hg : IsSkewAdjoint B g<GOAL>IsSkewAdjoint B ⁅f, g⁆
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>B : BilinForm R M<VAR>f g : Module.End R M<VAR>hf : IsSkewAdjoint B f<VAR>hg : IsSkewAdjoint B g<VAR>hfg : IsAdjointPair B B (f * g) (g * f)<GOAL>IsSkewAdjoint B ⁅f, g⁆
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>B : BilinForm R M<VAR>f g : Module.End R M<VAR>hf : IsSkewAdjoint B f<VAR>hg : IsSkewAdjoint B g<VAR>hfg : IsAdjointPair B B (f * g) (g * f)<VAR>hgf : IsAdjointPair B B (g * f) (f * g)<GOAL>IsSkewAdjoint B ⁅f, g⁆
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>B : BilinForm R M<VAR>f g : Module.End R M<VAR>hf : IsSkewAdjoint B f<VAR>hg : IsSkewAdjoint B g<VAR>hfg : IsAdjointPair B B (f * g) (g * f)<VAR>hgf : IsAdjointPair B B (g * f) (f * g)<GOAL>IsAdjointPair B B (f * g - g * f) (-(f * g - g * f))
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>B : BilinForm R M<VAR>f g : Module.End R M<VAR>hf : IsSkewAdjoint B f<VAR>hg : IsSkewAdjoint B g<VAR>hfg : IsAdjointPair B B (f * g) (g * f)<VAR>hgf : IsAdjointPair B B (g * f) (f * g)<GOAL>IsAdjointPair B B (f * g - g * f) (g * f - f * g)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : CompleteSpace E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>μ ν : Measure α<VAR>s t : Set α<VAR>f✝ g f : α → E<GOAL>⨍ (x : α), f x ∂0 = 0
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Set V<VAR>hs : ∀ v ∈ s, v ≠ 0<VAR>p₁ : P<GOAL>(LinearIndependent k fun (v : ↑s) => ↑v) ↔ AffineIndependent k fun p => ↑p
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Set V<VAR>hs : ∀ v ∈ s, v ≠ 0<VAR>p₁ : P<GOAL>(LinearIndependent k fun (v : ↑s) => ↑v) ↔ LinearIndependent k fun (v : ↑((fun p => p -ᵥ p₁) '' (({p₁} ∪ (fun v => v +ᵥ p₁) '' s) \ {p₁}))) => ↑v
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Set V<VAR>hs : ∀ v ∈ s, v ≠ 0<VAR>p₁ : P<VAR>h : (fun p => p -ᵥ p₁) '' (({p₁} ∪ (fun v => v +ᵥ p₁) '' s) \ {p₁}) = s<GOAL>(LinearIndependent k fun (v : ↑s) => ↑v) ↔ LinearIndependent k fun (v : ↑((fun p => p -ᵥ p₁) '' (({p₁} ∪ (fun v => v +ᵥ p₁) '' s) \ {p₁}))) => ↑v
<VAR>α : Type u_1<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a✝ b a : α<GOAL>Icc a a = {a}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedAddCommGroup F<VAR>p : ℝ≥0∞<VAR>μ : Measure α<VAR>f g : ↥(simpleFunc E p μ)<GOAL>↑(toSimpleFunc (f + g)) =ᶠ[ae μ] ↑(toSimpleFunc f) + ↑(toSimpleFunc g)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedAddCommGroup F<VAR>p : ℝ≥0∞<VAR>μ : Measure α<VAR>f g : ↥(simpleFunc E p μ)<VAR>a✝ : α<GOAL>↑(toSimpleFunc (f + g)) a✝ = ↑↑↑(f + g) a✝ → ↑(toSimpleFunc f) a✝ = ↑↑↑f a✝ → ↑(toSimpleFunc g) a✝ = ↑↑↑g a✝ → ↑↑(↑f + ↑g) a✝ = (↑↑↑f + ↑↑↑g) a✝ → ↑(toSimpleFunc (f + g)) a✝ = (↑(toSimpleFunc f) + ↑(toSimpleFunc g)) a✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedAddCommGroup F<VAR>p : ℝ≥0∞<VAR>μ : Measure α<VAR>f g : ↥(simpleFunc E p μ)<VAR>a✝ : α<GOAL>↑(toSimpleFunc (f + g)) a✝ = ↑(↑↑f + ↑↑g) a✝ → ↑(toSimpleFunc f) a✝ = ↑↑↑f a✝ → ↑(toSimpleFunc g) a✝ = ↑↑↑g a✝ → ↑(↑↑f + ↑↑g) a✝ = ↑↑↑f a✝ + ↑↑↑g a✝ → ↑(toSimpleFunc (f + g)) a✝ = ↑(toSimpleFunc f) a✝ + ↑(toSimpleFunc g) a✝
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>f✝ : α → β<VAR>f : α → ℝ<VAR>s : Set α<VAR>K : ℝ≥0<VAR>hf : LipschitzOnWith K f s<GOAL>∃ g, LipschitzWith K g ∧ EqOn f g s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>f✝ : α → β<VAR>f : α → ℝ<VAR>K : ℝ≥0<VAR>hf : LipschitzOnWith K f ∅<GOAL>∃ g, LipschitzWith K g ∧ EqOn f g ∅
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>f✝ : α → β<VAR>f : α → ℝ<VAR>s : Set α<VAR>K : ℝ≥0<VAR>hf : LipschitzOnWith K f s<VAR>hs : s.Nonempty<GOAL>∃ g, LipschitzWith K g ∧ EqOn f g s