ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>β : ι → Type u_4<VAR>mβ : (i : ι) → MeasurableSpace (β i)<VAR>_mα : MeasurableSpace α<VAR>m : ι → MeasurableSpace Ω<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μ : Measure α<VAR>π : ι → Set (Set Ω)<VAR>s : ι → Set Ω<VAR>S : Finset ι<VAR>f : (x : ι) → Ω → β x<VAR>inst✝ : Fintype ι<VAR>h : iIndepSets π κ μ<VAR>hs : ∀ (i : ι), s i ∈ π i<GOAL>∀ᵐ (a : α) ∂μ, (κ a) (⋂ i, s i) = ∏ i : ι, (κ a) (s i)
<VAR>X : Scheme<VAR>inst✝¹ : IsIntegral X<VAR>U : X.Opens<VAR>hU : IsAffineOpen U<VAR>inst✝ : Nonempty ↑↑(↑U).toPresheafedSpace<VAR>this : IsAffine ↑U<GOAL>IsFractionRing ↑Γ(X, U) ↑X.functionField
<VAR>X : Scheme<VAR>inst✝¹ : IsIntegral X<VAR>U : X.Opens<VAR>hU : IsAffineOpen U<VAR>inst✝ : Nonempty ↑↑(↑U).toPresheafedSpace<VAR>this✝ : IsAffine ↑U<VAR>this : IsIntegral ↑U<GOAL>IsFractionRing ↑Γ(X, U) ↑X.functionField
<VAR>X : Scheme<VAR>inst✝¹ : IsIntegral X<VAR>U : X.Opens<VAR>hU : IsAffineOpen U<VAR>inst✝ : Nonempty ↑↑(↑U).toPresheafedSpace<VAR>this✝ : IsAffine ↑U<VAR>this : IsIntegral ↑U<GOAL>IsLocalization (nonZeroDivisors ↑Γ(X, U)) ↑(X.presheaf.stalk (genericPoint ↑↑X.toPresheafedSpace))
<VAR>X : Scheme<VAR>inst✝¹ : IsIntegral X<VAR>U : X.Opens<VAR>hU : IsAffineOpen U<VAR>inst✝ : Nonempty ↑↑(↑U).toPresheafedSpace<VAR>this✝ : IsAffine ↑U<VAR>this : IsIntegral ↑U<GOAL>nonZeroDivisors ↑Γ(X, U) = (hU.primeIdealOf ⟨genericPoint ↑↑X.toPresheafedSpace, ⋯⟩).asIdeal.primeCompl
<VAR>X : Scheme<VAR>inst✝¹ : IsIntegral X<VAR>U : X.Opens<VAR>hU : IsAffineOpen U<VAR>inst✝ : Nonempty ↑↑(↑U).toPresheafedSpace<VAR>this✝ : IsAffine ↑U<VAR>this : IsIntegral ↑U<GOAL>nonZeroDivisors ↑Γ(X, U) = ⊥.asIdeal.primeCompl
<VAR>X : Scheme<VAR>inst✝¹ : IsIntegral X<VAR>U : X.Opens<VAR>hU : IsAffineOpen U<VAR>inst✝ : Nonempty ↑↑(↑U).toPresheafedSpace<VAR>this✝ : IsAffine ↑U<VAR>this : IsIntegral ↑U<VAR>x✝ : ↑Γ(X, U)<GOAL>x✝ ∈ nonZeroDivisors ↑Γ(X, U) ↔ x✝ ∈ ⊥.asIdeal.primeCompl
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν✝ μ ν : Measure α<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : IsFiniteMeasure ν<VAR>h : ¬μ ⟂ₘ ν<GOAL>∃ ε, 0 < ε ∧ ∃ E, MeasurableSet E ∧ 0 < ν E ∧ VectorMeasure.restrict 0 E ≤ VectorMeasure.restrict (μ.toSignedMeasure - (ε • ν).toSignedMeasure) E
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν✝ μ ν : Measure α<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : IsFiniteMeasure ν<VAR>h : ¬μ ⟂ₘ ν<VAR>this : ∀ (n : ℕ), ∃ i, MeasurableSet i ∧ VectorMeasure.restrict 0 i ≤ VectorMeasure.restrict (μ.toSignedMeasure - ((1 / (↑n + 1)) • ν).toSignedMeasure) i ∧ VectorMeasure.restrict (μ.toSignedMeasure - ((1 / (↑n + 1)) • ν).toSignedMeasure) iᶜ ≤ VectorMeasure.restrict 0 iᶜ<GOAL>∃ ε, 0 < ε ∧ ∃ E, MeasurableSet E ∧ 0 < ν E ∧ VectorMeasure.restrict 0 E ≤ VectorMeasure.restrict (μ.toSignedMeasure - (ε • ν).toSignedMeasure) E
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν✝ μ ν : Measure α<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : IsFiniteMeasure ν<VAR>h : ¬μ ⟂ₘ ν<VAR>f : ℕ → Set α<VAR>hf₁ : ∀ (n : ℕ), MeasurableSet (f n)<VAR>hf₂ : ∀ (n : ℕ), VectorMeasure.restrict 0 (f n) ≤ VectorMeasure.restrict (μ.toSignedMeasure - ((1 / (↑n + 1)) • ν).toSignedMeasure) (f n)<VAR>hf₃ : ∀ (n : ℕ), VectorMeasure.restrict (μ.toSignedMeasure - ((1 / (↑n + 1)) • ν).toSignedMeasure) (f n)ᶜ ≤ VectorMeasure.restrict 0 (f n)ᶜ<VAR>A : Set α := ⋂ n, (f n)ᶜ<GOAL>∃ ε, 0 < ε ∧ ∃ E, MeasurableSet E ∧ 0 < ν E ∧ VectorMeasure.restrict 0 E ≤ VectorMeasure.restrict (μ.toSignedMeasure - (ε • ν).toSignedMeasure) E
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν✝ μ ν : Measure α<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : IsFiniteMeasure ν<VAR>h : ¬μ ⟂ₘ ν<VAR>f : ℕ → Set α<VAR>hf₁ : ∀ (n : ℕ), MeasurableSet (f n)<VAR>hf₂ : ∀ (n : ℕ), VectorMeasure.restrict 0 (f n) ≤ VectorMeasure.restrict (μ.toSignedMeasure - ((1 / (↑n + 1)) • ν).toSignedMeasure) (f n)<VAR>hf₃ : ∀ (n : ℕ), VectorMeasure.restrict (μ.toSignedMeasure - ((1 / (↑n + 1)) • ν).toSignedMeasure) (f n)ᶜ ≤ VectorMeasure.restrict 0 (f n)ᶜ<VAR>A : Set α := ⋂ n, (f n)ᶜ<VAR>hAmeas : MeasurableSet A<GOAL>∃ ε, 0 < ε ∧ ∃ E, MeasurableSet E ∧ 0 < ν E ∧ VectorMeasure.restrict 0 E ≤ VectorMeasure.restrict (μ.toSignedMeasure - (ε • ν).toSignedMeasure) E
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν✝ μ ν : Measure α<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : IsFiniteMeasure ν<VAR>h : ¬μ ⟂ₘ ν<VAR>f : ℕ → Set α<VAR>hf₁ : ∀ (n : ℕ), MeasurableSet (f n)<VAR>hf₂ : ∀ (n : ℕ), VectorMeasure.restrict 0 (f n) ≤ VectorMeasure.restrict (μ.toSignedMeasure - ((1 / (↑n + 1)) • ν).toSignedMeasure) (f n)<VAR>hf₃ : ∀ (n : ℕ), VectorMeasure.restrict (μ.toSignedMeasure - ((1 / (↑n + 1)) • ν).toSignedMeasure) (f n)ᶜ ≤ VectorMeasure.restrict 0 (f n)ᶜ<VAR>A : Set α := ⋂ n, (f n)ᶜ<VAR>hAmeas : MeasurableSet A<VAR>hA₂ : ∀ (n : ℕ), VectorMeasure.restrict (μ.toSignedMeasure - ((1 / (↑n + 1)) • ν).toSignedMeasure) A ≤ VectorMeasure.restrict 0 A<GOAL>∃ ε, 0 < ε ∧ ∃ E, MeasurableSet E ∧ 0 < ν E ∧ VectorMeasure.restrict 0 E ≤ VectorMeasure.restrict (μ.toSignedMeasure - (ε • ν).toSignedMeasure) E
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν✝ μ ν : Measure α<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : IsFiniteMeasure ν<VAR>h : ¬μ ⟂ₘ ν<VAR>f : ℕ → Set α<VAR>hf₁ : ∀ (n : ℕ), MeasurableSet (f n)<VAR>hf₂ : ∀ (n : ℕ), VectorMeasure.restrict 0 (f n) ≤ VectorMeasure.restrict (μ.toSignedMeasure - ((1 / (↑n + 1)) • ν).toSignedMeasure) (f n)<VAR>hf₃ : ∀ (n : ℕ), VectorMeasure.restrict (μ.toSignedMeasure - ((1 / (↑n + 1)) • ν).toSignedMeasure) (f n)ᶜ ≤ VectorMeasure.restrict 0 (f n)ᶜ<VAR>A : Set α := ⋂ n, (f n)ᶜ<VAR>hAmeas : MeasurableSet A<VAR>hA₂ : ∀ (n : ℕ), VectorMeasure.restrict (μ.toSignedMeasure - ((1 / (↑n + 1)) • ν).toSignedMeasure) A ≤ VectorMeasure.restrict 0 A<VAR>hA₃ : ∀ (n : ℕ), μ A ≤ ↑(1 / (↑n + 1)) * ν A<GOAL>∃ ε, 0 < ε ∧ ∃ E, MeasurableSet E ∧ 0 < ν E ∧ VectorMeasure.restrict 0 E ≤ VectorMeasure.restrict (μ.toSignedMeasure - (ε • ν).toSignedMeasure) E
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν✝ μ ν : Measure α<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : IsFiniteMeasure ν<VAR>f : ℕ → Set α<VAR>hf₁ : ∀ (n : ℕ), MeasurableSet (f n)<VAR>hf₂ : ∀ (n : ℕ), VectorMeasure.restrict 0 (f n) ≤ VectorMeasure.restrict (μ.toSignedMeasure - ((1 / (↑n + 1)) • ν).toSignedMeasure) (f n)<VAR>hf₃ : ∀ (n : ℕ), VectorMeasure.restrict (μ.toSignedMeasure - ((1 / (↑n + 1)) • ν).toSignedMeasure) (f n)ᶜ ≤ VectorMeasure.restrict 0 (f n)ᶜ<VAR>A : Set α := ⋂ n, (f n)ᶜ<VAR>hAmeas : MeasurableSet A<VAR>hA₂ : ∀ (n : ℕ), VectorMeasure.restrict (μ.toSignedMeasure - ((1 / (↑n + 1)) • ν).toSignedMeasure) A ≤ VectorMeasure.restrict 0 A<VAR>hA₃ : ∀ (n : ℕ), μ A ≤ ↑(1 / (↑n + 1)) * ν A<VAR>hμ : μ A = 0<VAR>h : ∀ (s : Set α), MeasurableSet s → μ s = 0 → ν sᶜ ≠ 0<VAR>this : ν Aᶜ ≠ 0<GOAL>∃ ε, 0 < ε ∧ ∃ E, MeasurableSet E ∧ 0 < ν E ∧ VectorMeasure.restrict 0 E ≤ VectorMeasure.restrict (μ.toSignedMeasure - (ε • ν).toSignedMeasure) E
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν✝ μ ν : Measure α<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : IsFiniteMeasure ν<VAR>f : ℕ → Set α<VAR>hf₁ : ∀ (n : ℕ), MeasurableSet (f n)<VAR>hf₂ : ∀ (n : ℕ), VectorMeasure.restrict 0 (f n) ≤ VectorMeasure.restrict (μ.toSignedMeasure - ((1 / (↑n + 1)) • ν).toSignedMeasure) (f n)<VAR>hf₃ : ∀ (n : ℕ), VectorMeasure.restrict (μ.toSignedMeasure - ((1 / (↑n + 1)) • ν).toSignedMeasure) (f n)ᶜ ≤ VectorMeasure.restrict 0 (f n)ᶜ<VAR>A : Set α := ⋂ n, (f n)ᶜ<VAR>hAmeas : MeasurableSet A<VAR>hA₂ : ∀ (n : ℕ), VectorMeasure.restrict (μ.toSignedMeasure - ((1 / (↑n + 1)) • ν).toSignedMeasure) A ≤ VectorMeasure.restrict 0 A<VAR>hA₃ : ∀ (n : ℕ), μ A ≤ ↑(1 / (↑n + 1)) * ν A<VAR>hμ : μ A = 0<VAR>h : ∀ (s : Set α), MeasurableSet s → μ s = 0 → ν sᶜ ≠ 0<VAR>this : ν (⋃ i, f i) ≠ 0<GOAL>∃ ε, 0 < ε ∧ ∃ E, MeasurableSet E ∧ 0 < ν E ∧ VectorMeasure.restrict 0 E ≤ VectorMeasure.restrict (μ.toSignedMeasure - (ε • ν).toSignedMeasure) E
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν✝ μ ν : Measure α<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : IsFiniteMeasure ν<VAR>f : ℕ → Set α<VAR>hf₁ : ∀ (n : ℕ), MeasurableSet (f n)<VAR>hf₂ : ∀ (n : ℕ), VectorMeasure.restrict 0 (f n) ≤ VectorMeasure.restrict (μ.toSignedMeasure - ((1 / (↑n + 1)) • ν).toSignedMeasure) (f n)<VAR>hf₃ : ∀ (n : ℕ), VectorMeasure.restrict (μ.toSignedMeasure - ((1 / (↑n + 1)) • ν).toSignedMeasure) (f n)ᶜ ≤ VectorMeasure.restrict 0 (f n)ᶜ<VAR>A : Set α := ⋂ n, (f n)ᶜ<VAR>hAmeas : MeasurableSet A<VAR>hA₂ : ∀ (n : ℕ), VectorMeasure.restrict (μ.toSignedMeasure - ((1 / (↑n + 1)) • ν).toSignedMeasure) A ≤ VectorMeasure.restrict 0 A<VAR>hA₃ : ∀ (n : ℕ), μ A ≤ ↑(1 / (↑n + 1)) * ν A<VAR>hμ : μ A = 0<VAR>h : ∀ (s : Set α), MeasurableSet s → μ s = 0 → ν sᶜ ≠ 0<VAR>this : ν (⋃ i, f i) ≠ 0<VAR>n : ℕ<VAR>hn : 0 < ν (f n)<GOAL>∃ ε, 0 < ε ∧ ∃ E, MeasurableSet E ∧ 0 < ν E ∧ VectorMeasure.restrict 0 E ≤ VectorMeasure.restrict (μ.toSignedMeasure - (ε • ν).toSignedMeasure) E
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>X Y : Cᵒᵖ<VAR>f : X ⟶ Y<GOAL>IsIso f.unop ↔ IsIso f
<VAR>F : Type u_1<VAR>inst✝ : Field F<VAR>S✝ S : Set F<VAR>hS : IsSubfield S<VAR>x y : F<VAR>hx : x ∈ S<VAR>hy : y ∈ S<GOAL>x / y ∈ S
<VAR>F : Type u_1<VAR>inst✝ : Field F<VAR>S✝ S : Set F<VAR>hS : IsSubfield S<VAR>x y : F<VAR>hx : x ∈ S<VAR>hy : y ∈ S<GOAL>x * y⁻¹ ∈ S
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : Semiring S<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Algebra R S<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<VAR>hinj : Function.Injective ⇑(algebraMap R S)<VAR>v : ι → M<VAR>li : LinearIndependent S v<GOAL>Function.Injective fun r => r • 1
<VAR>α : Type u_1<VAR>inst✝ : OrderedCommGroup α<VAR>a b : α<GOAL>Pairwise fun x y => Disjoint (Ico (a * b ^ x) (a * b ^ (x + 1))) (Ico (a * b ^ y) (a * b ^ (y + 1)))
<VAR>α : Type u_1<VAR>inst✝ : OrderedCommGroup α<VAR>a b : α<GOAL>Pairwise fun x y => Ico (a * b ^ x) (a * b ^ (x + 1)) ∩ Ico (a * b ^ y) (a * b ^ (y + 1)) ⊆ ∅
<VAR>α : Type u_1<VAR>inst✝ : OrderedCommGroup α<VAR>a b : α<VAR>m n : ℤ<VAR>hmn : m ≠ n<VAR>x : α<VAR>hx : x ∈ Ico (a * b ^ m) (a * b ^ (m + 1)) ∩ Ico (a * b ^ n) (a * b ^ (n + 1))<GOAL>m = n
<VAR>α : Type u_1<VAR>inst✝ : OrderedCommGroup α<VAR>a b : α<VAR>m n : ℤ<VAR>hmn : m ≠ n<VAR>x : α<VAR>hx : x ∈ Ico (a * b ^ m) (a * b ^ (m + 1)) ∩ Ico (a * b ^ n) (a * b ^ (n + 1))<VAR>hb : 1 < b<GOAL>m = n
<VAR>α : Type u_1<VAR>inst✝ : OrderedCommGroup α<VAR>a b : α<VAR>m n : ℤ<VAR>hmn : m ≠ n<VAR>x : α<VAR>hx : x ∈ Ico (a * b ^ m) (a * b ^ (m + 1)) ∩ Ico (a * b ^ n) (a * b ^ (n + 1))<VAR>hb : 1 < b<VAR>i1 : a * b ^ m < a * b ^ (n + 1)<GOAL>m = n
<VAR>α : Type u_1<VAR>inst✝ : OrderedCommGroup α<VAR>a b : α<VAR>m n : ℤ<VAR>hmn : m ≠ n<VAR>x : α<VAR>hx : x ∈ Ico (a * b ^ m) (a * b ^ (m + 1)) ∩ Ico (a * b ^ n) (a * b ^ (n + 1))<VAR>hb : 1 < b<VAR>i1 : a * b ^ m < a * b ^ (n + 1)<VAR>i2 : a * b ^ n < a * b ^ (m + 1)<GOAL>m = n
<VAR>α : Type u_1<VAR>inst✝ : OrderedCommGroup α<VAR>a b : α<VAR>m n : ℤ<VAR>hmn : m ≠ n<VAR>x : α<VAR>hx : x ∈ Ico (a * b ^ m) (a * b ^ (m + 1)) ∩ Ico (a * b ^ n) (a * b ^ (n + 1))<VAR>hb : 1 < b<VAR>i1 : m ≤ n<VAR>i2 : n ≤ m<GOAL>m = n
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasColimits C<VAR>X Y : PresheafedSpace C<VAR>α β : X ⟶ Y<VAR>h : α = β<VAR>x : ↑↑X<GOAL>Hom.stalkMap α x = eqToHom ⋯ ≫ Hom.stalkMap β x
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>S₁ : Type u_3<VAR>R₂ : Type u_4<VAR>S₂ : Type u_5<VAR>M✝ : Type u_6<VAR>M₁ : Type u_7<VAR>M₂ : Type u_8<VAR>M₁' : Type u_9<VAR>M₂' : Type u_10<VAR>N₂ : Type u_11<VAR>n : Type u_12<VAR>m : Type u_13<VAR>n' : Type u_14<VAR>m' : Type u_15<VAR>ι : Type u_16<VAR>inst✝¹⁸ : CommSemiring R<VAR>inst✝¹⁷ : AddCommMonoid M₁<VAR>inst✝¹⁶ : Module R M₁<VAR>inst✝¹⁵ : AddCommMonoid M₂<VAR>inst✝¹⁴ : Module R M₂<VAR>inst✝¹³ : AddCommMonoid N₂<VAR>inst✝¹² : Module R N₂<VAR>inst✝¹¹ : DecidableEq n<VAR>inst✝¹⁰ : Fintype n<VAR>inst✝⁹ : DecidableEq m<VAR>inst✝⁸ : Fintype m<VAR>b₁✝ : Basis n R M₁<VAR>b₂✝ : Basis m R M₂<VAR>b₁ : Basis n R M₁<VAR>b₂ : Basis m R M₂<VAR>inst✝⁷ : AddCommMonoid M₁'<VAR>inst✝⁶ : Module R M₁'<VAR>inst✝⁵ : AddCommMonoid M₂'<VAR>inst✝⁴ : Module R M₂'<VAR>b₁' : Basis n' R M₁'<VAR>b₂' : Basis m' R M₂'<VAR>inst✝³ : Fintype n'<VAR>inst✝² : Fintype m'<VAR>inst✝¹ : DecidableEq n'<VAR>inst✝ : DecidableEq m'<VAR>M : Matrix n m R<VAR>P : Matrix n n' R<VAR>Q : Matrix m m' R<GOAL>(toMatrix₂ b₁' b₂') (((toLinearMap₂ b₁ b₂) M).compl₁₂ ((toLin b₁' b₁) P) ((toLin b₂' b₂) Q)) = (toMatrix₂ b₁' b₂') ((toLinearMap₂ b₁' b₂') (Pᵀ * M * Q))
<VAR>α : Type u<VAR>β : α → Type v<VAR>l l₁✝ l₂✝ : List (Sigma β)<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>l₁ l₂ : List (Sigma β)<VAR>nd₁ : l₁.NodupKeys<VAR>nd₂ : l₂.NodupKeys<VAR>p : l₁ ~ l₂<VAR>b : β a<GOAL>b ∈ dlookup a l₁ ↔ b ∈ dlookup a l₂
<VAR>α : Type u<VAR>β : α → Type v<VAR>l l₁✝ l₂✝ : List (Sigma β)<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>l₁ l₂ : List (Sigma β)<VAR>nd₁ : l₁.NodupKeys<VAR>nd₂ : l₂.NodupKeys<VAR>p : l₁ ~ l₂<VAR>b : β a<GOAL>⟨a, b⟩ ∈ l₁ ↔ ⟨a, b⟩ ∈ l₂
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s : Set α<VAR>ν : Measure α<VAR>hμν : μ ≪ ν<VAR>hm : m ≤ m0<GOAL>μ.trim hm ≪ ν.trim hm
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s✝ : Set α<VAR>ν : Measure α<VAR>hμν : μ ≪ ν<VAR>hm : m ≤ m0<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hsν : (ν.trim hm) s = 0<GOAL>(μ.trim hm) s = 0
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s✝ : Set α<VAR>ν : Measure α<VAR>hμν : μ ≪ ν<VAR>hm : m ≤ m0<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hsν : ν s = 0<GOAL>μ s = 0
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f✝ f₀ f₁ g : E → F<VAR>f'✝ f₀' f₁' g' e : E →L[𝕜] F<VAR>x✝ : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>iso : E ≃L[𝕜] F<VAR>f : F → G<VAR>x : E<VAR>f' : F →L[𝕜] G<GOAL>HasFDerivAt (f ∘ ⇑iso) (f'.comp ↑iso) x ↔ HasFDerivAt f f' (iso x)
<VAR>α : Type u_1<VAR>inst✝ : EMetricSpace α<VAR>cs : CompleteSpace α<VAR>K : ℝ≥0<VAR>f : α → α<VAR>hf : ContractingWith K f<GOAL>0 < 1 - ↑K
<VAR>A : Type u₁<VAR>inst✝⁷ : Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>inst✝⁶ : Category.{v₂, u₂} B<VAR>T : Type u₃<VAR>inst✝⁵ : Category.{v₃, u₃} T<VAR>A' : Type u_1<VAR>B' : Type u_2<VAR>T' : Type u_3<VAR>inst✝⁴ : Category.{?u.158446, u_1} A'<VAR>inst✝³ : Category.{?u.158450, u_2} B'<VAR>inst✝² : Category.{?u.158454, u_3} T'<VAR>L✝ : A ⥤ T<VAR>R✝ : B ⥤ T<VAR>C : Type u₄<VAR>inst✝¹ : Category.{v₄, u₄} C<VAR>D : Type u₅<VAR>inst✝ : Category.{v₅, u₅} D<VAR>L : A ⥤ T<VAR>R : B ⥤ T<VAR>F : T ⥤ C<VAR>X✝ Y✝ : Comma L R<VAR>f : X✝ ⟶ Y✝<GOAL>(L ⋙ F).map f.left ≫ ((fun X => { left := X.left, right := X.right, hom := F.map X.hom }) Y✝).hom = ((fun X => { left := X.left, right := X.right, hom := F.map X.hom }) X✝).hom ≫ (R ⋙ F).map f.right
<VAR>V : Type u_1<VAR>V₁ : Type u_2<VAR>V₂ : Type u_3<VAR>V₃ : Type u_4<VAR>inst✝³ : SeminormedAddCommGroup V<VAR>inst✝² : SeminormedAddCommGroup V₁<VAR>inst✝¹ : SeminormedAddCommGroup V₂<VAR>inst✝ : SeminormedAddCommGroup V₃<VAR>f g : NormedAddGroupHom V₁ V₂<GOAL>∀ (v : V), ‖(AddMonoidHom.id V) v‖ ≤ 1 * ‖v‖
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁷ : CommMonoid α✝<VAR>inst✝⁶ : TopologicalSpace α✝<VAR>f✝ g : β✝ → α✝<VAR>a✝ b✝ : α✝<VAR>s : Finset β✝<VAR>inst✝⁵ : ContinuousMul α✝<VAR>α : Type u_5<VAR>β : Type u_6<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : CommMonoid α<VAR>inst✝² : T2Space α<VAR>inst✝¹ : ContinuousMul α<VAR>inst✝ : DecidableEq β<VAR>f : β → α<VAR>a : α<VAR>hf : HasProd f a<VAR>b : β<VAR>a' : α<VAR>hf' : HasProd (fun n => if n = b then 1 else f n) a'<GOAL>a = a' * f b
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁷ : CommMonoid α✝<VAR>inst✝⁶ : TopologicalSpace α✝<VAR>f✝ g : β✝ → α✝<VAR>a✝ b✝ : α✝<VAR>s : Finset β✝<VAR>inst✝⁵ : ContinuousMul α✝<VAR>α : Type u_5<VAR>β : Type u_6<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : CommMonoid α<VAR>inst✝² : T2Space α<VAR>inst✝¹ : ContinuousMul α<VAR>inst✝ : DecidableEq β<VAR>f : β → α<VAR>a : α<VAR>hf : HasProd f a<VAR>b : β<VAR>a' : α<VAR>hf' : HasProd (fun n => if n = b then 1 else f n) a'<GOAL>HasProd (update f b 1) a'
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁷ : CommMonoid α✝<VAR>inst✝⁶ : TopologicalSpace α✝<VAR>f✝ g : β✝ → α✝<VAR>a✝ b✝ : α✝<VAR>s : Finset β✝<VAR>inst✝⁵ : ContinuousMul α✝<VAR>α : Type u_5<VAR>β : Type u_6<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : CommMonoid α<VAR>inst✝² : T2Space α<VAR>inst✝¹ : ContinuousMul α<VAR>inst✝ : DecidableEq β<VAR>f : β → α<VAR>a : α<VAR>hf : HasProd f a<VAR>b : β<VAR>a' : α<VAR>hf' : HasProd (fun n => if n = b then 1 else f n) a'<VAR>x✝ : β<GOAL>update f b 1 x✝ = if x✝ = b then 1 else f x✝
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝¹ : RCLike K<VAR>z✝ : K<VAR>n : ℕ<VAR>inst✝ : n.AtLeastTwo<VAR>z : K<GOAL>im (OfNat.ofNat n * z) = OfNat.ofNat n * im z
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>inst✝¹ : AddZeroClass δ<VAR>inst✝ : Min δ<VAR>C : Cost α β δ<VAR>xs : List α<VAR>ys : List β<GOAL>(suffixLevenshtein C xs ys).val = List.map (fun xs' => levenshtein C xs' ys) xs.tails
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝¹ : TopologicalSpace α<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝ : (i : ι) → TopologicalSpace (π i)<VAR>I : Set ι<VAR>s : (i : ι) → Set (π i)<VAR>x : (i : ι) → π i<GOAL>𝓝[I.pi s] x = ⊥ ↔ ∃ i ∈ I, 𝓝[s i] x i = ⊥
<VAR>K : Set ℍ<VAR>hK : IsCompact K<GOAL>∃ A B, 0 < B ∧ K ⊆ verticalStrip A B
<VAR>hK : IsCompact ∅<GOAL>∃ A B, 0 < B ∧ ∅ ⊆ verticalStrip A B
<VAR>K : Set ℍ<VAR>hK : IsCompact K<VAR>hne : K.Nonempty<GOAL>∃ A B, 0 < B ∧ K ⊆ verticalStrip A B
<VAR>K : Set ℍ<VAR>hK : IsCompact K<VAR>hne : K.Nonempty<VAR>u : ℍ<VAR>left✝ : u ∈ K<VAR>hu : IsMaxOn (_root_.abs ∘ re) K u<GOAL>∃ A B, 0 < B ∧ K ⊆ verticalStrip A B
<VAR>K : Set ℍ<VAR>hK : IsCompact K<VAR>hne : K.Nonempty<VAR>u : ℍ<VAR>left✝¹ : u ∈ K<VAR>hu : IsMaxOn (_root_.abs ∘ re) K u<VAR>v : ℍ<VAR>left✝ : v ∈ K<VAR>hv : IsMinOn im K v<GOAL>∃ A B, 0 < B ∧ K ⊆ verticalStrip A B
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>x y z : Part α<VAR>hx : x ≤ z<VAR>hy : y ≤ z<GOAL>x ≤ y ∨ y ≤ x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>x y z : Part α<VAR>hx : x ≤ z<VAR>hy : y ≤ z<VAR>h : x = none<GOAL>x ≤ y ∨ y ≤ x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>x y z : Part α<VAR>hx : x ≤ z<VAR>hy : y ≤ z<VAR>b : α<VAR>h₀ : x = some b<GOAL>x ≤ y ∨ y ≤ x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>x y z : Part α<VAR>hx : x ≤ z<VAR>hy : y ≤ z<VAR>b : α<VAR>h₀ : x = some b<VAR>b' : α<VAR>h₁ : b' ∈ y<GOAL>b' ∈ x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>x y z : Part α<VAR>hx : x ≤ z<VAR>hy : y ≤ z<VAR>b : α<VAR>h₀ : b ∈ x<VAR>b' : α<VAR>h₁ : b' ∈ y<GOAL>b' ∈ x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>x y z : Part α<VAR>hx✝ : x ≤ z<VAR>hy✝ : y ≤ z<VAR>b : α<VAR>h₀ : b ∈ x<VAR>b' : α<VAR>h₁ : b' ∈ y<VAR>hx : b ∈ z<VAR>hy : b' ∈ z<GOAL>b' ∈ x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>x y z : Part α<VAR>hx✝¹ : x ≤ z<VAR>hy✝ : y ≤ z<VAR>b : α<VAR>h₀ : b ∈ x<VAR>b' : α<VAR>h₁ : b' ∈ y<VAR>hx✝ : b ∈ z<VAR>hy : b' ∈ z<VAR>hx : b = b'<GOAL>b' ∈ x
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>σ τ : Perm α<GOAL>IsConj σ τ ↔ σ.partition = τ.partition
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>σ τ : Perm α<GOAL>σ.cycleType = τ.cycleType ↔ σ.partition = τ.partition
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>ℰ : Type u₂<VAR>inst✝³ : Category.{v₁, u₂} ℰ<VAR>A✝ A : C ⥤ ℰ<VAR>inst✝² : yoneda.HasPointwiseLeftKanExtension A<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₁, u₂} D<VAR>F : C ⥤ D<VAR>inst✝ : ∀ (P : Cᵒᵖ ⥤ Type v₁), F.op.HasLeftKanExtension P<VAR>X✝ : C<VAR>G : (Cᵒᵖ ⥤ Type v₁) ⥤ Dᵒᵖ ⥤ Type v₁<VAR>φ : F ⋙ yoneda ⟶ yoneda ⋙ G<VAR>X : C<GOAL>(F.op.lan.obj (yoneda.obj X)).descOfIsLeftKanExtension (F.op.lanUnit.app (yoneda.obj X)) (G.obj (yoneda.obj X)) (presheafHom φ (yoneda.obj X)) = (compYonedaIsoYonedaCompLan F).inv.app X ≫ φ.app X
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>ℰ : Type u₂<VAR>inst✝³ : Category.{v₁, u₂} ℰ<VAR>A✝ A : C ⥤ ℰ<VAR>inst✝² : yoneda.HasPointwiseLeftKanExtension A<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₁, u₂} D<VAR>F : C ⥤ D<VAR>inst✝ : ∀ (P : Cᵒᵖ ⥤ Type v₁), F.op.HasLeftKanExtension P<VAR>X✝ : C<VAR>G : (Cᵒᵖ ⥤ Type v₁) ⥤ Dᵒᵖ ⥤ Type v₁<VAR>φ : F ⋙ yoneda ⟶ yoneda ⋙ G<VAR>X : C<GOAL>F.op.lanUnit.app (yoneda.obj X) ≫ whiskerLeft F.op ((F.op.lan.obj (yoneda.obj X)).descOfIsLeftKanExtension (F.op.lanUnit.app (yoneda.obj X)) (G.obj (yoneda.obj X)) (presheafHom φ (yoneda.obj X))) = F.op.lanUnit.app (yoneda.obj X) ≫ whiskerLeft F.op ((compYonedaIsoYonedaCompLan F).inv.app X ≫ φ.app X)
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>ℰ : Type u₂<VAR>inst✝³ : Category.{v₁, u₂} ℰ<VAR>A✝ A : C ⥤ ℰ<VAR>inst✝² : yoneda.HasPointwiseLeftKanExtension A<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₁, u₂} D<VAR>F : C ⥤ D<VAR>inst✝ : ∀ (P : Cᵒᵖ ⥤ Type v₁), F.op.HasLeftKanExtension P<VAR>X✝ : C<VAR>G : (Cᵒᵖ ⥤ Type v₁) ⥤ Dᵒᵖ ⥤ Type v₁<VAR>φ : F ⋙ yoneda ⟶ yoneda ⋙ G<VAR>X : C<GOAL>presheafHom φ (yoneda.obj X) = F.op.lanUnit.app (yoneda.obj X) ≫ whiskerLeft F.op ((compYonedaIsoYonedaCompLan F).inv.app X ≫ φ.app X)
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>ℰ : Type u₂<VAR>inst✝³ : Category.{v₁, u₂} ℰ<VAR>A✝ A : C ⥤ ℰ<VAR>inst✝² : yoneda.HasPointwiseLeftKanExtension A<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₁, u₂} D<VAR>F : C ⥤ D<VAR>inst✝ : ∀ (P : Cᵒᵖ ⥤ Type v₁), F.op.HasLeftKanExtension P<VAR>X✝ : C<VAR>G : (Cᵒᵖ ⥤ Type v₁) ⥤ Dᵒᵖ ⥤ Type v₁<VAR>φ : F ⋙ yoneda ⟶ yoneda ⋙ G<VAR>X : C<GOAL>yonedaEquiv (presheafHom φ (yoneda.obj X)) = yonedaEquiv (F.op.lanUnit.app (yoneda.obj X) ≫ whiskerLeft F.op ((compYonedaIsoYonedaCompLan F).inv.app X ≫ φ.app X))
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>ℰ : Type u₂<VAR>inst✝³ : Category.{v₁, u₂} ℰ<VAR>A✝ A : C ⥤ ℰ<VAR>inst✝² : yoneda.HasPointwiseLeftKanExtension A<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₁, u₂} D<VAR>F : C ⥤ D<VAR>inst✝ : ∀ (P : Cᵒᵖ ⥤ Type v₁), F.op.HasLeftKanExtension P<VAR>X✝ : C<VAR>G : (Cᵒᵖ ⥤ Type v₁) ⥤ Dᵒᵖ ⥤ Type v₁<VAR>φ : F ⋙ yoneda ⟶ yoneda ⋙ G<VAR>X : C<GOAL>(φ.app X).app (F.op.obj (Opposite.op X)) (𝟙 (Opposite.unop (F.op.obj (Opposite.op X)))) = yonedaEquiv (F.op.lanUnit.app (yoneda.obj X) ≫ whiskerLeft F.op ((compYonedaIsoYonedaCompLan F).inv.app X ≫ φ.app X))
<VAR>J : Type u₁<VAR>K : Type u₂<VAR>inst✝¹¹ : SmallCategory J<VAR>inst✝¹⁰ : Category.{v₂, u₂} K<VAR>inst✝⁹ : Small.{v, u₂} K<VAR>inst✝⁸ : FinCategory J<VAR>F✝ : J × K ⥤ Type v<VAR>inst✝⁷ : IsFiltered K<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>inst✝⁵ : ConcreteCategory C<VAR>inst✝⁴ : HasLimitsOfShape J C<VAR>inst✝³ : HasColimitsOfShape K C<VAR>inst✝² : ReflectsLimitsOfShape J (forget C)<VAR>inst✝¹ : PreservesColimitsOfShape K (forget C)<VAR>inst✝ : PreservesLimitsOfShape J (forget C)<VAR>F : J ⥤ K ⥤ C<VAR>a : K<VAR>b : J<GOAL>colimit.ι (limit F) a ≫ (((isLimitOfPreserves colim (limit.isLimit F)).conePointUniqueUpToIso (limit.isLimit (F ⋙ colim))).hom ≫ (HasLimit.isoOfNatIso (colimitFlipIsoCompColim F).symm).hom) ≫ limit.π (colimit F.flip) b = (limit.π F b).app a ≫ (colimit.ι F.flip a).app b
<VAR>J : Type u₁<VAR>K : Type u₂<VAR>inst✝¹¹ : SmallCategory J<VAR>inst✝¹⁰ : Category.{v₂, u₂} K<VAR>inst✝⁹ : Small.{v, u₂} K<VAR>inst✝⁸ : FinCategory J<VAR>F✝ : J × K ⥤ Type v<VAR>inst✝⁷ : IsFiltered K<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>inst✝⁵ : ConcreteCategory C<VAR>inst✝⁴ : HasLimitsOfShape J C<VAR>inst✝³ : HasColimitsOfShape K C<VAR>inst✝² : ReflectsLimitsOfShape J (forget C)<VAR>inst✝¹ : PreservesColimitsOfShape K (forget C)<VAR>inst✝ : PreservesLimitsOfShape J (forget C)<VAR>F : J ⥤ K ⥤ C<VAR>a : K<VAR>b : J<GOAL>(limit.π F b).app a ≫ colimit.ι (F.obj b) a ≫ (HasColimit.isoOfNatIso (flipCompEvaluation F b)).inv ≫ (colimitObjIsoColimitCompEvaluation F.flip b).inv = (limit.π F b).app a ≫ (colimit.ι F.flip a).app b