mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Parser.Extension
Lean.Parser.addBuiltinLeadingParser : Lean.Name → Lean.Name → Lean.Parser.Parser → ℕ → IO Unit
-- Mathlib.Algebra.Polynomial.Mirror
Polynomial.mirror_eq_zero : ∀ {R : Type u_1} [inst : Semiring R] {p : Polynomial R}, p.mirror = 0 ↔ p = 0
-- Init.Tactics
/-- Configuration for the `impossible` tactic.
 -/
Lean.Parser.Tactic.ImpossibleConfig : Type
-- Lean.Parser.Command
Lean.Parser.Command.printEqns.formatter : Lean.PrettyPrinter.Formatter
-- Std.Http.Data.Body.Any
/-- Selector that resolves when a chunk is available or EOF is reached.
 -/
Std.Http.Body.Any.recvSelector : Std.Http.Body.Any → Std.Async.Selector (Option Std.Http.Chunk)
-- Init.Data.SInt.Lemmas
Int16.sub_right_inj : ∀ {a b : Int16} (c : Int16), c - a = c - b ↔ a = b
-- Mathlib.Order.Completion
DedekindCut.left_principal : ∀ {α : Type u_1} [inst : Preorder α] (a : α), (DedekindCut.principal a).left = Set.Iic a
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.DiagnosticWith.mk.injEq : ∀ {α : Type} (range : Lean.Lsp.Range) (fullRange? : Option Lean.Lsp.Range)
  (severity? : Option Lean.Lsp.DiagnosticSeverity) (isSilent? : Option Bool) (code? : Option Lean.Lsp.DiagnosticCode)
  (source? : Option String) (message : α) (tags? : Option (Array Lean.Lsp.DiagnosticTag))
  (leanTags? : Option (Array Lean.Lsp.LeanDiagnosticTag))
  (relatedInformation? : Option (Array Lean.Lsp.DiagnosticRelatedInformation)) (data? : Option Lean.Json)
  (range_1 : Lean.Lsp.Range) (fullRange?_1 : Option Lean.Lsp.Range) (severity?_1 : Option Lean.Lsp.DiagnosticSeverity)
  (isSilent?_1 : Option Bool) (code?_1 : Option Lean.Lsp.DiagnosticCode) (source?_1 : Option String) (message_1 : α)
  (tags?_1 : Option (Array Lean.Lsp.DiagnosticTag)) (leanTags?_1 : Option (Array Lean.Lsp.LeanDiagnosticTag))
  (relatedInformation?_1 : Option (Array Lean.Lsp.DiagnosticRelatedInformation)) (data?_1 : Option Lean.Json),
  ({ range := range, fullRange? := fullRange?, severity? := severity?, isSilent? := isSilent?, code? := code?,
        source? := source?, message := message, tags? := tags?, leanTags? := leanTags?,
        relatedInformation? := relatedInformation?, data? := data? } =
      { range := range_1, fullRange? := fullRange?_1, severity? := severity?_1, isSilent? := isSilent?_1,
        code? := code?_1, source? := source?_1, message := message_1, tags? := tags?_1, leanTags? := leanTags?_1,
        relatedInformation? := relatedInformation?_1, data? := data?_1 }) =
    (range = range_1 ∧
      fullRange? = fullRange?_1 ∧
        severity? = severity?_1 ∧
          isSilent? = isSilent?_1 ∧
            code? = code?_1 ∧
              source? = source?_1 ∧
                message = message_1 ∧
                  tags? = tags?_1 ∧
                    leanTags? = leanTags?_1 ∧ relatedInformation? = relatedInformation?_1 ∧ data? = data?_1)
-- Mathlib.Algebra.Category.ModuleCat.Sheaf
SheafOfModules.forgetToSheafModuleCat_obj_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  (R : CategoryTheory.Sheaf J RingCat) (X : Cᵒᵖ) (hX : CategoryTheory.Limits.IsInitial X) (M : SheafOfModules R),
  ((SheafOfModules.forgetToSheafModuleCat R X hX).obj M).obj =
    (PresheafOfModules.forgetToPresheafModuleCat X hX).obj M.val
-- Mathlib.Algebra.Module.Congruence.Defs
ModuleCon.instSMulQuotient : {S : Type u_2} →
  (M : Type u_3) → [inst : SMul S M] → [inst_1 : Add M] → (c : ModuleCon S M) → SMul S (ModuleCon.Quotient M c)
