ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>Γ : Type u_1<VAR>inst✝² : Inhabited Γ<VAR>Λ : Type u_2<VAR>inst✝¹ : Inhabited Λ<VAR>σ : Type u_3<VAR>inst✝ : Inhabited σ<VAR>n : ℕ<VAR>enc : Γ → Vector Bool n<VAR>dec : Vector Bool n → Γ<VAR>enc0 : enc default = Vector.replicate n false<VAR>M : Λ → Stmt₁<VAR>encdec : ∀ (a : Γ), dec (enc a) = a<VAR>f : Γ → Stmt Bool Λ' σ<VAR>v : σ<VAR>L : ListBlank Γ<VAR>a : Γ<VAR>R : ListBlank Γ<GOAL>∀ (f : Vector Bool n → Stmt Bool Λ' σ), stepAux (readAux n f) v (Tape.mk' (L.bind (fun x => (enc x).toList.reverse) ⋯) (ListBlank.append (enc a).toList (R.bind (fun x => (enc x).toList) ⋯))) = stepAux (f (enc a)) v (Tape.mk' (ListBlank.append (enc a).toList.reverse (L.bind (fun x => (enc x).toList.reverse) ⋯)) (R.bind (fun x => (enc x).toList) ⋯))
<VAR>Γ : Type u_1<VAR>inst✝² : Inhabited Γ<VAR>Λ : Type u_2<VAR>inst✝¹ : Inhabited Λ<VAR>σ : Type u_3<VAR>inst✝ : Inhabited σ<VAR>n : ℕ<VAR>enc : Γ → Vector Bool n<VAR>dec : Vector Bool n → Γ<VAR>enc0 : enc default = Vector.replicate n false<VAR>M : Λ → Stmt₁<VAR>encdec : ∀ (a : Γ), dec (enc a) = a<VAR>f : Γ → Stmt Bool Λ' σ<VAR>v : σ<VAR>L : ListBlank Γ<VAR>a : Γ<VAR>R : ListBlank Γ<GOAL>∀ (i : ℕ) (f : Vector Bool i → Stmt Bool Λ' σ) (L' R' : ListBlank Bool) (l₁ l₂ : List Bool) (h : l₂.length = i), stepAux (readAux i f) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂ R')) = stepAux (f ⟨l₂, h⟩) v (Tape.mk' (ListBlank.append (l₂.reverseAux l₁) L') R')
<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>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>inst✝ : DecidableEq ι<VAR>i j : ι<VAR>h : i ≠ j<VAR>c : k<GOAL>affineCombinationLineMapWeights i j c i = 1 - c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LinearOrder β<VAR>f : α → β<VAR>s : Set α<VAR>a a₁ a₂ b b₁ b₂ c d x : α<GOAL>a ∈ [[b, c]] ↔ b ≤ a ∧ a ≤ c ∨ c ≤ a ∧ a ≤ b
<VAR>J : Type v<VAR>inst✝ : SmallCategory J<VAR>F : J ⥤ MonCat<VAR>j j' : J<VAR>f : j ⟶ j'<VAR>x : ↑(F.obj j)<GOAL>(coconeMorphism F j') ((F.map f) x) = (coconeMorphism F j) x
<VAR>J : Type v<VAR>inst✝ : SmallCategory J<VAR>F : J ⥤ MonCat<VAR>j j' : J<VAR>f : j ⟶ j'<VAR>x : ↑(F.obj j)<GOAL>(coconeMorphism F j') ((F.map f) x) = (F.map f ≫ coconeMorphism F j') x
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>inst✝¹ : (i : ι) → Monoid (M i)<VAR>N : Type u_3<VAR>inst✝ : Monoid N<VAR>C : CoprodI M → Prop<VAR>m : CoprodI M<VAR>one : C 1<VAR>mul : ∀ {i : ι} (m : M i) (x : CoprodI M), C x → C (of m * x)<GOAL>C m
<VAR>R : Type uR<VAR>inst✝⁴ : Semiring R<VAR>S : Type uS<VAR>inst✝³ : CommSemiring S<VAR>T : Type uT<VAR>A : Type uA<VAR>inst✝² : Semiring A<VAR>inst✝¹ : Algebra S A<VAR>r✝¹ : R → R → Prop<VAR>inst✝ : Semiring T<VAR>r✝ : R → R → Prop<VAR>f : R →+* T<VAR>h : ∀ ⦃x y : R⦄, r✝ x y → f x = f y<VAR>x : RingQuot r✝<VAR>a✝ b✝ : R<VAR>r : Rel r✝ a✝ b✝<GOAL>f a✝ = f b✝
<VAR>R : Type uR<VAR>inst✝⁴ : Semiring R<VAR>S : Type uS<VAR>inst✝³ : CommSemiring S<VAR>T : Type uT<VAR>A : Type uA<VAR>inst✝² : Semiring A<VAR>inst✝¹ : Algebra S A<VAR>r✝ : R → R → Prop<VAR>inst✝ : Semiring T<VAR>r : R → R → Prop<VAR>f : R →+* T<VAR>h : ∀ ⦃x y : R⦄, r x y → f x = f y<GOAL>(↑{ toFun := fun x => Quot.lift ⇑f ⋯ x.toQuot, map_one' := ⋯, map_mul' := ⋯ }).toFun 0 = 0
<VAR>R : Type uR<VAR>inst✝⁴ : Semiring R<VAR>S : Type uS<VAR>inst✝³ : CommSemiring S<VAR>T : Type uT<VAR>A : Type uA<VAR>inst✝² : Semiring A<VAR>inst✝¹ : Algebra S A<VAR>r✝ : R → R → Prop<VAR>inst✝ : Semiring T<VAR>r : R → R → Prop<VAR>f : R →+* T<VAR>h : ∀ ⦃x y : R⦄, r x y → f x = f y<VAR>toQuot✝¹ : Quot (Rel r)<VAR>x : R<VAR>toQuot✝ : Quot (Rel r)<VAR>y : R<GOAL>(↑{ toFun := fun x => Quot.lift ⇑f ⋯ x.toQuot, map_one' := ⋯, map_mul' := ⋯ }).toFun ({ toQuot := Quot.mk (Rel r) x } + { toQuot := Quot.mk (Rel r) y }) = (↑{ toFun := fun x => Quot.lift ⇑f ⋯ x.toQuot, map_one' := ⋯, map_mul' := ⋯ }).toFun { toQuot := Quot.mk (Rel r) x } + (↑{ toFun := fun x => Quot.lift ⇑f ⋯ x.toQuot, map_one' := ⋯, map_mul' := ⋯ }).toFun { toQuot := Quot.mk (Rel r) y }
<VAR>R : Type uR<VAR>inst✝⁴ : Semiring R<VAR>S : Type uS<VAR>inst✝³ : CommSemiring S<VAR>T : Type uT<VAR>A : Type uA<VAR>inst✝² : Semiring A<VAR>inst✝¹ : Algebra S A<VAR>r✝ : R → R → Prop<VAR>inst✝ : Semiring T<VAR>r : R → R → Prop<VAR>f : R →+* T<VAR>h : ∀ ⦃x y : R⦄, r x y → f x = f y<GOAL>(fun x => Quot.lift ⇑f ⋯ x.toQuot) 1 = 1
<VAR>R : Type uR<VAR>inst✝⁴ : Semiring R<VAR>S : Type uS<VAR>inst✝³ : CommSemiring S<VAR>T : Type uT<VAR>A : Type uA<VAR>inst✝² : Semiring A<VAR>inst✝¹ : Algebra S A<VAR>r✝ : R → R → Prop<VAR>inst✝ : Semiring T<VAR>r : R → R → Prop<VAR>f : R →+* T<VAR>h : ∀ ⦃x y : R⦄, r x y → f x = f y<VAR>toQuot✝¹ : Quot (Rel r)<VAR>x : R<VAR>toQuot✝ : Quot (Rel r)<VAR>y : R<GOAL>{ toFun := fun x => Quot.lift ⇑f ⋯ x.toQuot, map_one' := ⋯ }.toFun ({ toQuot := Quot.mk (Rel r) x } * { toQuot := Quot.mk (Rel r) y }) = { toFun := fun x => Quot.lift ⇑f ⋯ x.toQuot, map_one' := ⋯ }.toFun { toQuot := Quot.mk (Rel r) x } * { toFun := fun x => Quot.lift ⇑f ⋯ x.toQuot, map_one' := ⋯ }.toFun { toQuot := Quot.mk (Rel r) y }
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>hm : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : BorelSpace α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>g : α → E<VAR>l : Filter ι<VAR>x₀ : α<VAR>s t✝ : Set α<VAR>φ : ι → α → ℝ<VAR>a : E<VAR>inst✝ : CompleteSpace E<VAR>hs : MeasurableSet s<VAR>t : Set α<VAR>ht : MeasurableSet t<VAR>hts : t ⊆ s<VAR>h'ts : t ∈ 𝓝[s] x₀<VAR>h't : μ t ≠ ⊤<VAR>hnφ : ∀ᶠ (i : ι) in l, ∀ x ∈ s, 0 ≤ φ i x<VAR>hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)<VAR>hiφ : Tendsto (fun i => ∫ (x : α) in t, φ i x ∂μ) l (𝓝 1)<VAR>h'iφ : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (φ i) (μ.restrict s)<VAR>hmg : IntegrableOn g s μ<VAR>hcg : Tendsto g (𝓝[s] x₀) (𝓝 a)<VAR>h : α → E := g - t.indicator fun x => a<VAR>A : Tendsto (fun i => ∫ (x : α) in s, φ i x • h x ∂μ + (∫ (x : α) in t, φ i x ∂μ) • a) l (𝓝 (0 + 1 • a))<GOAL>Tendsto (fun i => ∫ (x : α) in s, φ i x • g x ∂μ) l (𝓝 a)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>hm : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : BorelSpace α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>g : α → E<VAR>l : Filter ι<VAR>x₀ : α<VAR>s t✝ : Set α<VAR>φ : ι → α → ℝ<VAR>a : E<VAR>inst✝ : CompleteSpace E<VAR>hs : MeasurableSet s<VAR>t : Set α<VAR>ht : MeasurableSet t<VAR>hts : t ⊆ s<VAR>h'ts : t ∈ 𝓝[s] x₀<VAR>h't : μ t ≠ ⊤<VAR>hnφ : ∀ᶠ (i : ι) in l, ∀ x ∈ s, 0 ≤ φ i x<VAR>hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)<VAR>hiφ : Tendsto (fun i => ∫ (x : α) in t, φ i x ∂μ) l (𝓝 1)<VAR>h'iφ : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (φ i) (μ.restrict s)<VAR>hmg : IntegrableOn g s μ<VAR>hcg : Tendsto g (𝓝[s] x₀) (𝓝 a)<VAR>h : α → E := g - t.indicator fun x => a<VAR>A : Tendsto (fun i => ∫ (x : α) in s, φ i x • h x ∂μ + (∫ (x : α) in t, φ i x ∂μ) • a) l (𝓝 a)<GOAL>Tendsto (fun i => ∫ (x : α) in s, φ i x • g x ∂μ) l (𝓝 a)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>hm : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : BorelSpace α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>g : α → E<VAR>l : Filter ι<VAR>x₀ : α<VAR>s t✝ : Set α<VAR>φ : ι → α → ℝ<VAR>a : E<VAR>inst✝ : CompleteSpace E<VAR>hs : MeasurableSet s<VAR>t : Set α<VAR>ht : MeasurableSet t<VAR>hts : t ⊆ s<VAR>h'ts : t ∈ 𝓝[s] x₀<VAR>h't : μ t ≠ ⊤<VAR>hnφ : ∀ᶠ (i : ι) in l, ∀ x ∈ s, 0 ≤ φ i x<VAR>hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)<VAR>hiφ : Tendsto (fun i => ∫ (x : α) in t, φ i x ∂μ) l (𝓝 1)<VAR>h'iφ : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (φ i) (μ.restrict s)<VAR>hmg : IntegrableOn g s μ<VAR>hcg : Tendsto g (𝓝[s] x₀) (𝓝 a)<VAR>h : α → E := g - t.indicator fun x => a<VAR>A : Tendsto (fun i => ∫ (x : α) in s, φ i x • h x ∂μ + (∫ (x : α) in t, φ i x ∂μ) • a) l (𝓝 a)<GOAL>(fun i => ∫ (x : α) in s, φ i x • h x ∂μ + (∫ (x : α) in t, φ i x ∂μ) • a) =ᶠ[l] fun i => ∫ (x : α) in s, φ i x • g x ∂μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>hm : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : BorelSpace α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>g : α → E<VAR>l : Filter ι<VAR>x₀ : α<VAR>s t✝ : Set α<VAR>φ : ι → α → ℝ<VAR>a : E<VAR>inst✝ : CompleteSpace E<VAR>hs : MeasurableSet s<VAR>t : Set α<VAR>ht : MeasurableSet t<VAR>hts : t ⊆ s<VAR>h'ts : t ∈ 𝓝[s] x₀<VAR>h't : μ t ≠ ⊤<VAR>hnφ : ∀ᶠ (i : ι) in l, ∀ x ∈ s, 0 ≤ φ i x<VAR>hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)<VAR>hiφ : Tendsto (fun i => ∫ (x : α) in t, φ i x ∂μ) l (𝓝 1)<VAR>h'iφ : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (φ i) (μ.restrict s)<VAR>hmg : IntegrableOn g s μ<VAR>hcg : Tendsto g (𝓝[s] x₀) (𝓝 a)<VAR>h : α → E := g - t.indicator fun x => a<VAR>A : Tendsto (fun i => ∫ (x : α) in s, φ i x • h x ∂μ + (∫ (x : α) in t, φ i x ∂μ) • a) l (𝓝 a)<VAR>i : ι<VAR>hi : IntegrableOn (fun x => φ i x • g x) s μ<VAR>h'i : ‖∫ (x : α) in t, φ i x ∂μ - 1‖ < 1<GOAL>∫ (x : α) in s, φ i x • h x ∂μ + (∫ (x : α) in t, φ i x ∂μ) • a = ∫ (x : α) in s, φ i x • g x ∂μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>hm : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : BorelSpace α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>g : α → E<VAR>l : Filter ι<VAR>x₀ : α<VAR>s t✝ : Set α<VAR>φ : ι → α → ℝ<VAR>a : E<VAR>inst✝ : CompleteSpace E<VAR>hs : MeasurableSet s<VAR>t : Set α<VAR>ht : MeasurableSet t<VAR>hts : t ⊆ s<VAR>h'ts : t ∈ 𝓝[s] x₀<VAR>h't : μ t ≠ ⊤<VAR>hnφ : ∀ᶠ (i : ι) in l, ∀ x ∈ s, 0 ≤ φ i x<VAR>hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)<VAR>hiφ : Tendsto (fun i => ∫ (x : α) in t, φ i x ∂μ) l (𝓝 1)<VAR>h'iφ : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (φ i) (μ.restrict s)<VAR>hmg : IntegrableOn g s μ<VAR>hcg : Tendsto g (𝓝[s] x₀) (𝓝 a)<VAR>h : α → E := g - t.indicator fun x => a<VAR>A : Tendsto (fun i => ∫ (x : α) in s, φ i x • h x ∂μ + (∫ (x : α) in t, φ i x ∂μ) • a) l (𝓝 a)<VAR>i : ι<VAR>hi : IntegrableOn (fun x => φ i x • g x) s μ<VAR>h'i : ‖∫ (x : α) in t, φ i x ∂μ - 1‖ < 1<GOAL>∫ (x : α) in s, φ i x • g x - t.indicator (fun a_1 => φ i a_1 • a) x ∂μ + (∫ (x : α) in t, φ i x ∂μ) • a = ∫ (x : α) in s, φ i x • g x ∂μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>hm : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : BorelSpace α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>g : α → E<VAR>l : Filter ι<VAR>x₀ : α<VAR>s t✝ : Set α<VAR>φ : ι → α → ℝ<VAR>a : E<VAR>inst✝ : CompleteSpace E<VAR>hs : MeasurableSet s<VAR>t : Set α<VAR>ht : MeasurableSet t<VAR>hts : t ⊆ s<VAR>h'ts : t ∈ 𝓝[s] x₀<VAR>h't : μ t ≠ ⊤<VAR>hnφ : ∀ᶠ (i : ι) in l, ∀ x ∈ s, 0 ≤ φ i x<VAR>hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)<VAR>hiφ : Tendsto (fun i => ∫ (x : α) in t, φ i x ∂μ) l (𝓝 1)<VAR>h'iφ : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (φ i) (μ.restrict s)<VAR>hmg : IntegrableOn g s μ<VAR>hcg : Tendsto g (𝓝[s] x₀) (𝓝 a)<VAR>h : α → E := g - t.indicator fun x => a<VAR>A : Tendsto (fun i => ∫ (x : α) in s, φ i x • h x ∂μ + (∫ (x : α) in t, φ i x ∂μ) • a) l (𝓝 a)<VAR>i : ι<VAR>hi : IntegrableOn (fun x => φ i x • g x) s μ<VAR>h'i : ‖∫ (x : α) in t, φ i x ∂μ - 1‖ < 1<GOAL>Integrable (t.indicator fun a_1 => φ i a_1 • a) (μ.restrict s)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>hm : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : BorelSpace α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>g : α → E<VAR>l : Filter ι<VAR>x₀ : α<VAR>s t✝ : Set α<VAR>φ : ι → α → ℝ<VAR>a : E<VAR>inst✝ : CompleteSpace E<VAR>hs : MeasurableSet s<VAR>t : Set α<VAR>ht : MeasurableSet t<VAR>hts : t ⊆ s<VAR>h'ts : t ∈ 𝓝[s] x₀<VAR>h't : μ t ≠ ⊤<VAR>hnφ : ∀ᶠ (i : ι) in l, ∀ x ∈ s, 0 ≤ φ i x<VAR>hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)<VAR>hiφ : Tendsto (fun i => ∫ (x : α) in t, φ i x ∂μ) l (𝓝 1)<VAR>h'iφ : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (φ i) (μ.restrict s)<VAR>hmg : IntegrableOn g s μ<VAR>hcg : Tendsto g (𝓝[s] x₀) (𝓝 a)<VAR>h : α → E := g - t.indicator fun x => a<VAR>A : Tendsto (fun i => ∫ (x : α) in s, φ i x • h x ∂μ + (∫ (x : α) in t, φ i x ∂μ) • a) l (𝓝 a)<VAR>i : ι<VAR>hi : IntegrableOn (fun x => φ i x • g x) s μ<VAR>h'i : ‖∫ (x : α) in t, φ i x ∂μ - 1‖ < 1<GOAL>IntegrableOn (fun a_1 => φ i a_1 • a) t (μ.restrict s)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>hm : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : BorelSpace α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>g : α → E<VAR>l : Filter ι<VAR>x₀ : α<VAR>s t✝ : Set α<VAR>φ : ι → α → ℝ<VAR>a : E<VAR>inst✝ : CompleteSpace E<VAR>hs : MeasurableSet s<VAR>t : Set α<VAR>ht : MeasurableSet t<VAR>hts : t ⊆ s<VAR>h'ts : t ∈ 𝓝[s] x₀<VAR>h't : μ t ≠ ⊤<VAR>hnφ : ∀ᶠ (i : ι) in l, ∀ x ∈ s, 0 ≤ φ i x<VAR>hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)<VAR>hiφ : Tendsto (fun i => ∫ (x : α) in t, φ i x ∂μ) l (𝓝 1)<VAR>h'iφ : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (φ i) (μ.restrict s)<VAR>hmg : IntegrableOn g s μ<VAR>hcg : Tendsto g (𝓝[s] x₀) (𝓝 a)<VAR>h : α → E := g - t.indicator fun x => a<VAR>A : Tendsto (fun i => ∫ (x : α) in s, φ i x • h x ∂μ + (∫ (x : α) in t, φ i x ∂μ) • a) l (𝓝 a)<VAR>i : ι<VAR>hi : IntegrableOn (fun x => φ i x • g x) s μ<VAR>h'i : ‖∫ (x : α) in t, φ i x ∂μ - 1‖ < 1<GOAL>Integrable (φ i) ((μ.restrict s).restrict t)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>hm : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : BorelSpace α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>g : α → E<VAR>l : Filter ι<VAR>x₀ : α<VAR>s t✝ : Set α<VAR>φ : ι → α → ℝ<VAR>a : E<VAR>inst✝ : CompleteSpace E<VAR>hs : MeasurableSet s<VAR>t : Set α<VAR>ht : MeasurableSet t<VAR>hts : t ⊆ s<VAR>h'ts : t ∈ 𝓝[s] x₀<VAR>h't : μ t ≠ ⊤<VAR>hnφ : ∀ᶠ (i : ι) in l, ∀ x ∈ s, 0 ≤ φ i x<VAR>hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)<VAR>hiφ : Tendsto (fun i => ∫ (x : α) in t, φ i x ∂μ) l (𝓝 1)<VAR>h'iφ : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (φ i) (μ.restrict s)<VAR>hmg : IntegrableOn g s μ<VAR>hcg : Tendsto g (𝓝[s] x₀) (𝓝 a)<VAR>h : α → E := g - t.indicator fun x => a<VAR>A : Tendsto (fun i => ∫ (x : α) in s, φ i x • h x ∂μ + (∫ (x : α) in t, φ i x ∂μ) • a) l (𝓝 a)<VAR>i : ι<VAR>hi : IntegrableOn (fun x => φ i x • g x) s μ<VAR>h'i : ‖∫ (x : α) in t, φ i x ∂μ - 1‖ < 1<GOAL>Integrable (φ i) (μ.restrict t)
<VAR>X✝ : Type u_1<VAR>Y : Type u_2<VAR>ι : Type u_3<VAR>ι' : Sort u_4<VAR>X : Type u_5<VAR>inst✝ : TopologicalSpace X<VAR>s : Set X<GOAL>IsClosed s ∧ IsNowhereDense s ↔ IsOpen sᶜ ∧ Dense sᶜ
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDomain R<VAR>inst✝² : ValuationRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : IsDomain S<VAR>f : R →+* S<VAR>hf : Function.Surjective ⇑f<VAR>a b : R<GOAL>∃ c, f a * c = f b ∨ f b * c = f a
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDomain R<VAR>inst✝² : ValuationRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : IsDomain S<VAR>f : R →+* S<VAR>hf : Function.Surjective ⇑f<VAR>a c : R<GOAL>∃ c_1, f a * c_1 = f (a * c) ∨ f (a * c) * c_1 = f a
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDomain R<VAR>inst✝² : ValuationRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : IsDomain S<VAR>f : R →+* S<VAR>hf : Function.Surjective ⇑f<VAR>b c : R<GOAL>∃ c_1, f (b * c) * c_1 = f b ∨ f b * c_1 = f (b * c)
<VAR>K : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝² : DivisionRing K<VAR>inst✝¹ : DivisionRing L<VAR>inst✝ : DivisionRing M<VAR>S : Set (Subfield K)<GOAL>IsGLB S (sInf S)
<VAR>K : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝² : DivisionRing K<VAR>inst✝¹ : DivisionRing L<VAR>inst✝ : DivisionRing M<VAR>S : Set (Subfield K)<VAR>this : ∀ {s t : Subfield K}, ↑s ≤ ↑t ↔ s ≤ t<GOAL>IsGLB S (sInf S)
<VAR>K : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝² : DivisionRing K<VAR>inst✝¹ : DivisionRing L<VAR>inst✝ : DivisionRing M<VAR>S : Set (Subfield K)<VAR>this : ∀ {s t : Subfield K}, ↑s ≤ ↑t ↔ s ≤ t<GOAL>IsGLB ((fun {x} => ↑x) '' S) ↑(sInf S)
<VAR>K : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝² : DivisionRing K<VAR>inst✝¹ : DivisionRing L<VAR>inst✝ : DivisionRing M<VAR>S : Set (Subfield K)<VAR>this : ∀ {s t : Subfield K}, ↑s ≤ ↑t ↔ s ≤ t<GOAL>↑(sInf S) = ⨅ x ∈ S, ↑x
<VAR>C✝ : Type u<VAR>inst✝² : Category.{v, u} C✝<VAR>X : TopCat<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_3, u_1} C<VAR>inst✝ : ConcreteCategory C<VAR>F G : Presheaf C X<VAR>e : F ⟶ G<VAR>U V : Opens ↑X<VAR>h : U ≤ V<VAR>x : (forget C).obj (F.obj (op V))<GOAL>(e.app (op U)) ((F.map (homOfLE h).op) x) = (G.map (homOfLE h).op) ((e.app (op V)) x)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : StrictOrderedCommRing R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>s : AffineSubspace R P<VAR>x y : P<VAR>f : P →ᵃ[R] P'<VAR>p₁ : P<VAR>hp₁ : p₁ ∈ s<VAR>p₂ : P<VAR>hp₂ : p₂ ∈ s<VAR>h : SameRay R (x -ᵥ p₁) (y -ᵥ p₂)<GOAL>(AffineSubspace.map f s).WSameSide (f x) (f y)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : StrictOrderedCommRing R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>s : AffineSubspace R P<VAR>x y : P<VAR>f : P →ᵃ[R] P'<VAR>p₁ : P<VAR>hp₁ : p₁ ∈ s<VAR>p₂ : P<VAR>hp₂ : p₂ ∈ s<VAR>h : SameRay R (x -ᵥ p₁) (y -ᵥ p₂)<GOAL>SameRay R (f x -ᵥ f p₁) (f y -ᵥ f p₂)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : StrictOrderedCommRing R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>s : AffineSubspace R P<VAR>x y : P<VAR>f : P →ᵃ[R] P'<VAR>p₁ : P<VAR>hp₁ : p₁ ∈ s<VAR>p₂ : P<VAR>hp₂ : p₂ ∈ s<VAR>h : SameRay R (x -ᵥ p₁) (y -ᵥ p₂)<GOAL>SameRay R (f.linear (x -ᵥ p₁)) (f.linear (y -ᵥ p₂))
<VAR>f g : CircleDeg1Lift<VAR>x : ℝ<VAR>m : ℤ<VAR>n : ℕ<VAR>hn : 0 < n<GOAL>x + ↑n * ↑m < (⇑f)^[n] x ↔ x + ↑m < f x
<VAR>b e : Pos<VAR>x✝ : Substring<VAR>h₁ : x✝.Valid<VAR>h₂ : { str := x✝.toString, startPos := b, stopPos := e }.Valid<GOAL>(x✝.extract b e).Valid
<VAR>b e : Pos<VAR>x✝ : Substring<VAR>h₁✝ : x✝.Valid<VAR>h₂ : { str := x✝.toString, startPos := b, stopPos := e }.Valid<VAR>l m r : List Char<VAR>h₁ : ValidFor l m r x✝<GOAL>(x✝.extract b e).Valid
<VAR>b e : Pos<VAR>x✝ : Substring<VAR>h₁✝ : x✝.Valid<VAR>l m : List Char<VAR>h₂ : { str := { data := m }, startPos := b, stopPos := e }.Valid<VAR>r : List Char<VAR>h₁ : ValidFor l m r x✝<GOAL>(x✝.extract b e).Valid
<VAR>b e : Pos<VAR>x✝ : Substring<VAR>h₁✝ : x✝.Valid<VAR>l m : List Char<VAR>h₂✝ : { str := { data := m }, startPos := b, stopPos := e }.Valid<VAR>r : List Char<VAR>h₁ : ValidFor l m r x✝<VAR>ml mm mr : List Char<VAR>h₂ : ValidFor ml mm mr { str := { data := m }, startPos := b, stopPos := e }<GOAL>(x✝.extract b e).Valid
<VAR>b e : Pos<VAR>x✝ : Substring<VAR>h₁✝ : x✝.Valid<VAR>l m : List Char<VAR>h₂✝ : { str := { data := m }, startPos := b, stopPos := e }.Valid<VAR>r : List Char<VAR>h₁ : ValidFor l m r x✝<VAR>ml mm mr : List Char<VAR>h₂ : ValidFor ml mm mr { str := { data := m }, startPos := b, stopPos := e }<VAR>l' r' : List Char<VAR>h₃ : ValidFor l' mm r' (x✝.extract b e)<GOAL>(x✝.extract b e).Valid
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.6986, u_1} C<VAR>inst✝ : Abelian C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>A B : Cᵒᵖ<VAR>g : A ⟶ B<GOAL>(cokernel.π f.op).unop ≫ f = 0
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.6986, u_1} C<VAR>inst✝ : Abelian C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>A B : Cᵒᵖ<VAR>g : A ⟶ B<GOAL>(f.op ≫ cokernel.π f.op).unop = 0
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.6986, u_1} C<VAR>inst✝ : Abelian C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>A B : Cᵒᵖ<VAR>g : A ⟶ B<GOAL>f.op ≫ (kernel.ι f).op = 0
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.6986, u_1} C<VAR>inst✝ : Abelian C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>A B : Cᵒᵖ<VAR>g : A ⟶ B<GOAL>kernel.lift f (cokernel.π f.op).unop ⋯ ≫ (cokernel.desc f.op (kernel.ι f).op ⋯).unop = 𝟙 (Opposite.unop (cokernel f.op))
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.6986, u_1} C<VAR>inst✝ : Abelian C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>A B : Cᵒᵖ<VAR>g : A ⟶ B<GOAL>(cokernel.desc f.op (kernel.ι f).op ⋯ ≫ (kernel.lift f (cokernel.π f.op).unop ⋯).op).unop = (𝟙 (cokernel f.op)).unop
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.6986, u_1} C<VAR>inst✝ : Abelian C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>A B : Cᵒᵖ<VAR>g : A ⟶ B<GOAL>coequalizer.π f.op 0 ≫ cokernel.desc f.op (kernel.ι f).op ⋯ ≫ (kernel.lift f (cokernel.π f.op).unop ⋯).op = coequalizer.π f.op 0 ≫ 𝟙 (cokernel f.op)
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.6986, u_1} C<VAR>inst✝ : Abelian C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>A B : Cᵒᵖ<VAR>g : A ⟶ B<GOAL>((cokernel.desc f.op (kernel.ι f).op ⋯).unop ≫ kernel.lift f (cokernel.π f.op).unop ⋯) ≫ equalizer.ι f 0 = 𝟙 (kernel f) ≫ equalizer.ι f 0
<VAR>R : Type u<VAR>inst✝⁶ : Semiring R<VAR>ι : Type v<VAR>dec_ι : DecidableEq ι<VAR>M : ι → Type w<VAR>inst✝⁵ : (i : ι) → AddCommMonoid (M i)<VAR>inst✝⁴ : (i : ι) → Module R (M i)<VAR>N : Type u₁<VAR>inst✝³ : AddCommMonoid N<VAR>inst✝² : Module R N<VAR>φ : (i : ι) → M i →ₗ[R] N<VAR>ψ ψ' : (⨁ (i : ι), M i) →ₗ[R] N<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>i : ι<VAR>m : M i<VAR>a : ι<GOAL>DFinsupp.equivFunOnFintype ((lof R ι M i) m) a = Pi.single i m a
<VAR>μ : YoungDiagram<VAR>j : ℕ<GOAL>∃ i, (i, j) ∉ μ.cells
<VAR>μ : YoungDiagram<VAR>j : ℕ<GOAL>(fun i => (i, j) ∉ μ.cells) = fun j_1 => (j, j_1) ∉ μ.transpose
<VAR>α : Type u_1<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : Fintype α<VAR>γ : α → Type u_2<VAR>δ : α → Type u_3<VAR>s✝ : (a : α) → Finset (γ a)<VAR>inst✝ : (a : α) → DecidableEq (δ a)<VAR>s : (i : α) → Finset (δ i)<VAR>i : α<VAR>t : Finset (δ i)<VAR>hts : t ⊆ s i<VAR>f : (a : α) → δ a<GOAL>f ∈ piFinset (update s i t) ↔ f ∈ filter (fun f => f i ∈ t) (piFinset s)
<VAR>α : Type u_1<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : Fintype α<VAR>γ : α → Type u_2<VAR>δ : α → Type u_3<VAR>s✝ : (a : α) → Finset (γ a)<VAR>inst✝ : (a : α) → DecidableEq (δ a)<VAR>s : (i : α) → Finset (δ i)<VAR>i : α<VAR>t : Finset (δ i)<VAR>hts : t ⊆ s i<VAR>f : (a : α) → δ a<GOAL>(∀ (a : α), f a ∈ update s i t a) ↔ (∀ (a : α), f a ∈ s a) ∧ f i ∈ t
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>R : Type u_4<VAR>inst✝ : DivisionCommMonoid α<VAR>a b : α<VAR>ha : IsSquare a<VAR>hb : IsSquare b<GOAL>IsSquare (a / b)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>R : Type u_4<VAR>inst✝ : DivisionCommMonoid α<VAR>a b : α<VAR>ha : IsSquare a<VAR>hb : IsSquare b<GOAL>IsSquare (a * b⁻¹)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>ι : Sort u_5<VAR>ι' : ι → Sort u_6<VAR>f : (i : ι) → ι' i → α → ℝ≥0∞<GOAL>⨆ i, ⨆ j, ∫⁻ (a : α), f i j a ∂μ ≤ ∫⁻ (a : α), ⨆ i, ⨆ j, f i j a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>ι : Sort u_5<VAR>ι' : ι → Sort u_6<VAR>f : (i : ι) → ι' i → α → ℝ≥0∞<VAR>a : α<GOAL>⨆ i, ⨆ j, f i j a = (⨆ i, ⨆ j, f i j) a
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M✝ : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<VAR>X Y : Mon_ C<VAR>M N : Bimod X Y<VAR>f : M ⟶ N<GOAL>({ X := X.X, actLeft := X.mul, one_actLeft := ⋯, left_assoc := ⋯, actRight := X.mul, actRight_one := ⋯, right_assoc := ⋯, middle_assoc := ⋯ }.whiskerLeft f).hom = ((isoOfIso { hom := LeftUnitorBimod.hom M, inv := LeftUnitorBimod.inv M, hom_inv_id := ⋯, inv_hom_id := ⋯ } ⋯ ⋯).hom ≫ f ≫ (isoOfIso { hom := LeftUnitorBimod.hom N, inv := LeftUnitorBimod.inv N, hom_inv_id := ⋯, inv_hom_id := ⋯ } ⋯ ⋯).inv).hom