ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>inst✝² : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : IsFiniteMeasure ν<VAR>d : Set α → ℝ := fun s => ↑(μ s).toNNReal - ↑(ν s).toNNReal<VAR>c : Set ℝ := d '' {s | MeasurableSet s}<VAR>γ : ℝ := sSup c<VAR>hμ : ∀ (s : Set α), μ s ≠ ⊤<VAR>hν : ∀ (s : Set α), ν s ≠ ⊤<VAR>to_nnreal_μ : ∀ (s : Set α), ↑(μ s).toNNReal = μ s<VAR>to_nnreal_ν : ∀ (s : Set α), ↑(ν s).toNNReal = ν s<VAR>d_split : ∀ (s t : Set α), MeasurableSet t → d s = d (s \ t) + d (s ∩ t)<VAR>d_Union : ∀ (s : ℕ → Set α), Monotone s → Tendsto (fun n => d (s n)) atTop (𝓝 (d (⋃ n, s n)))<VAR>d_Inter : ∀ (s : ℕ → Set α), (∀ (n : ℕ), MeasurableSet (s n)) → (∀ (n m : ℕ), n ≤ m → s m ⊆ s n) → Tendsto (fun n => d (s n)) atTop (𝓝 (d (⋂ n, s n)))<VAR>bdd_c : BddAbove c<VAR>c_nonempty : c.Nonempty<VAR>d_le_γ : ∀ (s : Set α), MeasurableSet s → d s ≤ γ<VAR>this : ∀ (n : ℕ), ∃ s, MeasurableSet s ∧ γ - (1 / 2) ^ n < d s<VAR>e : ℕ → Set α<VAR>he : ∀ (x : ℕ), MeasurableSet (e x) ∧ γ - (1 / 2) ^ x < d (e x)<VAR>he₁ : ∀ (n : ℕ), MeasurableSet (e n)<VAR>he₂ : ∀ (n : ℕ), γ - (1 / 2) ^ n < d (e n)<VAR>f : ℕ → ℕ → Set α := fun n m => (Finset.Ico n (m + 1)).inf e<VAR>hf : ∀ (n m : ℕ), MeasurableSet (f n m)<VAR>f_subset_f : ∀ {a b c d : ℕ}, a ≤ b → c ≤ d → f a d ⊆ f b c<VAR>f_succ : ∀ (n m : ℕ), n ≤ m → f n (m + 1) = f n m ∩ e (m + 1)<VAR>le_d_f : ∀ (n m : ℕ), m ≤ n → γ - 2 * (1 / 2) ^ m + (1 / 2) ^ n ≤ d (f m n)<VAR>s : Set α := ⋃ m, ⋂ n, f m n<VAR>γ_le_d_s : γ ≤ d s<VAR>hs : MeasurableSet s<GOAL>∃ s, MeasurableSet s ∧ (∀ (t : Set α), MeasurableSet t → t ⊆ s → ν t ≤ μ t) ∧ ∀ (t : Set α), MeasurableSet t → t ⊆ sᶜ → μ t ≤ ν t
<VAR>R : Type u<VAR>S : Type v<VAR>k : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Field R<VAR>p q : R[X]<VAR>h : p.degree = 1<GOAL>p.IsRoot (-(p.coeff 0 / p.coeff 1))
<VAR>R : Type u<VAR>S : Type v<VAR>k : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Field R<VAR>p q : R[X]<VAR>h : p.degree = 1<VAR>this : p.coeff 1 ≠ 0<GOAL>p.IsRoot (-(p.coeff 0 / p.coeff 1))
<VAR>R : Type u<VAR>S : Type v<VAR>k : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Field R<VAR>p q : R[X]<VAR>h : p.degree = 1<VAR>this : p.coeff 1 ≠ 0<GOAL>(C (p.coeff 1) * X + C (p.coeff 0)).IsRoot (-(p.coeff 0 / p.coeff 1))
<VAR>α✝ : Sort u<VAR>β : Sort v<VAR>γ : Sort w<VAR>α : Type u_1<VAR>s t : Set α<VAR>h : s ⊆ t<VAR>inst✝ : DecidablePred fun x => x ∈ s<VAR>x : ↑t<VAR>hx : ↑x ∉ s<GOAL>(Set.sumDiffSubset h).symm x = Sum.inr ⟨↑x, ⋯⟩
<VAR>α✝ : Sort u<VAR>β : Sort v<VAR>γ : Sort w<VAR>α : Type u_1<VAR>s t : Set α<VAR>h : s ⊆ t<VAR>inst✝ : DecidablePred fun x => x ∈ s<VAR>x : ↑t<VAR>hx : ↑x ∉ s<GOAL>(Set.sumDiffSubset h) ((Set.sumDiffSubset h).symm x) = (Set.sumDiffSubset h) (Sum.inr ⟨↑x, ⋯⟩)
<VAR>α✝ : Sort u<VAR>β : Sort v<VAR>γ : Sort w<VAR>α : Type u_1<VAR>s t : Set α<VAR>h : s ⊆ t<VAR>inst✝ : DecidablePred fun x => x ∈ s<VAR>x : ↑t<VAR>hx : ↑x ∉ s<GOAL>x = inclusion ⋯ ⟨↑x, ⋯⟩
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>β : Type u_2<VAR>s✝ : Rel β β<VAR>s : RelSeries r<VAR>x : α<VAR>irrefl : Irreflexive r<GOAL>s.length ≠ 0 ↔ {x | x ∈ s}.Nontrivial
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>β : Type u_2<VAR>s✝ : Rel β β<VAR>s : RelSeries r<VAR>x : α<VAR>irrefl : Irreflexive r<VAR>h : s.length ≠ 0<VAR>rid : s.toFun 0 = s.toFun 1<GOAL>r (s.toFun 0) (s.toFun 0)
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>β : Type u_2<VAR>s✝ : Rel β β<VAR>s : RelSeries r<VAR>x : α<VAR>irrefl : Irreflexive r<VAR>h : s.length ≠ 0<VAR>rid : s.toFun 0 = s.toFun 1<GOAL>r (s.toFun 0) (s.toFun 1)
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>β : Type u_2<VAR>s✝ : Rel β β<VAR>s : RelSeries r<VAR>x : α<VAR>irrefl : Irreflexive r<VAR>h : s.length ≠ 0<VAR>rid : s.toFun 0 = s.toFun 1<GOAL>1 = ⟨0, ⋯⟩.succ
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>β : Type u_2<VAR>s✝ : Rel β β<VAR>s : RelSeries r<VAR>x : α<VAR>irrefl : Irreflexive r<VAR>h : s.length ≠ 0<VAR>rid : s.toFun 0 = s.toFun 1<GOAL>↑1 = ↑⟨0, ⋯⟩.succ
<VAR>E : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : FiniteDimensional ℝ V<VAR>inst✝¹ : MeasurableSpace V<VAR>inst✝ : BorelSpace V<VAR>f✝ : V → E<VAR>f : ℝ → E<VAR>hf : Integrable f volume<VAR>h'f : Differentiable ℝ f<VAR>hf' : Integrable (deriv f) volume<VAR>x : ℝ<GOAL>𝓕 (deriv f) x = (2 * ↑π * I * ↑x) • 𝓕 f x
<VAR>E : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : FiniteDimensional ℝ V<VAR>inst✝¹ : MeasurableSpace V<VAR>inst✝ : BorelSpace V<VAR>f✝ : V → E<VAR>f : ℝ → E<VAR>hf : Integrable f volume<VAR>h'f : Differentiable ℝ f<VAR>hf' : Integrable (deriv f) volume<VAR>x : ℝ<VAR>I : Integrable (fun x => fderiv ℝ f x) volume<GOAL>𝓕 (deriv f) x = (2 * ↑π * Complex.I * ↑x) • 𝓕 f x
<VAR>E : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : FiniteDimensional ℝ V<VAR>inst✝¹ : MeasurableSpace V<VAR>inst✝ : BorelSpace V<VAR>f✝ : V → E<VAR>f : ℝ → E<VAR>hf : Integrable f volume<VAR>h'f : Differentiable ℝ f<VAR>hf' : Integrable (deriv f) volume<VAR>x : ℝ<VAR>I : Integrable (fun x => fderiv ℝ f x) volume<VAR>this : 𝓕 (deriv f) x = (𝓕 (fderiv ℝ f) x) 1<GOAL>𝓕 (deriv f) x = (2 * ↑π * Complex.I * ↑x) • 𝓕 f x
<VAR>E : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : FiniteDimensional ℝ V<VAR>inst✝¹ : MeasurableSpace V<VAR>inst✝ : BorelSpace V<VAR>f✝ : V → E<VAR>f : ℝ → E<VAR>hf : Integrable f volume<VAR>h'f : Differentiable ℝ f<VAR>hf' : Integrable (deriv f) volume<VAR>x : ℝ<VAR>I : Integrable (fun x => fderiv ℝ f x) volume<VAR>this : 𝓕 (deriv f) x = (𝓕 (fderiv ℝ f) x) 1<GOAL>(fourierSMulRight (-innerSL ℝ) (𝓕 f) x) 1 = (2 * ↑π * Complex.I * ↑x) • 𝓕 f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v}<VAR>a : Ordinal.{max v u}<GOAL>lsub f ≤ a ↔ ∀ (i : ι), f i < a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v}<VAR>a : Ordinal.{max v u}<VAR>a✝ : ι<GOAL>f a✝ < a ↔ (succ ∘ f) a✝ ≤ a
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_5, u_1} C<VAR>inst✝³ : Preadditive C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>I₁₂ : Type u_4<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K L M : HomologicalComplex₂ C c₁ c₂<VAR>φ : K ⟶ L<VAR>e : K ≅ L<VAR>ψ : L ⟶ M<VAR>c₁₂ : ComplexShape I₁₂<VAR>inst✝² : DecidableEq I₁₂<VAR>inst✝¹ : TotalComplexShape c₁ c₂ c₁₂<VAR>inst✝ : K.HasTotal c₁₂<VAR>i₁₂ i₁₂' : I₁₂<VAR>i₁ : I₁<VAR>i₂ : I₂<VAR>h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂<GOAL>K.ιTotal c₁₂ i₁ i₂ i₁₂ h ≫ K.D₁ c₁₂ i₁₂ i₁₂' = K.d₁ c₁₂ i₁ i₂ 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>l₁ l₂ : Filter α<GOAL>(diagonal α)ᶜ ∈ l₁ ×ˢ l₂ ↔ Disjoint l₁ l₂
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝⁴ : PartialOrder α<VAR>inst✝³ : PartialOrder β<VAR>inst✝² : OrderBot α<VAR>inst✝¹ : IsAtomic α<VAR>inst✝ : OrderBot β<VAR>l : α → β<VAR>u : β → α<VAR>gi : GaloisInsertion l u<VAR>hbot : u ⊥ = ⊥<VAR>h_atom : ∀ (a : α), IsAtom a → u (l a) = a<VAR>b : β<GOAL>IsAtom (u b) ↔ IsAtom b
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>R : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝³ : MeasurableSpace β<VAR>inst✝² : MeasurableSpace γ<VAR>inst✝¹ : MeasurableSpace δ<VAR>f g : α → β<VAR>μ✝ ν : Measure α<VAR>inst✝ : Countable ι<VAR>μ : ι → Measure α<VAR>h : ∀ (i : ι), AEMeasurable f (μ i)<VAR>a✝ : Nontrivial β<VAR>inhabited_h : Inhabited β<VAR>s : ι → Set α := fun i => toMeasurable (μ i) {x | f x ≠ mk f ⋯ x}<GOAL>AEMeasurable f (sum μ)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>R : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝³ : MeasurableSpace β<VAR>inst✝² : MeasurableSpace γ<VAR>inst✝¹ : MeasurableSpace δ<VAR>f g : α → β<VAR>μ✝ ν : Measure α<VAR>inst✝ : Countable ι<VAR>μ : ι → Measure α<VAR>h : ∀ (i : ι), AEMeasurable f (μ i)<VAR>a✝ : Nontrivial β<VAR>inhabited_h : Inhabited β<VAR>s : ι → Set α := fun i => toMeasurable (μ i) {x | f x ≠ mk f ⋯ x}<VAR>hsμ : ∀ (i : ι), (μ i) (s i) = 0<GOAL>AEMeasurable f (sum μ)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>R : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝³ : MeasurableSpace β<VAR>inst✝² : MeasurableSpace γ<VAR>inst✝¹ : MeasurableSpace δ<VAR>f g : α → β<VAR>μ✝ ν : Measure α<VAR>inst✝ : Countable ι<VAR>μ : ι → Measure α<VAR>h : ∀ (i : ι), AEMeasurable f (μ i)<VAR>a✝ : Nontrivial β<VAR>inhabited_h : Inhabited β<VAR>s : ι → Set α := fun i => toMeasurable (μ i) {x | f x ≠ mk f ⋯ x}<VAR>hsμ : ∀ (i : ι), (μ i) (s i) = 0<VAR>hsm : MeasurableSet (⋂ i, s i)<GOAL>AEMeasurable f (sum μ)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>R : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝³ : MeasurableSpace β<VAR>inst✝² : MeasurableSpace γ<VAR>inst✝¹ : MeasurableSpace δ<VAR>f g : α → β<VAR>μ✝ ν : Measure α<VAR>inst✝ : Countable ι<VAR>μ : ι → Measure α<VAR>h : ∀ (i : ι), AEMeasurable f (μ i)<VAR>a✝ : Nontrivial β<VAR>inhabited_h : Inhabited β<VAR>s : ι → Set α := fun i => toMeasurable (μ i) {x | f x ≠ mk f ⋯ x}<VAR>hsμ : ∀ (i : ι), (μ i) (s i) = 0<VAR>hsm : MeasurableSet (⋂ i, s i)<VAR>hs : ∀ (i : ι), ∀ x ∉ s i, f x = mk f ⋯ x<GOAL>AEMeasurable f (sum μ)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>R : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝³ : MeasurableSpace β<VAR>inst✝² : MeasurableSpace γ<VAR>inst✝¹ : MeasurableSpace δ<VAR>f g✝ : α → β<VAR>μ✝ ν : Measure α<VAR>inst✝ : Countable ι<VAR>μ : ι → Measure α<VAR>h : ∀ (i : ι), AEMeasurable f (μ i)<VAR>a✝ : Nontrivial β<VAR>inhabited_h : Inhabited β<VAR>s : ι → Set α := fun i => toMeasurable (μ i) {x | f x ≠ mk f ⋯ x}<VAR>hsμ : ∀ (i : ι), (μ i) (s i) = 0<VAR>hsm : MeasurableSet (⋂ i, s i)<VAR>hs : ∀ (i : ι), ∀ x ∉ s i, f x = mk f ⋯ x<VAR>g : α → β := (⋂ i, s i).piecewise (const α default) f<GOAL>AEMeasurable f (sum μ)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>R : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝³ : MeasurableSpace β<VAR>inst✝² : MeasurableSpace γ<VAR>inst✝¹ : MeasurableSpace δ<VAR>f g✝ : α → β<VAR>μ✝ ν : Measure α<VAR>inst✝ : Countable ι<VAR>μ : ι → Measure α<VAR>h : ∀ (i : ι), AEMeasurable f (μ i)<VAR>a✝ : Nontrivial β<VAR>inhabited_h : Inhabited β<VAR>s : ι → Set α := fun i => toMeasurable (μ i) {x | f x ≠ mk f ⋯ x}<VAR>hsμ : ∀ (i : ι), (μ i) (s i) = 0<VAR>hsm : MeasurableSet (⋂ i, s i)<VAR>hs : ∀ (i : ι), ∀ x ∉ s i, f x = mk f ⋯ x<VAR>g : α → β := (⋂ i, s i).piecewise (const α default) f<GOAL>Measurable ((⋂ i, s i).restrict g)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>R : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝³ : MeasurableSpace β<VAR>inst✝² : MeasurableSpace γ<VAR>inst✝¹ : MeasurableSpace δ<VAR>f g✝ : α → β<VAR>μ✝ ν : Measure α<VAR>inst✝ : Countable ι<VAR>μ : ι → Measure α<VAR>h : ∀ (i : ι), AEMeasurable f (μ i)<VAR>a✝ : Nontrivial β<VAR>inhabited_h : Inhabited β<VAR>s : ι → Set α := fun i => toMeasurable (μ i) {x | f x ≠ mk f ⋯ x}<VAR>hsμ : ∀ (i : ι), (μ i) (s i) = 0<VAR>hsm : MeasurableSet (⋂ i, s i)<VAR>hs : ∀ (i : ι), ∀ x ∉ s i, f x = mk f ⋯ x<VAR>g : α → β := (⋂ i, s i).piecewise (const α default) f<GOAL>Measurable ((⋂ i, s i)ᶜ.restrict g)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>R : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝³ : MeasurableSpace β<VAR>inst✝² : MeasurableSpace γ<VAR>inst✝¹ : MeasurableSpace δ<VAR>f g✝ : α → β<VAR>μ✝ ν : Measure α<VAR>inst✝ : Countable ι<VAR>μ : ι → Measure α<VAR>h : ∀ (i : ι), AEMeasurable f (μ i)<VAR>a✝ : Nontrivial β<VAR>inhabited_h : Inhabited β<VAR>s : ι → Set α := fun i => toMeasurable (μ i) {x | f x ≠ mk f ⋯ x}<VAR>hsμ : ∀ (i : ι), (μ i) (s i) = 0<VAR>hsm : MeasurableSet (⋂ i, s i)<VAR>hs : ∀ (i : ι), ∀ x ∉ s i, f x = mk f ⋯ x<VAR>g : α → β := (⋂ i, s i).piecewise (const α default) f<VAR>i : ι<GOAL>∀ᵐ (x : α) ∂μ i, f x = g x
<VAR>α : Type u_1<VAR>inst✝ : AddCommGroup α<VAR>p a a₁ a₂ b b₁ b₂ c : α<VAR>n : ℕ<VAR>z : ℤ<VAR>x✝ : a₂ ≡ b₂ [PMOD p]<VAR>m : ℤ<VAR>hm : b₂ - a₂ = m • p<GOAL>(∃ b, b₁ + b₂ - (a₁ + a₂) = (Equiv.symm (Equiv.addRight m)).symm b • p) ↔ a₁ ≡ b₁ [PMOD p]
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : 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>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>F : ι → β → α<VAR>S : Set β<VAR>u : α → γ<VAR>hu : UniformInducing u<GOAL>UniformEquicontinuousOn F S ↔ UniformEquicontinuousOn ((fun x => u ∘ x) ∘ F) S
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : 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>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>F : ι → β → α<VAR>S : Set β<VAR>u : α → γ<VAR>hu : UniformInducing u<VAR>this : UniformInducing (⇑UniformFun.ofFun ∘ (fun x => u ∘ x) ∘ ⇑toFun)<GOAL>UniformEquicontinuousOn F S ↔ UniformEquicontinuousOn ((fun x => u ∘ x) ∘ F) S
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : 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>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>F : ι → β → α<VAR>S : Set β<VAR>u : α → γ<VAR>hu : UniformInducing u<VAR>this : UniformInducing (⇑UniformFun.ofFun ∘ (fun x => u ∘ x) ∘ ⇑toFun)<GOAL>UniformContinuousOn ((⇑UniformFun.ofFun ∘ (fun x => u ∘ x) ∘ ⇑toFun) ∘ ⇑UniformFun.ofFun ∘ swap F) S ↔ UniformContinuousOn (⇑UniformFun.ofFun ∘ swap ((fun x => u ∘ x) ∘ F)) S
<VAR>F : Type u_1<VAR>K✝¹ : Type u_2<VAR>L : Type u_3<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Field K✝¹<VAR>inst✝³ : Field L<VAR>inst✝² : Algebra F K✝¹<VAR>inst✝¹ : Algebra F L<VAR>K✝ K' : IntermediateField F L<VAR>inst✝ : Normal F L<VAR>K : IntermediateField F L<GOAL>Normal F ↥K ↔ ∀ (σ : ↥K →ₐ[F] L), σ.fieldRange ≤ K
<VAR>P : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Membership P L<VAR>inst✝² : ProjectivePlane P L<VAR>inst✝¹ : Finite P<VAR>inst✝ : Finite L<VAR>p : P<GOAL>2 < lineCount L p
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x✝ y x : V<VAR>hx : x ≠ 0<GOAL>angle (-x) x = π
<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>σ : Equiv.Perm α<VAR>s : Finset α<VAR>f : α → β<VAR>hs : {a | σ a ≠ a} ⊆ ↑s<GOAL>∏ x ∈ s, f (σ x) = ∏ x ∈ s, f x
<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>σ : Equiv.Perm α<VAR>s : Finset α<VAR>f : α → β<VAR>hs : {a | σ a ≠ a} ⊆ ↑s<GOAL>s = map (Equiv.toEmbedding σ) s
<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✝ : RegularSpace β<VAR>f : α → β<VAR>a b : α<VAR>la : β<VAR>hab : a < b<VAR>hf : ContinuousOn f (Ioo a b)<VAR>ha : Tendsto f (𝓝[>] a) (𝓝 la)<GOAL>ContinuousOn (extendFrom (Ioo a b) f) (Ico 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✝ : RegularSpace β<VAR>f : α → β<VAR>a b : α<VAR>la : β<VAR>hab : a < b<VAR>hf : ContinuousOn f (Ioo a b)<VAR>ha : Tendsto f (𝓝[>] a) (𝓝 la)<GOAL>Ico a 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✝ : RegularSpace β<VAR>f : α → β<VAR>a b : α<VAR>la : β<VAR>hab : a < b<VAR>hf : ContinuousOn f (Ioo a b)<VAR>ha : Tendsto f (𝓝[>] a) (𝓝 la)<GOAL>∀ x ∈ Ico a b, ∃ y, Tendsto f (𝓝[Ioo a b] x) (𝓝 y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_4<VAR>inst✝³ : Primcodable α<VAR>inst✝² : Primcodable β<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Primcodable σ<VAR>n : ℕ<VAR>f : Fin (n + 1) → α → σ<VAR>hf : ∀ (i : Fin (n + 1)), Primrec (f i)<GOAL>Primrec fun a => List.ofFn fun i => f i a
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace ℝ F'<VAR>inst✝¹ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>f✝ g : α → E<VAR>μ' : Measure α<VAR>hT_add : DominatedFinMeasAdditive (μ + μ') T C'<VAR>hT : DominatedFinMeasAdditive μ' T C<VAR>f : α → E<VAR>hf : Integrable f (μ + μ')<GOAL>setToFun (μ + μ') T hT_add f = setToFun μ' T hT f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace ℝ F'<VAR>inst✝¹ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>f✝ g : α → E<VAR>μ' : Measure α<VAR>hT_add : DominatedFinMeasAdditive (μ + μ') T C'<VAR>hT : DominatedFinMeasAdditive μ' T C<VAR>f : α → E<VAR>hf : Integrable f (μ + μ')<GOAL>μ' ≤ 1 • (μ + μ')
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace ℝ F'<VAR>inst✝¹ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>f✝ g : α → E<VAR>μ' : Measure α<VAR>hT_add : DominatedFinMeasAdditive (μ + μ') T C'<VAR>hT : DominatedFinMeasAdditive μ' T C<VAR>f : α → E<VAR>hf : Integrable f (μ + μ')<GOAL>μ' ≤ μ + μ'
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace ℝ F'<VAR>inst✝¹ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>f✝ g : α → E<VAR>μ' : Measure α<VAR>hT_add : DominatedFinMeasAdditive (μ + μ') T C'<VAR>hT : DominatedFinMeasAdditive μ' T C<VAR>f : α → E<VAR>hf : Integrable f (μ + μ')<GOAL>0 + μ' ≤ μ + μ'
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝¹ : EMetricSpace X<VAR>inst✝ : EMetricSpace Y<VAR>m✝ : Set X → ℝ≥0∞<VAR>r : ℝ≥0∞<VAR>μ : OuterMeasure X<VAR>s✝ : Set X<VAR>m : Set X → ℝ≥0∞<VAR>s : Set X<GOAL>(mkMetric' m) s = (⨆ n, pre m (↑n)⁻¹) s
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝¹ : EMetricSpace X<VAR>inst✝ : EMetricSpace Y<VAR>m✝ : Set X → ℝ≥0∞<VAR>r : ℝ≥0∞<VAR>μ : OuterMeasure X<VAR>s✝ : Set X<VAR>m : Set X → ℝ≥0∞<VAR>s : Set X<GOAL>(mkMetric' m) s = ⨆ i, (pre m (↑i)⁻¹) s
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>R : Type u_5<VAR>α : Type v<VAR>β : Type w<VAR>ι : Type u_6<VAR>M : Matrix m n α<VAR>i✝ : m<VAR>j : n<VAR>b : n → α<VAR>c : m → α<VAR>inst✝¹ : DecidableEq l<VAR>inst✝ : DecidableEq m<VAR>A : Matrix m n α<VAR>i : m<VAR>r : n → α<VAR>e : l ≃ m<VAR>f : o ≃ n<GOAL>(A.updateRow i r).submatrix ⇑e ⇑f = (A.updateRow (e (e.symm i)) fun j => r (f (f.symm j))).submatrix ⇑e ⇑f
<VAR>n p : ℕ<VAR>hpos : n ≠ 0<VAR>h : ∀ {d : ℕ}, Prime d → d ∣ n → d = p<VAR>k : ℕ := n.primeFactorsList.length<GOAL>n = p ^ k
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x✝ y✝ x y z : V<VAR>h : angle x y = π<GOAL>angle x z + angle y z = π
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x✝ y x z : V<VAR>left✝ : x ≠ 0<VAR>r : ℝ<VAR>hr : r < 0<VAR>h : angle x (r • x) = π<GOAL>angle x z + angle (r • x) z = π
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝¹ : Category.{v, u} V<VAR>inst✝ : HasZeroMorphisms V<VAR>X₀ X₁ X₂ : V<VAR>d₀ : X₁ ⟶ X₀<VAR>d₁ : X₂ ⟶ X₁<VAR>s : d₁ ≫ d₀ = 0<VAR>succ : (S : ShortComplex V) → (X₃ : V) ×' (d₂ : X₃ ⟶ S.X₁) ×' d₂ ≫ S.f = 0<VAR>succ' : {X₀ X₁ : V} → (f : X₁ ⟶ X₀) → (X₂ : V) ×' (d : X₂ ⟶ X₁) ×' d ≫ f = 0<GOAL>(if 1 = 0 + 1 then 𝟙 X₁ ≫ d₀ else 0) = d₀
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r r₁ r₂ : α → α → Prop<VAR>s t : Set α<VAR>a b x : α<VAR>inst✝ : IsAntisymm α r<GOAL>x ∈ maximals r s ↔ x ∈ s ∧ ∀ ⦃y : α⦄, y ∈ s → r x y → x = y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r r₁ r₂ : α → α → Prop<VAR>s t : Set α<VAR>a b x : α<VAR>inst✝ : IsAntisymm α r<GOAL>x ∈ s → ((∀ ⦃b : α⦄, b ∈ s → r x b → r b x) ↔ ∀ ⦃y : α⦄, y ∈ s → r x y → x = y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r r₁ r₂ : α → α → Prop<VAR>s t : Set α<VAR>a b x : α<VAR>inst✝ : IsAntisymm α r<VAR>x✝ : x ∈ s<VAR>h : ∀ ⦃y : α⦄, y ∈ s → r x y → x = y<VAR>y : α<VAR>hys : y ∈ s<VAR>hxy : r x y<GOAL>r y x
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : MonoidalCategory C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>inst✝ : MonoidalCategory D<VAR>F : OplaxMonoidalFunctor C D<VAR>X Y X' Y' : C<VAR>f : X ⟶ Y<VAR>g : X' ⟶ Y'<GOAL>F.δ X X' ≫ (F.map f ⊗ F.map g) = F.map (f ⊗ g) ≫ F.δ Y Y'
<VAR>α β : Type u<VAR>c : Cardinal.{u_1}<GOAL>2 ≤ c ↔ 1 < c
<VAR>α β : Type u<VAR>c : Cardinal.{u_1}<GOAL>2 = ↑1 + 1
<VAR>x : ℝ≥0∞<GOAL>0 < ↑x ↔ 0 < x
<VAR>α : Type u_1<VAR>inst✝⁵ : AddCommSemigroup α<VAR>inst✝⁴ : PartialOrder α<VAR>inst✝³ : ExistsAddOfLE α<VAR>inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝¹ : Sub α<VAR>inst✝ : OrderedSub α<VAR>a b c d : α<VAR>h : a ≤ b<GOAL>b - a + a = b
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>𝕜 : Type u_4<VAR>E : Type u_5<VAR>s : Finset ℕ<VAR>k n a b : ℕ<GOAL>addRothNumber (Ico a b) = rothNumberNat (b - a)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>𝕜 : Type u_4<VAR>E : Type u_5<VAR>s : Finset ℕ<VAR>k n a b : ℕ<VAR>h : b ≤ a<GOAL>addRothNumber (Ico a b) = rothNumberNat (b - a)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>𝕜 : Type u_4<VAR>E : Type u_5<VAR>s : Finset ℕ<VAR>k n a b : ℕ<VAR>h : a ≤ b<GOAL>addRothNumber (Ico a b) = rothNumberNat (b - a)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>𝕜 : Type u_4<VAR>E : Type u_5<VAR>s : Finset ℕ<VAR>k n a b : ℕ<VAR>h : a ≤ b<GOAL>Ico a b = map (addLeftEmbedding a) (range (b - a))
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>𝕜 : Type u_4<VAR>E : Type u_5<VAR>s : Finset ℕ<VAR>k n a b : ℕ<VAR>h : a ≤ b<GOAL>Ico a b = image (⇑(addLeftEmbedding a)) (Ico 0 (b - a))
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>𝕜 : Type u_4<VAR>E : Type u_5<VAR>s : Finset ℕ<VAR>k n a b : ℕ<VAR>h : a ≤ b<GOAL>b = a + (b - a)