mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Tactic.BVDecide.LRAT.Internal.LRATCheckerSound
Std.Tactic.BVDecide.LRAT.Internal.lratChecker.match_3.congr_eq_4 : ∀ {α : Type u_1} {β : Type u_2} (motive : List (Std.Tactic.BVDecide.LRAT.Action β α) → Sort u_3)
  (prf : List (Std.Tactic.BVDecide.LRAT.Action β α)) (h_1 : Unit → motive [])
  (h_2 :
    (id : ℕ) →
      (rupHints : Array ℕ) →
        (tail : List (Std.Tactic.BVDecide.LRAT.Action β α)) →
          motive (Std.Tactic.BVDecide.LRAT.Action.addEmpty id rupHints :: tail))
  (h_3 :
    (id : ℕ) →
      (c : β) →
        (rupHints : Array ℕ) →
          (restPrf : List (Std.Tactic.BVDecide.LRAT.Action β α)) →
            motive (Std.Tactic.BVDecide.LRAT.Action.addRup id c rupHints :: restPrf))
  (h_4 :
    (id : ℕ) →
      (c : β) →
        (pivot : Std.Sat.Literal α) →
          (rupHints : Array ℕ) →
            (ratHints : Array (ℕ × Array ℕ)) →
              (restPrf : List (Std.Tactic.BVDecide.LRAT.Action β α)) →
                motive (Std.Tactic.BVDecide.LRAT.Action.addRat id c pivot rupHints ratHints :: restPrf))
  (h_5 :
    (ids : Array ℕ) →
      (restPrf : List (Std.Tactic.BVDecide.LRAT.Action β α)) →
        motive (Std.Tactic.BVDecide.LRAT.Action.del ids :: restPrf))
  (id : ℕ) (c : β) (pivot : Std.Sat.Literal α) (rupHints : Array ℕ) (ratHints : Array (ℕ × Array ℕ))
  (restPrf : List (Std.Tactic.BVDecide.LRAT.Action β α)),
  prf = Std.Tactic.BVDecide.LRAT.Action.addRat id c pivot rupHints ratHints :: restPrf →
    (match prf with
      | [] => h_1 ()
      | Std.Tactic.BVDecide.LRAT.Action.addEmpty id rupHints :: tail => h_2 id rupHints tail
      | Std.Tactic.BVDecide.LRAT.Action.addRup id c rupHints :: restPrf => h_3 id c rupHints restPrf
      | Std.Tactic.BVDecide.LRAT.Action.addRat id c pivot rupHints ratHints :: restPrf =>
        h_4 id c pivot rupHints ratHints restPrf
      | Std.Tactic.BVDecide.LRAT.Action.del ids :: restPrf => h_5 ids restPrf) ≍
      h_4 id c pivot rupHints ratHints restPrf
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.RestrictScalars
ContinuousLinearMap.restrictScalars_neg : ∀ {A : Type u_1} {R : Type u_2} {M₁ : Type u_4} {M₂ : Type u_5} [inst : Ring A] [inst_1 : Ring R]
  [inst_2 : AddCommGroup M₁] [inst_3 : Module A M₁] [inst_4 : Module R M₁] [inst_5 : TopologicalSpace M₁]
  [inst_6 : AddCommGroup M₂] [inst_7 : Module A M₂] [inst_8 : Module R M₂] [inst_9 : TopologicalSpace M₂]
  [inst_10 : LinearMap.CompatibleSMul M₁ M₂ R A] [inst_11 : IsTopologicalAddGroup M₂] (f : M₁ →L[A] M₂),
  ContinuousLinearMap.restrictScalars R (-f) = -ContinuousLinearMap.restrictScalars R f
-- Mathlib.Topology.LocalAtTarget
IsClosedMap.restrictPreimage : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β},
  IsClosedMap f → ∀ (s : Set β), IsClosedMap (s.restrictPreimage f)