-- Mathlib.Combinatorics.Additive.VerySmallDoubling
_private.Mathlib.Combinatorics.Additive.VerySmallDoubling.0.Finset.le_card_mul_inv_eq : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] {K : ℝ} {A B : Finset G} {x : G},
  ↑(B * A).card ≤ K * ↑A.card → x ∈ B⁻¹ * B → (2 - K) * ↑A.card ≤ ↑{ab ∈ A ×ˢ A | ab.1 * ab.2⁻¹ = x}.card
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
MulLECancellable.inj : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : PartialOrder α] {a b c : α}, MulLECancellable a → (a * b = a * c ↔ b = c)
-- Mathlib.Algebra.Category.CommAlgCat.FiniteType
FGAlgCatSkeleton.mk.inj : ∀ {R : Type u} {inst : CommRing R} {n : ℕ} {I : Ideal (MvPolynomial (Fin n) R)} {n_1 : ℕ}
  {I_1 : Ideal (MvPolynomial (Fin n_1) R)}, { n := n, I := I } = { n := n_1, I := I_1 } → n = n_1 ∧ I ≍ I_1
-- Mathlib.Topology.Algebra.Module.LinearPMap
/-- Assuming that `f` is invertible and closable, then the closure is invertible if and only
if the inverse of `f` is closable.  -/
LinearPMap.inverse_isClosable_iff : ∀ {R : Type u_1} {E : Type u_2} {F : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup E] [inst_2 : AddCommGroup F]
  [inst_3 : Module R E] [inst_4 : Module R F] [inst_5 : TopologicalSpace E] [inst_6 : TopologicalSpace F]
  {f : E →ₗ.[R] F} [inst_7 : ContinuousAdd E] [inst_8 : ContinuousAdd F] [inst_9 : TopologicalSpace R]
  [inst_10 : ContinuousSMul R E] [inst_11 : ContinuousSMul R F],
  f.toFun.ker = ⊥ → f.IsClosable → (f.inverse.IsClosable ↔ f.closure.toFun.ker = ⊥)
-- Mathlib.Data.List.Sigma
List.Perm.kreplace : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {a : α} {b : β a} {l₁ l₂ : List (Sigma β)},
  l₁.NodupKeys → l₁.Perm l₂ → (List.kreplace a b l₁).Perm (List.kreplace a b l₂)
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.IsSFiniteKernel.prodMkLeft : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsSFiniteKernel κ],
  ProbabilityTheory.IsSFiniteKernel (ProbabilityTheory.Kernel.prodMkLeft γ κ)
-- Mathlib.Analysis.Normed.Affine.AddTorsorBases
interior_convexHull_nonempty_iff_affineSpan_eq_top : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] [FiniteDimensional ℝ V] {s : Set V},
  (interior ((convexHull ℝ) s)).Nonempty ↔ affineSpan ℝ s = ⊤
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
eq_or_eq_neg_of_abs_eq : ∀ {α : Type u_1} [inst : AddGroup α] [inst_1 : LinearOrder α] {a b : α}, |a| = b → a = b ∨ a = -b
-- Mathlib.Algebra.Homology.Localization
/-- The category `HomologicalComplexUpToQuasiIso C c` which was defined as a localization of
`HomologicalComplex C c` with respect to quasi-isomorphisms also identifies to a localization
of the homotopy category with respect to quasi-isomorphisms.  -/
HomologicalComplexUpToQuasiIso.instIsLocalizationHomotopyCategoryQhQuasiIso : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] {ι : Type u_2} (c : ComplexShape ι)
  [inst_1 : CategoryTheory.Preadditive C] [inst_2 : CategoryTheory.CategoryWithHomology C]
  [inst_3 : (HomologicalComplex.quasiIso C c).HasLocalization] [inst_4 : c.QFactorsThroughHomotopy C]
  [(HomotopyCategory.quotient C c).IsLocalization (HomologicalComplex.homotopyEquivalences C c)],
  HomologicalComplexUpToQuasiIso.Qh.IsLocalization (HomotopyCategory.quasiIso C c)
