mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.Functor.toCostructuredArrow_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (G : CategoryTheory.Functor E C)
  (F : CategoryTheory.Functor C D) (X : D) (f : (Y : E) → F.obj (G.obj Y) ⟶ X)
  (h : ∀ {Y Z : E} (g : Y ⟶ Z), CategoryTheory.CategoryStruct.comp (F.map (G.map g)) (f Z) = f Y) {X_1 Y : E}
  (g : X_1 ⟶ Y), (G.toCostructuredArrow F X f h).map g = CategoryTheory.CostructuredArrow.homMk (G.map g) ⋯
-- Mathlib.LinearAlgebra.Multilinear.Basic
/-- Constructor for `MultilinearMap R M₁ M₂` when the
index type `ι` is already endowed with a `DecidableEq` instance.  -/
MultilinearMap.mk' : {R : Type uR} →
  {ι : Type uι} →
    {M₁ : ι → Type v₁} →
      {M₂ : Type v₂} →
        [inst : Semiring R] →
          [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] →
            [inst_2 : AddCommMonoid M₂] →
              [inst_3 : (i : ι) → Module R (M₁ i)] →
                [inst_4 : Module R M₂] →
                  [inst_5 : DecidableEq ι] →
                    (f : ((i : ι) → M₁ i) → M₂) →
                      autoParam
                          (∀ (m : (i : ι) → M₁ i) (i : ι) (x y : M₁ i),
                            f (Function.update m i (x + y)) = f (Function.update m i x) + f (Function.update m i y))
                          MultilinearMap.mk'._auto_1 →
                        autoParam
                            (∀ (m : (i : ι) → M₁ i) (i : ι) (c : R) (x : M₁ i),
                              f (Function.update m i (c • x)) = c • f (Function.update m i x))
                            MultilinearMap.mk'._auto_3 →
                          MultilinearMap R M₁ M₂
-- Lean.Server.FileWorker.SemanticHighlighting
/-- The other tokens whose intervals include the current token's start position.

Sorted by end position (increasing), because we've already passed their start positions. Only
their end positions may contribute new token boundaries.
 -/
_private.Lean.Server.FileWorker.SemanticHighlighting.0.Lean.Server.FileWorker.HandleOverlapState.surrounding : Lean.Server.FileWorker.HandleOverlapState✝ → List Lean.Server.FileWorker.AbsoluteLspSemanticToken
-- Mathlib.Probability.Independence.CharacteristicFunction
/-- Two random variables are independent if and only if their joint characteristic function is equal
to the product of the characteristic functions. This is the version for Hilbert spaces, see
`indepFun_iff_charFunDual_prod` for the Banach space version.  -/
ProbabilityTheory.indepFun_iff_charFun_prod : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {E : Type u_2}
  {F : Type u_3} {mE : MeasurableSpace E} [inst : NormedAddCommGroup E] [BorelSpace E] [SecondCountableTopology E]
  {mF : MeasurableSpace F} [inst_3 : NormedAddCommGroup F] [CompleteSpace F] [BorelSpace F] [SecondCountableTopology F]
  {X : Ω → E} {Y : Ω → F} [inst_7 : InnerProductSpace ℝ E] [inst_8 : InnerProductSpace ℝ F] [CompleteSpace E],
  AEMeasurable X P →
    AEMeasurable Y P →
      (ProbabilityTheory.IndepFun X Y P ↔
        ∀ (t : WithLp 2 (E × F)),
          MeasureTheory.charFun (MeasureTheory.Measure.map (fun ω => WithLp.toLp 2 (X ω, Y ω)) P) t =
            MeasureTheory.charFun (MeasureTheory.Measure.map X P) t.ofLp.1 *
              MeasureTheory.charFun (MeasureTheory.Measure.map Y P) t.ofLp.2)