-- Mathlib.Order.Hom.Lattice
SupHom.instMax : {α : Type u_2} → {β : Type u_3} → [inst : Max α] → [inst_1 : SemilatticeSup β] → Max (SupHom α β)
-- Lean.Elab.App
Lean.Elab.Term.ElabElim.State.mk.inj : ∀ {f fType : Lean.Expr} {namedArgs : List Lean.Elab.Term.NamedArg} {args : List Lean.Elab.Term.Arg}
  {instMVars : Array Lean.MVarId} {idx : ℕ} {motive? : Option Lean.Expr} {f_1 fType_1 : Lean.Expr}
  {namedArgs_1 : List Lean.Elab.Term.NamedArg} {args_1 : List Lean.Elab.Term.Arg} {instMVars_1 : Array Lean.MVarId}
  {idx_1 : ℕ} {motive?_1 : Option Lean.Expr},
  { f := f, fType := fType, namedArgs := namedArgs, args := args, instMVars := instMVars, idx := idx,
        motive? := motive? } =
      { f := f_1, fType := fType_1, namedArgs := namedArgs_1, args := args_1, instMVars := instMVars_1, idx := idx_1,
        motive? := motive?_1 } →
    f = f_1 ∧
      fType = fType_1 ∧
        namedArgs = namedArgs_1 ∧ args = args_1 ∧ instMVars = instMVars_1 ∧ idx = idx_1 ∧ motive? = motive?_1
-- Mathlib.CategoryTheory.Abelian.Projective.Resolution
CategoryTheory.ProjectiveResolution.homotopyEquiv_hom_π : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X : C}
  (P Q : CategoryTheory.ProjectiveResolution X), CategoryTheory.CategoryStruct.comp (P.homotopyEquiv Q).hom Q.π = P.π
-- Mathlib.Topology.NhdsSet
Filter.Eventually.union : ∀ {X : Type u_2} [inst : TopologicalSpace X] {s t : Set X} {p : X → Prop},
  (∀ᶠ (x : X) in nhdsSet s, p x) → (∀ᶠ (x : X) in nhdsSet t, p x) → ∀ᶠ (x : X) in nhdsSet (s ∪ t), p x
-- Mathlib.Analysis.Normed.Group.Basic
vadd_closedBall'' : ∀ {E : Type u_5} [inst : SeminormedAddCommGroup E] {a b : E} {r : ℝ},
  a +ᵥ Metric.closedBall b r = Metric.closedBall (a +ᵥ b) r
-- Mathlib.CategoryTheory.Monad.Limits
CategoryTheory.hasColimit_of_coreflective : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type u} [inst_2 : CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J D)
  (R : CategoryTheory.Functor D C) [CategoryTheory.Limits.HasColimit (F.comp R)] [CategoryTheory.Coreflective R],
  CategoryTheory.Limits.HasColimit F
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology
/-- The subgroup of `Cocycle K L n` consisting of coboundaries.  -/
CochainComplex.HomComplex.coboundaries : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      (K L : CochainComplex C ℤ) → (n : ℤ) → AddSubgroup (CochainComplex.HomComplex.Cocycle K L n)
-- Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm
PiTensorProduct.projectiveSeminorm_zero : ∀ {ι : Type u_1} [inst : Fintype ι] {𝕜 : Type u_2} {E : ι → Type u_3} [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)]
  [inst_2 : NormedField 𝕜] [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)], ‖0‖ = 0
-- Mathlib.Analysis.Normed.Group.Uniform
SeparationQuotient.instMulNorm : {E : Type u_2} → [inst : SeminormedCommGroup E] → Norm (SeparationQuotient E)
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.mapₘ.eq_1 : ∀ {α : Type u} {β : α → Type v} {δ : α → Type w} (m : Std.DHashMap.Internal.Raw₀ α β) (f : (a : α) → β a → δ a),
  m.mapₘ f =
    ⟨{ size := (↑m).size,
        buckets := Std.DHashMap.Internal.updateAllBuckets (↑m).buckets (Std.DHashMap.Internal.AssocList.map f) },
      ⋯⟩
-- Aesop.Tree.Traversal
Aesop.TreeRef.mvarCluster.inj : ∀ {cref cref_1 : Aesop.MVarClusterRef},
  Aesop.TreeRef.mvarCluster cref = Aesop.TreeRef.mvarCluster cref_1 → cref = cref_1
