ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>inst✝ : LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<VAR>hf : StrictConvexOn 𝕜 s f<VAR>x y z : 𝕜<VAR>hx : x ∈ s<VAR>hz : z ∈ s<VAR>hxy : 0 < y - x<VAR>hyz : 0 < z - y<VAR>hxz : 0 < z - x<VAR>hxz' : x ≠ z<VAR>a : 𝕜 := (z - y) / (z - x)<VAR>b : 𝕜 := (y - x) / (z - x)<VAR>hy : a • x + b • z = y<GOAL>f y / (y - x) + f y / (z - y) < f x / (y - x) + f z / (z - y)
<VAR>𝕜 : Type u_1<VAR>inst✝ : LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<VAR>hf : StrictConvexOn 𝕜 s f<VAR>x y z : 𝕜<VAR>hx : x ∈ s<VAR>hz : z ∈ s<VAR>hxy : 0 < y - x<VAR>hyz : 0 < z - y<VAR>hxz : 0 < z - x<VAR>hxz' : x ≠ z<VAR>a : 𝕜 := (z - y) / (z - x)<VAR>b : 𝕜 := (y - x) / (z - x)<VAR>hy : a • x + b • z = y<VAR>key : f (((z - y) / (z - x)) • x + ((y - x) / (z - x)) • z) < ((z - y) / (z - x)) • f x + ((y - x) / (z - x)) • f z<GOAL>f y / (y - x) + f y / (z - y) < f x / (y - x) + f z / (z - y)
<VAR>𝕜 : Type u_1<VAR>inst✝ : LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<VAR>hf : StrictConvexOn 𝕜 s f<VAR>x y z : 𝕜<VAR>hx : x ∈ s<VAR>hz : z ∈ s<VAR>hxy : 0 < y - x<VAR>hyz : 0 < z - y<VAR>hxz : 0 < z - x<VAR>hxz' : x ≠ z<VAR>a : 𝕜 := (z - y) / (z - x)<VAR>b : 𝕜 := (y - x) / (z - x)<VAR>hy : a • x + b • z = y<VAR>key : f y < ((z - y) / (z - x)) • f x + ((y - x) / (z - x)) • f z<GOAL>f y / (y - x) + f y / (z - y) < f x / (y - x) + f z / (z - y)
<VAR>𝕜 : Type u_1<VAR>inst✝ : LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<VAR>hf : StrictConvexOn 𝕜 s f<VAR>x y z : 𝕜<VAR>hx : x ∈ s<VAR>hz : z ∈ s<VAR>hxy : 0 < y - x<VAR>hyz : 0 < z - y<VAR>hxz : 0 < z - x<VAR>hxz' : x ≠ z<VAR>a : 𝕜 := (z - y) / (z - x)<VAR>b : 𝕜 := (y - x) / (z - x)<VAR>hy : a • x + b • z = y<VAR>key : (z - x) * f y < (z - x) * (((z - y) / (z - x)) • f x + ((y - x) / (z - x)) • f z)<GOAL>f y / (y - x) + f y / (z - y) < f x / (y - x) + f z / (z - y)
<VAR>𝕜 : Type u_1<VAR>inst✝ : LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<VAR>hf : StrictConvexOn 𝕜 s f<VAR>x y z : 𝕜<VAR>hx : x ∈ s<VAR>hz : z ∈ s<VAR>hxy : 0 < y - x<VAR>hyz : 0 < z - y<VAR>hxz : 0 < z - x<VAR>hxz' : x ≠ z<VAR>a : 𝕜 := (z - y) / (z - x)<VAR>b : 𝕜 := (y - x) / (z - x)<VAR>hy : a • x + b • z = y<VAR>key : f y * (z - x) < (z - y) * f x + (y - x) * f z<GOAL>(f y * (z - y) + f y * (y - x)) / ((y - x) * (z - y)) < (f x * (z - y) + f z * (y - x)) / ((y - x) * (z - y))
<VAR>𝕜 : Type u_1<VAR>inst✝ : LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<VAR>hf : StrictConvexOn 𝕜 s f<VAR>x y z : 𝕜<VAR>hx : x ∈ s<VAR>hz : z ∈ s<VAR>hxy : 0 < y - x<VAR>hyz : 0 < z - y<VAR>hxz : 0 < z - x<VAR>hxz' : x ≠ z<VAR>a : 𝕜 := (z - y) / (z - x)<VAR>b : 𝕜 := (y - x) / (z - x)<VAR>hy : a • x + b • z = y<VAR>key : f y * (z - x) < (z - y) * f x + (y - x) * f z<GOAL>f y * (z - y) + f y * (y - x) < f x * (z - y) + f z * (y - x)
<VAR>𝕜 : Type u_1<VAR>inst✝ : LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<VAR>hf : StrictConvexOn 𝕜 s f<VAR>x y z : 𝕜<VAR>hx : x ∈ s<VAR>hz : z ∈ s<VAR>hxy : 0 < y - x<VAR>hyz : 0 < z - y<VAR>hxz : 0 < z - x<VAR>hxz' : x ≠ z<VAR>a : 𝕜 := (z - y) / (z - x)<VAR>b : 𝕜 := (y - x) / (z - x)<VAR>hy : a • x + b • z = y<VAR>key : f y * (z - x) < (z - y) * f x + (y - x) * f z<GOAL>0 < (y - x) * (z - y)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>inst✝² : SMulCommClass ℝ 𝕜 E<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace E<GOAL>Continuous fun f => integralCLM f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort uι<VAR>s t u : Set α<VAR>π : δ → Type u_6<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : (a : δ) → MeasurableSpace (π a)<VAR>inst✝² : MeasurableSpace γ<VAR>inst✝¹ : Unique δ<VAR>inst✝ : (i : δ) → MeasurableSpace (π i)<GOAL>Measurable uniqueElim
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort uι<VAR>s t u : Set α<VAR>π : δ → Type u_6<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : (a : δ) → MeasurableSpace (π a)<VAR>inst✝² : MeasurableSpace γ<VAR>inst✝¹ : Unique δ<VAR>inst✝ : (i : δ) → MeasurableSpace (π i)<GOAL>Measurable fun x => x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : CommMonoid β<VAR>f : Fin 6 → β<GOAL>∏ i : Fin 6, f i = f 0 * f 1 * f 2 * f 3 * f 4 * f 5
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : CommMonoid β<VAR>f : Fin 6 → β<GOAL>f (castSucc 0) * f (castSucc 1) * f (castSucc 2) * f (castSucc 3) * f (castSucc 4) * f (last 5) = f 0 * f 1 * f 2 * f 3 * f 4 * f 5
<VAR>α : Type u<VAR>β : Type v<VAR>l✝ l₁ l₂ : List α<VAR>r : α → α → Prop<VAR>a b : α<VAR>l : List α<GOAL>l.Nodup ↔ ∀ (i j : ℕ), i < j → j < l.length → l.get? i ≠ l.get? j
<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>q : Stmt Bool Λ' σ<VAR>v : σ<VAR>a b : Γ<VAR>L R : ListBlank Γ<GOAL>stepAux (write (enc a).toList q) v (trTape' enc0 L (ListBlank.cons b R)) = stepAux q v (trTape' enc0 (ListBlank.cons a L) R)
<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>q : Stmt Bool Λ' σ<VAR>v : σ<VAR>a b : Γ<VAR>L R : ListBlank Γ<GOAL>stepAux (write (enc a).toList q) v (Tape.mk' (L.bind (fun x => (enc x).toList.reverse) ⋯) (ListBlank.append (enc b).toList (R.bind (fun x => (enc x).toList) ⋯))) = stepAux q 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>q : Stmt Bool Λ' σ<VAR>v : σ<VAR>a b : Γ<VAR>L R : ListBlank Γ<GOAL>∀ {L' R' : ListBlank Bool} (l₁ l₂ l₂' : List Bool), l₂'.length = l₂.length → stepAux (write l₂ q) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂' R')) = stepAux q v (Tape.mk' (ListBlank.append (l₂.reverseAux l₁) L') R')
<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>q : Stmt Bool Λ' σ<VAR>v : σ<VAR>L' R' : ListBlank Bool<VAR>a : Bool<VAR>l₂ : List Bool<VAR>IH : ∀ (l₁ l₂' : List Bool), l₂'.length = l₂.length → stepAux (write l₂ q) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂' R')) = stepAux q v (Tape.mk' (ListBlank.append (l₂.reverseAux l₁) L') R')<VAR>l₁ l₂' : List Bool<VAR>e : l₂'.length = (a :: l₂).length<GOAL>stepAux (write (a :: l₂) q) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂' R')) = stepAux q v (Tape.mk' (ListBlank.append ((a :: l₂).reverseAux l₁) L') R')
<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>q : Stmt Bool Λ' σ<VAR>v : σ<VAR>L' R' : ListBlank Bool<VAR>a : Bool<VAR>l₂ : List Bool<VAR>IH : ∀ (l₁ l₂' : List Bool), l₂'.length = l₂.length → stepAux (write l₂ q) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂' R')) = stepAux q v (Tape.mk' (ListBlank.append (l₂.reverseAux l₁) L') R')<VAR>l₁ : List Bool<VAR>b : Bool<VAR>l₂' : List Bool<VAR>e : l₂'.length = l₂.length<GOAL>stepAux (write (a :: l₂) q) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append (b :: l₂') R')) = stepAux q v (Tape.mk' (ListBlank.append ((a :: l₂).reverseAux l₁) L') R')
<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>q : Stmt Bool Λ' σ<VAR>v : σ<VAR>L' R' : ListBlank Bool<VAR>a : Bool<VAR>l₂ : List Bool<VAR>IH : ∀ (l₁ l₂' : List Bool), l₂'.length = l₂.length → stepAux (write l₂ q) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂' R')) = stepAux q v (Tape.mk' (ListBlank.append (l₂.reverseAux l₁) L') R')<VAR>l₁ : List Bool<VAR>b : Bool<VAR>l₂' : List Bool<VAR>e : l₂'.length = l₂.length<GOAL>stepAux (write (a :: l₂) q) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append (b :: l₂') R')) = stepAux (write l₂ q) v (Tape.mk' (ListBlank.append (a :: l₁) L') (ListBlank.append l₂' R'))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a b c w✝ : α<VAR>h : s(b, c) = s(a, w✝)<GOAL>a = b ∨ a = c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a b c w✝ : α<VAR>h : b = a ∧ c = w✝ ∨ b = w✝ ∧ c = a<GOAL>a = b ∨ a = c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a b : α<GOAL>Sym2.Mem a s(b, a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a b : α<GOAL>Sym2.Mem a s(a, b)
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_2, u_1} C<VAR>inst✝² : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.RightHomologyData<VAR>h₂ : S₂.RightHomologyData<VAR>γ : RightHomologyMapData φ h₁ h₂<VAR>inst✝¹ : S₁.HasRightHomology<VAR>inst✝ : S₂.HasRightHomology<GOAL>opcyclesMap φ ≫ h₂.opcyclesIso.hom = h₁.opcyclesIso.hom ≫ γ.φQ
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X✝ Y✝ : C<VAR>𝒯 : LimitCone (Functor.empty C)<VAR>ℬ : (X Y : C) → LimitCone (pair X Y)<VAR>X X' Y Y' : C<VAR>f : X ⟶ Y<VAR>g : X' ⟶ Y'<GOAL>(ℬ Y Y').isLimit.lift (BinaryFan.mk (BinaryFan.fst (ℬ X X').cone ≫ f) (BinaryFan.snd (ℬ X X').cone ≫ g)) ≫ ((ℬ Y Y').isLimit.conePointUniqueUpToIso (ℬ Y' Y).isLimit.swapBinaryFan).hom = ((ℬ X X').isLimit.conePointUniqueUpToIso (ℬ X' X).isLimit.swapBinaryFan).hom ≫ (ℬ Y' Y).isLimit.lift (BinaryFan.mk (BinaryFan.fst (ℬ X' X).cone ≫ g) (BinaryFan.snd (ℬ X' X).cone ≫ f))
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X✝ Y✝ : C<VAR>𝒯 : LimitCone (Functor.empty C)<VAR>ℬ : (X Y : C) → LimitCone (pair X Y)<VAR>X X' Y Y' : C<VAR>f : X ⟶ Y<VAR>g : X' ⟶ Y'<GOAL>∀ (j : Discrete WalkingPair), ((ℬ Y Y').isLimit.lift (BinaryFan.mk (BinaryFan.fst (ℬ X X').cone ≫ f) (BinaryFan.snd (ℬ X X').cone ≫ g)) ≫ ((ℬ Y Y').isLimit.conePointUniqueUpToIso (ℬ Y' Y).isLimit.swapBinaryFan).hom) ≫ (ℬ Y' Y).cone.π.app j = (((ℬ X X').isLimit.conePointUniqueUpToIso (ℬ X' X).isLimit.swapBinaryFan).hom ≫ (ℬ Y' Y).isLimit.lift (BinaryFan.mk (BinaryFan.fst (ℬ X' X).cone ≫ g) (BinaryFan.snd (ℬ X' X).cone ≫ f))) ≫ (ℬ Y' Y).cone.π.app j
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝² : Category.{u_4, u_1} C<VAR>inst✝¹ : Category.{?u.61160, u_2} D<VAR>inst✝ : Category.{?u.61164, u_3} E<VAR>X B : C<VAR>π : X ⟶ B<VAR>c : PullbackCone π π<VAR>hc : IsLimit c<GOAL>(parallelPair (Over.homMk c.fst ⋯).op (Over.homMk c.snd ⋯).op).Initial
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝² : Category.{u_4, u_1} C<VAR>inst✝¹ : Category.{?u.61160, u_2} D<VAR>inst✝ : Category.{?u.61164, u_3} E<VAR>X B : C<VAR>π : X ⟶ B<VAR>c : PullbackCone π π<VAR>hc : IsLimit c<GOAL>∀ (Z : (Sieve.ofArrows (fun x => X) fun x => π).arrows.categoryᵒᵖ), Nonempty (op ((Sieve.ofArrows (fun x => X) fun x => π).arrows.categoryMk π ⋯) ⟶ Z)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝² : Category.{u_4, u_1} C<VAR>inst✝¹ : Category.{?u.61160, u_2} D<VAR>inst✝ : Category.{?u.61164, u_3} E<VAR>X B : C<VAR>π : X ⟶ B<VAR>c : PullbackCone π π<VAR>hc : IsLimit c<GOAL>∀ ⦃Z : (Sieve.ofArrows (fun x => X) fun x => π).arrows.categoryᵒᵖ⦄ (i j : op ((Sieve.ofArrows (fun x => X) fun x => π).arrows.categoryMk π ⋯) ⟶ Z), ∃ a, i = (Over.homMk c.fst ⋯).op ≫ a ∧ j = (Over.homMk c.snd ⋯).op ≫ a
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : LinearOrder α<VAR>p : α → Prop<VAR>x✝ y✝ x y : α<GOAL>max x y = if x < y then y else x
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : LinearOrder α<VAR>p : α → Prop<VAR>x✝ y✝ x y : α<GOAL>(if ¬y ≤ x then y else x) = if x < y then y else x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a b : α<VAR>h : a ≤ b<VAR>x✝ x : α<VAR>hx : x ∈ Iic b<VAR>y : α<VAR>hy : y ∈ Iic b<VAR>hxy : x < y<GOAL>projIic b x < projIic b y
<VAR>n m : ℕ<VAR>a b : Fin (n + 1)<VAR>ha : a.castSucc ≠ 0<GOAL>b ≤ a.castSucc.pred ha ↔ b < a
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹⁹ : RCLike 𝕜<VAR>inst✝¹⁸ : NormedAddCommGroup E<VAR>inst✝¹⁷ : InnerProductSpace 𝕜 E<VAR>inst✝¹⁶ : CompleteSpace E<VAR>inst✝¹⁵ : NormedAddCommGroup E'<VAR>inst✝¹⁴ : InnerProductSpace 𝕜 E'<VAR>inst✝¹³ : CompleteSpace E'<VAR>inst✝¹² : NormedSpace ℝ E'<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedSpace 𝕜 F<VAR>inst✝⁹ : NormedAddCommGroup G<VAR>inst✝⁸ : NormedAddCommGroup G'<VAR>inst✝⁷ : NormedSpace ℝ G'<VAR>inst✝⁶ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>E'' : Type u_8<VAR>𝕜' : Type u_9<VAR>inst✝⁵ : RCLike 𝕜'<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : InnerProductSpace 𝕜' E''<VAR>inst✝² : CompleteSpace E''<VAR>inst✝¹ : NormedSpace ℝ E''<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>x : E'<GOAL>Integrable (↑↑↑((condexpL2 E' 𝕜 hm) (indicatorConstLp 2 hs hμs x))) μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹⁹ : RCLike 𝕜<VAR>inst✝¹⁸ : NormedAddCommGroup E<VAR>inst✝¹⁷ : InnerProductSpace 𝕜 E<VAR>inst✝¹⁶ : CompleteSpace E<VAR>inst✝¹⁵ : NormedAddCommGroup E'<VAR>inst✝¹⁴ : InnerProductSpace 𝕜 E'<VAR>inst✝¹³ : CompleteSpace E'<VAR>inst✝¹² : NormedSpace ℝ E'<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedSpace 𝕜 F<VAR>inst✝⁹ : NormedAddCommGroup G<VAR>inst✝⁸ : NormedAddCommGroup G'<VAR>inst✝⁷ : NormedSpace ℝ G'<VAR>inst✝⁶ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>E'' : Type u_8<VAR>𝕜' : Type u_9<VAR>inst✝⁵ : RCLike 𝕜'<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : InnerProductSpace 𝕜' E''<VAR>inst✝² : CompleteSpace E''<VAR>inst✝¹ : NormedSpace ℝ E''<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>x : E'<GOAL>AEStronglyMeasurable (↑↑↑((condexpL2 E' 𝕜 hm) (indicatorConstLp 2 hs hμs x))) μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹⁹ : RCLike 𝕜<VAR>inst✝¹⁸ : NormedAddCommGroup E<VAR>inst✝¹⁷ : InnerProductSpace 𝕜 E<VAR>inst✝¹⁶ : CompleteSpace E<VAR>inst✝¹⁵ : NormedAddCommGroup E'<VAR>inst✝¹⁴ : InnerProductSpace 𝕜 E'<VAR>inst✝¹³ : CompleteSpace E'<VAR>inst✝¹² : NormedSpace ℝ E'<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedSpace 𝕜 F<VAR>inst✝⁹ : NormedAddCommGroup G<VAR>inst✝⁸ : NormedAddCommGroup G'<VAR>inst✝⁷ : NormedSpace ℝ G'<VAR>inst✝⁶ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>E'' : Type u_8<VAR>𝕜' : Type u_9<VAR>inst✝⁵ : RCLike 𝕜'<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : InnerProductSpace 𝕜' E''<VAR>inst✝² : CompleteSpace E''<VAR>inst✝¹ : NormedSpace ℝ E''<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>x : E'<GOAL>∀ (s_1 : Set α), MeasurableSet s_1 → μ s_1 ≠ ⊤ → ∫⁻ (x_1 : α) in s_1, ↑‖↑↑↑((condexpL2 E' 𝕜 hm) (indicatorConstLp 2 hs hμs x)) x_1‖₊ ∂μ ≤ μ s * ↑‖x‖₊
<VAR>α : Type u<VAR>inst✝² : Group α<VAR>inst✝¹ : LT α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b c : α<GOAL>1 < b⁻¹ * a ↔ b < a
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>R : Type v<VAR>inst✝ : CommRing R<GOAL>det 1 = 1
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>R : Type v<VAR>inst✝ : CommRing R<GOAL>(diagonal fun x => 1).det = 1
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>w : W<GOAL>∃ ω, ω.length = cs.length w ∧ w = cs.wordProd ω
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>w : W<VAR>this : ∃ ω, ω.length = Nat.find ⋯ ∧ cs.wordProd ω = w<GOAL>∃ ω, ω.length = cs.length w ∧ w = cs.wordProd ω
<VAR>β : Type u_1<VAR>G : Type u_2<VAR>α : Type u_3<VAR>γ : Type u_4<VAR>inst✝³ : Group G<VAR>inst✝² : AddGroup α<VAR>inst✝¹ : SMul γ α<VAR>inst✝ : SlashAction β G α γ<VAR>k : β<VAR>g : G<VAR>a : α<GOAL>(-a) ∣[k;γ] g + a ∣[k;γ] g = 0
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>R : Type u_5<VAR>inst✝⁵ : MeasurableSpace X<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : MeasurableSpace Y<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedAddCommGroup F<VAR>f✝ g : X → E<VAR>μ : Measure X<VAR>s✝ : Set X<VAR>ι : Type u_6<VAR>s : Finset ι<VAR>f : ι → X → E<VAR>hf : ∀ i ∈ s, LocallyIntegrable (f i) μ<GOAL>LocallyIntegrable (fun a => ∑ i ∈ s, f i a) μ
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : Preorder α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a a₁ a₂ b b₁ b₂ c x : α<GOAL>(Ico a b).Nonempty ↔ a < b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>M : Type u_3<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : LinearOrderedAddCommMonoid M<VAR>v w : VectorMeasure α M<VAR>i j : Set α<VAR>hi : ¬v.restrict i ≤ restrict 0 i<GOAL>∃ j, MeasurableSet j ∧ j ⊆ i ∧ 0 < ↑v j
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>M : Type u_3<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : LinearOrderedAddCommMonoid M<VAR>v w : VectorMeasure α M<VAR>i j : Set α<VAR>hi : ¬v.restrict i ≤ restrict 0 i<VAR>hi₁ : MeasurableSet i<GOAL>∃ j, MeasurableSet j ∧ j ⊆ i ∧ 0 < ↑v j
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>M : Type u_3<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : LinearOrderedAddCommMonoid M<VAR>v w : VectorMeasure α M<VAR>i j : Set α<VAR>hi : ¬∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ i → ↑v j ≤ ↑0 j<VAR>hi₁ : MeasurableSet i<GOAL>∃ j, MeasurableSet j ∧ j ⊆ i ∧ 0 < ↑v j
<VAR>E : Type u_1<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>x : E<VAR>r : ℝ<VAR>hr : r ≠ 0<GOAL>interior (sphere x r) = ∅
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : LieRing L<VAR>inst✝⁹ : LieAlgebra R L<VAR>inst✝⁸ : LieAlgebra.IsNilpotent R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>M₂ : Type u_5<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<VAR>χ : L → R<VAR>f : M →ₗ⁅R,L⁆ M₂<VAR>e : M ≃ₗ⁅R,L⁆ M₂<GOAL>LieSubmodule.map e.toLieModuleHom (posFittingComp R L M) = posFittingComp R L M₂
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : LieRing L<VAR>inst✝⁹ : LieAlgebra R L<VAR>inst✝⁸ : LieAlgebra.IsNilpotent R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>M₂ : Type u_5<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<VAR>χ : L → R<VAR>f : M →ₗ⁅R,L⁆ M₂<VAR>e : M ≃ₗ⁅R,L⁆ M₂<GOAL>posFittingComp R L M₂ ≤ LieSubmodule.map e.toLieModuleHom (posFittingComp R L M)
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : LieRing L<VAR>inst✝⁹ : LieAlgebra R L<VAR>inst✝⁸ : LieAlgebra.IsNilpotent R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>M₂ : Type u_5<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<VAR>χ : L → R<VAR>f : M →ₗ⁅R,L⁆ M₂<VAR>e : M ≃ₗ⁅R,L⁆ M₂<GOAL>posFittingComp R L M₂ = LieSubmodule.map e.toLieModuleHom (LieSubmodule.map e.symm.toLieModuleHom (posFittingComp R L M₂))
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : LieRing L<VAR>inst✝⁹ : LieAlgebra R L<VAR>inst✝⁸ : LieAlgebra.IsNilpotent R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>M₂ : Type u_5<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<VAR>χ : L → R<VAR>f : M →ₗ⁅R,L⁆ M₂<VAR>e : M ≃ₗ⁅R,L⁆ M₂<GOAL>posFittingComp R L M₂ = LieSubmodule.map (e.comp e.symm.toLieModuleHom) (posFittingComp R L M₂)
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : LieRing L<VAR>inst✝⁹ : LieAlgebra R L<VAR>inst✝⁸ : LieAlgebra.IsNilpotent R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>M₂ : Type u_5<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<VAR>χ : L → R<VAR>f : M →ₗ⁅R,L⁆ M₂<VAR>e : M ≃ₗ⁅R,L⁆ M₂<GOAL>posFittingComp R L M₂ = LieSubmodule.map LieModuleHom.id (LieSubmodule.map (e.comp e.symm.toLieModuleHom) (posFittingComp R L M₂))
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : Type x<VAR>inst✝² : Mul R<VAR>inst✝¹ : Add R<VAR>inst✝ : RightDistribClass R<VAR>a b c d : R<GOAL>(a + b + c) * d = a * d + b * d + c * d
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : Category.{v₁, u₂} D<VAR>G : D ⥤ C<VAR>F : C ⥤ D<VAR>adj : F ⊣ G<VAR>inst✝ : ∀ (A : adj.toMonad.Algebra), HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))<VAR>A : adj.toMonad.Algebra<GOAL>((comparisonAdjunction adj).unit.app A).f = (beckCoequalizer A).desc (unitCofork A)
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : Category.{v₁, u₂} D<VAR>G : D ⥤ C<VAR>F : C ⥤ D<VAR>adj : F ⊣ G<VAR>inst✝ : ∀ (A : adj.toMonad.Algebra), HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))<VAR>A : adj.toMonad.Algebra<GOAL>(beckCofork A).π ≫ ((comparisonAdjunction adj).unit.app A).f = (beckCofork A).π ≫ (beckCoequalizer A).desc (unitCofork A)
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : Category.{v₁, u₂} D<VAR>G : D ⥤ C<VAR>F : C ⥤ D<VAR>adj : F ⊣ G<VAR>inst✝ : ∀ (A : adj.toMonad.Algebra), HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))<VAR>A : adj.toMonad.Algebra<GOAL>(beckCofork A).π ≫ ((comparisonAdjunction adj).unit.app A).f = (unitCofork A).π
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : Category.{v₁, u₂} D<VAR>G : D ⥤ C<VAR>F : C ⥤ D<VAR>adj : F ⊣ G<VAR>inst✝ : ∀ (A : adj.toMonad.Algebra), HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))<VAR>A : adj.toMonad.Algebra<GOAL>A.a ≫ ((comparisonAdjunction adj).unit.app A).f = G.map (coequalizer.π (F.map A.a) (adj.counit.app (F.obj A.A)))
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : Category.{v₁, u₂} D<VAR>G : D ⥤ C<VAR>F : C ⥤ D<VAR>adj : F ⊣ G<VAR>inst✝ : ∀ (A : adj.toMonad.Algebra), HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))<VAR>A : adj.toMonad.Algebra<GOAL>adj.unit.app (adj.toMonad.obj A.A) ≫ G.map (adj.counit.app (F.obj A.A)) ≫ G.map (coequalizer.π (F.map A.a) (adj.counit.app (F.obj A.A))) = G.map (coequalizer.π (F.map A.a) (adj.counit.app (F.obj A.A)))
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>p1 p2 p3 : P<GOAL>dist p1 p3 * dist p1 p3 = dist p1 p2 * dist p1 p2 + dist p3 p2 * dist p3 p2 - 2 * dist p1 p2 * dist p3 p2 * Real.cos (∠ p1 p2 p3)