-- Mathlib.Data.Set.Restrict
/-- **Alias** of `Set.domRestrict₂_comp_domRestrict₂`. -/
Set.restrict₂_comp_restrict₂ : ∀ {α : Type u_1} {π : α → Type u_6} {s t u : Set α} (hst : s ⊆ t) (htu : t ⊆ u),
  Set.domRestrict₂ hst ∘ Set.domRestrict₂ htu = Set.domRestrict₂ ⋯
-- Init.Data.List.Nat.Prod
List.prod_eq_foldl_nat : ∀ {xs : List ℕ}, xs.prod = List.foldl (fun x1 x2 => x1 * x2) 1 xs
-- Mathlib.Order.Filter.ENNReal
NNReal.isCoboundedUnder_le_toReal : ∀ {ι : Type u_1} {f : Filter ι} {u : ι → NNReal} [f.NeBot],
  (Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f fun i => ↑(u i)) ↔
    Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f u
-- Init.Data.Int.Compare
Int.compare_swap : ∀ (a b : ℤ), (compare a b).swap = compare b a
-- Mathlib.Control.Monad.Cont
_private.Mathlib.Control.Monad.Cont.0.ExceptT.run_bind.match_1.eq_2 : ∀ {ε α : Type u_1} (motive : Except ε α → Sort u_2) (e : ε) (h_1 : (x : α) → motive (Except.ok x))
  (h_2 : (e : ε) → motive (Except.error e)),
  (match Except.error e with
    | Except.ok x => h_1 x
    | Except.error e => h_2 e) =
    h_2 e
-- Aesop.Tree.Data
Aesop.GoalUnsafe.brecOn_10.eq : ∀ {motive_1 : Aesop.GoalUnsafe → Sort u} {motive_2 : Aesop.MVarClusterUnsafe → Sort u}
  {motive_3 : Aesop.RappUnsafe → Sort u} {motive_4 : Aesop.GoalData Aesop.RappUnsafe Aesop.MVarClusterUnsafe → Sort u}
  {motive_5 : Aesop.MVarClusterData Aesop.GoalUnsafe Aesop.RappUnsafe → Sort u}
  {motive_6 : Aesop.RappData Aesop.GoalUnsafe Aesop.MVarClusterUnsafe → Sort u}
  {motive_7 : Array (IO.Ref Aesop.RappUnsafe) → Sort u} {motive_8 : Option (IO.Ref Aesop.RappUnsafe) → Sort u}
  {motive_9 : Array (IO.Ref Aesop.GoalUnsafe) → Sort u} {motive_10 : Array (IO.Ref Aesop.MVarClusterUnsafe) → Sort u}
  {motive_11 : List (IO.Ref Aesop.RappUnsafe) → Sort u} {motive_12 : List (IO.Ref Aesop.GoalUnsafe) → Sort u}
  {motive_13 : List (IO.Ref Aesop.MVarClusterUnsafe) → Sort u} (t : List (IO.Ref Aesop.MVarClusterUnsafe))
  (F_1 : (t : Aesop.GoalUnsafe) → t.below → motive_1 t) (F_2 : (t : Aesop.MVarClusterUnsafe) → t.below → motive_2 t)
  (F_3 : (t : Aesop.RappUnsafe) → t.below → motive_3 t)
  (F_4 : (t : Aesop.GoalData Aesop.RappUnsafe Aesop.MVarClusterUnsafe) → Aesop.GoalUnsafe.below_1 t → motive_4 t)
  (F_5 : (t : Aesop.MVarClusterData Aesop.GoalUnsafe Aesop.RappUnsafe) → Aesop.GoalUnsafe.below_2 t → motive_5 t)
  (F_6 : (t : Aesop.RappData Aesop.GoalUnsafe Aesop.MVarClusterUnsafe) → Aesop.GoalUnsafe.below_3 t → motive_6 t)
  (F_7 : (t : Array (IO.Ref Aesop.RappUnsafe)) → Aesop.GoalUnsafe.below_4 t → motive_7 t)
  (F_8 : (t : Option (IO.Ref Aesop.RappUnsafe)) → Aesop.GoalUnsafe.below_5 t → motive_8 t)
  (F_9 : (t : Array (IO.Ref Aesop.GoalUnsafe)) → Aesop.GoalUnsafe.below_6 t → motive_9 t)
  (F_10 : (t : Array (IO.Ref Aesop.MVarClusterUnsafe)) → Aesop.GoalUnsafe.below_7 t → motive_10 t)
  (F_11 : (t : List (IO.Ref Aesop.RappUnsafe)) → Aesop.GoalUnsafe.below_8 t → motive_11 t)
  (F_12 : (t : List (IO.Ref Aesop.GoalUnsafe)) → Aesop.GoalUnsafe.below_9 t → motive_12 t)
  (F_13 : (t : List (IO.Ref Aesop.MVarClusterUnsafe)) → Aesop.GoalUnsafe.below_10 t → motive_13 t),
  Aesop.GoalUnsafe.brecOn_10 t F_1 F_2 F_3 F_4 F_5 F_6 F_7 F_8 F_9 F_10 F_11 F_12 F_13 =
    F_13 t (Aesop.GoalUnsafe.brecOn_10.go t F_1 F_2 F_3 F_4 F_5 F_6 F_7 F_8 F_9 F_10 F_11 F_12 F_13).2