-- Init.Data.String.Basic
String.Pos.isValidUTF8_extract : ∀ {s : String} (pos₁ pos₂ : s.Pos), (s.toByteArray.extract pos₁.offset.byteIdx pos₂.offset.byteIdx).IsValidUTF8
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Under.mono_homMk : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T} {U V : CategoryTheory.Under X}
  {f : U.right ⟶ V.right} [CategoryTheory.Mono f] (w : CategoryTheory.CategoryStruct.comp U.hom f = V.hom),
  CategoryTheory.Mono (CategoryTheory.Under.homMk f w)
-- Lean.Compiler.ExportAttr
_private.Lean.Compiler.ExportAttr.0.Lean.isValidCppId : String → Bool
-- Mathlib.Data.Sym.Basic
Sym.toMultiset_zero : ∀ {α : Type u_1}, ↑0 = 0
-- Mathlib.Order.BooleanAlgebra.Set
Set.inter_subset_ite : ∀ {α : Type u_1} (t s s' : Set α), s ∩ s' ⊆ t.ite s s'
-- Mathlib.Algebra.Group.Conj
IsConj.conjugatesOf_eq : ∀ {α : Type u} [inst : Monoid α] {a b : α}, IsConj a b → conjugatesOf a = conjugatesOf b
-- Mathlib.Analysis.Convex.Hull
IsLinearMap.image_convexHull : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid F] [inst_4 : Module 𝕜 E] [inst_5 : Module 𝕜 F] {f : E → F},
  IsLinearMap 𝕜 f → ∀ (s : Set E), f '' (convexHull 𝕜) s = (convexHull 𝕜) (f '' s)
-- Mathlib.Algebra.Order.Ring.Synonym
Lex.instNonAssocSemiring : {R : Type u_1} → [NonAssocSemiring R] → NonAssocSemiring (Lex R)
-- Mathlib.GroupTheory.Subgroup.Centralizer
/-- If all the elements of a set `s` commute, then `closure s` is an additive commutative group.  -/
AddSubgroup.closureAddCommGroupOfComm : {G : Type u_1} →
  [inst : AddGroup G] → {k : Set G} → (∀ x ∈ k, ∀ y ∈ k, x + y = y + x) → AddCommGroup ↥(AddSubgroup.closure k)
-- Lean.Meta.Tactic.Simp.SimpTheorems
/-- A `SimpTheoremsArray` is a collection of `SimpTheorems`. The first entry is the default simp set
and possible extensions as simp args (`simp [thm]`), further entries are custom simp sets added
a s simp arguments (`simp [my_simp_set]`). The array is scanned linear during rewriting.
This avoids the need for efficiently merging the `SimpTheorems` data structure.
 -/
Lean.Meta.SimpTheoremsArray : Type
-- Mathlib.Order.UpperLower.CompleteLattice
LowerSet.compl_sSup : ∀ {α : Type u_1} [inst : LE α] (S : Set (LowerSet α)), (sSup S).compl = ⨆ s ∈ S, s.compl
-- Mathlib.Algebra.Opposites
MulOpposite.unop_ne_zero_iff : ∀ {α : Type u_1} [inst : Zero α] (a : αᵐᵒᵖ), MulOpposite.unop a ≠ 0 ↔ a ≠ 0
-- Init.Prelude
/-- The implementation of `a ||| b : α`. See `HOr`.  -/
OrOp.or : {α : Type u} → [self : OrOp α] → α → α → α
-- Init.Data.String.FindPos
/-- Returns the previous valid position before the given position, or `none` if the position is
the start position.  -/
String.Slice.Pos.prev? : {s : String.Slice} → s.Pos → Option s.Pos
-- Mathlib.Analysis.Convex.Topology
convexHull_interior_subset : ∀ {𝕜 : Type u_2} {E : Type u_3} [inst : Field 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] [inst_4 : TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousConstSMul 𝕜 E]
  [ZeroLEOneClass 𝕜] (s : Set E), (convexHull 𝕜) (interior s) ⊆ interior ((convexHull 𝕜) s)
