mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Tactic.Grind.Types
/-- The E-matching module instantiates theorems using the `EMatchTheorem proof` and a (partial) assignment.
We want to avoid instantiating the same theorem with the same assignment more than once.
Therefore, we store the (pre-)instance information in set.
Recall that the proofs of activated theorems have been hash-consed.
The assignment contains internalized expressions, which have also been hash-consed.

**Note**: We used to use pointer equality to implement `PreInstanceSet`. However,
this low-level trick was incorrect in interactive mode because we add new
`EMatchTheorem` objects using `instantiate [...]`. For example, suppose we write
```
instantiate [thm_1]; instantiate [thm_1]
```
The `EMatchTheorem` object `thm_1` is created twice. Using pointer equality will
miss instances created using the two different objects. Recall we do not use
hash-consing on proof objects. If we hash-cons the proof objects, it would be ok
to use pointer equality.
 -/
Lean.Meta.Grind.PreInstance : Type
-- Mathlib.Topology.Instances.TrivSqZeroExt
TrivSqZeroExt.nhds_inr : ∀ {R : Type u_3} {M : Type u_4} [inst : TopologicalSpace R] [inst_1 : TopologicalSpace M] [inst_2 : Zero R] (m : M),
  nhds (TrivSqZeroExt.inr m) = nhds 0 ×ˢ nhds m
-- Mathlib.Lean.Meta.RefinedDiscrTree.Encode
/-- Encode `e` as a sequence of keys, computing only the first `Key`.  -/
_private.Mathlib.Lean.Meta.RefinedDiscrTree.Encode.0.Lean.Meta.RefinedDiscrTree.initializeLazyEntry : Lean.Expr → Bool → Lean.MetaM (Lean.Meta.RefinedDiscrTree.Key × Lean.Meta.RefinedDiscrTree.LazyEntry)
-- Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
ModelWithCorners.boundaryPoint_inl : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {M' : Type u_5} [inst_6 : TopologicalSpace M']
  [inst_7 : ChartedSpace H M'] (x : M), I.IsBoundaryPoint x → I.IsBoundaryPoint (Sum.inl x)
-- Mathlib.Algebra.Group.Hom.Defs
map_comp_nsmul : ∀ {ι : Type u_1} {G : Type u_7} {H : Type u_8} {F : Type u_9} [inst : FunLike F G H] [inst_1 : AddMonoid G]
  [inst_2 : AddMonoid H] [AddMonoidHomClass F G H] (f : F) (g : ι → G) (n : ℕ), ⇑f ∘ (n • g) = n • ⇑f ∘ g
-- Mathlib.CategoryTheory.GlueData
CategoryTheory.GlueData.t'_iji : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v, u₁} C] (D : CategoryTheory.GlueData C) (i j : D.J),
  D.t' i j i =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (D.f i j) (D.f i i))
      (CategoryTheory.CategoryStruct.comp (D.t i j)
        (CategoryTheory.inv (CategoryTheory.Limits.pullback.snd (D.f j i) (D.f j i))))
-- Mathlib.Analysis.Normed.Group.Constructions
Pi.nnnorm_def' : ∀ {ι : Type u_1} {G : ι → Type u_4} [inst : Fintype ι] [inst_1 : (i : ι) → SeminormedGroup (G i)] (f : (i : ι) → G i),
  ‖f‖₊ = Finset.univ.sup fun b => ‖f b‖₊
-- Mathlib.Order.CountableSupClosed
CountableInfClosed.mk : ∀ {α : Type u_2} [inst : LE α] {s : Set α},
  (∀ t ⊆ s, t.Nonempty → t.Countable → ∀ (x : α), IsGLB t x → x ∈ s) → CountableInfClosed s
-- Init.Data.List.Lemmas
List.getElem?_map : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {l : List α} {i : ℕ}, (List.map f l)[i]? = Option.map f l[i]?
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.Scheme.Pullback.cocycle_snd_fst_snd : ∀ {X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst : ∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g]
  (i j k : 𝒰.I₀),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.t' 𝒰 f g i j k)
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.t' 𝒰 f g j k i)
        (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.t' 𝒰 f g k i j)
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g i j)
              (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g i k))
            (CategoryTheory.CategoryStruct.comp
              (CategoryTheory.Limits.pullback.fst
                (CategoryTheory.CategoryStruct.comp
                  (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g) (𝒰.f i))
                (𝒰.f k))
              (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g))))) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g i j)
        (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g i k))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.fst
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g) (𝒰.f i))
          (𝒰.f k))
        (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g))