-- Mathlib.MeasureTheory.Integral.Lebesgue.Map
MeasureTheory.lintegral_map : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {f : β → ENNReal} {g : α → β},
  Measurable f → Measurable g → ∫⁻ (a : β), f a ∂MeasureTheory.Measure.map g μ = ∫⁻ (a : α), f (g a) ∂μ
-- Lean.Elab.Do.Basic
Lean.Elab.Do.Context.mk.inj : ∀ {monadInfo : Lean.Elab.Do.MonadInfo} {mutVars : Array Lean.Elab.Do.MutVar}
  {mutVarDefs : Std.HashMap Lean.Name Lean.Elab.Do.MutVar} {doBlockResultType : Lean.Expr}
  {contInfo : Lean.Elab.Do.ContInfoRef} {deadCode : Lean.Elab.Do.CodeLiveness} {ops : Lean.Elab.Do.DoOpsRef}
  {monadInfo_1 : Lean.Elab.Do.MonadInfo} {mutVars_1 : Array Lean.Elab.Do.MutVar}
  {mutVarDefs_1 : Std.HashMap Lean.Name Lean.Elab.Do.MutVar} {doBlockResultType_1 : Lean.Expr}
  {contInfo_1 : Lean.Elab.Do.ContInfoRef} {deadCode_1 : Lean.Elab.Do.CodeLiveness} {ops_1 : Lean.Elab.Do.DoOpsRef},
  { monadInfo := monadInfo, mutVars := mutVars, mutVarDefs := mutVarDefs, doBlockResultType := doBlockResultType,
        contInfo := contInfo, deadCode := deadCode, ops := ops } =
      { monadInfo := monadInfo_1, mutVars := mutVars_1, mutVarDefs := mutVarDefs_1,
        doBlockResultType := doBlockResultType_1, contInfo := contInfo_1, deadCode := deadCode_1, ops := ops_1 } →
    monadInfo = monadInfo_1 ∧
      mutVars = mutVars_1 ∧
        mutVarDefs = mutVarDefs_1 ∧
          doBlockResultType = doBlockResultType_1 ∧ contInfo = contInfo_1 ∧ deadCode = deadCode_1 ∧ ops = ops_1
-- Mathlib.Order.Hom.Bounded
BotHomClass.mk : ∀ {F : Type u_6} {α : outParam (Type u_7)} {β : outParam (Type u_8)} [inst : Bot α] [inst_1 : Bot β]
  [inst_2 : FunLike F α β], (∀ (f : F), f ⊥ = ⊥) → BotHomClass F α β