-- Mathlib.CategoryTheory.Shift.Adjunction
/-- Given an adjunction `adj : F ⊣ G`, `a` in `A` and commutation isomorphisms
`e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a` and
`e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a`, if `e₁` and `e₂` are compatible with the
unit of the adjunction `adj`, then `e₂` uniquely determines `e₁`.
 -/
CategoryTheory.Adjunction.CommShift.compatibilityUnit_unique_left : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  (adj : F ⊣ G) {A : Type u_3} [inst_2 : AddMonoid A] [inst_3 : CategoryTheory.HasShift C A]
  [inst_4 : CategoryTheory.HasShift D A] {a : A}
  (e₁ e₁' : (CategoryTheory.shiftFunctor C a).comp F ≅ F.comp (CategoryTheory.shiftFunctor D a))
  (e₂ : (CategoryTheory.shiftFunctor D a).comp G ≅ G.comp (CategoryTheory.shiftFunctor C a)),
  CategoryTheory.Adjunction.CommShift.CompatibilityUnit adj e₁ e₂ →
    CategoryTheory.Adjunction.CommShift.CompatibilityUnit adj e₁' e₂ → e₁ = e₁'
-- Std.Async.TCP
_private.Std.Async.TCP.0.Std.Async.TCP.Socket.Server.ofNative.injEq : ∀ (native native_1 : Std.Internal.UV.TCP.Socket), ({ native := native } = { native := native_1 }) = (native = native_1)
-- Mathlib.Data.Fin.Embedding
Fin.natAddEmb_apply : ∀ (n : ℕ) {m : ℕ} (i : Fin m), (Fin.natAddEmb n) i = Fin.natAdd n i
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtensionAt.isoLimit_inv_π_assoc : ∀ {C : Type u_1} {D : Type u_2} {H : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_4, u_4} H]
  {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} {E : L.RightExtension F} {Y : D}
  (h : E.IsPointwiseRightKanExtensionAt Y)
  [inst_3 : CategoryTheory.Limits.HasLimit ((CategoryTheory.StructuredArrow.proj Y L).comp F)]
  (g : CategoryTheory.StructuredArrow Y L) {Z : H} (h_1 : F.obj g.right ⟶ Z),
  CategoryTheory.CategoryStruct.comp h.isoLimit.inv
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.CostructuredArrow.left E).map g.hom)
        (CategoryTheory.CategoryStruct.comp ((CategoryTheory.CostructuredArrow.hom E).app g.right) h_1)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.limit.π ((CategoryTheory.StructuredArrow.proj Y L).comp F) g) h_1
-- Mathlib.Topology.Basic
isOpen_iff_of_cover : ∀ {X : Type u} {α : Type u_1} {s : Set X} [inst : TopologicalSpace X] {f : α → Set X},
  (∀ (i : α), IsOpen (f i)) → ⋃ i, f i = Set.univ → (IsOpen s ↔ ∀ (i : α), IsOpen (f i ∩ s))
-- Lean.Elab.Tactic.Simp
/-- Specializes the `elabSimpConfigAux` configuration elaborator to a specific `Simp` default configuration.
This is necessary for `(config := {...})` to elaborate the `{...}` expression with the correct expected type.
 -/
_private.Lean.Elab.Tactic.Simp.0.Lean.Elab.Tactic.commandMake_elab_simp_config__ : Lean.ParserDescr
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
CategoryTheory.Limits.opCoproductIsoProduct'_hom_comp_proj_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C}
  {c : CategoryTheory.Limits.Cofan Z} {f : CategoryTheory.Limits.Fan fun x => Opposite.op (Z x)}
  (hc : CategoryTheory.Limits.IsColimit c) (hf : CategoryTheory.Limits.IsLimit f) (i : α) {Z_1 : Cᵒᵖ}
  (h : Opposite.op (Z i) ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.opCoproductIsoProduct' hc hf).hom
      (CategoryTheory.CategoryStruct.comp (f.proj i) h) =
    CategoryTheory.CategoryStruct.comp (c.inj i).op h
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.ObjectProperty.IsCodetecting.of_le : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.ObjectProperty C},
  P.IsCodetecting → ∀ {Q : CategoryTheory.ObjectProperty C}, P ≤ Q → Q.IsCodetecting