-- Init.PropLemmas
not_and_of_not_left : ∀ {a : Prop} (b : Prop), ¬a → ¬(a ∧ b)
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
HomotopicalAlgebra.PathObject.symm_p₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : C}
  [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C] (P : HomotopicalAlgebra.PathObject A), P.symm.p₀ = P.p₁
-- Mathlib.MeasureTheory.SetSemiring
MeasureTheory.IsSetSemiring.sdiff_sUnion_eq_sUnion_disjointOfDiffUnion : ∀ {α : Type u_1} {C : Set (Set α)} {s : Set α} {I : Finset (Set α)} (hC : MeasureTheory.IsSetSemiring C) (hs : s ∈ C)
  (hI : ↑I ⊆ C), s \ ⋃₀ ↑I = ⋃₀ ↑(hC.disjointOfDiffUnion hs hI)
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.sum_subset : ∀ {ι : Type u_1} {M : Type u_4} {s₁ s₂ : Finset ι} [inst : AddCommMonoid M] {f : ι → M},
  s₁ ⊆ s₂ → (∀ x ∈ s₂, x ∉ s₁ → f x = 0) → ∑ x ∈ s₁, f x = ∑ x ∈ s₂, f x
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.mem_iff_contains : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} {k : α},
  k ∈ t ↔ t.contains k = true
-- Lean.Data.KVMap
Lean.KVMap.findD : Lean.KVMap → Lean.Name → Lean.DataValue → Lean.DataValue
-- Mathlib.AlgebraicGeometry.Normalization
/-- [Stacks Tag 0AXN](https://stacks.math.columbia.edu/tag/0AXN) -/
AlgebraicGeometry.Scheme.Hom.instIsReducedNormalization : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.QuasiCompact f]
  [inst_1 : AlgebraicGeometry.QuasiSeparated f] [AlgebraicGeometry.IsReduced X],
  AlgebraicGeometry.IsReduced (AlgebraicGeometry.Scheme.Hom.normalization f)
-- Lean.Data.OpenDecl
Lean.OpenDecl.instInhabited : Inhabited Lean.OpenDecl
-- Init.Data.List.Find
List.find?_replicate_eq_none_iff : ∀ {α : Type u_1} {n : ℕ} {a : α} {p : α → Bool}, List.find? p (List.replicate n a) = none ↔ n = 0 ∨ (!p a) = true
-- Mathlib.Data.Fintype.Card
Finset.card_le_univ : ∀ {α : Type u_1} [inst : Fintype α] (s : Finset α), s.card ≤ Fintype.card α
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.restrict_trim : ∀ {α : Type u_1} {m : MeasurableSpace α} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M]
  {n : MeasurableSpace α} {v : MeasureTheory.VectorMeasure α M} (hle : m ≤ n) {i : Set α},
  MeasurableSet i → (v.trim hle).restrict i = (v.restrict i).trim hle
-- Mathlib.CategoryTheory.Adhesive.Subobject
/-- Given an object `X` of an adhesive category `C`, the coproduct of two subobjects of `X` is their
pushout in `C` over their pullback.  -/
CategoryTheory.Adhesive.isColimitBinaryCofan : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Adhesive C] →
      {X : C} →
        (a b : CategoryTheory.Subobject X) →
          CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk ⋯.hom ⋯.hom)
-- Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
/-- The canonical map from the additive to the multiplicative circle, as an `AddChar`.  -/
AddCircle.toCircle_addChar : {T : ℝ} → AddChar (AddCircle T) Circle
-- Mathlib.Analysis.Calculus.FormalMultilinearSeries
FormalMultilinearSeries.coeff_fslope : ∀ {𝕜 : Type u} {E : Type v} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {p : FormalMultilinearSeries 𝕜 𝕜 E} {n : ℕ}, p.fslope.coeff n = p.coeff (n + 1)
-- Mathlib.NumberTheory.Zsqrtd.GaussianInt
GaussianInt.instMod : Mod GaussianInt
-- Std.Net.Addr
/-- The name of the network interface.
 -/
Std.Net.InterfaceAddress.name : Std.Net.InterfaceAddress → String
-- Lean.Meta.Tactic.Grind.Types
_private.Lean.Meta.Tactic.Grind.Types.0.Lean.Meta.Grind.hashRoot : Lean.Meta.Grind.ENodeMap → Lean.Expr → UInt64
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.integral_le_measure : ∀ {X : Type u_1} {mX : MeasurableSpace X} {μ : MeasureTheory.Measure X} {f : X → ℝ} {s : Set X},
  (∀ x ∈ s, f x ≤ 1) → (∀ x ∈ sᶜ, f x ≤ 0) → ENNReal.ofReal (∫ (x : X), f x ∂μ) ≤ μ s