-- Mathlib.RingTheory.Polynomial.Content
Polynomial.content_monomial : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : NormalizedGCDMonoid R] {r : R} {k : ℕ},
  ((Polynomial.monomial k) r).content = normalize r
-- Std.Tactic.BVDecide.Bitblast.BoolExpr.Basic
_private.Std.Tactic.BVDecide.Bitblast.BoolExpr.Basic.0.Std.Tactic.BVDecide.Gate.toString.match_1.eq_4 : ∀ (motive : Std.Tactic.BVDecide.Gate → Sort u_1) (h_1 : Unit → motive Std.Tactic.BVDecide.Gate.and)
  (h_2 : Unit → motive Std.Tactic.BVDecide.Gate.xor) (h_3 : Unit → motive Std.Tactic.BVDecide.Gate.beq)
  (h_4 : Unit → motive Std.Tactic.BVDecide.Gate.or),
  (match Std.Tactic.BVDecide.Gate.or with
    | Std.Tactic.BVDecide.Gate.and => h_1 ()
    | Std.Tactic.BVDecide.Gate.xor => h_2 ()
    | Std.Tactic.BVDecide.Gate.beq => h_3 ()
    | Std.Tactic.BVDecide.Gate.or => h_4 ()) =
    h_4 ()
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
SheafOfModules.LocalGeneratorsData.mk.inj : ∀ {C : Type u'} {inst : CategoryTheory.Category.{v', u'} C} {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} {M : SheafOfModules R}
  {inst_1 : ∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat}
  {inst_2 : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat} {I : Type w} {X : I → C}
  {coversTop : J.CoversTop X} {generators : (i : I) → (M.over (X i)).GeneratingSections} {I_1 : Type w} {X_1 : I_1 → C}
  {coversTop_1 : J.CoversTop X_1} {generators_1 : (i : I_1) → (M.over (X_1 i)).GeneratingSections},
  { I := I, X := X, coversTop := coversTop, generators := generators } =
      { I := I_1, X := X_1, coversTop := coversTop_1, generators := generators_1 } →
    I = I_1 ∧ X ≍ X_1 ∧ generators ≍ generators_1
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.size_map : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} {γ : α → Type w} [EquivBEq α]
  [LawfulHashable α] {f : (a : α) → β a → γ a}, (Std.DHashMap.map f m).size = m.size
-- Mathlib.Topology.Algebra.Module.ClosedSubmodule
ClosedSubmodule.instCompleteSemilatticeSup : {R : Type u_2} →
  {N : Type u_4} →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid N] →
        [inst_2 : TopologicalSpace N] →
          [inst_3 : Module R N] →
            [ContinuousAdd N] → [ContinuousConstSMul R N] → CompleteSemilatticeSup (ClosedSubmodule R N)