-- Mathlib.Data.PFunctor.Univariate.M
PFunctor.M.head_mk : ∀ {F : PFunctor.{uA, uB}} (x : ↑F F.M), (PFunctor.M.mk x).head = x.fst
-- Mathlib.Order.Minimal
/-- **Alias** of the forward direction of `not_maximal_iff_exists_gt`. -/
exists_gt_of_not_maximal : ∀ {α : Type u_2} {P : α → Prop} {x : α} [inst : Preorder α], P x → ¬Maximal P x → ∃ y, x < y ∧ P y
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.NeWord.append_prod : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] {i j k l : ι} {w₁ : Monoid.CoprodI.NeWord M i j}
  {hne : j ≠ k} {w₂ : Monoid.CoprodI.NeWord M k l}, (w₁.append hne w₂).prod = w₁.prod * w₂.prod
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.Equiv.any_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp] {p : α → Bool},
  t₁.Equiv t₂ → t₁.any p = t₂.any p
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.isSome_minKey?_insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α} {v : β}, (t.insert k v).minKey?.isSome = true
-- Mathlib.MeasureTheory.Integral.Average
/-- **First moment method**. A measurable function is smaller than its integral on a set f
positive measure.  -/
MeasureTheory.measure_le_lintegral_pos : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal}
  [MeasureTheory.IsProbabilityMeasure μ], AEMeasurable f μ → 0 < μ {x | f x ≤ ∫⁻ (a : α), f a ∂μ}
-- Mathlib.Logic.Equiv.Fin.Basic
/-- The natural `Equiv` between `(Fin m → α) × (Fin n → α)` and `Fin (m + n) → α`  -/
Fin.appendEquiv : {α : Type u_1} → (m n : ℕ) → (Fin m → α) × (Fin n → α) ≃ (Fin (m + n) → α)
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getD_toList_rio_eq_fallback : ∀ {n i fallback : ℕ}, n ≤ i → (*...n).toList.getD i fallback = fallback
-- Mathlib.Data.Int.Bitwise
Int.shiftLeft_eq_mul_pow : ∀ (m : ℤ) (n : ℕ), m <<< ↑n = m * ↑(2 ^ n)
-- Mathlib.CategoryTheory.Idempotents.HomologicalComplex
CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_unitIso_inv_app_f_f : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] (α : Type u_3)
  [inst_2 : AddRightCancelSemigroup α] [inst_3 : One α]
  (P : CategoryTheory.Idempotents.Karoubi (HomologicalComplex C (ComplexShape.up α))) (n : α),
  ((CategoryTheory.Idempotents.karoubiCochainComplexEquivalence C α).unitIso.inv.app P).f.f n = P.p.f n
-- Mathlib.Algebra.Order.Interval.Set.SuccPred
Set.Ioo_add_one_right_eq_Ioc : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : One α] [inst_2 : Add α] [SuccAddOrder α] [NoMaxOrder α] (a b : α),
  Set.Ioo a (b + 1) = Set.Ioc a b
-- Mathlib.Algebra.Group.Units.Basic
IsAddUnit.eq_sub_of_add_eq : ∀ {α : Type u} [inst : SubtractionMonoid α] {a b c : α}, IsAddUnit c → a + c = b → a = b - c
-- Mathlib.CategoryTheory.Adjunction.Lifting.Right
/-- Construct the object part of the desired right adjoint as the equalizer of `U'Fη_Y` with
`otherMap`.
 -/