-- Mathlib.Tactic.NormNum.Ordinal
/-- The `norm_num` extension for multiplication on ordinals.  -/
Mathlib.Meta.NormNum.evalOrdinalMul : Mathlib.Meta.NormNum.NormNumExt
-- Mathlib.Analysis.InnerProductSpace.Adjoint
LinearMap.isAdjointPair_inner : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : InnerProductSpace 𝕜 E] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : FiniteDimensional 𝕜 E] [inst_6 : FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F),
  (innerₛₗ 𝕜).flip.IsAdjointPair (innerₛₗ 𝕜).flip ⇑A ⇑(LinearMap.adjoint A)
-- Mathlib.Topology.Algebra.InfiniteSum.Module
/-- Given a subgroup `Γ` of an additive group `G`, and a function `f : G → M`, we
automorphize `f` to a function `G ⧸ Γ → M` by summing over `Γ` orbits,
`g ↦ ∑' (γ : Γ), f(γ • g)`.  -/
QuotientAddGroup.automorphize : {M : Type u_11} →
  [TopologicalSpace M] →
    [AddCommMonoid M] → {G : Type u_13} → [inst : AddGroup G] → {Γ : AddSubgroup G} → (G → M) → G ⧸ Γ → M
-- Init.Grind.Ring.CommSolver
_private.Init.Grind.Ring.CommSolver.0.Lean.Grind.CommRing.Poly.denote'.go.match_1.splitter : (motive : Lean.Grind.CommRing.Poly → Sort u_1) →
  (p : Lean.Grind.CommRing.Poly) →
    (Unit → motive (Lean.Grind.CommRing.Poly.num 0)) →
      ((k : ℤ) → (k = 0 → False) → motive (Lean.Grind.CommRing.Poly.num k)) →
        ((k : ℤ) →
            (m : Lean.Grind.CommRing.Mon) →
              (p : Lean.Grind.CommRing.Poly) → motive (Lean.Grind.CommRing.Poly.add k m p)) →
          motive p
-- Mathlib.Dynamics.Ergodic.Conservative
/-- Poincaré recurrence theorem: given a conservative map `f` and a measurable set `s`,
almost every point `x ∈ s` returns back to `s` infinitely many times.  -/
MeasureTheory.Conservative.ae_mem_imp_frequently_image_mem : ∀ {α : Type u_1} [inst : MeasurableSpace α] {f : α → α} {s : Set α} {μ : MeasureTheory.Measure α},
  MeasureTheory.Conservative f μ →
    MeasureTheory.NullMeasurableSet s μ → ∀ᵐ (x : α) ∂μ, x ∈ s → ∃ᶠ (n : ℕ) in Filter.atTop, f^[n] x ∈ s
-- Lean.Meta.Tactic.Grind.Extension
/-- A theorem marked with `@[grind inj]`  -/
Lean.Meta.Grind.InjectiveTheorem : Type
-- Mathlib.Algebra.Notation.Indicator
Set.mulIndicator_const_eq_mulIndicator_const : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_3} [inst : One M] {s : Set α} {a : α} {t : Set β} {b : β} {c : M},
  (a ∈ s ↔ b ∈ t) → s.mulIndicator (fun x => c) a = t.mulIndicator (fun x => c) b
-- Mathlib.InformationTheory.KullbackLeibler.KLFun
/-- `klFun` is measurable.  -/
InformationTheory.measurable_klFun : Measurable InformationTheory.klFun
-- Mathlib.RingTheory.Finiteness.Defs
/-- A ring morphism `A →+* B` is `RingHom.Finite` if `B` is finitely generated as `A`-module.  -/
RingHom.Finite : {A : Type u_1} → {B : Type u_2} → [inst : CommRing A] → [inst_1 : CommRing B] → (A →+* B) → Prop
-- Mathlib.AlgebraicGeometry.StructureSheaf
AlgebraicGeometry.instCommRingObjOppositeOpensCarrierTopObjFunctorTypeIsSheafGrothendieckTopologyStructureSheafInType : {R A : Type u} →
  [inst : CommRing R] →
    [inst_1 : CommRing A] →
      [inst_2 : Algebra R A] →
        (U : (TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R))ᵒᵖ) →
          CommRing ((AlgebraicGeometry.structureSheafInType R A).obj.obj U)