-- Mathlib.Data.Vector.Basic
List.Vector.map₂_nil : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ),
  List.Vector.map₂ f List.Vector.nil List.Vector.nil = List.Vector.nil
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.CooperSplitPred.c₃? : Lean.Meta.Grind.Arith.Cutsat.CooperSplitPred → Option Lean.Meta.Grind.Arith.Cutsat.DvdCnstr
-- Mathlib.CategoryTheory.Localization.Equivalence
CategoryTheory.Localization.equivalence_counitIso_app : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_4} {D₂ : Type u_5} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_4, u_4} D₁]
  [inst_3 : CategoryTheory.Category.{v_5, u_5} D₂] (L₁ : CategoryTheory.Functor C₁ D₁)
  (W₁ : CategoryTheory.MorphismProperty C₁) [inst_4 : L₁.IsLocalization W₁] (L₂ : CategoryTheory.Functor C₂ D₂)
  (W₂ : CategoryTheory.MorphismProperty C₂) [inst_5 : L₂.IsLocalization W₂] (G : CategoryTheory.Functor C₁ D₂)
  (G' : CategoryTheory.Functor D₁ D₂) [inst_6 : CategoryTheory.Localization.Lifting L₁ W₁ G G']
  (F : CategoryTheory.Functor C₂ D₁) (F' : CategoryTheory.Functor D₂ D₁)
  [inst_7 : CategoryTheory.Localization.Lifting L₂ W₂ F F'] (α : G.comp F' ≅ L₁) (β : F.comp G' ≅ L₂) (X : C₂),
  (CategoryTheory.Localization.equivalence L₁ W₁ L₂ W₂ G G' F F' α β).counitIso.app (L₂.obj X) =
    (CategoryTheory.Localization.Lifting.iso L₂ W₂ (F.comp G') (F'.comp G')).app X ≪≫ β.app X
-- Mathlib.MeasureTheory.Measure.Tight
/-- In a complete second-countable pseudo-metric space, finite measures are tight.  -/
MeasureTheory.isTightMeasureSet_singleton : ∀ {α : Type u_3} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α]
  [TopologicalSpace.IsCompletelyPseudoMetrizableSpace α] [SecondCountableTopology α] [BorelSpace α]
  {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ], MeasureTheory.IsTightMeasureSet {μ}
-- Init.Data.Range.Polymorphic.UpwardEnumerable
Std.PRange.LinearlyUpwardEnumerable.mk : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α],
  (∀ (a b : α), Std.PRange.succ? a = Std.PRange.succ? b → a = b) → Std.PRange.LinearlyUpwardEnumerable α
-- Lean.Elab.ParseImportsFast
Lean.ParseImports.keywordCore : String → Lean.ParseImports.Parser → Lean.ParseImports.Parser → Lean.ParseImports.Parser
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.getD_ofList_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} [inst : Std.TransCmp cmp] [inst_1 : BEq α] [Std.LawfulBEqCmp cmp]
  {l : List (α × β)} {k : α} {fallback : β},
  (List.map Prod.fst l).contains k = false →
    Std.ExtDTreeMap.Const.getD (Std.ExtDTreeMap.Const.ofList l cmp) k fallback = fallback
-- Lean.Elab.MutualDef
/-- Expression used to replace occurrences of the let-rec `FVarId`.  -/
Lean.Elab.Term.MutualClosure.LetRecClosure.closed : Lean.Elab.Term.MutualClosure.LetRecClosure → Lean.Expr
-- Mathlib.Topology.Algebra.Algebra
ContinuousAlgHom.map_sum : ∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u_2} [inst_1 : Semiring A] [inst_2 : TopologicalSpace A]
  {B : Type u_3} [inst_3 : Semiring B] [inst_4 : TopologicalSpace B] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  {ι : Type u_4} (f : A →A[R] B) (s : Finset ι) (g : ι → A), f (∑ i ∈ s, g i) = ∑ i ∈ s, f (g i)
-- Init.Data.Int.Order
_private.Init.Data.Int.Order.0.Int.add.match_1.eq_2 : ∀ (motive : ℤ → ℤ → Sort u_1) (m n : ℕ) (h_1 : (m n : ℕ) → motive (Int.ofNat m) (Int.ofNat n))
  (h_2 : (m n : ℕ) → motive (Int.ofNat m) (Int.negSucc n)) (h_3 : (m n : ℕ) → motive (Int.negSucc m) (Int.ofNat n))
  (h_4 : (m n : ℕ) → motive (Int.negSucc m) (Int.negSucc n)),
  (match Int.ofNat m, Int.negSucc n with
    | Int.ofNat m, Int.ofNat n => h_1 m n
    | Int.ofNat m, Int.negSucc n => h_2 m n
    | Int.negSucc m, Int.ofNat n => h_3 m n
    | Int.negSucc m, Int.negSucc n => h_4 m n) =
    h_2 m n
