mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Set.Lattice
Set.Iic_iInf : ∀ {α : Type u_1} {ι : Sort u_5} [inst : CompleteLattice α] (f : ι → α), Set.Iic (⨅ i, f i) = ⋂ i, Set.Iic (f i)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.GetLsbD
Std.Tactic.BVDecide.BVPred.GetLsbDTarget.vec : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {aig : Std.Sat.AIG α} → (self : Std.Tactic.BVDecide.BVPred.GetLsbDTarget aig) → aig.RefVec self.w
-- Mathlib.LinearAlgebra.Multilinear.DFinsupp
/-- When applied to a family of finitely-supported functions each supported on a single element,
`dfinsuppFamily` is itself supported on a single element, with value equal to the map `f` applied
at that point.  -/
MultilinearMap.dfinsuppFamily_single : ∀ {ι : Type uι} {κ : ι → Type uκ} {R : Type uR} {M : (i : ι) → κ i → Type uM} {N : ((i : ι) → κ i) → Type uN}
  [inst : DecidableEq ι] [inst_1 : Fintype ι] [inst_2 : Semiring R]
  [inst_3 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)] [inst_4 : (p : (i : ι) → κ i) → AddCommMonoid (N p)]
  [inst_5 : (i : ι) → (k : κ i) → Module R (M i k)] [inst_6 : (p : (i : ι) → κ i) → Module R (N p)]
  [inst_7 : (i : ι) → DecidableEq (κ i)] (f : (p : (i : ι) → κ i) → MultilinearMap R (fun i => M i (p i)) (N p))
  (p : (i : ι) → κ i) (m : (i : ι) → M i (p i)),
  ((MultilinearMap.dfinsuppFamily f) fun i => fun₀ | p i => m i) = fun₀ | p => (f p) m