-- Init.Data.UInt.Basic
instXorOpUInt8 : XorOp UInt8
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_rcc_eq_singleton_iff : ∀ {k m n : ℕ}, (m...=n).toList = [k] ↔ n = m ∧ m = k
-- Init.Data.Vector.MapIdx
Vector.mapFinIdxM.map.congr_simp : ∀ {n : ℕ} {α : Type u} {β : Type v} {m : Type v → Type w} [inst : Monad m] (xs xs_1 : Vector α n),
  xs = xs_1 →
    ∀ (f f_1 : (i : ℕ) → α → i < n → m β),
      f = f_1 →
        ∀ (i j j_1 : ℕ) (e_j : j = j_1) (inv : i + j = n) (ys ys_1 : Vector β (n - i)),
          ys = ys_1 → Vector.mapFinIdxM.map xs f i j inv ys = Vector.mapFinIdxM.map xs_1 f_1 i j_1 ⋯ ys_1
-- Mathlib.Data.Finset.Lattice.Fold
Finset.apply_inf'_eq_inf'_comp : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : SemilatticeInf α] [inst_1 : SemilatticeInf γ] {s : Finset β}
  (H : s.Nonempty) {f : β → α} (g : α → γ), (∀ (x y : α), g (x ⊓ y) = g x ⊓ g y) → g (s.inf' H f) = s.inf' H (g ∘ f)
-- Mathlib.Topology.Connected.Clopen
/-- Preconnected sets are either contained in or disjoint to any given clopen set.  -/
disjoint_or_subset_of_isClopen : ∀ {α : Type u} [inst : TopologicalSpace α] {s t : Set α}, IsPreconnected s → IsClopen t → Disjoint s t ∨ s ⊆ t
-- Batteries.Recycling.RBTree.WF
_private.Batteries.Recycling.RBTree.WF.0.RBTree.RBNode.fold.match_1.eq_2 : ∀ {α : Type u_1} (motive : RBTree.RBNode α → Sort u_2) (c : RBTree.RBColor) (l : RBTree.RBNode α) (v : α)
  (r : RBTree.RBNode α) (h_1 : Unit → motive RBTree.RBNode.nil)
  (h_2 :
    (c : RBTree.RBColor) →
      (l : RBTree.RBNode α) → (v : α) → (r : RBTree.RBNode α) → motive (RBTree.RBNode.node c l v r)),
  (match RBTree.RBNode.node c l v r with
    | RBTree.RBNode.nil => h_1 ()
    | RBTree.RBNode.node c l v r => h_2 c l v r) =
    h_2 c l v r
-- Init.Data.Order.FactoriesExtra
Std.compare_ne_eq_iff_ne : ∀ {α : Type u} [inst : Ord α] [Std.LawfulEqOrd α] {a b : α}, compare a b ≠ Ordering.eq ↔ a ≠ b
-- Mathlib.LinearAlgebra.Dual.Lemmas
Submodule.finite_dualAnnihilator_iff : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {W : Submodule R M}
  [Module.Free R (M ⧸ W)], Module.Finite R ↥W.dualAnnihilator ↔ Module.Finite R (M ⧸ W)
-- Mathlib.Algebra.Homology.Embedding.TruncLE
/-- Given an embedding `e : Embedding c c'` of complex shapes which satisfy `e.IsTruncLE`,
this is the (canonical) truncation functor
`HomologicalComplex C c' ⥤ HomologicalComplex C c`.  -/
ComplexShape.Embedding.truncLE'Functor : {ι : Type u_1} →
  {ι' : Type u_2} →
    {c : ComplexShape ι} →
      {c' : ComplexShape ι'} →
        (e : c.Embedding c') →
          [e.IsTruncLE] →
            (C : Type u_4) →
              [inst : CategoryTheory.Category.{v_2, u_4} C] →
                [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
                  [CategoryTheory.CategoryWithHomology C] →
                    CategoryTheory.Functor (HomologicalComplex C c') (HomologicalComplex C c)
-- Mathlib.Topology.ShrinkingLemma
/-- **Shrinking lemma** . A point-finite open cover of a compact subset of a `T2Space`
`LocallyCompactSpace` can be "shrunk" to a new open cover so that the closure of each new open set
is contained in the corresponding original open set.  -/
exists_subset_iUnion_closure_subset_t2space : ∀ {ι : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {u : ι → Set X} {s : Set X} [T2Space X]
  [LocallyCompactSpace X],
  IsCompact s →
    (∀ (i : ι), IsOpen (u i)) →
      (∀ x ∈ s, {i | x ∈ u i}.Finite) →
        s ⊆ ⋃ i, u i →
          ∃ v,
            s ⊆ Set.iUnion v ∧
              (∀ (i : ι), IsOpen (v i)) ∧ (∀ (i : ι), closure (v i) ⊆ u i) ∧ ∀ (i : ι), IsCompact (closure (v i))
-- Mathlib.RingTheory.RingHom.StandardSmooth
RingHom.IsStandardSmoothOfRelativeDimension.eq_1 : ∀ (n : ℕ) {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
  RingHom.IsStandardSmoothOfRelativeDimension n f = Algebra.IsStandardSmoothOfRelativeDimension n R S
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.toLpCLM.congr_simp : ∀ (𝕜 : Type u_2) {E : Type u_5} (F : Type u_6) [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : MeasurableSpace E]
  [inst_5 : OpensMeasurableSpace E] [inst_6 : NormedField 𝕜] [inst_7 : NormedSpace 𝕜 F] [inst_8 : SMulCommClass ℝ 𝕜 F]
  [inst_9 : SecondCountableTopologyEither E F] (p : ENNReal) [inst_10 : Fact (1 ≤ p)] (μ : MeasureTheory.Measure E)
  [hμ : μ.HasTemperateGrowth], SchwartzMap.toLpCLM 𝕜 F p μ = SchwartzMap.toLpCLM 𝕜 F p μ
-- Mathlib.Analysis.Asymptotics.TVS
Asymptotics.IsLittleOTVS.tendsto_inv_smul : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} [inst : NontriviallyNormedField 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] {l : Filter α} [ContinuousSMul 𝕜 E] {f : α → 𝕜} {g : α → E},
  g =o[𝕜; l] f → Filter.Tendsto (fun x => (f x)⁻¹ • g x) l (nhds 0)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.not_mem_diff_of_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  k ∈ t₂ → k ∉ t₁ \ t₂
-- Mathlib.CategoryTheory.Localization.SmallShiftedHom
/-- Given `f : SmallHom W X Y` and `a : M`, this is the element
in `SmallHom W (X⟦a⟧) (Y⟦a⟧)` obtained by shifting by `a`.  -/
CategoryTheory.Localization.SmallHom.shift : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {W : CategoryTheory.MorphismProperty C} →
      {M : Type w'} →
        [inst_1 : AddMonoid M] →
          [inst_2 : CategoryTheory.HasShift C M] →
            [W.IsCompatibleWithShift M] →
              {X Y : C} →
                [inst_4 : CategoryTheory.Localization.HasSmallLocalizedHom W X Y] →
                  CategoryTheory.Localization.SmallHom W X Y →
                    (a : M) →
                      [inst_5 :
                          CategoryTheory.Localization.HasSmallLocalizedHom W ((CategoryTheory.shiftFunctor C a).obj X)
                            ((CategoryTheory.shiftFunctor C a).obj Y)] →
                        CategoryTheory.Localization.SmallHom W ((CategoryTheory.shiftFunctor C a).obj X)
                          ((CategoryTheory.shiftFunctor C a).obj Y)
-- Mathlib.MeasureTheory.Measure.Portmanteau
MeasureTheory.tendsto_of_forall_isClosed_limsup_le_nat : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} [inst : TopologicalSpace Ω] [inst_1 : OpensMeasurableSpace Ω]
  {μ : MeasureTheory.ProbabilityMeasure Ω} {μs : ℕ → MeasureTheory.ProbabilityMeasure Ω},
  (∀ (F : Set Ω), IsClosed F → Filter.limsup (fun i => (μs i) F) Filter.atTop ≤ μ F) →
    Filter.Tendsto μs Filter.atTop (nhds μ)
-- Mathlib.Algebra.Ring.Hom.Defs
RingHom.instMonoid : {α : Type u_2} → {x : NonAssocSemiring α} → Monoid (α →+* α)
-- Init.Data.AC
Lean.Data.AC.Variable.value : {α : Sort u} → {op : α → α → α} → Lean.Data.AC.Variable op → α
-- Mathlib.Dynamics.Ergodic.Extreme
/-- An extreme point of the set of invariant probability measures is an ergodic measure.  -/
Ergodic.of_mem_extremePoints : ∀ {X : Type u_1} {m : MeasurableSpace X} {μ : MeasureTheory.Measure X} {f : X → X},
  μ ∈ Set.extremePoints ENNReal {ν | MeasureTheory.MeasurePreserving f ν ν ∧ MeasureTheory.IsProbabilityMeasure ν} →
    Ergodic f μ
-- Mathlib.Algebra.Order.Kleene
IdemSemiring.toMulRightMono : ∀ {α : Type u_1} [inst : IdemSemiring α], MulRightMono α
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get!_insertManyIfNewUnit!_list : ∀ {α : Type u} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α fun x => Unit} {l : List α} {k : α},
  Std.DTreeMap.Internal.Impl.Const.get! (↑(Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit! t l)) k = ()
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
/-- Forgets the second fraction.  -/
CategoryTheory.MorphismProperty.LeftFraction₃.forgetSnd : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {W : CategoryTheory.MorphismProperty C} → {X Y : C} → W.LeftFraction₃ X Y → W.LeftFraction₂ X Y
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
IsUniformGroup.isRightUniformGroup : ∀ (α : Type u_1) [inst : UniformSpace α] [inst_1 : Group α] [IsUniformGroup α], IsRightUniformGroup α
-- Mathlib.Probability.Independence.BoundedContinuousFunction
indepSets_comap_pi_of_bcf : ∀ {Ω : Type u_1} {S : Type u_2} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {E : S → Type u_4}
  [inst : (s : S) → TopologicalSpace (E s)] [inst_1 : (s : S) → MeasurableSpace (E s)] [∀ (s : S), BorelSpace (E s)]
  [∀ (s : S), HasOuterApproxClosed (E s)] {X : (s : S) → Ω → E s} [MeasureTheory.IsProbabilityMeasure P] [Finite S]
  {𝒜 : Set (Set Ω)},
  (∀ A ∈ 𝒜, MeasureTheory.NullMeasurableSet A P) →
    (∀ (s : S), AEMeasurable (X s) P) →
      (∀ A ∈ 𝒜,
          ∀ (f : BoundedContinuousFunction ((s : S) → E s) ℝ),
            ∫ (ω : Ω) in A, f fun x => X x ω ∂P = P.real A * ∫ (ω : Ω), f fun x => X x ω ∂P) →
        ProbabilityTheory.IndepSets 𝒜 {A | MeasurableSet A} P
-- Mathlib.Probability.Kernel.Posterior
/-- Posterior of the kernel `κ` with respect to the measure `μ`.  -/
ProbabilityTheory.posterior : {Ω : Type u_1} →
  {𝓧 : Type u_2} →
    {mΩ : MeasurableSpace Ω} →
      {m𝓧 : MeasurableSpace 𝓧} →
        [StandardBorelSpace Ω] →
          [Nonempty Ω] →
            (κ : ProbabilityTheory.Kernel Ω 𝓧) →
              (μ : MeasureTheory.Measure Ω) →
                [MeasureTheory.IsFiniteMeasure μ] → [ProbabilityTheory.IsFiniteKernel κ] → ProbabilityTheory.Kernel 𝓧 Ω
-- Mathlib.MeasureTheory.Measure.Haar.Basic
MeasureTheory.Measure.haar.chaar_nonneg : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalGroup G]
  (K₀ : TopologicalSpace.PositiveCompacts G) (K : TopologicalSpace.Compacts G),
  0 ≤ MeasureTheory.Measure.haar.chaar K₀ K
-- Mathlib.Data.DFinsupp.Sigma
/-- The natural map between `Π₀ i (j : α i), δ i j` and `Π₀ (i : Σ i, α i), δ i.1 i.2`, inverse of
`curry`.  -/
DFinsupp.sigmaUncurry : {ι : Type u} →
  {α : ι → Type u_2} →
    {δ : (i : ι) → α i → Type v} →
      [DecidableEq ι] →
        [inst : (i : ι) → (j : α i) → Zero (δ i j)] →
          (Π₀ (i : ι) (j : α i), δ i j) → Π₀ (i : (x : ι) × α x), δ i.fst i.snd
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarSubalgebra.iSupLift_comp_inclusion : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : NonUnitalSemiring A] [inst_2 : StarRing A]
  [inst_3 : Module R A] [inst_4 : NonUnitalSemiring B] [inst_5 : StarRing B] [inst_6 : Module R B] {ι : Type u_1}
  [inst_7 : StarRing R] [inst_8 : IsScalarTower R A A] [inst_9 : SMulCommClass R A A] [inst_10 : StarModule R A]
  [inst_11 : Nonempty ι] {K : ι → NonUnitalStarSubalgebra R A} {dir : Directed (fun x1 x2 => x1 ≤ x2) K}
  {f : (i : ι) → ↥(K i) →⋆ₙₐ[R] B}
  {hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (NonUnitalStarSubalgebra.inclusion h)}
  {T : NonUnitalStarSubalgebra R A} {hT : T = iSup K} {i : ι} (h : K i ≤ T),
  (NonUnitalStarSubalgebra.iSupLift K dir f hf T hT).comp (NonUnitalStarSubalgebra.inclusion h) = f i
-- Mathlib.CategoryTheory.FinCategory.AsType
CategoryTheory.FinCategory.asTypeFinCategory : (α : Type u_1) →
  [inst : Fintype α] →
    [inst_1 : CategoryTheory.SmallCategory α] →
      [inst_2 : CategoryTheory.FinCategory α] → CategoryTheory.FinCategory (CategoryTheory.FinCategory.AsType α)
-- Lean.Meta.Tactic.Simp.Rewrite
_private.Lean.Meta.Tactic.Simp.Rewrite.0.Lean.Meta.Simp.useImplicitDefEqProof : Lean.Meta.SimpTheorem → Lean.Meta.SimpM Bool
-- Mathlib.Order.Bounds.Basic
isLUB_Iic : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, IsLUB (Set.Iic a) a
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.ofList_nil : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} [EquivBEq α] [LawfulHashable α], Std.ExtHashMap.ofList [] = ∅
-- Mathlib.NumberTheory.NumberField.CMField
NumberField.IsCMField.complexConj_apply_apply : ∀ (K : Type u_1) [inst : Field K] [inst_1 : CharZero K] [inst_2 : NumberField.IsCMField K]
  [inst_3 : Algebra.IsIntegral ℚ K] (x : K),
  (NumberField.IsCMField.complexConj K) ((NumberField.IsCMField.complexConj K) x) = x
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
IsPrimitiveRoot.dvd_of_pow_eq_one : ∀ {M : Type u_1} [inst : CommMonoid M] {ζ : M} {k : ℕ}, IsPrimitiveRoot ζ k → ∀ (l : ℕ), ζ ^ l = 1 → k ∣ l
-- Mathlib.Order.Sublattice
Sublattice.map_symm_eq_iff_eq_map : ∀ {α : Type u_2} {β : Type u_3} [inst : Lattice α] [inst_1 : Lattice β] {L : Sublattice α} {M : Sublattice β}
  {e : β ≃o α},
  Sublattice.map { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯ } L = M ↔
    L = Sublattice.map { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯ } M
-- Init.Data.SInt.Lemmas
Int64.instIsLinearOrder : Std.IsLinearOrder Int64
-- Mathlib.Analysis.InnerProductSpace.LaxMilgram
IsCoercive.unique_continuousLinearEquivOfBilin : ∀ {V : Type u} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : CompleteSpace V]
  {B : V →L[ℝ] V →L[ℝ] ℝ} (coercive : IsCoercive B) {v f : V},
  (∀ (w : V), inner ℝ f w = (B v) w) → f = coercive.continuousLinearEquivOfBilin v
-- Mathlib.MeasureTheory.Measure.WithDensity
MeasureTheory.restrict_withDensity' : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.SFinite μ] (s : Set α)
  (f : α → ENNReal), (μ.withDensity f).restrict s = (μ.restrict s).withDensity f
-- Mathlib.NumberTheory.Zsqrtd.Basic
/-- The representative of `√d` in the ring  -/
Zsqrtd.sqrtd : {d : ℤ} → ℤ√d
-- Mathlib.FieldTheory.Relrank
IntermediateField.relfinrank_bot_right : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (A : IntermediateField F E),
  A.relfinrank ⊥ = 1
-- Mathlib.Data.List.Perm.Subperm
/-- **Alias** of the forward direction of `List.subperm_cons`. -/
List.subperm.of_cons : ∀ {α : Type u_1} (a : α) {l₁ l₂ : List α}, (a :: l₁).Subperm (a :: l₂) → l₁.Subperm l₂
-- Mathlib.Topology.Instances.CantorSet
/-- The Cantor space is homeomorphic to a countable product of copies of itself.  -/
cantorSpaceHomeomorphNatToCantorSpace : (ℕ → Bool) ≃ₜ (ℕ → ℕ → Bool)