-- Mathlib.Geometry.Diffeology.Basic
/-- The D-topology consists of exactly those sets whose preimages under plots are all open.  -/
DiffeologicalSpace.isOpen_iff_preimages_plots : ∀ {X : Type u_1} [self : DiffeologicalSpace X] {u : Set X},
  TopologicalSpace.IsOpen u ↔ ∀ {n : ℕ}, ∀ p ∈ DiffeologicalSpace.plots n, IsOpen (p ⁻¹' u)
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
MonoidAlgebra.range_map : ∀ {R : Type u_3} {S : Type u_4} {M : Type u_6} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+ S),
  Set.range (MonoidAlgebra.map f) = {x | ∀ (i : M), x.coeff i ∈ Set.range ⇑f}
-- Mathlib.Data.ENNReal.Operations
ENNReal.mul_left_strictMono : ∀ {a : ENNReal}, a ≠ 0 → a ≠ ⊤ → StrictMono fun x => x * a
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKeyD_filter_containsKey_of_containsKey_eq_false_left : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l₁ l₂ : List ((a : α) × β a)} {k fallback : α},
  Std.Internal.List.DistinctKeys l₁ →
    Std.Internal.List.containsKey k l₁ = false →
      Std.Internal.List.getKeyD k (List.filter (fun p => Std.Internal.List.containsKey p.fst l₂) l₁) fallback = fallback
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.HomEquiv.ρ_naturality : ∀ {C : Type u} {X Y : CategoryTheory.FreeMonoidalCategory C} (f : X.Hom Y),
  CategoryTheory.FreeMonoidalCategory.HomEquiv
    ((f.whiskerRight CategoryTheory.FreeMonoidalCategory.unit).comp (CategoryTheory.FreeMonoidalCategory.Hom.ρ_hom Y))
    ((CategoryTheory.FreeMonoidalCategory.Hom.ρ_hom X).comp f)
-- Mathlib.FieldTheory.PurelyInseparable.Basic
/-- If a subalgebra of `E / F` is both purely inseparable and separable, then it is equal
to `F`.  -/
Subalgebra.eq_bot_of_isPurelyInseparable_of_isSeparable : ∀ {F : Type u_1} {E : Type u_2} [inst : CommRing F] [inst_1 : Ring E] [inst_2 : Algebra F E] (L : Subalgebra F E)
  [IsPurelyInseparable F ↥L] [Algebra.IsSeparable F ↥L], L = ⊥
-- Mathlib.Algebra.Module.ZLattice.Summable
ZLattice.abs_repr_le : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  {L : Submodule ℤ E} [inst_3 : DiscreteTopology ↥L] {ι : Type u_3} (b : Module.Basis ι ℤ ↥L) (x : ↥L) (i : ι),
  ↑|(b.repr x) i| ≤ (ZLattice.normBound b)⁻¹ * ‖x‖
-- Mathlib.Algebra.Order.GroupWithZero.Basic
mul_le_one₀ : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] [inst_1 : Preorder M₀] {a b : M₀} [MulPosMono M₀],
  a ≤ 1 → 0 ≤ b → b ≤ 1 → a * b ≤ 1
-- Mathlib.MeasureTheory.Integral.IntegrableOn
MeasureTheory.IntegrableOn.inter_of_restrict : ∀ {α : Type u_1} {ε : Type u_3} {mα : MeasurableSpace α} {f : α → ε} {s t : Set α} {μ : MeasureTheory.Measure α}
  [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε],
  MeasureTheory.IntegrableOn f s (μ.restrict t) → MeasureTheory.IntegrableOn f (s ∩ t) μ