CategoryTheory.LiftRightAdjoint.constructRightAdjointObj : {A : Type u₁} →
  {B : Type u₂} →
    {C : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} A] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            {U : CategoryTheory.Functor A B} →
              {F : CategoryTheory.Functor B A} →
                (L : CategoryTheory.Functor C B) →
                  (U' : CategoryTheory.Functor A C) →
                    (F ⊣ U) → (L.comp F ⊣ U') → [CategoryTheory.Limits.HasCoreflexiveEqualizers C] → B → C
-- Mathlib.Algebra.Group.Submonoid.Defs
SubmonoidClass.subtype_injective : ∀ {M : Type u_1} {A : Type u_3} [inst : MulOneClass M] [inst_1 : SetLike A M] [hA : SubmonoidClass A M] (S' : A),
  Function.Injective ⇑(SubmonoidClass.subtype S')
-- Mathlib.MeasureTheory.Function.ConditionalLExpectation
MeasureTheory.condLExp_def : ∀ {Ω : Type u_2} {mΩ₀ : MeasurableSpace Ω} (mΩ : MeasurableSpace Ω) (P : MeasureTheory.Measure Ω) (X : Ω → ENNReal),
  P⁻[X | mΩ] =
    if hm : mΩ ≤ mΩ₀ then
      if MeasureTheory.SigmaFinite (P.trim hm) then
        if Measurable X then X else ((P.withDensity X).trim hm).rnDeriv (P.trim hm)
      else 0
    else 0
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.Functor.opComp_inv_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u_1} [inst_2 : CategoryTheory.Category.{v_1, u_1} E] (F : CategoryTheory.Functor C D)
  (G : CategoryTheory.Functor D E) (X : Cᵒᵖ),
  (F.opComp G).inv.app X = CategoryTheory.CategoryStruct.id (Opposite.op (G.obj (F.obj (Opposite.unop X))))
-- Mathlib.Algebra.Group.Hom.End
AddMonoid.End.instAddMonoidWithOne : (M : Type u_1) → [inst : AddCommMonoid M] → AddMonoidWithOne (AddMonoid.End M)
-- Mathlib.Topology.MetricSpace.Snowflaking
Metric.Snowflaking.instEMetricSpace : {X : Type u_1} →
  {α : ℝ} → {hα₀ : 0 < α} → {hα₁ : α ≤ 1} → [EMetricSpace X] → EMetricSpace (Metric.Snowflaking X α hα₀ hα₁)
-- Mathlib.Algebra.Notation.Pi.Defs
Function.const_pow : ∀ {ι : Type u_1} {α : Type u_2} {M : Type u_7} [inst : Pow M α] (a : M) (b : α),
  Function.const ι a ^ b = Function.const ι (a ^ b)
-- Mathlib.Algebra.DirectSum.Module
/-- Reindexing terms of a direct sum is linear.  -/
DirectSum.lequivCongrLeft : (R : Type u) →
  [inst : Semiring R] →
    {ι : Type v} →
      {M : ι → Type w} →
        [inst_1 : (i : ι) → AddCommMonoid (M i)] →
          [inst_2 : (i : ι) → Module R (M i)] →
            {κ : Type u_1} → (h : ι ≃ κ) → (DirectSum ι fun i => M i) ≃ₗ[R] DirectSum κ fun k => M (h.symm k)
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubMulAction.SMulMemClass.subtype.eq_1 : ∀ {R : Type u} {M : Type v} [inst : Monoid R] [inst_1 : MulAction R M] {A : Type u_1} [inst_2 : SetLike A M]
  [hA : SMulMemClass A R M] (S' : A), SubMulAction.SMulMemClass.subtype S' = { toFun := Subtype.val, map_smul' := ⋯ }
-- Mathlib.MeasureTheory.OuterMeasure.Induced
Option.elim'.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (b : β) (f : α → β) (a : α), Option.elim' b f (some a) = f a
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
/-- Eta-expanded form of `MeasureTheory.AEStronglyMeasurable.inv₀` -/
MeasureTheory.AEStronglyMeasurable.fun_inv₀ : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {f : α → β} [inst_1 : GroupWithZero β] [ContinuousInv₀ β] [TopologicalSpace.MetrizableSpace β],
  MeasureTheory.AEStronglyMeasurable f μ → MeasureTheory.AEStronglyMeasurable (fun i => (f i)⁻¹) μ
-- Mathlib.CategoryTheory.Sites.MorphismProperty
/-- If `P` is also multiplicative, the coverage induced by `P` is the pretopology induced by `P`.  -/
CategoryTheory.MorphismProperty.coverage_eq_toCoverage_pretopology : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P : CategoryTheory.MorphismProperty C}
  [inst_1 : P.IsStableUnderBaseChange] [inst_2 : CategoryTheory.Limits.HasPullbacks C] [inst_3 : P.IsMultiplicative],
  P.coverage = P.pretopology.toCoverage
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Substructure
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Substructure.0.Std.Tactic.BVDecide.BVLogicalExpr.bitblast.go.match_3.eq_3 : ∀ (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.beq 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_3 ()
-- Mathlib.MeasureTheory.Measure.Haar.Unique
/-- **Uniqueness of left-invariant measures**:
Given two left-invariant measures which are finite on
compacts and inner regular for finite measure sets with respect to compact sets,
they coincide in the following sense: they give the same value to finite measure sets,
up to a multiplicative constant.  -/
MeasureTheory.Measure.measure_isMulLeftInvariant_eq_smul_of_ne_top : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : Group G] [inst_2 : IsTopologicalGroup G]
  [inst_3 : MeasurableSpace G] [inst_4 : BorelSpace G] [LocallyCompactSpace G] (μ' μ : MeasureTheory.Measure G)
  [inst_6 : μ.IsHaarMeasure] [inst_7 : MeasureTheory.IsFiniteMeasureOnCompacts μ'] [inst_8 : μ'.IsMulLeftInvariant]
  [μ.InnerRegularCompactLTTop] [μ'.InnerRegularCompactLTTop] {s : Set G},
  μ s ≠ ⊤ → μ' s ≠ ⊤ → μ' s = μ'.haarScalarFactor μ • μ s
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
/-- This should be autogenerated by `@[simps]` but we need to give `s` the correct type here.  -/
ModuleCat.RestrictionCoextensionAdj.HomEquiv.fromRestriction_hom_apply_apply : ∀ {R : Type u₁} {S : Type u₂} [inst : Ring R] [inst_1 : Ring S] (f : R →+* S) {X : ModuleCat R} {Y : ModuleCat S}
  (g : (ModuleCat.restrictScalars f).obj Y ⟶ X) (y : ↑Y) (s : S),
  ((ModuleCat.CoextendScalars.equiv f X)
        ((ModuleCat.Hom.hom (ModuleCat.RestrictionCoextensionAdj.HomEquiv.fromRestriction f g)) y))
      s =
    (CategoryTheory.ConcreteCategory.hom g) (s • y)
-- Init.Data.String.Lemmas.Pattern.String.ForwardPattern
String.Slice.dropPrefix_string_eq_dropPrefix_toSlice : ∀ {pat : String} {s : String.Slice}, s.dropPrefix pat = s.dropPrefix pat.toSlice
-- Init.Data.Array.Erase
_private.Init.Data.Array.Erase.0.List.eraseP_filterMap.match_1.splitter : {β : Type u_1} →
  (motive : Option β → Sort u_2) → (x : Option β) → ((y : β) → motive (some y)) → (Unit → motive none) → motive x
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVPred.getLsbD.inj : ∀ {w : ℕ} {expr : Std.Tactic.BVDecide.BVExpr w} {idx w_1 : ℕ} {expr_1 : Std.Tactic.BVDecide.BVExpr w_1} {idx_1 : ℕ},
  Std.Tactic.BVDecide.BVPred.getLsbD expr idx = Std.Tactic.BVDecide.BVPred.getLsbD expr_1 idx_1 →
    w = w_1 ∧ expr ≍ expr_1 ∧ idx = idx_1
-- Mathlib.LinearAlgebra.RootSystem.RootPairingCat
/-- The root pairing structure.  -/
RootPairingCat.pairing : {R : Type u} → [inst : CommRing R] → (self : RootPairingCat R) → RootPairing self.index R self.weight self.coweight
-- Mathlib.CategoryTheory.MorphismProperty.Representable
/-- When `F` is full, given a representable morphism `f' : F.obj b ⟶ Y`, then `hf'.fst' g` denotes
the preimage of `hf'.fst g` under `F`.  -/
CategoryTheory.Functor.relativelyRepresentable.fst' : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F : CategoryTheory.Functor C D} →
          {Y : D} →
            {b : C} →
              {f' : F.obj b ⟶ Y} →
                (hf' : F.relativelyRepresentable f') → {a : C} → (g : F.obj a ⟶ Y) → [F.Full] → hf'.pullback g ⟶ b