ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>f : α → E<VAR>hf : LocallyIntegrable f μ<VAR>u : ℕ → Set α<VAR>u_open : ∀ (n : ℕ), IsOpen (u n)<VAR>u_univ : ⋃ n, u n = univ<VAR>hu : ∀ (n : ℕ), IntegrableOn f (u n) μ<VAR>this : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, Tendsto (fun a => (∫⁻ (y : α) in a, ↑‖(u n).indicator f y - (u n).indicator f x‖₊ ∂μ) / μ a) (v.filterAt x) (𝓝 0)<VAR>x : α<VAR>hx : ∀ (i : ℕ), Tendsto (fun a => (∫⁻ (y : α) in a, ↑‖(u i).indicator f y - (u i).indicator f x‖₊ ∂μ) / μ a) (v.filterAt x) (𝓝 0)<VAR>n : ℕ<VAR>hn : x ∈ u n<VAR>a : Set α<VAR>ha : a ⊆ u n<VAR>h'a : MeasurableSet a<VAR>y : α<VAR>hy : y ∈ a<GOAL>↑‖(u n).indicator f y - (u n).indicator f x‖₊ = ↑‖f y - f x‖₊
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : TopologicalSpace 𝕜<VAR>inst✝ : OrderTopology 𝕜<VAR>p q : 𝕜<VAR>hp : Fact (0 < p)<VAR>n : ℕ<GOAL>Nat.card { u // addOrderOf u = n } = n.totient
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : TopologicalSpace 𝕜<VAR>inst✝ : OrderTopology 𝕜<VAR>p q : 𝕜<VAR>hp : Fact (0 < p)<GOAL>Nat.card { u // addOrderOf u = 0 } = Nat.totient 0
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : TopologicalSpace 𝕜<VAR>inst✝ : OrderTopology 𝕜<VAR>p q : 𝕜<VAR>hp : Fact (0 < p)<VAR>n : ℕ<VAR>hn : n > 0<GOAL>Nat.card { u // addOrderOf u = n } = n.totient
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>a : Ordinal.{u_4}<GOAL>a - 0 = a
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>E' : Type u_5<VAR>M' : Type u_6<VAR>H' : Type u_7<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : TopologicalSpace H<VAR>inst✝⁵ : TopologicalSpace M<VAR>f f' : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>inst✝⁴ : NormedAddCommGroup E'<VAR>inst✝³ : NormedSpace 𝕜 E'<VAR>inst✝² : TopologicalSpace H'<VAR>inst✝¹ : TopologicalSpace M'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>s t : Set M<VAR>inst✝ : ChartedSpace H M<VAR>hf : f ∈ maximalAtlas I M<VAR>hf' : f' ∈ maximalAtlas I M<VAR>x : E<VAR>hx : x ∈ ((f'.extend I).symm ≫ f.extend I).source<GOAL>ContDiffWithinAt 𝕜 ⊤ (↑(f.extend I) ∘ ↑(f'.extend I).symm) (range ↑I) x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>E' : Type u_5<VAR>M' : Type u_6<VAR>H' : Type u_7<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : TopologicalSpace H<VAR>inst✝⁵ : TopologicalSpace M<VAR>f f' : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>inst✝⁴ : NormedAddCommGroup E'<VAR>inst✝³ : NormedSpace 𝕜 E'<VAR>inst✝² : TopologicalSpace H'<VAR>inst✝¹ : TopologicalSpace M'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>s t : Set M<VAR>inst✝ : ChartedSpace H M<VAR>hf : f ∈ maximalAtlas I M<VAR>hf' : f' ∈ maximalAtlas I M<VAR>x : E<VAR>hx : x ∈ ((f'.extend I).symm ≫ f.extend I).source<GOAL>((f'.extend I).symm ≫ f.extend I).source ∈ 𝓝[range ↑I] x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>E' : Type u_5<VAR>M' : Type u_6<VAR>H' : Type u_7<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : TopologicalSpace H<VAR>inst✝⁵ : TopologicalSpace M<VAR>f f' : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>inst✝⁴ : NormedAddCommGroup E'<VAR>inst✝³ : NormedSpace 𝕜 E'<VAR>inst✝² : TopologicalSpace H'<VAR>inst✝¹ : TopologicalSpace M'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>s t : Set M<VAR>inst✝ : ChartedSpace H M<VAR>hf : f ∈ maximalAtlas I M<VAR>hf' : f' ∈ maximalAtlas I M<VAR>x : E<VAR>hx : x ∈ ↑I '' (f'.symm ≫ₕ f).source<GOAL>↑I '' (f'.symm ≫ₕ f).source ∈ 𝓝[range ↑I] x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>E' : Type u_5<VAR>M' : Type u_6<VAR>H' : Type u_7<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : TopologicalSpace H<VAR>inst✝⁵ : TopologicalSpace M<VAR>f f' : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>inst✝⁴ : NormedAddCommGroup E'<VAR>inst✝³ : NormedSpace 𝕜 E'<VAR>inst✝² : TopologicalSpace H'<VAR>inst✝¹ : TopologicalSpace M'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>s t : Set M<VAR>inst✝ : ChartedSpace H M<VAR>hf : f ∈ maximalAtlas I M<VAR>hf' : f' ∈ maximalAtlas I M<VAR>z : H<VAR>hz : z ∈ (f'.symm ≫ₕ f).source<GOAL>↑I '' (f'.symm ≫ₕ f).source ∈ 𝓝[range ↑I] ↑I z
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁸ : MeasurableSpace α<VAR>K : Type u_5<VAR>inst✝⁷ : SemilatticeSup β<VAR>inst✝⁶ : OrderBot β<VAR>inst✝⁵ : Zero β<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : OrderClosedTopology β<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : OpensMeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>i : ℕ → β<VAR>f : γ → β<VAR>g : α → γ<VAR>n : ℕ<VAR>a : α<VAR>hf : Measurable f<VAR>hg : Measurable g<GOAL>↑(approx i (f ∘ g) n) a = ↑(approx i f n) (g a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : LinearOrder α<VAR>inst✝³ : DenselyOrdered α<VAR>inst✝² : OrderTopology α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : T2Space β<VAR>f : α → β<VAR>a b : α<VAR>lb : β<VAR>hab : a < b<VAR>hb : Tendsto f (𝓝[<] b) (𝓝 lb)<GOAL>extendFrom (Ioo a b) f b = lb
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : LinearOrder α<VAR>inst✝³ : DenselyOrdered α<VAR>inst✝² : OrderTopology α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : T2Space β<VAR>f : α → β<VAR>a b : α<VAR>lb : β<VAR>hab : a < b<VAR>hb : Tendsto f (𝓝[<] b) (𝓝 lb)<GOAL>b ∈ closure (Ioo a b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : LinearOrder α<VAR>inst✝³ : DenselyOrdered α<VAR>inst✝² : OrderTopology α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : T2Space β<VAR>f : α → β<VAR>a b : α<VAR>lb : β<VAR>hab : a < b<VAR>hb : Tendsto f (𝓝[<] b) (𝓝 lb)<GOAL>Tendsto f (𝓝[Ioo a b] b) (𝓝 lb)
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : Group G'<VAR>inst✝³ : Group G''<VAR>A : Type u_4<VAR>inst✝² : AddGroup A<VAR>N : Type u_5<VAR>P : Type u_6<VAR>inst✝¹ : Group N<VAR>inst✝ : Group P<VAR>K H : Subgroup G<GOAL>H.subtype.range = H
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : Group G'<VAR>inst✝³ : Group G''<VAR>A : Type u_4<VAR>inst✝² : AddGroup A<VAR>N : Type u_5<VAR>P : Type u_6<VAR>inst✝¹ : Group N<VAR>inst✝ : Group P<VAR>K H : Subgroup G<GOAL>Subtype.val '' ↑⊤ = ↑H
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>a : ZMod p<VAR>hap : a ≠ 0<GOAL>Multiset.map (fun x => (a * ↑x).valMinAbs.natAbs) (Ico 1 (p / 2).succ).val = Multiset.map (fun a => a) (Ico 1 (p / 2).succ).val
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>a : ZMod p<VAR>hap : a ≠ 0<VAR>he : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x ≠ 0 ∧ x ≤ p / 2<GOAL>Multiset.map (fun x => (a * ↑x).valMinAbs.natAbs) (Ico 1 (p / 2).succ).val = Multiset.map (fun a => a) (Ico 1 (p / 2).succ).val
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>a : ZMod p<VAR>hap : a ≠ 0<VAR>he : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x ≠ 0 ∧ x ≤ p / 2<VAR>hep : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x < p<GOAL>Multiset.map (fun x => (a * ↑x).valMinAbs.natAbs) (Ico 1 (p / 2).succ).val = Multiset.map (fun a => a) (Ico 1 (p / 2).succ).val
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>a : ZMod p<VAR>hap : a ≠ 0<VAR>he : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x ≠ 0 ∧ x ≤ p / 2<VAR>hep : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x < p<VAR>hpe : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → ¬p ∣ x<GOAL>Multiset.map (fun x => (a * ↑x).valMinAbs.natAbs) (Ico 1 (p / 2).succ).val = Multiset.map (fun a => a) (Ico 1 (p / 2).succ).val
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>a : ZMod p<VAR>hap : a ≠ 0<VAR>he : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x ≠ 0 ∧ x ≤ p / 2<VAR>hep : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x < p<VAR>hpe : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → ¬p ∣ x<VAR>hmem : ∀ x ∈ Ico 1 (p / 2).succ, (a * ↑x).valMinAbs.natAbs ∈ Ico 1 (p / 2).succ<GOAL>Multiset.map (fun x => (a * ↑x).valMinAbs.natAbs) (Ico 1 (p / 2).succ).val = Multiset.map (fun a => a) (Ico 1 (p / 2).succ).val
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>a : ZMod p<VAR>hap : a ≠ 0<VAR>he : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x ≠ 0 ∧ x ≤ p / 2<VAR>hep : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x < p<VAR>hpe : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → ¬p ∣ x<VAR>hmem : ∀ x ∈ Ico 1 (p / 2).succ, (a * ↑x).valMinAbs.natAbs ∈ Ico 1 (p / 2).succ<VAR>hsurj : ∀ b ∈ Ico 1 (p / 2).succ, ∃ x, ∃ (_ : x ∈ Ico 1 (p / 2).succ), (a * ↑x).valMinAbs.natAbs = b<GOAL>Multiset.map (fun x => (a * ↑x).valMinAbs.natAbs) (Ico 1 (p / 2).succ).val = Multiset.map (fun a => a) (Ico 1 (p / 2).succ).val
<VAR>α : Type u_1<VAR>inst✝³ : DistribLattice α<VAR>inst✝² : OrderBot α<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidablePred SupIrred<VAR>a b : α<GOAL>(if h : IsEmpty α then ofIsEmpty else let_fun this := Fintype.toOrderBot α; RelEmbedding.trans OrderIso.lowerSetSupIrred.toOrderEmbedding { toFun := SetLike.coe, inj' := ⋯, map_rel_iff' := ⋯ }) (a ⊔ b) = (if h : IsEmpty α then ofIsEmpty else let_fun this := Fintype.toOrderBot α; RelEmbedding.trans OrderIso.lowerSetSupIrred.toOrderEmbedding { toFun := SetLike.coe, inj' := ⋯, map_rel_iff' := ⋯ }) a ∪ (if h : IsEmpty α then ofIsEmpty else let_fun this := Fintype.toOrderBot α; RelEmbedding.trans OrderIso.lowerSetSupIrred.toOrderEmbedding { toFun := SetLike.coe, inj' := ⋯, map_rel_iff' := ⋯ }) b
<VAR>α : Sort u_1<VAR>r p q : α → Prop<VAR>P Q : (x : α) → p x → Prop<VAR>b : Prop<GOAL>(∃ x x_1, r x) ↔ (∃ x x_1, r x) ∨ ∃ x x_1, r x
<VAR>α : Sort u_1<VAR>r p q : α → Prop<VAR>P Q : (x : α) → p x → Prop<VAR>b : Prop<GOAL>(∃ x, (p x ∨ q x) ∧ r x) ↔ (∃ x, p x ∧ r x) ∨ ∃ x, q x ∧ r x
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>e : Sym2 V<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableRel G.Adj<VAR>inst✝ : Nonempty V<GOAL>∃ v, G.maxDegree = G.degree v
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>e : Sym2 V<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableRel G.Adj<VAR>inst✝ : Nonempty V<VAR>t : ℕ<VAR>ht : (image (fun v => G.degree v) univ).max = ↑t<GOAL>∃ v, G.maxDegree = G.degree v
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>e : Sym2 V<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableRel G.Adj<VAR>inst✝ : Nonempty V<VAR>t : ℕ<VAR>ht : (image (fun v => G.degree v) univ).max = ↑t<VAR>ht₂ : t ∈ image (fun v => G.degree v) univ<GOAL>∃ v, G.maxDegree = G.degree v
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>e : Sym2 V<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableRel G.Adj<VAR>inst✝ : Nonempty V<VAR>t : ℕ<VAR>ht : (image (fun v => G.degree v) univ).max = ↑t<VAR>ht₂ : ∃ a, True ∧ G.degree a = t<GOAL>∃ v, G.maxDegree = G.degree v
<VAR>m n✝ n : ℕ<VAR>inst✝ : NeZero n<VAR>a : ℤ<GOAL>(fun p => p.1 * ↑n + ↑↑p.2) ((fun a => (a / ↑n, ↑(a.natMod ↑n))) a) = a
<VAR>m n✝ n : ℕ<VAR>inst✝ : NeZero n<VAR>x✝ : ℤ × Fin n<VAR>q : ℤ<VAR>r : ℕ<VAR>hrn : r < n<GOAL>(fun a => (a / ↑n, ↑(a.natMod ↑n))) ((fun p => p.1 * ↑n + ↑↑p.2) (q, ⟨r, hrn⟩)) = (q, ⟨r, hrn⟩)
<VAR>m n✝ n : ℕ<VAR>inst✝ : NeZero n<VAR>x✝ : ℤ × Fin n<VAR>q : ℤ<VAR>r : ℕ<VAR>hrn : r < n<GOAL>(q * ↑n + ↑r) / ↑n = q ∧ ↑↑((q * ↑n + ↑r).natMod ↑n) = r
<VAR>m n✝ n : ℕ<VAR>inst✝ : NeZero n<VAR>x✝ : ℤ × Fin n<VAR>q : ℤ<VAR>r : ℕ<VAR>hrn : r < n<VAR>h1 : 0 ≤ ↑r<VAR>h2 : ↑r < ↑n<GOAL>(q * ↑n + ↑r) / ↑n = q ∧ ↑↑((q * ↑n + ↑r).natMod ↑n) = r
<VAR>m n✝ n : ℕ<VAR>inst✝ : NeZero n<VAR>x✝ : ℤ × Fin n<VAR>q : ℤ<VAR>r : ℕ<VAR>hrn : r < n<VAR>h1 : 0 ≤ ↑r<VAR>h2 : ↑r < ↑n<GOAL>0 + q = q ∧ ↑↑r = r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι✝ : Sort u_4<VAR>ι' : Sort u_5<VAR>l✝ l' : Filter α<VAR>p✝ : ι✝ → Prop<VAR>s✝ : ι✝ → Set α<VAR>t : Set α<VAR>i : ι✝<VAR>p' : ι' → Prop<VAR>s' : ι' → Set α<VAR>i' : ι'<VAR>I : Type u_7<VAR>inst✝ : Finite I<VAR>l : I → Filter α<VAR>ι : I → Sort u_6<VAR>p : (i : I) → ι i → Prop<VAR>s : (i : I) → ι i → Set α<VAR>hd : Pairwise (Disjoint on l)<VAR>h : ∀ (i : I), (l i).HasBasis (p i) (s i)<GOAL>∃ ind, (∀ (i : I), p i (ind i)) ∧ Pairwise (Disjoint on fun i => s i (ind i))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι✝ : Sort u_4<VAR>ι' : Sort u_5<VAR>l✝ l' : Filter α<VAR>p✝ : ι✝ → Prop<VAR>s✝ : ι✝ → Set α<VAR>t✝ : Set α<VAR>i : ι✝<VAR>p' : ι' → Prop<VAR>s' : ι' → Set α<VAR>i' : ι'<VAR>I : Type u_7<VAR>inst✝ : Finite I<VAR>l : I → Filter α<VAR>ι : I → Sort u_6<VAR>p : (i : I) → ι i → Prop<VAR>s : (i : I) → ι i → Set α<VAR>hd✝ : Pairwise (Disjoint on l)<VAR>h : ∀ (i : I), (l i).HasBasis (p i) (s i)<VAR>t : I → Set α<VAR>htl : ∀ (i : I), t i ∈ l i<VAR>hd : Pairwise (Disjoint on t)<GOAL>∃ ind, (∀ (i : I), p i (ind i)) ∧ Pairwise (Disjoint on fun i => s i (ind i))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι✝ : Sort u_4<VAR>ι' : Sort u_5<VAR>l✝ l' : Filter α<VAR>p✝ : ι✝ → Prop<VAR>s✝ : ι✝ → Set α<VAR>t✝ : Set α<VAR>i : ι✝<VAR>p' : ι' → Prop<VAR>s' : ι' → Set α<VAR>i' : ι'<VAR>I : Type u_7<VAR>inst✝ : Finite I<VAR>l : I → Filter α<VAR>ι : I → Sort u_6<VAR>p : (i : I) → ι i → Prop<VAR>s : (i : I) → ι i → Set α<VAR>hd✝ : Pairwise (Disjoint on l)<VAR>h : ∀ (i : I), (l i).HasBasis (p i) (s i)<VAR>t : I → Set α<VAR>htl : ∀ (i : I), t i ∈ l i<VAR>hd : Pairwise (Disjoint on t)<VAR>ind : (i : I) → ι i<VAR>hp : ∀ (i : I), p i (ind i)<VAR>ht : ∀ (i : I), s i (ind i) ⊆ t i<GOAL>∃ ind, (∀ (i : I), p i (ind i)) ∧ Pairwise (Disjoint on fun i => s i (ind i))
<VAR>n : ℕ<GOAL>r 1 ^ n = 1
<VAR>n : ℕ<GOAL>r ↑n = r 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrderedCommMonoid α<VAR>a : α<GOAL>a * a < 1 ↔ a < 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>m : Measure α<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>(m.bind 0) s = 0 s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>m : Measure α<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>∫⁻ (μ : Measure β), μ s ∂map 0 m = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>m : Measure α<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>∫⁻ (a : α), (0 a) s ∂m = 0
<VAR>𝕜 : Type u_1<VAR>inst✝³⁷ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³⁶ : NormedAddCommGroup E<VAR>inst✝³⁵ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝³⁴ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝³³ : TopologicalSpace M<VAR>inst✝³² : ChartedSpace H M<VAR>inst✝³¹ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝³⁰ : NormedAddCommGroup E'<VAR>inst✝²⁹ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝²⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝²⁷ : TopologicalSpace M'<VAR>inst✝²⁶ : ChartedSpace H' M'<VAR>inst✝²⁵ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝²⁴ : NormedAddCommGroup E''<VAR>inst✝²³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝²² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝²¹ : TopologicalSpace M''<VAR>inst✝²⁰ : ChartedSpace H'' M''<VAR>F : Type u_11<VAR>inst✝¹⁹ : NormedAddCommGroup F<VAR>inst✝¹⁸ : NormedSpace 𝕜 F<VAR>G : Type u_12<VAR>inst✝¹⁷ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_13<VAR>inst✝¹⁶ : TopologicalSpace N<VAR>inst✝¹⁵ : ChartedSpace G N<VAR>inst✝¹⁴ : SmoothManifoldWithCorners J N<VAR>F' : Type u_14<VAR>inst✝¹³ : NormedAddCommGroup F'<VAR>inst✝¹² : NormedSpace 𝕜 F'<VAR>G' : Type u_15<VAR>inst✝¹¹ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_16<VAR>inst✝¹⁰ : TopologicalSpace N'<VAR>inst✝⁹ : ChartedSpace G' N'<VAR>inst✝⁸ : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_17<VAR>inst✝⁷ : NormedAddCommGroup F₁<VAR>inst✝⁶ : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_18<VAR>inst✝⁵ : NormedAddCommGroup F₂<VAR>inst✝⁴ : NormedSpace 𝕜 F₂<VAR>F₃ : Type u_19<VAR>inst✝³ : NormedAddCommGroup F₃<VAR>inst✝² : NormedSpace 𝕜 F₃<VAR>F₄ : Type u_20<VAR>inst✝¹ : NormedAddCommGroup F₄<VAR>inst✝ : NormedSpace 𝕜 F₄<VAR>e : PartialHomeomorph M H<VAR>e' : PartialHomeomorph M' H'<VAR>f f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x : M<VAR>m n : ℕ∞<GOAL>ContMDiffOn I I' n f s ↔ ContinuousOn f s ∧ ∀ (y : M'), ContMDiffOn I 𝓘(𝕜, E') n (↑(extChartAt I' y) ∘ f) (s ∩ f ⁻¹' (extChartAt I' y).source)
<VAR>𝕜 : Type u_1<VAR>inst✝³⁷ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³⁶ : NormedAddCommGroup E<VAR>inst✝³⁵ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝³⁴ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝³³ : TopologicalSpace M<VAR>inst✝³² : ChartedSpace H M<VAR>inst✝³¹ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝³⁰ : NormedAddCommGroup E'<VAR>inst✝²⁹ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝²⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝²⁷ : TopologicalSpace M'<VAR>inst✝²⁶ : ChartedSpace H' M'<VAR>inst✝²⁵ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝²⁴ : NormedAddCommGroup E''<VAR>inst✝²³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝²² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝²¹ : TopologicalSpace M''<VAR>inst✝²⁰ : ChartedSpace H'' M''<VAR>F : Type u_11<VAR>inst✝¹⁹ : NormedAddCommGroup F<VAR>inst✝¹⁸ : NormedSpace 𝕜 F<VAR>G : Type u_12<VAR>inst✝¹⁷ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_13<VAR>inst✝¹⁶ : TopologicalSpace N<VAR>inst✝¹⁵ : ChartedSpace G N<VAR>inst✝¹⁴ : SmoothManifoldWithCorners J N<VAR>F' : Type u_14<VAR>inst✝¹³ : NormedAddCommGroup F'<VAR>inst✝¹² : NormedSpace 𝕜 F'<VAR>G' : Type u_15<VAR>inst✝¹¹ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_16<VAR>inst✝¹⁰ : TopologicalSpace N'<VAR>inst✝⁹ : ChartedSpace G' N'<VAR>inst✝⁸ : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_17<VAR>inst✝⁷ : NormedAddCommGroup F₁<VAR>inst✝⁶ : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_18<VAR>inst✝⁵ : NormedAddCommGroup F₂<VAR>inst✝⁴ : NormedSpace 𝕜 F₂<VAR>F₃ : Type u_19<VAR>inst✝³ : NormedAddCommGroup F₃<VAR>inst✝² : NormedSpace 𝕜 F₃<VAR>F₄ : Type u_20<VAR>inst✝¹ : NormedAddCommGroup F₄<VAR>inst✝ : NormedSpace 𝕜 F₄<VAR>e : PartialHomeomorph M H<VAR>e' : PartialHomeomorph M' H'<VAR>f f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x : M<VAR>m n : ℕ∞<GOAL>ContinuousOn f s → ((∀ (x : M) (y : M'), ContDiffOn 𝕜 n (↑((chartAt H' y).toPartialEquiv ≫ I'.toPartialEquiv) ∘ f ∘ ↑((chartAt H x).toPartialEquiv ≫ I.toPartialEquiv).symm) (((chartAt H x).toPartialEquiv ≫ I.toPartialEquiv).target ∩ ↑((chartAt H x).toPartialEquiv ≫ I.toPartialEquiv).symm ⁻¹' (s ∩ f ⁻¹' ((chartAt H' y).toPartialEquiv ≫ I'.toPartialEquiv).source))) ↔ ∀ (y : M'), ContinuousOn (↑((chartAt H' y).toPartialEquiv ≫ I'.toPartialEquiv) ∘ f) (s ∩ f ⁻¹' ((chartAt H' y).toPartialEquiv ≫ I'.toPartialEquiv).source) ∧ ∀ (x : M), E' → ContDiffOn 𝕜 n (↑𝓘(𝕜, E').toPartialEquiv ∘ (↑((chartAt H' y).toPartialEquiv ≫ I'.toPartialEquiv) ∘ f) ∘ ↑((chartAt H x).toPartialEquiv ≫ I.toPartialEquiv).symm) (((chartAt H x).toPartialEquiv ≫ I.toPartialEquiv).target ∩ ↑((chartAt H x).toPartialEquiv ≫ I.toPartialEquiv).symm ⁻¹' (s ∩ f ⁻¹' ((chartAt H' y).toPartialEquiv ≫ I'.toPartialEquiv).source)))
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : Zero X<GOAL>Continuous toNNReal
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : Zero X<GOAL>Continuous (_root_.toContinuousMap ∘ toNNReal)
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : Zero X<GOAL>Continuous (ContinuousMap.toNNReal ∘ _root_.toContinuousMap)
<VAR>m n✝ n : ℕ<VAR>inst✝ : NeZero n<VAR>x : ZMod n<GOAL>x.valMinAbs * 2 ∈ Set.Ioc (-↑n) ↑n
<VAR>m n✝ n : ℕ<VAR>inst✝ : NeZero n<VAR>x : ZMod n<GOAL>(if ↑x.val * 2 ≤ ↑n then ↑x.val else ↑x.val - ↑n) * 2 ∈ Set.Ioc (-↑n) ↑n
<VAR>ι : Type u<VAR>X : Type v<VAR>inst✝² : TopologicalSpace X<VAR>s : Set X<VAR>f : BumpCovering ι X s<VAR>inst✝¹ : NormalSpace X<VAR>inst✝ : ParacompactSpace X<VAR>hs : IsClosed s<VAR>U : ι → Set X<VAR>ho : ∀ (i : ι), IsOpen (U i)<VAR>hU : s ⊆ ⋃ i, U i<GOAL>∃ f, f.IsSubordinate U
<VAR>ι : Type u<VAR>X : Type v<VAR>inst✝² : TopologicalSpace X<VAR>s : Set X<VAR>f : BumpCovering ι X s<VAR>inst✝¹ : NormalSpace X<VAR>inst✝ : ParacompactSpace X<VAR>hs : IsClosed s<VAR>U : ι → Set X<VAR>ho : ∀ (i : ι), IsOpen (U i)<VAR>hU : s ⊆ ⋃ i, U i<VAR>V : ι → Set X<VAR>hVo : ∀ (i : ι), IsOpen (V i)<VAR>hsV : s ⊆ ⋃ i, V i<VAR>hVf : LocallyFinite V<VAR>hVU : ∀ (i : ι), V i ⊆ U i<GOAL>∃ f, f.IsSubordinate U
<VAR>ι : Type u<VAR>X : Type v<VAR>inst✝² : TopologicalSpace X<VAR>s : Set X<VAR>f✝ : BumpCovering ι X s<VAR>inst✝¹ : NormalSpace X<VAR>inst✝ : ParacompactSpace X<VAR>hs : IsClosed s<VAR>U : ι → Set X<VAR>ho : ∀ (i : ι), IsOpen (U i)<VAR>hU : s ⊆ ⋃ i, U i<VAR>V : ι → Set X<VAR>hVo : ∀ (i : ι), IsOpen (V i)<VAR>hsV : s ⊆ ⋃ i, V i<VAR>hVf : LocallyFinite V<VAR>hVU : ∀ (i : ι), V i ⊆ U i<VAR>f : BumpCovering ι X s<VAR>hf : f.IsSubordinate V<GOAL>∃ f, f.IsSubordinate U
<VAR>α : Type u_1<VAR>M N : Matroid α<VAR>h : Disjoint M.E N.E<VAR>I X : Set α<GOAL>(M.disjointSum N h).Basis I X ↔ M.Basis (I ∩ M.E) (X ∩ M.E) ∧ N.Basis (I ∩ N.E) (X ∩ N.E) ∧ I ⊆ X ∧ X ⊆ M.E ∪ N.E
<VAR>M : Type u_1<VAR>inst✝⁵ : Monoid M<VAR>inst✝⁴ : MeasurableSpace M<VAR>inst✝³ : MeasurableMul₂ M<VAR>μ ν ρ : Measure M<VAR>inst✝² : SFinite μ<VAR>inst✝¹ : SFinite ν<VAR>inst✝ : SFinite ρ<GOAL>map (fun x => x.1 * x.2) ((μ + ν).prod ρ) = map (fun x => x.1 * x.2) (μ.prod ρ) + map (fun x => x.1 * x.2) (ν.prod ρ)
<VAR>M : Type u_1<VAR>inst✝⁵ : Monoid M<VAR>inst✝⁴ : MeasurableSpace M<VAR>inst✝³ : MeasurableMul₂ M<VAR>μ ν ρ : Measure M<VAR>inst✝² : SFinite μ<VAR>inst✝¹ : SFinite ν<VAR>inst✝ : SFinite ρ<GOAL>Measurable fun x => x.1 * x.2
<VAR>E : Type u_1<VAR>inst✝ : SeminormedCommGroup E<VAR>ε δ : ℝ<VAR>s t : Set E<VAR>x y : E<GOAL>ball x δ * {y} = ball (x * y) δ
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝¹² : EMetricSpace X<VAR>inst✝¹¹ : EMetricSpace Y<VAR>inst✝¹⁰ : MeasurableSpace X<VAR>inst✝⁹ : BorelSpace X<VAR>inst✝⁸ : MeasurableSpace Y<VAR>inst✝⁷ : BorelSpace Y<VAR>𝕜 : Type u_4<VAR>E : Type u_5<VAR>P : Type u_6<VAR>inst✝⁶ : NormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : MeasurableSpace P<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor E P<VAR>inst✝ : BorelSpace P<VAR>d : ℝ<VAR>hd : 0 ≤ d<VAR>x : P<VAR>c : 𝕜<VAR>hc : c ≠ 0<VAR>s : Set P<VAR>this✝¹ : MeasurableSpace E := borel E<VAR>this✝ : BorelSpace E<GOAL>μH[d] (⇑(IsometryEquiv.vaddConst x) '' ((fun x => c • x) '' (⇑(IsometryEquiv.vaddConst x).symm '' s))) = ‖c‖₊ ^ d • μH[d] s
<VAR>P : TopCat → Prop<VAR>X Y B : CompHausLike P<VAR>f : X ⟶ B<VAR>g : Y ⟶ B<VAR>inst✝ : HasExplicitPullback f g<VAR>Z : CompHausLike P<VAR>a b : Z ⟶ pullback f g<VAR>z : (forget (CompHausLike P)).obj Z<VAR>hfst : (a ≫ fst f g) z = (b ≫ fst f g) z<VAR>hsnd : (a ≫ snd f g) z = (b ≫ snd f g) z<GOAL>a z = b z
<VAR>P : TopCat → Prop<VAR>X Y B : CompHausLike P<VAR>f : X ⟶ B<VAR>g : Y ⟶ B<VAR>inst✝ : HasExplicitPullback f g<VAR>Z : CompHausLike P<VAR>a b : Z ⟶ pullback f g<VAR>z : (forget (CompHausLike P)).obj Z<VAR>hfst : (a ≫ fst f g) z = (b ≫ fst f g) z<VAR>hsnd : (a ≫ snd f g) z = (b ≫ snd f g) z<GOAL>↑(a z) = ↑(b z)
<VAR>P : TopCat → Prop<VAR>X Y B : CompHausLike P<VAR>f : X ⟶ B<VAR>g : Y ⟶ B<VAR>inst✝ : HasExplicitPullback f g<VAR>Z : CompHausLike P<VAR>a b : Z ⟶ pullback f g<VAR>z : (forget (CompHausLike P)).obj Z<VAR>hfst : (a ≫ fst f g) z = (b ≫ fst f g) z<VAR>hsnd : (a ≫ snd f g) z = (b ≫ snd f g) z<GOAL>(↑(a z)).1 = (↑(b z)).1
<VAR>P : TopCat → Prop<VAR>X Y B : CompHausLike P<VAR>f : X ⟶ B<VAR>g : Y ⟶ B<VAR>inst✝ : HasExplicitPullback f g<VAR>Z : CompHausLike P<VAR>a b : Z ⟶ pullback f g<VAR>z : (forget (CompHausLike P)).obj Z<VAR>hfst : (a ≫ fst f g) z = (b ≫ fst f g) z<VAR>hsnd : (a ≫ snd f g) z = (b ≫ snd f g) z<GOAL>(↑(a z)).2 = (↑(b z)).2
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s t : Set X<VAR>inst✝ : CompactSpace X<VAR>hs : s.Infinite<GOAL>∃ x, AccPt x (cofinite ⊓ 𝓟 s)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>X : Type u_5<VAR>inst✝¹ : TopologicalSpace X<VAR>ι' : Sort u_6<VAR>inst✝ : Mul M<VAR>t₁ t₂ : TopologicalSpace M<VAR>h₁ : ContinuousMul M<VAR>h₂ : ContinuousMul M<GOAL>ContinuousMul M