-- Batteries.Util.ProofWanted
/-- File-local registry of `instance_wanted` declarations. Each registered name is
automatically included as an instance parameter binder in every later wanted declaration's
signature, so Lean's typeclass synth can pick it up without an explicit `❰…❱` reference. The
extension is non-persistent across imports (the placeholder defs are `private` and don't
propagate).  -/
_private.Batteries.Util.ProofWanted.0.wantedInstancesExt : Lean.SimplePersistentEnvExtension Lean.Name (Array Lean.Name)
-- Mathlib.GroupTheory.IsPerfect
Subgroup.isPerfect_iff : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G}, Group.IsPerfect ↥H ↔ ⁅H, H⁆ = H
-- Mathlib.CategoryTheory.Sigma.Basic
/-- If `q` when restricted to each subcategory `C i` agrees with `F i`, then `q` is isomorphic to
`desc F`.
 -/
CategoryTheory.Sigma.descUniq : {I : Type w₁} →
  {C : I → Type u₁} →
    [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] →
      {D : Type u₂} →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
          (F : (i : I) → CategoryTheory.Functor (C i) D) →
            (q : CategoryTheory.Functor ((i : I) × C i) D) →
              ((i : I) → (CategoryTheory.Sigma.incl i).comp q ≅ F i) → (q ≅ CategoryTheory.Sigma.desc F)
-- Mathlib.Algebra.Group.Subgroup.Even
AddSubgroup.even.eq_1 : ∀ (G : Type u_1) [inst : AddCommGroup G], AddSubgroup.even G = { toAddSubmonoid := AddSubmonoid.even G, neg_mem' := ⋯ }
-- Mathlib.Order.Hom.CompleteLattice
sInfHom.cancel_right : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : InfSet α] [inst_1 : InfSet β] [inst_2 : InfSet γ]
  {g₁ g₂ : sInfHom β γ} {f : sInfHom α β}, Function.Surjective ⇑f → (g₁.comp f = g₂.comp f ↔ g₁ = g₂)
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.lift_comp_of' : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] {N : Type u_4} [inst_1 : Monoid N]
  (f : Monoid.CoprodI M →* N), (Monoid.CoprodI.lift fun i => f.comp Monoid.CoprodI.of) = f
-- Std.Time.Format.Modifier
Std.Time.instInhabitedDayPeriod : Inhabited Std.Time.DayPeriod
-- Mathlib.CategoryTheory.Limits.Types.ColimitType
/-- The colimit type of a functor `F : J ⥤ Type w₀`. (It may not
be in `Type w₀`.)  -/
CategoryTheory.Functor.ColimitType : {J : Type u} → [inst : CategoryTheory.Category.{v, u} J] → CategoryTheory.Functor J (Type w₀) → Type (max u w₀)
-- Mathlib.Analysis.Convex.Function
/-- Strict convexity of functions  -/
StrictConvexOn : (𝕜 : Type u_1) →
  {E : Type u_2} →
    {β : Type u_5} →
      [Semiring 𝕜] →
        [PartialOrder 𝕜] →
          [AddCommMonoid E] → [AddCommMonoid β] → [PartialOrder β] → [SMul 𝕜 E] → [SMul 𝕜 β] → Set E → (E → β) → Prop
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
/-- The type of objects for the diagram indexing a wide (co)equalizer.  -/
CategoryTheory.Limits.WalkingParallelFamily : Type w → Type w
-- Aesop.Tree.Data
Aesop.instInhabitedNodeState.default : Aesop.NodeState
-- Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
/-- When j and j - 1728 are both units,
`Y² + (j - 1728)XY = X³ - 36(j - 1728)³X - (j - 1728)⁵` is an elliptic curve.
It is of j-invariant j (see `WeierstrassCurve.ofJNe0Or1728_j`).  -/
WeierstrassCurve.instIsEllipticOfJNe0Or1728OfFactIsUnitHSubOfNat : ∀ {R : Type u_1} [inst : CommRing R] (j : R) [h1 : Fact (IsUnit j)] [h2 : Fact (IsUnit (j - 1728))],
  (WeierstrassCurve.ofJNe0Or1728 j).IsElliptic