-- Mathlib.CategoryTheory.PathCategory.Basic
CategoryTheory.Paths.lift_toPath : ∀ {V : Type u₁} [inst : Quiver V] {C : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} C] (φ : V ⥤q C) {X Y : V}
  (f : X ⟶ Y), (CategoryTheory.Paths.lift φ).map f.toPath = φ.map f
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.RightExtension.postcompose₂ObjMkIso_inv_left_app : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} {D' : Type u_5} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  [inst_3 : CategoryTheory.Category.{v_5, u_5} D'] {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H}
  (G : CategoryTheory.Functor H D') {F' : CategoryTheory.Functor D H} (α : L.comp F' ⟶ F) (X : D),
  (CategoryTheory.Functor.RightExtension.postcompose₂ObjMkIso G α).inv.left.app X =
    CategoryTheory.CategoryStruct.id (G.obj (F'.obj X))
-- Mathlib.Tactic.SplitIfs
/-- Finds an if condition to split. If successful, returns the position and the condition.
 -/
_private.Mathlib.Tactic.SplitIfs.0.Mathlib.Tactic.findIfCondAt : Lean.Elab.Tactic.Location → Lean.Elab.Tactic.TacticM (Option (Mathlib.Tactic.SplitPosition✝ × Lean.Expr))
-- Mathlib.Data.Finset.Max
/-- `{a}.min' _` is `a`.  -/
Finset.min'_singleton : ∀ {α : Type u_2} [inst : LinearOrder α] (a : α), {a}.min' ⋯ = a
-- Mathlib.Analysis.Normed.Algebra.QuaternionExponential
/-- Note that this implies that exponentials of pure imaginary quaternions are unit quaternions
since in that case the RHS is `1` via `NormedSpace.exp_zero` and `norm_one`.  -/
Quaternion.norm_exp : ∀ (q : Quaternion ℝ), ‖NormedSpace.exp q‖ = ‖NormedSpace.exp q.re‖
-- Init.Data.String.Subslice
String.Slice.Subslice.extendLeft.congr_simp : ∀ {s : String.Slice} (sl sl_1 : s.Subslice) (e_sl : sl = sl_1) (newStart newStart_1 : s.Pos)
  (e_newStart : newStart = newStart_1) (h : newStart ≤ sl.startInclusive),
  sl.extendLeft newStart h = sl_1.extendLeft newStart_1 ⋯
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.intValuation_eq_one_iff : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] {v : IsDedekindDomain.HeightOneSpectrum R} {x : R},
  v.intValuation x = 1 ↔ x ∉ v.asIdeal
-- Mathlib.Order.RelSeries
RelSeries.fromListIsChain_length : ∀ {α : Type u_1} {r : SetRel α α} (x : List α) (x_ne_nil : x ≠ []) (hx : List.IsChain (fun x1 x2 => (x1, x2) ∈ r) x),
  (RelSeries.fromListIsChain x x_ne_nil hx).length = x.length - 1
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.instCommMonoidOfMonoidHomClass : {ι : Type u_2} →
  [inst : Preorder ι] →
    {G : ι → Type u_3} →
      {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} →
        {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} →
          [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] →
            [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] →
              [inst_3 : IsDirectedOrder ι] →
                [Nonempty ι] →
                  [inst_5 : (i : ι) → CommMonoid (G i)] →
                    [∀ (i j : ι) (h : i ≤ j), MonoidHomClass (T h) (G i) (G j)] → CommMonoid (DirectLimit G f)
-- Mathlib.Order.BooleanAlgebra.Basic
sdiff_ne_right : ∀ {α : Type u} {x y : α} [inst : GeneralizedBooleanAlgebra α], x \ y ≠ y ↔ x ≠ ⊥ ∨ y ≠ ⊥
-- Mathlib.Data.Matrix.Mul
Matrix.neg_vecMul_neg : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : NonUnitalNonAssocRing α] [inst_1 : Fintype m] (v : m → α)
  (A : Matrix m n α), Matrix.vecMul (-v) (-A) = Matrix.vecMul v A
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.toListModel_rotateR : ∀ {α : Type u} {β : α → Type v} {k : α} {v : β k} {lk : α} {lv : β lk} {ll lr r : Std.DTreeMap.Internal.Impl α β},
  (Std.DTreeMap.Internal.Impl.rotateR k v lk lv ll lr r).toListModel =
    ll.toListModel ++ ⟨lk, lv⟩ :: lr.toListModel ++ ⟨k, v⟩ :: r.toListModel
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.Option.eq_get_iff_some_eq : ∀ {α : Type u} {o : Option α} {h : o.isSome = true} {k : α}, k = o.get h ↔ some k = o
-- Mathlib.ModelTheory.LanguageMap
/-- The constant symbol indexed by a particular element.  -/
FirstOrder.Language.con : (L : FirstOrder.Language) → {α : Type w'} → α → (L.withConstants α).Constants
-- Mathlib.Logic.Basic
imp_iff_or_not : ∀ {b a : Prop}, b → a ↔ a ∨ ¬b
-- Init.Data.Ord.Vector
Vector.instLawfulBEqCmpCompareLex : ∀ {α : Type u_1} {cmp : α → α → Ordering} [inst : BEq α] [Std.LawfulBEqCmp cmp] {n : ℕ},
  Std.LawfulBEqCmp (Vector.compareLex cmp)
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanClass.mk_le_mk_of_mabs : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M] {a b : M},
  |a|ₘ ≤ |b|ₘ → MulArchimedeanClass.mk b ≤ MulArchimedeanClass.mk a
-- Mathlib.InformationTheory.Coding.KraftMcMillan
_private.Mathlib.InformationTheory.Coding.KraftMcMillan.0.InformationTheory.concatFn.eq_1 : ∀ {α : Type u_1} {S : Finset (List α)} {r : ℕ} (w : Fin r → ↥S),
  InformationTheory.concatFn✝ w = (List.ofFn fun i => ↑(w i)).flatten
-- Mathlib.Algebra.Algebra.Defs
Algebra.smul_def : ∀ {R : Type u} {A : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (r : R) (x : A),
  r • x = (algebraMap R A) r * x
-- Mathlib.AlgebraicTopology.EilenbergSteenrod
/-- The regular homology functor of a `HomologyPretheory`.  -/
TopPair.HomologyPretheory.H : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {ι : Type u_2} → {c : ComplexShape ι} → TopPair.HomologyPretheory C c → ι → CategoryTheory.Functor TopCat C
-- Mathlib.LinearAlgebra.Dimension.Constructions
/-- If `m` and `n` are finite and lie in the same universe, the rank of `m × n` matrices over a
module `M` is `(#m * #n).lift * rank R M`.  -/
rank_matrix_module' : ∀ (R : Type u) (M : Type v) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [StrongRankCondition R]
  [Module.Free R M] (m n : Type w) [Finite m] [Finite n],
  Module.rank R (Matrix m n M) =
    Cardinal.lift.{v, w} (Cardinal.mk m * Cardinal.mk n) * Cardinal.lift.{w, v} (Module.rank R M)
-- Mathlib.Data.Set.Operations
Set.ofPred_mem_eq : ∀ {α : Type u} {s : Set α}, {x | x ∈ s} = s
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.size_filterMap!_eq_size_iff : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} {γ : α → Type w} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] {f : (a : α) → β a → Option (γ a)},
  t.WF →
    ((Std.DTreeMap.Internal.Impl.filterMap! f t).size = t.size ↔
      ∀ (a : α) (h : Std.DTreeMap.Internal.Impl.contains a t = true), (f a (t.get a h)).isSome = true)
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
Set.Ici_ciSup : ∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLattice α] [Nonempty ι] {f : ι → α},
  BddAbove (Set.range f) → Set.Ici (⨆ i, f i) = ⋂ i, Set.Ici (f i)