-- Mathlib.RingTheory.Unramified.Field
Algebra.FormallyUnramified.iff_isSeparable : ∀ (K : Type u_1) [inst : Field K] (L : Type u) [inst_1 : Field L] [inst_2 : Algebra K L] [Algebra.EssFiniteType K L],
  Algebra.FormallyUnramified K L ↔ Algebra.IsSeparable K L
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
CategoryTheory.Functor.OneHypercoverDenseData.essSurj.restriction.res_eq_res : ∀ {C₀ : Type u₀} {C : Type u} [inst : CategoryTheory.Category.{v₀, u₀} C₀] [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor C₀ C} {J₀ : CategoryTheory.GrothendieckTopology C₀}
  {J : CategoryTheory.GrothendieckTopology C} {A : Type u'} [inst_2 : CategoryTheory.Category.{v', u'} A]
  [inst_3 : CategoryTheory.Functor.IsDenseSubsite J₀ J F] (data : (X : C) → F.OneHypercoverDenseData J₀ J X)
  [inst_4 : CategoryTheory.Limits.HasLimitsOfSize.{w, w, v', u'} A] (G₀ : CategoryTheory.Sheaf J₀ A) {X : C}
  {X₀ Y₀ : C₀} {f : F.obj X₀ ⟶ X} {g : Y₀ ⟶ X₀} (h₁ h₂ : (data X).SieveStruct f g),
  CategoryTheory.Functor.OneHypercoverDenseData.essSurj.restriction.res data G₀ h₁ =
    CategoryTheory.Functor.OneHypercoverDenseData.essSurj.restriction.res data G₀ h₂
-- Mathlib.MeasureTheory.Integral.FinMeasAdditive
MeasureTheory.DominatedFinMeasAdditive.zero : ∀ {α : Type u_1} {β : Type u_7} [inst : SeminormedAddCommGroup β] {C : ℝ} {m : MeasurableSpace α}
  (μ : MeasureTheory.Measure α), 0 ≤ C → MeasureTheory.DominatedFinMeasAdditive μ 0 C
-- Mathlib.CategoryTheory.Limits.Types.ColimitType
/-- When `c : F.CoconeTypes` satisfies the property
`c.IsColimit`, this is a term in `IsColimitCore.{w₂} c`
for any universe `w₂`.  -/
CategoryTheory.Functor.CoconeTypes.IsColimit.isColimitCore : {J : Type u} →
  [inst : CategoryTheory.Category.{v, u} J] →
    {F : CategoryTheory.Functor J (Type w₀)} → {c : F.CoconeTypes} → c.IsColimit → c.IsColimitCore
-- Lean.Data.JsonRpc
Lean.IO.FS.Stream.readRequestAs : IO.FS.Stream → ℕ → String → (α : Type) → [Lean.FromJson α] → IO (Lean.JsonRpc.Request α)
-- Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv
HasDerivAt.clog_real : ∀ {f : ℝ → ℂ} {x : ℝ} {f' : ℂ},
  HasDerivAt f f' x → f x ∈ Complex.slitPlane → HasDerivAt (fun t => Complex.log (f t)) (f' / f x) x
-- Mathlib.Algebra.Group.Equiv.Defs
MulEquiv.toMonoidHom_injective : ∀ {M : Type u_4} {N : Type u_5} [inst : MulOneClass M] [inst_1 : MulOneClass N], Function.Injective MulEquiv.toMonoidHom
-- Mathlib.Order.Bounds.Basic
IsGreatest.dual : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α} {a : α},
  IsGreatest s a → IsLeast (⇑OrderDual.ofDual ⁻¹' s) (OrderDual.toDual a)
-- Mathlib.Combinatorics.SetFamily.AhlswedeZhang
AhlswedeZhang.IsAntichain.le_infSum : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {𝒜 : Finset (Finset α)},
  IsAntichain (fun x1 x2 => x1 ⊆ x2) ↑𝒜 →
    ∅ ∉ 𝒜 → ∑ s ∈ 𝒜, (↑((Fintype.card α).choose s.card))⁻¹ ≤ AhlswedeZhang.infSum 𝒜
-- Mathlib.Topology.Algebra.Group.Basic
/-- The map `(x, y) ↦ (x, x + y)` as a homeomorphism. This is a shear mapping.  -/
Homeomorph.shearAddRight : (G : Type w) → [inst : TopologicalSpace G] → [inst_1 : AddGroup G] → [IsTopologicalAddGroup G] → G × G ≃ₜ G × G
-- Mathlib.RingTheory.Invariant.Basic
/-- `G` acts transitively on the prime ideals of `B` above a given prime ideal of `A`.  -/
Algebra.IsInvariant.exists_smul_of_under_eq : ∀ (A : Type u_1) (B : Type u_2) (G : Type u_3) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B]
  [inst_3 : Group G] [inst_4 : MulSemiringAction G B] [Algebra.IsInvariant A B G] [Finite G] [SMulCommClass G A B]
  (P Q : Ideal B) [hP : P.IsPrime] [hQ : Q.IsPrime], Ideal.under A P = Ideal.under A Q → ∃ g, Q = g • P
-- Aesop.Rule
Aesop.UnfoldRule.mk.sizeOf_spec : ∀ (decl : Lean.Name) (unfoldThm? : Option Lean.Name),
  sizeOf { decl := decl, unfoldThm? := unfoldThm? } = 1 + sizeOf decl + sizeOf unfoldThm?
-- Init.Data.Float.Float
instDivFloat : Div Float
-- Init.Data.List.Pairwise
List.Pairwise.map : ∀ {β : Type u_1} {α : Type u_2} {R : α → α → Prop} {l : List α} {S : β → β → Prop} (f : α → β),
  (∀ (a b : α), R a b → S (f a) (f b)) → List.Pairwise R l → List.Pairwise S (List.map f l)
-- Init.Data.SInt.Lemmas
ISize.toNatClampNeg_ofIntTruncate_of_lt : ∀ {n : ℤ}, n < 2 ^ 31 → (ISize.ofIntClamp n).toNatClampNeg = n.toNat
-- Mathlib.RingTheory.Valuation.Discrete.Basic
Valuation.IsUniformizer.eq_1 : ∀ {Γ : Type u_1} [inst : LinearOrderedCommGroupWithZero Γ] {A : Type u_2} [inst_1 : Ring A] (v : Valuation A Γ)
  [hv : v.IsRankOneDiscrete] (π : A), v.IsUniformizer π = (v π = ↑(Valuation.IsRankOneDiscrete.generator v))