-- Mathlib.RingTheory.DividedPowers.RatAlgebra
DividedPowers.OfInvertibleFactorial.dpow_comp_of_mul_lt : ∀ {A : Type u_1} [inst : CommSemiring A] {I : Ideal A} [inst_1 : DecidablePred fun x => x ∈ I] {n : ℕ},
  IsUnit ↑(n - 1).factorial →
    ∀ {m k : ℕ},
      k ≠ 0 →
        m * k < n →
          ∀ {x : A},
            x ∈ I →
              DividedPowers.OfInvertibleFactorial.dpow I m (DividedPowers.OfInvertibleFactorial.dpow I k x) =
                ↑(m.uniformBell k) * DividedPowers.OfInvertibleFactorial.dpow I (m * k) x
-- Mathlib.Analysis.Normed.Operator.Completeness
/-- If a set `s` of semilinear functions is bounded and is closed in the weak-\* topology, then its
image under coercion to functions `E → F` is a closed set. We don't have a name for `E →SL[σ] F`
with weak-\* topology in `mathlib`, so we use an equivalent condition (see `isClosed_induced_iff'`).

TODO: reformulate this in terms of a type synonym with the right topology.  -/
ContinuousLinearMap.isClosed_image_coe_of_bounded_of_weak_closed : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {F : Type u_4} [inst : NormedAddCommGroup F] [inst_1 : NontriviallyNormedField 𝕜]
  [inst_2 : NontriviallyNormedField 𝕜₂] [inst_3 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} {E' : Type u_6}
  [inst_4 : SeminormedAddCommGroup E'] [inst_5 : NormedSpace 𝕜 E'] [inst_6 : RingHomIsometric σ₁₂]
  {s : Set (E' →SL[σ₁₂] F)},
  Bornology.IsBounded s →
    (∀ (f : E' →SL[σ₁₂] F), ⇑f ∈ closure (DFunLike.coe '' s) → f ∈ s) → IsClosed (DFunLike.coe '' s)
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
Std.DHashMap.Internal.AssocList.getCast?_eq : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l : Std.DHashMap.Internal.AssocList α β} {a : α},
  Std.DHashMap.Internal.AssocList.getCast? a l = Std.Internal.List.getValueCast? a l.toList
-- Batteries.Recycling.RBTree.WF
/-- The `setRed` function preserves the ordering invariants.  -/
RBTree.RBNode.Ordered.setRed : ∀ {α : Type u_1} {cmp : α → α → Ordering} {t : RBTree.RBNode α},
  RBTree.RBNode.Ordered cmp t.setRed ↔ RBTree.RBNode.Ordered cmp t
-- Lean.Compiler.CSimpAttr
/-- Tags compiler simplification theorems, which allow one value to be replaced by another equal value
in compiled code. This is typically used to replace a slow function whose definition is convenient
in proofs with a faster equivalent or to make noncomputable functions computable. In particular,
many operations on lists and arrays are replaced by tail-recursive equivalents.

A compiler simplification theorem cannot take any parameters and must prove a statement `@f = @g`
where `f` and `g` may be arbitrary constants. In functions defined after the theorem tagged
`@[csimp]`, any occurrence of `f` is replaced with `g` in compiled code, but not in the type
theory. In this sense, `@[csimp]` is a safer alternative to `@[implemented_by]`.

However it is still possible to register unsound `@[csimp]` lemmas by using `unsafe` or unsound
axioms (like `sorryAx`).
 -/
_private.Lean.Compiler.CSimpAttr.0.Lean.Compiler.CSimp.initFn : IO Unit
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get?_inter : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {m₁ m₂ : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  m₁.WF →
    m₂.WF →
      ∀ {k : α},
        Std.DTreeMap.Raw.Const.get? (m₁ ∩ m₂) k =
          if m₂.contains k = true then Std.DTreeMap.Raw.Const.get? m₁ k else none