ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>τ σ : Ω → ι<VAR>E : Type u_4<VAR>p : ℝ≥0∞<VAR>u : ι → Ω → E<VAR>inst✝⁴ : LinearOrder ι<VAR>inst✝³ : TopologicalSpace ι<VAR>inst✝² : OrderTopology ι<VAR>inst✝¹ : FirstCountableTopology ι<VAR>ℱ : Filtration ι m<VAR>inst✝ : NormedAddCommGroup E<VAR>hτ : IsStoppingTime ℱ τ<VAR>hu : ∀ (n : ι), Integrable (u n) μ<VAR>n : ι<VAR>s : Finset ι<VAR>hbdd : ∀ (ω : Ω), τ ω < n → τ ω ∈ s<GOAL>Integrable (stoppedProcess u τ n) μ
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>τ σ : Ω → ι<VAR>E : Type u_4<VAR>p : ℝ≥0∞<VAR>u : ι → Ω → E<VAR>inst✝⁴ : LinearOrder ι<VAR>inst✝³ : TopologicalSpace ι<VAR>inst✝² : OrderTopology ι<VAR>inst✝¹ : FirstCountableTopology ι<VAR>ℱ : Filtration ι m<VAR>inst✝ : NormedAddCommGroup E<VAR>hτ : IsStoppingTime ℱ τ<VAR>n : ι<VAR>s : Finset ι<VAR>hbdd : ∀ (ω : Ω), τ ω < n → τ ω ∈ s<VAR>hu : ∀ (n : ι), Memℒp (u n) 1 μ<GOAL>Memℒp (stoppedProcess u τ n) 1 μ
<VAR>C : Type u₁<VAR>inst✝⁵ : Category.{v₁, u₁} C<VAR>inst✝⁴ : MonoidalCategory C<VAR>inst✝³ : BraidedCategory C<VAR>D : Type u₂<VAR>inst✝² : Category.{v₂, u₂} D<VAR>inst✝¹ : MonoidalCategory D<VAR>inst✝ : BraidedCategory D<VAR>F : LaxBraidedFunctor C D<VAR>A : CommMon_ C<GOAL>(β_ (F.obj A.X) (F.obj A.X)).hom ≫ F.μ A.X A.X ≫ F.map A.mul = F.μ A.X A.X ≫ F.map A.mul
<VAR>C : Type u₁<VAR>inst✝⁵ : Category.{v₁, u₁} C<VAR>inst✝⁴ : MonoidalCategory C<VAR>inst✝³ : BraidedCategory C<VAR>D : Type u₂<VAR>inst✝² : Category.{v₂, u₂} D<VAR>inst✝¹ : MonoidalCategory D<VAR>inst✝ : BraidedCategory D<VAR>F : LaxBraidedFunctor C D<VAR>A : CommMon_ C<VAR>this : ∀ (X Y : C), F.μ X Y ≫ F.map (β_ X Y).hom = (β_ (F.obj X) (F.obj Y)).hom ≫ F.μ Y X<GOAL>(β_ (F.obj A.X) (F.obj A.X)).hom ≫ F.μ A.X A.X ≫ F.map A.mul = F.μ A.X A.X ≫ F.map A.mul
<VAR>C : Type u₁<VAR>inst✝⁵ : Category.{v₁, u₁} C<VAR>inst✝⁴ : MonoidalCategory C<VAR>inst✝³ : BraidedCategory C<VAR>D : Type u₂<VAR>inst✝² : Category.{v₂, u₂} D<VAR>inst✝¹ : MonoidalCategory D<VAR>inst✝ : BraidedCategory D<VAR>F : LaxBraidedFunctor C D<VAR>A : CommMon_ C<VAR>this : ∀ (X Y : C), F.μ X Y ≫ F.map (β_ X Y).hom = (β_ (F.obj X) (F.obj Y)).hom ≫ F.μ Y X<GOAL>(F.μ A.X A.X ≫ F.map (β_ A.X A.X).hom) ≫ F.map A.mul = F.μ A.X A.X ≫ F.map A.mul
<VAR>G✝ : Type u<VAR>inst✝² : AddCommGroup G✝<VAR>G : Type u_1<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : Finite G<GOAL>∃ ι x n, (∀ (i : ι), 1 < n i) ∧ Nonempty (G ≃+ ⨁ (i : ι), ZMod (n i))
<VAR>C : Type u<VAR>inst✝⁷ : Category.{v, u} C<VAR>X✝ Y✝ : C<VAR>D : Type u_1<VAR>inst✝⁶ : Category.{?u.241337, u_1} D<VAR>F : C ⥤ D<VAR>inst✝⁵ : HasTerminal C<VAR>inst✝⁴ : HasBinaryProducts C<VAR>inst✝³ : HasTerminal D<VAR>inst✝² : HasBinaryProducts D<VAR>inst✝¹ : PreservesLimit (empty C) F<VAR>inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>X' : C<GOAL>MonoidalCategory.whiskerRight (F.map f) (F.obj X') ≫ (fun X Y => (asIso (prodComparison F X Y)).inv) Y X' = (fun X Y => (asIso (prodComparison F X Y)).inv) X X' ≫ F.map (MonoidalCategory.whiskerRight f X')
<VAR>C : Type u<VAR>inst✝⁷ : Category.{v, u} C<VAR>X✝ Y✝ : C<VAR>D : Type u_1<VAR>inst✝⁶ : Category.{?u.241337, u_1} D<VAR>F : C ⥤ D<VAR>inst✝⁵ : HasTerminal C<VAR>inst✝⁴ : HasBinaryProducts C<VAR>inst✝³ : HasTerminal D<VAR>inst✝² : HasBinaryProducts D<VAR>inst✝¹ : PreservesLimit (empty C) F<VAR>inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F<VAR>X Y X' : C<VAR>g : X ⟶ Y<GOAL>MonoidalCategory.whiskerLeft (F.obj X') (F.map g) ≫ (fun X Y => (asIso (prodComparison F X Y)).inv) X' Y = (fun X Y => (asIso (prodComparison F X Y)).inv) X' X ≫ F.map (MonoidalCategory.whiskerLeft X' g)
<VAR>C : Type u<VAR>inst✝⁷ : Category.{v, u} C<VAR>X✝ Y✝ : C<VAR>D : Type u_1<VAR>inst✝⁶ : Category.{?u.241337, u_1} D<VAR>F : C ⥤ D<VAR>inst✝⁵ : HasTerminal C<VAR>inst✝⁴ : HasBinaryProducts C<VAR>inst✝³ : HasTerminal D<VAR>inst✝² : HasBinaryProducts D<VAR>inst✝¹ : PreservesLimit (empty C) F<VAR>inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F<VAR>X Y Z : C<GOAL>MonoidalCategory.whiskerRight ((fun X Y => (asIso (prodComparison F X Y)).inv) X Y) (F.obj Z) ≫ (fun X Y => (asIso (prodComparison F X Y)).inv) (MonoidalCategory.tensorObj X Y) Z ≫ F.map (MonoidalCategory.associator X Y Z).hom = (MonoidalCategory.associator (F.obj X) (F.obj Y) (F.obj Z)).hom ≫ MonoidalCategory.whiskerLeft (F.obj X) ((fun X Y => (asIso (prodComparison F X Y)).inv) Y Z) ≫ (fun X Y => (asIso (prodComparison F X Y)).inv) X (MonoidalCategory.tensorObj Y Z)
<VAR>C : Type u<VAR>inst✝⁷ : Category.{v, u} C<VAR>X✝ Y✝ : C<VAR>D : Type u_1<VAR>inst✝⁶ : Category.{?u.241337, u_1} D<VAR>F : C ⥤ D<VAR>inst✝⁵ : HasTerminal C<VAR>inst✝⁴ : HasBinaryProducts C<VAR>inst✝³ : HasTerminal D<VAR>inst✝² : HasBinaryProducts D<VAR>inst✝¹ : PreservesLimit (empty C) F<VAR>inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F<VAR>X Y Z : C<GOAL>MonoidalCategory.whiskerRight (asIso (prodComparison F X Y)).inv (F.obj Z) ≫ (asIso (prodComparison F (MonoidalCategory.tensorObj X Y) Z)).inv ≫ F.map (prod.lift (prod.fst ≫ prod.fst) (prod.lift (prod.fst ≫ prod.snd) prod.snd)) = prod.lift (prod.fst ≫ prod.fst) (prod.lift (prod.fst ≫ prod.snd) prod.snd) ≫ MonoidalCategory.whiskerLeft (F.obj X) (asIso (prodComparison F Y Z)).inv ≫ (asIso (prodComparison F X (MonoidalCategory.tensorObj Y Z))).inv
<VAR>C : Type u<VAR>inst✝⁷ : Category.{v, u} C<VAR>X✝ Y✝ : C<VAR>D : Type u_1<VAR>inst✝⁶ : Category.{?u.241337, u_1} D<VAR>F : C ⥤ D<VAR>inst✝⁵ : HasTerminal C<VAR>inst✝⁴ : HasBinaryProducts C<VAR>inst✝³ : HasTerminal D<VAR>inst✝² : HasBinaryProducts D<VAR>inst✝¹ : PreservesLimit (empty C) F<VAR>inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F<VAR>X Y Z : C<GOAL>prod.map (prodComparison F X Y) (𝟙 (F.obj Z)) ≫ MonoidalCategory.whiskerRight (asIso (prodComparison F X Y)).inv (F.obj Z) ≫ (asIso (prodComparison F (MonoidalCategory.tensorObj X Y) Z)).inv ≫ F.map (prod.lift (prod.fst ≫ prod.fst) (prod.lift (prod.fst ≫ prod.snd) prod.snd)) = prod.map (prodComparison F X Y) (𝟙 (F.obj Z)) ≫ prod.lift (prod.fst ≫ prod.fst) (prod.lift (prod.fst ≫ prod.snd) prod.snd) ≫ MonoidalCategory.whiskerLeft (F.obj X) (asIso (prodComparison F Y Z)).inv ≫ (asIso (prodComparison F X (MonoidalCategory.tensorObj Y Z))).inv
<VAR>C : Type u<VAR>inst✝⁷ : Category.{v, u} C<VAR>X✝ Y✝ : C<VAR>D : Type u_1<VAR>inst✝⁶ : Category.{?u.241337, u_1} D<VAR>F : C ⥤ D<VAR>inst✝⁵ : HasTerminal C<VAR>inst✝⁴ : HasBinaryProducts C<VAR>inst✝³ : HasTerminal D<VAR>inst✝² : HasBinaryProducts D<VAR>inst✝¹ : PreservesLimit (empty C) F<VAR>inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F<VAR>X Y Z : C<GOAL>prod.map (prodComparison F X Y) (𝟙 (F.obj Z)) ≫ prod.map (CategoryTheory.inv (prodComparison F X Y)) (𝟙 (F.obj Z)) ≫ CategoryTheory.inv (prodComparison F (X ⨯ Y) Z) ≫ F.map (prod.lift (prod.fst ≫ prod.fst) (prod.lift (prod.fst ≫ prod.snd) prod.snd)) = prod.map (prodComparison F X Y) (𝟙 (F.obj Z)) ≫ prod.lift (prod.fst ≫ prod.fst) (prod.lift (prod.fst ≫ prod.snd) prod.snd) ≫ prod.map (𝟙 (F.obj X)) (CategoryTheory.inv (prodComparison F Y Z)) ≫ CategoryTheory.inv (prodComparison F X (Y ⨯ Z))
<VAR>C : Type u<VAR>inst✝⁷ : Category.{v, u} C<VAR>X✝ Y✝ : C<VAR>D : Type u_1<VAR>inst✝⁶ : Category.{?u.241337, u_1} D<VAR>F : C ⥤ D<VAR>inst✝⁵ : HasTerminal C<VAR>inst✝⁴ : HasBinaryProducts C<VAR>inst✝³ : HasTerminal D<VAR>inst✝² : HasBinaryProducts D<VAR>inst✝¹ : PreservesLimit (empty C) F<VAR>inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F<VAR>X Y Z : C<GOAL>F.map (prod.lift (prod.fst ≫ prod.fst) (prod.lift (prod.fst ≫ prod.snd) prod.snd)) = prodComparison F (X ⨯ Y) Z ≫ prod.map (prodComparison F X Y) (𝟙 (F.obj Z)) ≫ prod.lift (prod.fst ≫ prod.fst) (prod.lift (prod.fst ≫ prod.snd) prod.snd ≫ CategoryTheory.inv (prodComparison F Y Z)) ≫ CategoryTheory.inv (prodComparison F X (Y ⨯ Z))
<VAR>C : Type u<VAR>inst✝⁷ : Category.{v, u} C<VAR>X✝ Y✝ : C<VAR>D : Type u_1<VAR>inst✝⁶ : Category.{?u.241337, u_1} D<VAR>F : C ⥤ D<VAR>inst✝⁵ : HasTerminal C<VAR>inst✝⁴ : HasBinaryProducts C<VAR>inst✝³ : HasTerminal D<VAR>inst✝² : HasBinaryProducts D<VAR>inst✝¹ : PreservesLimit (empty C) F<VAR>inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F<VAR>X Y Z : C<GOAL>F.map (prod.lift (prod.fst ≫ prod.fst) (prod.lift (prod.fst ≫ prod.snd) prod.snd)) ≫ prodComparison F X (Y ⨯ Z) = (prodComparison F (X ⨯ Y) Z ≫ prod.map (prodComparison F X Y) (𝟙 (F.obj Z)) ≫ prod.lift (prod.fst ≫ prod.fst) (prod.lift (prod.fst ≫ prod.snd) prod.snd ≫ CategoryTheory.inv (prodComparison F Y Z)) ≫ CategoryTheory.inv (prodComparison F X (Y ⨯ Z))) ≫ prodComparison F X (Y ⨯ Z)
<VAR>C : Type u<VAR>inst✝⁷ : Category.{v, u} C<VAR>X✝ Y✝ : C<VAR>D : Type u_1<VAR>inst✝⁶ : Category.{?u.241337, u_1} D<VAR>F : C ⥤ D<VAR>inst✝⁵ : HasTerminal C<VAR>inst✝⁴ : HasBinaryProducts C<VAR>inst✝³ : HasTerminal D<VAR>inst✝² : HasBinaryProducts D<VAR>inst✝¹ : PreservesLimit (empty C) F<VAR>inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F<VAR>X Y Z : C<GOAL>F.map (prod.lift (prod.fst ≫ prod.fst) (prod.lift (prod.fst ≫ prod.snd) prod.snd)) ≫ prodComparison F X (Y ⨯ Z) = prod.lift (F.map prod.fst ≫ F.map prod.fst) (prodComparison F (X ⨯ Y) Z ≫ prod.map (prodComparison F X Y) (𝟙 (F.obj Z)) ≫ prod.lift (prod.fst ≫ prod.snd) prod.snd ≫ CategoryTheory.inv (prodComparison F Y Z))
<VAR>C : Type u<VAR>inst✝⁷ : Category.{v, u} C<VAR>X Y✝ : C<VAR>D : Type u_1<VAR>inst✝⁶ : Category.{?u.241337, u_1} D<VAR>F : C ⥤ D<VAR>inst✝⁵ : HasTerminal C<VAR>inst✝⁴ : HasBinaryProducts C<VAR>inst✝³ : HasTerminal D<VAR>inst✝² : HasBinaryProducts D<VAR>inst✝¹ : PreservesLimit (empty C) F<VAR>inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F<VAR>Y : C<GOAL>(MonoidalCategory.leftUnitor (F.obj Y)).hom = MonoidalCategory.whiskerRight (asIso (terminalComparison F)).inv (F.obj Y) ≫ (fun X Y => (asIso (prodComparison F X Y)).inv) (𝟙_ C) Y ≫ F.map (MonoidalCategory.leftUnitor Y).hom
<VAR>C : Type u<VAR>inst✝⁷ : Category.{v, u} C<VAR>X Y✝ : C<VAR>D : Type u_1<VAR>inst✝⁶ : Category.{?u.241337, u_1} D<VAR>F : C ⥤ D<VAR>inst✝⁵ : HasTerminal C<VAR>inst✝⁴ : HasBinaryProducts C<VAR>inst✝³ : HasTerminal D<VAR>inst✝² : HasBinaryProducts D<VAR>inst✝¹ : PreservesLimit (empty C) F<VAR>inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F<VAR>Y : C<GOAL>prod.map (terminalComparison F) (𝟙 (F.obj Y)) ≫ (MonoidalCategory.leftUnitor (F.obj Y)).hom = prod.map (terminalComparison F) (𝟙 (F.obj Y)) ≫ MonoidalCategory.whiskerRight (asIso (terminalComparison F)).inv (F.obj Y) ≫ (fun X Y => (asIso (prodComparison F X Y)).inv) (𝟙_ C) Y ≫ F.map (MonoidalCategory.leftUnitor Y).hom
<VAR>C : Type u<VAR>inst✝⁷ : Category.{v, u} C<VAR>X Y✝ : C<VAR>D : Type u_1<VAR>inst✝⁶ : Category.{?u.241337, u_1} D<VAR>F : C ⥤ D<VAR>inst✝⁵ : HasTerminal C<VAR>inst✝⁴ : HasBinaryProducts C<VAR>inst✝³ : HasTerminal D<VAR>inst✝² : HasBinaryProducts D<VAR>inst✝¹ : PreservesLimit (empty C) F<VAR>inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F<VAR>Y : C<GOAL>prod.map (terminalComparison F) (𝟙 (F.obj Y)) ≫ prod.snd = prod.map (terminalComparison F) (𝟙 (F.obj Y)) ≫ prod.map (CategoryTheory.inv (terminalComparison F)) (𝟙 (F.obj Y)) ≫ CategoryTheory.inv (prodComparison F (⊤_ C) Y) ≫ F.map prod.snd
<VAR>C : Type u<VAR>inst✝⁷ : Category.{v, u} C<VAR>X Y✝ : C<VAR>D : Type u_1<VAR>inst✝⁶ : Category.{?u.241337, u_1} D<VAR>F : C ⥤ D<VAR>inst✝⁵ : HasTerminal C<VAR>inst✝⁴ : HasBinaryProducts C<VAR>inst✝³ : HasTerminal D<VAR>inst✝² : HasBinaryProducts D<VAR>inst✝¹ : PreservesLimit (empty C) F<VAR>inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F<VAR>Y : C<GOAL>prodComparison F (⊤_ C) Y ≫ prod.map (terminalComparison F) (𝟙 (F.obj Y)) ≫ prod.snd = F.map prod.snd
<VAR>C : Type u<VAR>inst✝⁷ : Category.{v, u} C<VAR>X✝ Y : C<VAR>D : Type u_1<VAR>inst✝⁶ : Category.{?u.241337, u_1} D<VAR>F : C ⥤ D<VAR>inst✝⁵ : HasTerminal C<VAR>inst✝⁴ : HasBinaryProducts C<VAR>inst✝³ : HasTerminal D<VAR>inst✝² : HasBinaryProducts D<VAR>inst✝¹ : PreservesLimit (empty C) F<VAR>inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F<VAR>X : C<GOAL>(MonoidalCategory.rightUnitor (F.obj X)).hom = MonoidalCategory.whiskerLeft (F.obj X) (asIso (terminalComparison F)).inv ≫ (fun X Y => (asIso (prodComparison F X Y)).inv) X (𝟙_ C) ≫ F.map (MonoidalCategory.rightUnitor X).hom
<VAR>C : Type u<VAR>inst✝⁷ : Category.{v, u} C<VAR>X✝ Y : C<VAR>D : Type u_1<VAR>inst✝⁶ : Category.{?u.241337, u_1} D<VAR>F : C ⥤ D<VAR>inst✝⁵ : HasTerminal C<VAR>inst✝⁴ : HasBinaryProducts C<VAR>inst✝³ : HasTerminal D<VAR>inst✝² : HasBinaryProducts D<VAR>inst✝¹ : PreservesLimit (empty C) F<VAR>inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F<VAR>X : C<GOAL>prod.map (𝟙 (F.obj X)) (terminalComparison F) ≫ (MonoidalCategory.rightUnitor (F.obj X)).hom = prod.map (𝟙 (F.obj X)) (terminalComparison F) ≫ MonoidalCategory.whiskerLeft (F.obj X) (asIso (terminalComparison F)).inv ≫ (fun X Y => (asIso (prodComparison F X Y)).inv) X (𝟙_ C) ≫ F.map (MonoidalCategory.rightUnitor X).hom
<VAR>C : Type u<VAR>inst✝⁷ : Category.{v, u} C<VAR>X✝ Y : C<VAR>D : Type u_1<VAR>inst✝⁶ : Category.{?u.241337, u_1} D<VAR>F : C ⥤ D<VAR>inst✝⁵ : HasTerminal C<VAR>inst✝⁴ : HasBinaryProducts C<VAR>inst✝³ : HasTerminal D<VAR>inst✝² : HasBinaryProducts D<VAR>inst✝¹ : PreservesLimit (empty C) F<VAR>inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F<VAR>X : C<GOAL>prod.map (𝟙 (F.obj X)) (terminalComparison F) ≫ prod.fst = prod.map (𝟙 (F.obj X)) (terminalComparison F) ≫ prod.map (𝟙 (F.obj X)) (CategoryTheory.inv (terminalComparison F)) ≫ CategoryTheory.inv (prodComparison F X (⊤_ C)) ≫ F.map prod.fst
<VAR>C : Type u<VAR>inst✝⁷ : Category.{v, u} C<VAR>X✝ Y : C<VAR>D : Type u_1<VAR>inst✝⁶ : Category.{?u.241337, u_1} D<VAR>F : C ⥤ D<VAR>inst✝⁵ : HasTerminal C<VAR>inst✝⁴ : HasBinaryProducts C<VAR>inst✝³ : HasTerminal D<VAR>inst✝² : HasBinaryProducts D<VAR>inst✝¹ : PreservesLimit (empty C) F<VAR>inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F<VAR>X : C<GOAL>prodComparison F X (⊤_ C) ≫ prod.map (𝟙 (F.obj X)) (terminalComparison F) ≫ prod.fst = F.map prod.fst
<VAR>α : Type u_1<VAR>M N : Matroid α<VAR>h : Disjoint M.E N.E<VAR>I : Set α<GOAL>(M.disjointSum N h).Indep I ↔ M.Indep (I ∩ M.E) ∧ N.Indep (I ∩ N.E) ∧ I ⊆ M.E ∪ N.E
<VAR>R : Type u<VAR>inst✝ : Ring R<VAR>n : ℕ<GOAL>descPochhammer ℤ n = (ascPochhammer ℤ n).comp (X - ↑n + 1)
<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>a + (b - a) = b
<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>a + (b - a) ≤ b
<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 c✝ d c : α<VAR>h : a ≤ a + c<GOAL>a + (a + c - a) ≤ a + c
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>inst✝⁴ : MulOneClass M<VAR>inst✝³ : MulOneClass N<VAR>inst✝² : MulOneClass P<VAR>S : Submonoid M<VAR>A : Type u_4<VAR>inst✝¹ : SetLike A M<VAR>hA : SubmonoidClass A M<VAR>S' : A<VAR>F : Type u_5<VAR>inst✝ : FunLike F M N<VAR>mc : MonoidHomClass F M N<VAR>x : M<GOAL>x ∈ mker (inl M N) ↔ x ∈ ⊥
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>K : Type u_3<VAR>inst✝² : Field K<VAR>inst✝¹ : Module K M<VAR>f g : End K M<VAR>inst✝ : FiniteDimensional K M<VAR>hf : f.IsSemisimple<VAR>a : End K M<VAR>ha : a ∈ Algebra.adjoin K {f}<GOAL>a.IsSemisimple
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>K : Type u_3<VAR>inst✝² : Field K<VAR>inst✝¹ : Module K M<VAR>f g : End K M<VAR>inst✝ : FiniteDimensional K M<VAR>hf : f.IsSemisimple<VAR>a : End K M<VAR>ha : a ∈ (aeval f).range<GOAL>a.IsSemisimple
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>K : Type u_3<VAR>inst✝² : Field K<VAR>inst✝¹ : Module K M<VAR>f g : End K M<VAR>inst✝ : FiniteDimensional K M<VAR>hf : f.IsSemisimple<VAR>p : K[X]<GOAL>((aeval f).toRingHom p).IsSemisimple
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>R : Type u_4<VAR>inst✝ : Ring α<VAR>a b : α<VAR>n : ℕ<VAR>ha : Odd a<VAR>hb : Odd b<GOAL>Even (a - b)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>R : Type u_4<VAR>inst✝ : Ring α<VAR>a b : α<VAR>n : ℕ<VAR>ha : Odd a<VAR>hb : Odd b<GOAL>Even (a + -b)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>I : Type u_3<VAR>J : Type u_4<VAR>inst✝⁷ : Category.{u_6, u_1} C<VAR>inst✝⁶ : Category.{u_5, u_2} D<VAR>inst✝⁵ : Zero I<VAR>inst✝⁴ : DecidableEq I<VAR>inst✝³ : HasInitial C<VAR>F : D ⥤ C ⥤ D<VAR>Y : C<VAR>e : F.flip.obj Y ≅ 𝟭 D<VAR>inst✝² : (X : D) → PreservesColimit (Functor.empty C) (F.obj X)<VAR>p : J × I → J<VAR>hp : ∀ (j : J), p (j, 0) = j<VAR>X X' : GradedObject J D<VAR>φ : X ⟶ X'<VAR>inst✝¹ : (((mapBifunctor F J I).obj X).obj ((single₀ I).obj Y)).HasMap p<VAR>inst✝ : (((mapBifunctor F J I).obj X').obj ((single₀ I).obj Y)).HasMap p<VAR>j : J<GOAL>ιMapBifunctorMapObj F p X ((single₀ I).obj Y) j 0 j ⋯ ≫ (CofanMapObjFun.iso (mapBifunctorRightUnitorCofanIsColimit F Y e p hp X j)).inv = (F.obj (X j)).map (singleObjApplyIso 0 Y).hom ≫ e.hom.app (X j)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>I : Type u_3<VAR>J : Type u_4<VAR>inst✝⁷ : Category.{u_6, u_1} C<VAR>inst✝⁶ : Category.{u_5, u_2} D<VAR>inst✝⁵ : Zero I<VAR>inst✝⁴ : DecidableEq I<VAR>inst✝³ : HasInitial C<VAR>F : D ⥤ C ⥤ D<VAR>Y : C<VAR>e : F.flip.obj Y ≅ 𝟭 D<VAR>inst✝² : (X : D) → PreservesColimit (Functor.empty C) (F.obj X)<VAR>p : J × I → J<VAR>hp : ∀ (j : J), p (j, 0) = j<VAR>X X' : GradedObject J D<VAR>φ : X ⟶ X'<VAR>inst✝¹ : (((mapBifunctor F J I).obj X).obj ((single₀ I).obj Y)).HasMap p<VAR>inst✝ : (((mapBifunctor F J I).obj X').obj ((single₀ I).obj Y)).HasMap p<VAR>j : J<GOAL>Cofan.inj (mapBifunctorRightUnitorCofan F Y e p hp X j) ⟨(j, 0), ⋯⟩ = (F.obj (X j)).map (singleObjApplyIso 0 Y).hom ≫ e.hom.app (X j)
<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>hT : DominatedFinMeasAdditive μ T C<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>x : E<GOAL>setToFun μ T hT (s.indicator fun x_1 => x) = (T s) x
<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>hT : DominatedFinMeasAdditive μ T C<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>x : E<GOAL>setToFun μ T hT ↑↑(indicatorConstLp 1 hs hμs x) = (T s) x
<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>hT : DominatedFinMeasAdditive μ T C<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>x : E<GOAL>(L1.setToL1 hT) (indicatorConstLp 1 hs hμs x) = (T s) x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>inst✝⁷ : OrderedSemiring 𝕜<VAR>inst✝⁶ : AddCommMonoid E<VAR>inst✝⁵ : AddCommMonoid F<VAR>inst✝⁴ : Module 𝕜 E<VAR>inst✝³ : Module 𝕜 F<VAR>s : Set E<VAR>x✝ : E<VAR>inst✝² : OrderedCancelAddCommMonoid β<VAR>inst✝¹ : Module 𝕜 β<VAR>inst✝ : OrderedSMul 𝕜 β<VAR>r x : β<VAR>hx : x ∈ Iio r<VAR>y : β<VAR>hy : y ∈ Iio r<VAR>a b : 𝕜<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>hab : a + b = 1<VAR>ha' : 0 < a<GOAL>a • x + b • y ∈ Iio r
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>inst✝⁷ : OrderedSemiring 𝕜<VAR>inst✝⁶ : AddCommMonoid E<VAR>inst✝⁵ : AddCommMonoid F<VAR>inst✝⁴ : Module 𝕜 E<VAR>inst✝³ : Module 𝕜 F<VAR>s : Set E<VAR>x✝ : E<VAR>inst✝² : OrderedCancelAddCommMonoid β<VAR>inst✝¹ : Module 𝕜 β<VAR>inst✝ : OrderedSMul 𝕜 β<VAR>r x : β<VAR>hx : x < r<VAR>y : β<VAR>hy : y < r<VAR>a b : 𝕜<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>hab : a + b = 1<VAR>ha' : 0 < a<GOAL>a • x + b • y ∈ Iio r
<VAR>α : Type u_1<VAR>inst✝³ : AddMonoidWithOne α<VAR>inst✝² : Preorder α<VAR>inst✝¹ : ZeroLEOneClass α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<GOAL>0 ≤ 4
<VAR>α : Type u_1<VAR>inst✝³ : AddMonoidWithOne α<VAR>inst✝² : Preorder α<VAR>inst✝¹ : ZeroLEOneClass α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<GOAL>0 ≤ 3 + 1
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : MulOneClass M<VAR>inst✝² : MulOneClass N<VAR>inst✝¹ : MulOneClass P<VAR>S : Submonoid M<VAR>A : Type u_4<VAR>inst✝ : SetLike A M<VAR>hA : SubmonoidClass A M<VAR>S' : A<VAR>s : Set M<VAR>x✝¹ : { x // x ∈ ↑(closure s) }<VAR>x : M<VAR>hx : x ∈ ↑(closure s)<VAR>x✝ : ⟨x, hx⟩ ∈ ⊤<GOAL>⟨x, hx⟩ ∈ closure (Subtype.val ⁻¹' s)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : MulOneClass M<VAR>inst✝² : MulOneClass N<VAR>inst✝¹ : MulOneClass P<VAR>S : Submonoid M<VAR>A : Type u_4<VAR>inst✝ : SetLike A M<VAR>hA : SubmonoidClass A M<VAR>S' : A<VAR>s : Set M<VAR>x✝¹ : { x // x ∈ ↑(closure s) }<VAR>x : M<VAR>hx : x ∈ ↑(closure s)<VAR>x✝ : ⟨x, hx⟩ ∈ ⊤<GOAL>(fun y hy => ⟨y, hy⟩ ∈ closure (Subtype.val ⁻¹' s)) 1 ⋯
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : MulOneClass M<VAR>inst✝² : MulOneClass N<VAR>inst✝¹ : MulOneClass P<VAR>S : Submonoid M<VAR>A : Type u_4<VAR>inst✝ : SetLike A M<VAR>hA : SubmonoidClass A M<VAR>S' : A<VAR>s : Set M<VAR>x✝¹ : { x // x ∈ ↑(closure s) }<VAR>x : M<VAR>hx : x ∈ ↑(closure s)<VAR>x✝ : ⟨x, hx⟩ ∈ ⊤<VAR>g₁ : M<VAR>g₂ : g₁ ∈ closure s<VAR>hg₁ : M<VAR>hg₂ : hg₁ ∈ closure s<GOAL>(fun y hy => ⟨y, hy⟩ ∈ closure (Subtype.val ⁻¹' s)) g₁ g₂ → (fun y hy => ⟨y, hy⟩ ∈ closure (Subtype.val ⁻¹' s)) hg₁ hg₂ → (fun y hy => ⟨y, hy⟩ ∈ closure (Subtype.val ⁻¹' s)) (g₁ * hg₁) ⋯
<VAR>α✝ : Type ua<VAR>β✝ : Type ub<VAR>γ✝ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>uγ : UniformSpace γ<VAR>f : α → β<VAR>g : β → γ<GOAL>𝓤 α = 𝓤 α
<VAR>α : Type u_1<VAR>c : Set (Set α)<VAR>hu : ⋃₀ c = Set.univ<VAR>H : c.PairwiseDisjoint id<VAR>a : α<GOAL>a ∈ Set.univ