-- Mathlib.Order.GaloisConnection.Basic
sSup_image2_eq_sSup_sInf : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : CompleteLattice α] [inst_1 : CompleteLattice β]
  [inst_2 : CompleteLattice γ] {s : Set α} {t : Set β} {l : α → β → γ} {u₁ : β → γ → α} {u₂ : α → γ → β},
  (∀ (b : β), GaloisConnection (Function.swap l b) (u₁ b)) →
    (∀ (a : α), GaloisConnection (l a ∘ ⇑OrderDual.ofDual) (⇑OrderDual.toDual ∘ u₂ a)) →
      sSup (Set.image2 l s t) = l (sSup s) (sInf t)
-- Lean.Server.Requests
/-- Finds the first `CommandParsedSnapshot` containing `hoverPos`, asynchronously.  -/
Lean.Server.RequestM.findCmdParsedSnap : Lean.Server.FileWorker.EditableDocument →
  String.Pos.Raw → Lean.Server.ServerTask (Option Lean.Language.Lean.CommandParsedSnapshot)
-- Std.Data.HashMap.Raw
/-- Checks if a mapping for the given key exists and returns the key if it does, otherwise `fallback`.
If a mapping exists the result is guaranteed to be pointer equal to the key in the map.
 -/
Std.HashMap.Raw.getKeyD : {α : Type u} → {β : Type v} → [BEq α] → [Hashable α] → Std.HashMap.Raw α β → α → α → α
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
AffineSubspace.direction_iInf : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] {ι : Sort u_4} (s : ι → AffineSubspace k P), (iInf s).direction ≤ ⨅ i, (s i).direction
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.opcyclesToE_ιE : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃)
  (f₁₂ : i₀ ⟶ i₂) (h₁₂ : CategoryTheory.CategoryStruct.comp f₁ f₂ = f₁₂) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.opcyclesToE_ιE._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.opcyclesToE_ιE._auto_3),
  CategoryTheory.CategoryStruct.comp (X.opcyclesToE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂)
      (X.ιE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂) =
    X.opcyclesMap f₁₂ f₃ f₂ f₃ (CategoryTheory.ComposableArrows.threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂) n₁
-- Mathlib.Tactic.Algebra.Basic
/-- The core of `proveEq` takes expressions `e₁ e₂ : α` where `α` is a `CommSemiring`,
and returns a proof that they are equal (or fails).  -/
_private.Mathlib.Tactic.Algebra.Basic.0.Mathlib.Tactic.Algebra.proveEq.algCore : {u v : Lean.Level} →
  {R : Q(Type u)} →
    {A : Q(Type v)} →
      {sR : Q(CommSemiring «$R»)} →
        {sA : Q(CommSemiring «$A»)} →
          Q(Algebra «$R» «$A») →
            Mathlib.Tactic.Algebra.Cache q(«$sR») →
              Mathlib.Tactic.Algebra.Cache q(«$sA») → (e₁ e₂ : Q(«$A»)) → Mathlib.Tactic.AtomM Q(«$e₁» = «$e₂»)
-- Mathlib.Order.CompleteBooleanAlgebra
CompletelyDistribLattice.toSDiff : {α : Type u} → [self : CompletelyDistribLattice α] → SDiff α
-- Mathlib.Topology.Homeomorph.Lemmas
/-- If `h : X → Y` is a homeomorphism, `h⁻¹(s)` is compact iff `s` is.  -/
Homeomorph.isCompact_preimage : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {s : Set Y} (h : X ≃ₜ Y),
  IsCompact (⇑h ⁻¹' s) ↔ IsCompact s
-- Mathlib.Data.EReal.Inv
EReal.abs_mul_sign : ∀ (x : EReal), ↑x.abs * ↑(SignType.sign x) = x
-- Mathlib.CategoryTheory.Limits.ColimitLimit
/-- Since `colimit_limit_to_limit_colimit` is a morphism from a colimit to a limit,
this lemma characterises it.
 -/
CategoryTheory.Limits.ι_colimitLimitToLimitColimit_π_assoc : ∀ {J : Type u₁} {K : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} J] [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  {C : Type u} [inst_2 : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor (J × K) C)
  [inst_3 : CategoryTheory.Limits.HasLimitsOfShape J C] [inst_4 : CategoryTheory.Limits.HasColimitsOfShape K C] (j : J)
  (k : K) {Z : C} (h : CategoryTheory.Limits.colim.obj ((CategoryTheory.Functor.curry.obj F).obj j) ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.colimit.ι
        ((CategoryTheory.Functor.curry.obj ((CategoryTheory.Prod.swap K J).comp F)).comp CategoryTheory.Limits.lim) k)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimitLimitToLimitColimit F)
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Limits.limit.π ((CategoryTheory.Functor.curry.obj F).comp CategoryTheory.Limits.colim) j)
          h)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.limit.π ((CategoryTheory.Functor.curry.obj ((CategoryTheory.Prod.swap K J).comp F)).obj k)
        j)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.colimit.ι ((CategoryTheory.Functor.curry.obj F).obj j) k) h)