-- Init.Data.Array.Count
Array.count_replicate_self : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {a : α} {n : ℕ}, Array.count a (Array.replicate n a) = n
-- Aesop.Script.Main
Aesop.Script.UScript.optimize : Aesop.Script.UScript →
  Bool →
    Lean.Meta.SavedState →
      Lean.MVarId → Lean.MetaM (Option (Lean.TSyntax `Lean.Parser.Tactic.tacticSeq × Aesop.ScriptGenerated))
-- Std.Data.Iterators.Lemmas.Equivalence.HetT
Std.Iterators.HetT.property_lift : ∀ {α : Type w} {m : Type w → Type w'} [inst : Monad m] {x : m α}, (Std.Iterators.HetT.lift x).Property = fun x => True
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.AddGrpObj.neg_eq_neg : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] {G : C}
  [inst_2 : CategoryTheory.AddGrpObj G], CategoryTheory.AddGrpObj.neg = -CategoryTheory.CategoryStruct.id G
-- Init.Data.SInt.Basic
instDivInt64 : Div Int64
-- Mathlib.Analysis.Complex.UnitDisc.Basic
/-- Conjugate point of the unit disc. Deprecated, use `star` instead.  -/
Complex.UnitDisc.conj : Complex.UnitDisc → Complex.UnitDisc
-- Mathlib.Probability.Kernel.Disintegration.CondCDF
ProbabilityTheory.isRatCondKernelCDFAux_preCDF : ∀ {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) [MeasureTheory.IsFiniteMeasure ρ],
  ProbabilityTheory.IsRatCondKernelCDFAux (fun p r => (ProbabilityTheory.preCDF ρ r p.2).toReal)
    (ProbabilityTheory.Kernel.const Unit ρ) (ProbabilityTheory.Kernel.const Unit ρ.fst)
-- Init.Control.Except
MonadFinally.mk : {m : Type u → Type v} → ({α β : Type u} → m α → (Option α → m β) → m (α × β)) → MonadFinally m
-- Mathlib.Topology.AlexandrovDiscrete
Sum.instAlexandrovDiscrete : ∀ {α : Type u_3} {β : Type u_4} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [AlexandrovDiscrete α]
  [AlexandrovDiscrete β], AlexandrovDiscrete (α ⊕ β)
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
borel_eq_top_of_discrete : ∀ {α : Type u_1} [inst : TopologicalSpace α] [DiscreteTopology α], borel α = ⊤
-- Init.Data.List.Find
_private.Init.Data.List.Find.0.List.findIdx_cons.findIdx_go_succ : ∀ {α : Type u_1} (p : α → Bool) (l : List α) (n : ℕ), List.findIdx.go p l (n + 1) = List.findIdx.go p l n + 1
-- Mathlib.Combinatorics.Quiver.Prefunctor
/-- Composition of morphisms between quivers.  -/
Prefunctor.comp : {U : Type u_1} →
  [inst : Quiver U] →
    {V : Type u_2} → [inst_1 : Quiver V] → {W : Type u_3} → [inst_2 : Quiver W] → U ⥤q V → V ⥤q W → U ⥤q W
-- Init.Data.Array.Lemmas
Array.size_pos_iff_exists_mem : ∀ {α : Type u_1} {xs : Array α}, 0 < xs.size ↔ ∃ a, a ∈ xs
-- Mathlib.GroupTheory.Subsemigroup.Centralizer
AddSubsemigroup.centralizer.eq_1 : ∀ {M : Type u_1} (S : Set M) [inst : AddSemigroup M],
  AddSubsemigroup.centralizer S = { carrier := S.addCentralizer, add_mem' := ⋯ }
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToIntInfo
Lean.Meta.Grind.Arith.Cutsat.SymbolicIntInterval.ii : Lean.Meta.Grind.Arith.Cutsat.SymbolicIntInterval
-- Mathlib.NumberTheory.LucasLehmer
LucasLehmer.norm_num_ext.isNat_lucasLehmerTest : ∀ {p np : ℕ}, Mathlib.Meta.NormNum.IsNat p np → LucasLehmerTest np → LucasLehmerTest p
-- Init.Data.Vector.Lemmas
Vector.getElem?_set!_self_of_lt : ∀ {α : Type u_1} {n i : ℕ} {xs : Vector α n} {x : α}, i < n → (xs.set! i x)[i]? = some x
-- Mathlib.Analysis.Normed.Operator.Fredholm.Basic
FredholmDecomposition.isTopCompl : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] (self : FredholmDecomposition 𝕜 E), Submodule.IsTopCompl self.X₁ self.X₀
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.mapRightId_hom_app_right : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) {P : CategoryTheory.MorphismProperty T}
  {Q : CategoryTheory.MorphismProperty A} {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsMultiplicative]
  [inst_4 : W.IsMultiplicative] [inst_5 : Q.RespectsIso] [inst_6 : W.RespectsIso]
  (X : CategoryTheory.MorphismProperty.Comma L R P Q W),
  ((CategoryTheory.MorphismProperty.Comma.mapRightId L R).hom.app X).right = CategoryTheory.CategoryStruct.id X.right
-- Mathlib.Algebra.FreeMonoid.UniqueProds
/-- Any `FreeAddMonoid` has the `TwoUniqueSums` property.  -/
FreeAddMonoid.instTwoUniqueSums : ∀ {κ : Type u_1}, TwoUniqueSums (FreeAddMonoid κ)
-- Mathlib.MeasureTheory.Group.Prod
/-- The map `(x, y) ↦ y + x` is quasi-measure-preserving.  -/
MeasureTheory.quasiMeasurePreserving_add_swap : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : AddGroup G] [MeasurableAdd₂ G] (μ ν : MeasureTheory.Measure G)
  [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] [μ.IsAddLeftInvariant],
  MeasureTheory.Measure.QuasiMeasurePreserving (fun p => p.2 + p.1) (μ.prod ν) μ
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.map_add_toList_rco : ∀ {m n k : ℕ}, List.map (fun x => x + k) (m...n).toList = ((m + k)...n + k).toList
-- Lean.Elab.Tactic.Omega.Core
/-- The coefficients of a constraint.  -/
Lean.Elab.Tactic.Omega.Fact.coeffs : Lean.Elab.Tactic.Omega.Fact → Lean.Omega.Coeffs
-- Init.Grind.Ring.CommSemiringAdapter
Lean.Grind.CommRing.eq_normS_nc : ∀ {α : Type u_1} [inst : Lean.Grind.Semiring α] (ctx : Lean.Grind.CommRing.Context α)
  (lhs rhs : Lean.Grind.CommRing.Expr),
  Lean.Grind.CommRing.eq_normS_nc_cert lhs rhs = true →
    Lean.Grind.CommRing.Expr.denoteS ctx lhs = Lean.Grind.CommRing.Expr.denoteS ctx rhs
-- Mathlib.Probability.Martingale.Basic
MeasureTheory.submartingale_of_condExp_sub_nonneg : ∀ {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [inst : Preorder ι] {m0 : MeasurableSpace Ω}
  {μ : MeasureTheory.Measure Ω} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E]
  {ℱ : MeasureTheory.Filtration ι m0} [CompleteSpace E] [inst_4 : PartialOrder E] [IsOrderedAddMonoid E]
  [MeasureTheory.SigmaFiniteFiltration μ ℱ] {f : ι → Ω → E},
  MeasureTheory.StronglyAdapted ℱ f →
    (∀ (i : ι), MeasureTheory.Integrable (f i) μ) →
      (∀ (i j : ι), i ≤ j → 0 ≤ᵐ[μ] μ[f j - f i | ↑ℱ i]) → MeasureTheory.Submartingale f ℱ μ
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.polar_neg : ∀ {M : Type u_4} {N : Type u_5} [inst : AddCommGroup M] [inst_1 : AddCommGroup N] (f : M → N) (x y : M),
  QuadraticMap.polar (-f) x y = -QuadraticMap.polar f x y
-- Mathlib.LinearAlgebra.Dimension.Constructions
LinearIndepOn.union_id_of_quotient : ∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {M' : Submodule R M}
  {s : Set M}, s ⊆ ↑M' → LinearIndepOn R id s → ∀ {t : Set M}, LinearIndepOn R (⇑M'.mkQ) t → LinearIndepOn R id (s ∪ t)
-- Mathlib.Analysis.BoxIntegral.Box.Basic
BoxIntegral.Box.nndist_le_distortion_mul : ∀ {ι : Type u_1} [inst : Fintype ι] (I : BoxIntegral.Box ι) (i : ι),
  nndist I.lower I.upper ≤ I.distortion * nndist (I.lower i) (I.upper i)
-- Mathlib.Algebra.Free
Magma.AssocQuotient.instSemigroup.eq_1 : ∀ {α : Type u} [inst : Mul α],
  Magma.AssocQuotient.instSemigroup =
    { mul := fun x y => Quot.liftOn₂ x y (fun x y => Quot.mk (Magma.AssocRel α) (x * y)) ⋯ ⋯, mul_assoc := ⋯ }
-- Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv
_private.Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv.0.coe_symm_auxIsometry : ∀ {𝕜 : Type u_1} {V : Type u_2} {W : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] [inst_3 : CompleteSpace V] [inst_4 : NormedAddCommGroup W]
  [inst_5 : InnerProductSpace 𝕜 W] [inst_6 : CompleteSpace W] (e : V ≃L[𝕜] W) {α α' : 𝕜} (hα : α ≠ 0)
  (hα2 : α' * α' = α⁻¹) (he : ContinuousLinearMap.adjoint ↑e ∘SL ↑e = α • ContinuousLinearMap.id 𝕜 V)
  (he' : ↑e ∘SL ContinuousLinearMap.adjoint ↑e = α • ContinuousLinearMap.id 𝕜 W) (hαa : (starRingEnd 𝕜) α' = α'),
  ↑(↑(auxIsometry✝ e hα hα2 he he' hαa)).symm = α'⁻¹ • ↑e.symm
-- Std.Time.Date.Unit.Week
/-- `Ordinal` represents the aligned week number within a month, ranging between 1 and 5.
Aligned weeks are fixed 7-day slots counted from day 1 of the month: days 1-7 are
week 1, days 8-14 are week 2, and so on, independent of which weekday starts the month.
 -/
Std.Time.Week.Aligned.Ordinal : Type