-- Mathlib.Algebra.Group.Commute.Defs
AddCommute.add_neg_cancel_assoc : ∀ {G : Type u_1} [inst : AddGroup G] {a b : G}, AddCommute a b → a + (b + -a) = b
-- Mathlib.CategoryTheory.Countable
CategoryTheory.CountableCategory.mk : ∀ {J : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} J],
  autoParam (Countable J) CategoryTheory.CountableCategory.countableObj._autoParam →
    autoParam (∀ (j j' : J), Countable (j ⟶ j')) CategoryTheory.CountableCategory.countableHom._autoParam →
      CategoryTheory.CountableCategory J
-- Lean.Elab.Term.TermElabM
/-- Add the given metavariable to the list of pending synthetic metavariables.
The method `synthesizeSyntheticMVars` is used to process the metavariables on this list.  -/
Lean.Elab.Term.registerSyntheticMVar : Lean.Syntax → Lean.MVarId → Lean.Elab.Term.SyntheticMVarKind → Lean.Elab.TermElabM Unit
-- Std.Data.DTreeMap.Internal.Queries
Std.DTreeMap.Internal.Impl.maxEntry!.eq_def : ∀ {α : Type u} {β : α → Type v} [inst : Inhabited ((a : α) × β a)] (x : Std.DTreeMap.Internal.Impl α β),
  x.maxEntry! =
    match x with
    | Std.DTreeMap.Internal.Impl.leaf =>
      panicWithPosWithDecl "Std.Data.DTreeMap.Internal.Queries" "Std.DTreeMap.Internal.Impl.maxEntry!" 390 13
        "Map is empty"
    | Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf => ⟨k, v⟩
    | Std.DTreeMap.Internal.Impl.inner size k v l r@h:(Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r_1) =>
      r.maxEntry!
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get?_insert!_self : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t.WF → ∀ {k : α} {v : β}, Std.DTreeMap.Internal.Impl.Const.get? (Std.DTreeMap.Internal.Impl.insert! k v t) k = some v
-- Mathlib.Order.BoundedOrder.Monotone
forall_ge_iff : ∀ {α : Type u} [inst : Preorder α] {P : α → Prop} {x₀ : α}, Monotone P → ((∀ x ≥ x₀, P x) ↔ P x₀)
-- Init.Data.UInt.Lemmas
USize.toUInt64_toUInt8 : ∀ (n : USize), n.toUInt8.toUInt64 = n.toUInt64 % 256
-- Mathlib.Analysis.Calculus.LogDeriv
/-- If two functions agree on a codiscrete subset of an open set `U`, then so do their logarithmic
derivatives.
 -/
logDeriv_congr_codiscreteWithin : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {f g : 𝕜 → 𝕜'} {U : Set 𝕜},
  IsOpen U → f =ᶠ[Filter.codiscreteWithin U] g → logDeriv f =ᶠ[Filter.codiscreteWithin U] logDeriv g
-- Init.Omega.Constraint
Option.merge.eq_1 : ∀ {α : Type u_1} (fn : α → α → α), Option.merge fn none none = none
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Trivialization.codExtend_apply : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace Z] {s : Set B} (hs : IsOpen s) (nonempty : s.Nonempty) {proj : Z → ↑s}
  (e : Bundle.Trivialization F proj) (z : Z),
  ↑(Bundle.Trivialization.codExtend hs nonempty e) z = (↑(↑e.toPretrivialization z).1, (↑e.toPretrivialization z).2)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey!_union_of_not_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [inst : Inhabited α]
  [Std.TransCmp cmp], t₁.WF → t₂.WF → ∀ {k : α}, k ∉ t₂ → (t₁ ∪ t₂).getKey! k = t₁.getKey! k
-- Mathlib.Data.PFun
PFun.dom_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : β →. γ) (g : α →. β), (f.comp g).Dom = g.preimage f.Dom
-- Mathlib.Analysis.Normed.Affine.Isometry
LinearIsometryEquiv.toAffineIsometryEquiv_toAffineIsometry : ∀ {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup V]
  [inst_2 : NormedSpace 𝕜 V] [inst_3 : SeminormedAddCommGroup V₂] [inst_4 : NormedSpace 𝕜 V₂] (e : V ≃ₗᵢ[𝕜] V₂),
  e.toAffineIsometryEquiv.toAffineIsometry = e.toLinearIsometry.toAffineIsometry
-- Mathlib.Data.Fintype.EquivFin
Fintype.card_eq_one_iff : ∀ {α : Type u_1} [inst : Fintype α], Fintype.card α = 1 ↔ ∃ x, ∀ (y : α), y = x
-- Lean.DocString.Extension
_private.Lean.DocString.Extension.0.Lean.VersoModuleDocs.DocContext.mk : Array (Lean.Doc.Block Lean.ElabInline Lean.ElabBlock) →
  Array (Lean.Doc.Part Lean.ElabInline Lean.ElabBlock Empty) →
    Array Lean.VersoModuleDocs.DocFrame✝ → Lean.VersoModuleDocs.DocContext✝
-- Lean.Elab.ParseImportsFast
Lean.PrintImportsResult.imports : Lean.PrintImportsResult → Array Lean.PrintImportResult
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.all_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  {p : (a : α) → β a → Bool}, t₁.Equiv t₂ → t₁.all p = t₂.all p
-- Mathlib.Topology.ContinuousOn
IsOpenMap.continuousOn_image_of_leftInvOn : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {s : Set α},
  IsOpenMap (s.domRestrict f) → ∀ {finv : β → α}, Set.LeftInvOn finv f s → ContinuousOn finv (f '' s)
-- Init.Data.Array.Lemmas
Array.append_eq_append_iff_of_size_eq_left : ∀ {α : Type u_1} {ws xs ys zs : Array α}, ws.size = xs.size → (ws ++ ys = xs ++ zs ↔ ws = xs ∧ ys = zs)
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.removeUnused : Array Lean.Elab.Command.InductiveElabStep2 →
  Array Lean.Expr →
    List Lean.InductiveType → Lean.Elab.TermElabM (Lean.LocalContext × Lean.LocalInstances × Array Lean.Expr)
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
/-- If a set `s` separates `ν` from the singular part of `μ` with respect to `ν`,
then the singular part equals the restriction of `μ` to `s`.  -/
MeasureTheory.Measure.singularPart_eq_restrict : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} {s : Set α} [μ.HaveLebesgueDecomposition ν],
  (μ.singularPart ν) sᶜ = 0 → ν s = 0 → μ.singularPart ν = μ.restrict s
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEmbedding.equivRange_symm_apply_mk : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {f : α → β}
  (hf : MeasurableEmbedding f) (x : α), hf.equivRange.symm ⟨f x, ⋯⟩ = x
-- Mathlib.CategoryTheory.Groupoid.Grpd.Basic
/-- The product fan over an indexed family of groupoids, is a limit cone.  -/
CategoryTheory.Grpd.piLimitFanIsLimit : ⦃J : Type u⦄ → (F : J → CategoryTheory.Grpd) → CategoryTheory.Limits.IsLimit (CategoryTheory.Grpd.piLimitFan F)
-- Lean.Meta.Tactic.Simp.SimpAll
Lean.Meta.SimpAll.Entry.fvarId : Lean.Meta.SimpAll.Entry → Lean.FVarId
-- Lean.Parser.Basic
Lean.Parser.categoryParserFnExtension : Lean.EnvExtension Lean.Parser.CategoryParserFn
-- Mathlib.Probability.Independence.InfinitePi
/-- Given random variables `X i j : Ω i j → 𝓧 i j`, they are independent when viewed as random
variables defined on the product space `Π i, Π j, Ω i j`.  -/
ProbabilityTheory.iIndepFun_uncurry_infinitePi' : ∀ {ι : Type u_1} {κ : Type u_4} {𝓧 : ι → κ → Type u_5} {m𝓧 : (i : ι) → (j : κ) → MeasurableSpace (𝓧 i j)}
  {Ω : ι → κ → Type u_6} {mΩ : (i : ι) → (j : κ) → MeasurableSpace (Ω i j)} {X : (i : ι) → (j : κ) → Ω i j → 𝓧 i j}
  (μ : (i : ι) → (j : κ) → MeasureTheory.Measure (Ω i j))
  [∀ (i : ι) (j : κ), MeasureTheory.IsProbabilityMeasure (μ i j)],
  (∀ (i : ι) (j : κ), Measurable (X i j)) →
    ProbabilityTheory.iIndepFun (fun p ω => X p.1 p.2 (ω p.1 p.2))
      (MeasureTheory.Measure.infinitePi fun i => MeasureTheory.Measure.infinitePi (μ i))
-- Init.Data.Range.Polymorphic.RangeIterator
Std.Rxo.Iterator.mk.inj : ∀ {α : Type u} {next : Option α} {upperBound : α} {next_1 : Option α} {upperBound_1 : α},
  { next := next, upperBound := upperBound } = { next := next_1, upperBound := upperBound_1 } →
    next = next_1 ∧ upperBound = upperBound_1
-- Mathlib.Topology.Connected.Basic
/-- The biUnion of a family of preconnected sets is preconnected if the graph determined by
whether two sets intersect is preconnected.  -/
IsPreconnected.biUnion_of_reflTransGen : ∀ {α : Type u} [inst : TopologicalSpace α] {ι : Type u_3} {t : Set ι} {s : ι → Set α},
  (∀ i ∈ t, IsPreconnected (s i)) →
    (∀ i ∈ t, ∀ j ∈ t, Relation.ReflTransGen (fun i j => (s i ∩ s j).Nonempty ∧ i ∈ t) i j) →
      IsPreconnected (⋃ n ∈ t, s n)
-- Lean.Parser.Command
Lean.Parser.Command.optDeriving : Lean.Parser.Parser
-- Lean.MonadEnv
/-- Similar to `withoutModifyingEnv`, but also returns the updated environment  -/
Lean.withoutModifyingEnv' : {m : Type → Type} → [Monad m] → [Lean.MonadEnv m] → [MonadFinally m] → {α : Type} → m α → m (α × Lean.Environment)
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEquiv.preimage_symm : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] (e : α ≃ᵐ β) (s : Set α),
  ⇑e.symm ⁻¹' s = ⇑e '' s
-- Lean.Meta.InferType
/-- `isTypeQuick e` is an "approximate" predicate which returns `LBool.true` if `e` is a type.
 -/
Lean.Meta.isTypeQuick : Lean.Expr → Lean.MetaM Lean.LBool
-- Mathlib.CategoryTheory.Preadditive.Projective.LiftingProperties
CategoryTheory.projective_iff_llp_epimorphisms_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] (P : C),
  CategoryTheory.Projective P ↔ (CategoryTheory.MorphismProperty.epimorphisms C).llp 0
-- Mathlib.Algebra.Ring.Subsemiring.Defs
Subsemiring.coe_toSubmonoid : ∀ {R : Type u} [inst : NonAssocSemiring R] (s : Subsemiring R), ↑s.toSubmonoid = ↑s
-- Mathlib.CategoryTheory.Bicategory.Modification.Lax
CategoryTheory.Lax.LaxTrans.Modification.mk.injEq : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.LaxFunctor B C} {η θ : F ⟶ G} (app : (a : B) → η.app a ⟶ θ.app a)
  (naturality :
    autoParam
      (∀ {a b : B} (f : a ⟶ b),
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (app a) (G.map f)) (θ.naturality f) =
          CategoryTheory.CategoryStruct.comp (η.naturality f) (CategoryTheory.Bicategory.whiskerLeft (F.map f) (app b)))
      CategoryTheory.Lax.LaxTrans.Modification.naturality._autoParam)
  (app_1 : (a : B) → η.app a ⟶ θ.app a)
  (naturality_1 :
    autoParam
      (∀ {a b : B} (f : a ⟶ b),
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (app_1 a) (G.map f))
            (θ.naturality f) =
          CategoryTheory.CategoryStruct.comp (η.naturality f)
            (CategoryTheory.Bicategory.whiskerLeft (F.map f) (app_1 b)))
      CategoryTheory.Lax.LaxTrans.Modification.naturality._autoParam),
  ({ app := app, naturality := naturality } = { app := app_1, naturality := naturality_1 }) = (app = app_1)
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.trLList.eq_2 : ∀ (l : List ℕ) (ls : List (List ℕ)),
  Turing.PartrecToTM2.trLList (l :: ls) =
    Turing.PartrecToTM2.trList l ++ Turing.PartrecToTM2.Γ'.consₗ :: Turing.PartrecToTM2.trLList ls
-- Mathlib.Analysis.CStarAlgebra.Module.Defs
CStarModule.isSelfAdjoint_inner_self : ∀ {A : Type u_1} {E : Type u_2} [inst : NonUnitalRing A] [inst_1 : StarRing A] [inst_2 : AddCommGroup E]
  [inst_3 : Module ℂ A] [inst_4 : Module ℂ E] [inst_5 : PartialOrder A] [inst_6 : SMul A E] [inst_7 : Norm A]
  [inst_8 : Norm E] [inst_9 : CStarModule A E] {x : E}, IsSelfAdjoint (inner A x x)
-- Mathlib.Topology.Category.Profinite.Nobeling.Basic
Profinite.NobelingProof.GoodProducts.injective : ∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I],
  Function.Injective (Profinite.NobelingProof.GoodProducts.eval C)
-- Mathlib.Algebra.Group.Submonoid.Support
AddSubmonoid.support_toAddSubmonoid : ∀ {G : Type u_1} [inst : AddGroup G] (M : AddSubmonoid G), M.support.toAddSubmonoid = M ⊓ -M
-- Mathlib.Data.ENat.Lattice
ENat.iInf₂_add : ∀ {ι : Sort u_2} {a : ℕ∞} {κ : ι → Sort u_4} (f : (i : ι) → κ i → ℕ∞), (⨅ i, ⨅ j, f i j) + a = ⨅ i, ⨅ j, f i j + a
-- Mathlib.Combinatorics.Enumerative.DyckWord
DyckStep.D.sizeOf_spec : sizeOf DyckStep.D = 1
-- Mathlib.RingTheory.Ideal.Lattice
Ideal.mem_sInf : ∀ {R : Type u} [inst : Semiring R] {s : Set (Ideal R)} {x : R}, x ∈ sInf s ↔ ∀ ⦃I : Ideal R⦄, I ∈ s → x ∈ I
-- Mathlib.Data.Multiset.MapFold
Multiset.map_id' : ∀ {α : Type u_1} (s : Multiset α), Multiset.map (fun x => x) s = s
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.H2_induction_on : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep.{u, u, u} k G} {C : ↑(groupCohomology.H2 A) → Prop}
  (x : ↑(groupCohomology.H2 A)),
  (∀ (x : ↥(groupCohomology.cocycles₂ A)), C ((CategoryTheory.ConcreteCategory.hom (groupCohomology.H2π A)) x)) → C x
-- Mathlib.Data.Int.GCD
/-- **Alias** of `Int.gcd_ediv`. -/
Int.gcd_div : ∀ {a b c : ℤ}, c ∣ a → c ∣ b → (a / c).gcd (b / c) = a.gcd b / c.natAbs
-- Init.Data.List.MinMaxOn
List.minOn?_replicate_of_pos : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] [Std.IsLinearPreorder β] {n : ℕ} {a : α}
  {f : α → β}, 0 < n → List.minOn? f (List.replicate n a) = some a
-- Mathlib.Algebra.Algebra.Basic
Module.End.algebraMap_isUnit_inv_apply_eq_iff' : ∀ {R : Type u} (S : Type v) {M : Type w} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] [inst_4 : Module S M] [inst_5 : SMulCommClass S R M] [inst_6 : SMul R S]
  [inst_7 : IsScalarTower R S M] {x : R} (h : IsUnit ((algebraMap R (Module.End S M)) x)) (m m' : M),
  m' = ↑h.unit⁻¹ m ↔ m = x • m'